module Obs.Typing.Conversion

import Control.Monad.Identity

import Data.Bool
import Data.Nat

import Decidable.Equality

import Obs.Logging
import Obs.NormalForm
import Obs.NormalForm.Normalise
import Obs.Substitution
import Obs.Universe

%default total

-- Conversion ------------------------------------------------------------------

convertUntyped : (rel : Relevance) -> (left, right : NormalForm rel ctx) -> Identity Bool

export
convert : (rel : Relevance)
  -> (type : TypeNormalForm ctx)
  -> (left, right : NormalForm rel ctx)
  -> Identity Bool
convert rel type left right = convertUntyped rel left right

convertCnstr : (left, right : Constructor ctx) -> Identity Bool
convertCnstr (Universe {s}) (Universe {s = s'}) = pure (s == s')
convertCnstr
  (Pi {domainSort, codomainSort, domain, codomain})
  (Pi
    { domainSort = domainSort'
    , codomainSort = codomainSort'
    , domain = domain'
    , codomain = codomain'
    }) = do
  let Yes Refl = decEq (domainSort, codomainSort) (domainSort', codomainSort')
    | No _ => pure False

  convertDomain <- convert
    { rel = Relevant
    , type = cast domainSort
    , left = assert_smaller domain domain.type
    , right = assert_smaller domain' domain'.type
    }

  convertCodomain <- convert
    { rel = Relevant
    , type = cast codomainSort
    , left = codomain
    , right = codomain'
    }

  pure (convertDomain && convertCodomain)
convertCnstr
  (Lambda {domainRel, var = _, body})
  (Lambda {domainRel = domainRel', var = _, body = body'}) = do
  let Yes Refl = decEq domainRel domainRel'
    | No _ => pure False

  convertUntyped {rel = Relevant, left = body, right = body'}
convertCnstr
  (Sigma {indexSort, elementSort, index, element})
  (Sigma
    { indexSort = indexSort'
    , elementSort = elementSort'
    , index = index'
    , element = element'
    }) = do
  let Yes Refl = decEq (indexSort, elementSort) (indexSort', elementSort')
    | No _ => pure False

  convertIndex <- convert
    { rel = Relevant
    , type = cast indexSort
    , left = assert_smaller index index.type
    , right = assert_smaller index' index'.type
    }

  convertElement <- convert
    { rel = Relevant
    , type = cast elementSort
    , left = element
    , right = element'
    }

  pure (convertIndex && convertElement)
convertCnstr
  (Pair {indexRel, elementRel, prf = _, first, second})
  (Pair
    { indexRel = indexRel'
    , elementRel = elementRel'
    , prf = _
    , first = first'
    , second = second'
    }) = do
  let Yes Refl = decEq (indexRel, elementRel) (indexRel', elementRel')
    | No _ => pure False

  convertFirst <- convertUntyped {rel = indexRel, left = first, right = first'}
  convertSecond <- convertUntyped {rel = elementRel, left = second, right = second'}
  pure (convertFirst && convertSecond)
convertCnstr Bool Bool = pure True
convertCnstr True True = pure True
convertCnstr False False = pure True
convertCnstr (Box {prop}) (Box {prop = prop'}) =
  convert {rel = Relevant, type = cast Prop, left = prop, right = prop'}
convertCnstr MkBox MkBox = pure True
convertCnstr Top Top = pure True
convertCnstr Bottom Bottom = pure True
convertCnstr left right = pure False

convertNtrl : (left, right : Neutral ctx) -> Identity Bool
convertNtrl (Var {var = _, i}) (Var {var = _, i = j}) = pure (elemToNat i == elemToNat j)
convertNtrl (App {argRel, fun, arg}) (App {argRel = argRel', fun = fun', arg = arg'}) = do
  let Yes Refl = decEq argRel argRel'
    | No _ => pure False

  convertFun <- convertNtrl {left = fun, right = fun'}
  convertArg <- convertUntyped {rel = argRel, left = arg, right = arg'}
  pure (convertFun && convertArg)
convertNtrl (First {secondRel = _, arg}) (First {secondRel = _, arg = arg'}) =
  convertNtrl arg arg'
convertNtrl (Second {firstRel = _, arg}) (Second {firstRel = _, arg = arg'}) =
  convertNtrl arg arg'
convertNtrl
  (If {discriminant, true, false})
  (If {discriminant = discriminant', true = true', false = false'}) =
  do
  convertDiscriminant <- convertNtrl {left = discriminant, right = discriminant}
  convertTrue <- convertUntyped {rel = Relevant, left = true, right = true'}
  convertFalse <- convertUntyped {rel = Relevant, left = false, right = false'}
  pure (convertDiscriminant && convertTrue && convertFalse)
convertNtrl Absurd Absurd = pure True
convertNtrl
  (Equal {type, left, right})
  (Equal {type = type', left = left', right = right'}) =
  do
  convertType <- convertNtrl {left = type, right = type'}
  convertLeft <- convertUntyped {rel = Relevant, left = left, right = left'}
  convertRight <- convertUntyped {rel = Relevant, left = right, right = right'}
  pure (convertType && convertLeft && convertRight)
-- We don't need to check, e.g. EqualL and EqualR
-- Assume (EqualL left right) ~~ (EqualR left' right')
-- Then (Ntrl left) ~~ (Cnstr left')
-- This means left' is either Lambda or Pair
-- Lamda and Pair are not type constructors.
-- Hence we have a contradiction, so we are done.
convertNtrl (EqualL {left, right}) (EqualL {left = left', right = right'}) = do
  convertLeft <- convertNtrl {left = left, right = left'}
  convertRight <- convertUntyped {rel = Relevant, left = right, right = right'}
  pure (convertLeft && convertRight)
convertNtrl (EqualR {left, right}) (EqualR {left = left', right = right'}) = do
  convertLeft <- convertCnstr {left = left, right = left'}
  convertRight <- convertNtrl {left = right, right = right'}
  pure (convertLeft && convertRight)
convertNtrl (EqualStuck {left, right}) (EqualStuck {left = left', right = right'}) = do
  convertLeft <- convertCnstr {left = left, right = left'}
  convertRight <- convertCnstr {left = right, right = right'}
  pure (convertLeft && convertRight)
convertNtrl
  (CastL {oldType, newType, value})
  (CastL {oldType = oldType', newType = newType', value = value'}) =
  do
  convertOldType <- convertNtrl {left = oldType, right = oldType'}
  convertNewType <- convertUntyped {rel = Relevant, left = newType, right = newType'}
  convertValue <- convertUntyped {rel = Relevant, left = value, right = value'}
  pure (convertOldType && convertNewType && convertValue)
convertNtrl
  (CastR {oldType, newType, value})
  (CastR {oldType = oldType', newType = newType', value = value'}) =
  do
  convertOldType <- convertCnstr {left = oldType, right = oldType'}
  convertNewType <- convertNtrl {left = newType, right = newType'}
  convertValue <- convertUntyped {rel = Relevant, left = value, right = value'}
  pure (convertOldType && convertNewType && convertValue)
convertNtrl
  (CastStuck {oldType, newType, value})
  (CastStuck {oldType = oldType', newType = newType', value = value'}) =
  do
  convertOldType <- convertCnstr {left = oldType, right = oldType'}
  convertNewType <- convertCnstr {left = newType, right = newType'}
  convertValue <- convertUntyped {rel = Relevant, left = value, right = value'}
  pure (convertOldType && convertNewType && convertValue)
convertNtrl left right = pure False

convertEta : (left : Constructor ctx) -> (right : Neutral ctx) -> Identity Bool
convertEta (Lambda {domainRel, var, body}) right = do
  let right = weaken [domainRel] right
  let rightBody = App {argRel = domainRel, fun = right, arg = point Nothing Here}
  convertUntyped {rel = Relevant, left = body, right = Ntrl rightBody}
convertEta (Pair {indexRel = Relevant, elementRel = Relevant, prf, first, second}) right = do
  let rightFirst = First {secondRel = Relevant, arg = right}
  let rightSecond = Second {firstRel = Relevant, arg = right}
  convertFirst <- convertUntyped {rel = Relevant, left = first, right = Ntrl rightFirst}
  convertSecond <- convertUntyped {rel = Relevant, left = second, right = Ntrl rightSecond}
  pure (convertFirst && convertSecond)
convertEta (Pair {indexRel = Relevant, elementRel = Irrelevant, prf, first, second}) right = do
  let rightFirst = First {secondRel = Relevant, arg = right}
  convertUntyped {rel = Relevant, left = first, right = Ntrl rightFirst}
convertEta (Pair {indexRel = Irrelevant, elementRel = Relevant, prf, first, second}) right = do
  let rightSecond = Second {firstRel = Relevant, arg = right}
  convertUntyped {rel = Relevant, left = second, right = Ntrl rightSecond}
convertEta MkBox right = pure True
convertEta left right = pure False

convertUntyped Irrelevant left right = pure True
convertUntyped Relevant (Ntrl left) (Ntrl right) = convertNtrl left right
convertUntyped Relevant (Ntrl left) (Cnstr right) = assert_total (convertEta right left)
convertUntyped Relevant (Cnstr left) (Ntrl right) = convertEta left right
convertUntyped Relevant (Cnstr left) (Cnstr right) = convertCnstr left right