1 files changed, 190 insertions, 188 deletions
diff --git a/src/Obs/Typing/Conversion.idr b/src/Obs/Typing/Conversion.idr
index 766c21e..93812c1 100644
--- a/src/Obs/Typing/Conversion.idr
+++ b/src/Obs/Typing/Conversion.idr
@@ -1,7 +1,6 @@
 module Obs.Typing.Conversion
 
-import Control.Monad.Maybe
-import Control.Monad.Trans
+import Control.Monad.Identity
 
 import Data.Bool
 import Data.Nat
@@ -18,190 +17,193 @@ import Obs.Universe
 
 -- Conversion ------------------------------------------------------------------
 
+convertUntyped : (rel : Relevance) -> (left, right : NormalForm rel ctx) -> Identity Bool
+
 export
-convert : (s : Universe)
-  -> (a : TypeNormalForm ctx)
-  -> (t, u : NormalForm (relevance s) ctx)
-  -> MaybeT (Logging ann) (NormalForm (relevance s) ctx)
-
-untypedConvert : (t, u : NormalForm Relevant ctx) -> MaybeT (Logging ann) (NormalForm Relevant ctx)
--- Diagonals
-untypedConvert (Cnstr (Universe s)) (Cnstr (Universe s')) =
-  if s == s' then pure (Cnstr (Universe s)) else nothing
-untypedConvert (Cnstr (Pi s s' var a b)) (Cnstr (Pi l l' _ a' b')) = do
-  let Yes Refl = decEq s l
-    | No _ => nothing
-  lift $ trace "going back to type-directed conversion"
-  a <- assert_total (convert (succ s) (cast s) a a')
-  b <- assert_total (convert (succ s') (cast s') b b')
-  pure (Cnstr $ Pi s s' var a b)
-untypedConvert (Cnstr (Lambda s var t)) (Cnstr (Lambda s' _ u)) = do
-  let Yes Refl = decEq s s'
-    | No _ => nothing
-  lift $ trace "converting under lambda"
-  t <- untypedConvert t u
-  pure (Cnstr $ Lambda s var t)
-untypedConvert (Cnstr (Sigma s s' var a b)) (Cnstr (Sigma l l' _ a' b')) = do
-  let Yes Refl = decEq s l
-    | No _ => nothing
-  lift $ trace "going back to type-directed conversion"
-  a <- assert_total (convert (succ s) (cast s) a a')
-  b <- assert_total (convert (succ s') (cast s') b b')
-  pure (Cnstr $ Sigma s s' var a b)
-untypedConvert (Cnstr (Pair s@(Set _) s'@(Set _) prf t u)) (Cnstr (Pair l l' prf' t' u')) = do
-  let Yes Refl = decEq (s, s') (l, l')
-    | No _ => nothing
-  lift $ trace "converting pair pointwise"
-  t <- untypedConvert t t'
-  u <- untypedConvert u u'
-  pure (Cnstr $ Pair l l' Set t u)
-untypedConvert (Cnstr (Pair s@(Set _) Prop prf t u)) (Cnstr (Pair l Prop prf' t' u')) = do
-  let Yes Refl = decEq s l
-    | No _ => nothing
-  lift $ trace "converting pair pointwise"
-  t <- untypedConvert t t'
-  pure (Cnstr $ Pair l Prop Set t Irrel)
-untypedConvert (Cnstr (Pair Prop s'@(Set _) prf t u)) (Cnstr (Pair Prop l' prf' t' u')) = do
-  let Yes Refl = decEq s' l'
-    | No _ => nothing
-  lift $ trace "converting pair pointwise"
-  u <- untypedConvert u u'
-  pure (Cnstr $ Pair Prop l' Set Irrel u)
-untypedConvert (Cnstr Bool) (Cnstr Bool) = pure (Cnstr Bool)
-untypedConvert (Cnstr True) (Cnstr True) = pure (Cnstr True)
-untypedConvert (Cnstr False) (Cnstr False) = pure (Cnstr False)
-untypedConvert (Cnstr Top) (Cnstr Top) = pure (Cnstr Top)
-untypedConvert (Cnstr Bottom) (Cnstr Bottom) = pure (Cnstr Bottom)
-untypedConvert t@(Ntrl (Var _ _ _ i)) (Ntrl (Var _ _ _ j)) =
-  if elemToNat i == elemToNat j then pure t else nothing
-untypedConvert lhs@(Ntrl (App r t u)) rhs@(Ntrl (App r' t' u')) = do
-  let Yes Refl = decEq r r'
-    | No _ => nothing
-  lift $ trace "checking parts of a spine"
-  t <- untypedConvert (assert_smaller lhs (Ntrl t)) (assert_smaller rhs (Ntrl t'))
-  let Relevant = r'
-    | Irrelevant => lift $ doApp t Irrel
-  u <- untypedConvert u u'
-  lift $ doApp t u
-untypedConvert lhs@(Ntrl (Fst r t)) rhs@(Ntrl (Fst r' t')) = do
-  lift $ trace "checking full pair for fst"
-  t <- untypedConvert (assert_smaller lhs (Ntrl t)) (assert_smaller rhs (Ntrl t'))
-  lift $ doFst Relevant r t
-untypedConvert lhs@(Ntrl (Snd r t)) rhs@(Ntrl (Snd r' t')) = do
-  lift $ trace "checking full pair for snd"
-  t <- untypedConvert (assert_smaller lhs (Ntrl t)) (assert_smaller rhs (Ntrl t'))
-  lift $ doSnd r Relevant (rewrite pairRelevantRight r in t)
-untypedConvert lhs@(Ntrl (If t f g)) rhs@(Ntrl (If t' f' g')) = do
-  lift $ trace "checking all branches of if"
-  t <- untypedConvert (assert_smaller lhs (Ntrl t)) (assert_smaller rhs (Ntrl t'))
-  f <- untypedConvert f f'
-  g <- untypedConvert g g'
-  lift $ doIf t f g
-untypedConvert (Ntrl Absurd) (Ntrl Absurd) = pure (Ntrl Absurd)
-untypedConvert lhs@(Ntrl (Equal a t u)) rhs@(Ntrl (Equal a' t' u')) = do
-  lift $ trace "checking equal (stuck on type)"
-  a <- untypedConvert (assert_smaller lhs (Ntrl a)) (assert_smaller rhs (Ntrl a'))
-  t <- untypedConvert t t'
-  u <- untypedConvert u u'
-  lift $ doEqual _ a t u
-untypedConvert lhs@(Ntrl (EqualL t u)) rhs@(Ntrl (EqualL t' u')) = do
-  lift $ trace "checking equal (stuck on left)"
-  t <- untypedConvert (assert_smaller lhs (Ntrl t)) (assert_smaller rhs (Ntrl t'))
-  u <- untypedConvert u u'
-  lift $ doEqualSet t u
-untypedConvert lhs@(Ntrl (EqualR t u)) rhs@(Ntrl (EqualR t' u')) = do
-  lift $ trace "checking equal (stuck on right)"
-  t <- untypedConvert (assert_smaller lhs (Cnstr t)) (assert_smaller rhs (Cnstr t'))
-  u <- untypedConvert (assert_smaller lhs (Ntrl u)) (assert_smaller rhs (Ntrl u'))
-  lift $ doEqualSet t u
-untypedConvert lhs@(Ntrl (EqualStuck t u)) rhs@(Ntrl (EqualStuck t' u')) = do
-  lift $ trace "checking equal (head mismatch)"
-  t <- untypedConvert (assert_smaller lhs (Cnstr t)) (assert_smaller rhs (Cnstr t'))
-  u <- untypedConvert (assert_smaller lhs (Cnstr u)) (assert_smaller rhs (Cnstr u'))
-  lift $ doEqualSet t u
-untypedConvert lhs@(Ntrl (CastL a b t)) rhs@(Ntrl (CastL a' b' t')) = do
-  lift $ trace "checking cast (stuck on left)"
-  a <- untypedConvert (assert_smaller lhs (Ntrl a)) (assert_smaller rhs (Ntrl a'))
-  b <- untypedConvert b b'
-  t <- untypedConvert t t'
-  lift $ doCast _ a b t
-untypedConvert lhs@(Ntrl (CastR a b t)) rhs@(Ntrl (CastR a' b' t')) = do
-  lift $ trace "checking cast (stuck on right)"
-  a <- untypedConvert (assert_smaller lhs (Cnstr a)) (assert_smaller rhs (Cnstr a'))
-  b <- untypedConvert (assert_smaller lhs (Ntrl b)) (assert_smaller rhs (Ntrl b'))
-  t <- untypedConvert t t'
-  lift $ doCast _ a b t
-untypedConvert lhs@(Ntrl (CastStuck a b t)) rhs@(Ntrl (CastStuck a' b' t')) = do
-  lift $ trace "checking cast (stuck on left)"
-  a <- untypedConvert (assert_smaller lhs (Cnstr a)) (assert_smaller rhs (Cnstr a'))
-  b <- untypedConvert (assert_smaller lhs (Cnstr b)) (assert_smaller rhs (Cnstr b'))
-  t <- untypedConvert t t'
-  lift $ doCast _ a b t
--- Pi types
-untypedConvert t@(Cnstr (Lambda s var _)) (Ntrl u) = do
-  u <- lift $ doApp (Ntrl $ weaken [relevance s] u) (point (var, (s ** Refl)) Here)
-  assert_total (untypedConvert t (Cnstr (Lambda s var u)))
-untypedConvert (Ntrl t) u@(Cnstr (Lambda s var _)) = do
-  t <- lift $ doApp (Ntrl $ weaken [relevance s] t) (point (var, (s ** Refl)) Here)
-  assert_total (untypedConvert (Cnstr (Lambda s var t)) u)
--- Sigma types
-untypedConvert t@(Cnstr (Pair s s' prf _ _)) t'@(Ntrl _) =
-  let t'' : NormalForm (pair (relevance s) (relevance s')) ctx
-      t'' = rewrite trans (sym $ pairRelevance s s') (forgetIsRelevant prf) in t'
-  in do
-  t' <- lift $ doFst (relevance s) (relevance s') t''
-  u' <- lift $ doSnd (relevance s) (relevance s') t''
-  assert_total (untypedConvert t (Cnstr (Pair s s' prf t' u')))
-untypedConvert t@(Ntrl _) t'@(Cnstr (Pair s s' prf _ _)) =
-  let t'' : NormalForm (pair (relevance s) (relevance s')) ctx
-      t'' = rewrite trans (sym $ pairRelevance s s') (forgetIsRelevant prf) in t
-  in do
-  t <- lift $ doFst (relevance s) (relevance s') t''
-  u <- lift $ doSnd (relevance s) (relevance s') t''
-  assert_total (untypedConvert (Cnstr (Pair s s' prf t u)) t')
--- Bools
--- no cases because diagonals complete
--- Fallback
-untypedConvert _ _ = nothing
-
-convert Prop a Irrel Irrel = pure Irrel
-convert (Set k) (Ntrl a) t u = do
-  lift $ trace $ pretty {ann} "cannot do type-directed conversion on" <++> pretty a
-  untypedConvert t u
-convert (Set k) (Cnstr (Universe s)) t u = do
-  lift $ trace $ pretty {ann} "converting in type" <++> pretty s
-  untypedConvert t u
-convert (Set k) (Cnstr (Pi s s'@(Set _) var a b)) t u = do
-  -- s' must be Set, otherwise ty is in Prop
-  lift $ trace "converting pi type"
-  t' <- lift $ doApp (Sorted.weaken [relevance s] t) (point (var, (s ** Refl)) Here)
-  u' <- lift $ doApp (Sorted.weaken [relevance s] u) (point (var, (s ** Refl)) Here)
-  t <- convert s' b t' u'
-  pure (Cnstr $ Lambda s var t)
-convert (Set k) ty@(Cnstr (Sigma s@(Set j) s' var a b)) t u = do
-  lift $ trace "converting sigma type"
-  t1 <- lift $ doFst Relevant (relevance s') t
-  u1 <- lift $ doFst Relevant (relevance s') u
-  t1 <- convert s a t1 u1
-  t2 <- lift $ doSnd Relevant (relevance s') t
-  u2 <- lift $ doSnd Relevant (relevance s') u
-  b <- lift $ subst1 t1 b
-  t2 <- convert s' (assert_smaller ty b) t2 u2
-  pure (Cnstr $ Pair s s' Set t1 t2)
-convert (Set k) ty@(Cnstr (Sigma Prop s'@(Set _) var a b)) t u = do
-  lift $ trace "converting sigma type (snd only)"
-  t2 <- lift $ doSnd Irrelevant Relevant t
-  u2 <- lift $ doSnd Irrelevant Relevant u
-  b <- lift $ subst1 Irrel b
-  t2 <- convert s' (assert_smaller ty b) t2 u2
-  pure (Cnstr $ Pair Prop s' Set Irrel t2)
-convert (Set 0) (Cnstr Bool) (Cnstr True) (Cnstr True) = do
-  lift $ trace "converting bool (true)"
-  pure (Cnstr True)
-convert (Set 0) (Cnstr Bool) (Cnstr False) (Cnstr False) = do
-  lift $ trace "converting bool (false)"
-  pure (Cnstr False)
-convert (Set k) (Cnstr Bool) t@(Ntrl _) u@(Ntrl _) = do
-  lift $ trace "converting bool (neutral)"
-  untypedConvert t u
-convert (Set k) (Cnstr a) t u = lift $ inScope "bad type constructor" $ fatal a
+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
+  left@(Pair {indexRel, elementRel, prf = _, first, second})
+  right@(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 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 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