diff options
Diffstat (limited to 'src/Obs/Typing/Conversion.idr')
-rw-r--r-- | src/Obs/Typing/Conversion.idr | 90 |
1 files changed, 45 insertions, 45 deletions
diff --git a/src/Obs/Typing/Conversion.idr b/src/Obs/Typing/Conversion.idr index d5dc86a..766c21e 100644 --- a/src/Obs/Typing/Conversion.idr +++ b/src/Obs/Typing/Conversion.idr @@ -4,36 +4,36 @@ import Control.Monad.Maybe import Control.Monad.Trans import Data.Bool -import Data.So +import Data.Nat import Decidable.Equality import Obs.Logging import Obs.NormalForm import Obs.NormalForm.Normalise -import Obs.Sort import Obs.Substitution +import Obs.Universe %default total -- Conversion ------------------------------------------------------------------ export -convert : (s : Sort) - -> (a : NormalForm True ctx) - -> (t, u : NormalForm (isSet s) ctx) - -> MaybeT (Logging ann) (NormalForm (isSet s) ctx) +convert : (s : Universe) + -> (a : TypeNormalForm ctx) + -> (t, u : NormalForm (relevance s) ctx) + -> MaybeT (Logging ann) (NormalForm (relevance s) ctx) -untypedConvert : (t, u : NormalForm True ctx) -> MaybeT (Logging ann) (NormalForm True ctx) +untypedConvert : (t, u : NormalForm Relevant ctx) -> MaybeT (Logging ann) (NormalForm Relevant ctx) -- Diagonals -untypedConvert (Cnstr (Sort s)) (Cnstr (Sort s')) = - if s == s' then pure (Cnstr (Sort s)) else nothing +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 (suc s) (cast s) a a') - b <- assert_total (convert (suc s') (cast s') b b') + 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' @@ -45,8 +45,8 @@ 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 (suc s) (cast s) a a') - b <- assert_total (convert (suc s') (cast s') b b') + 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') @@ -54,19 +54,19 @@ untypedConvert (Cnstr (Pair s@(Set _) s'@(Set _) prf t u)) (Cnstr (Pair l l' prf lift $ trace "converting pair pointwise" t <- untypedConvert t t' u <- untypedConvert u u' - pure (Cnstr $ Pair l l' Oh t 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 Oh t Irrel) + 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' Oh Irrel 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) @@ -74,23 +74,23 @@ 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 b t u)) rhs@(Ntrl (App b' t' u')) = do - let Yes Refl = decEq b b' +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 True = b' - | False => lift $ doApp t Irrel + let Relevant = r' + | Irrelevant => lift $ doApp t Irrel u <- untypedConvert u u' lift $ doApp t u -untypedConvert lhs@(Ntrl (Fst b t)) rhs@(Ntrl (Fst b' t')) = do +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 True b t -untypedConvert lhs@(Ntrl (Snd b t)) rhs@(Ntrl (Snd b' t')) = do + 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 b True (rewrite orTrueTrue b in 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')) @@ -139,25 +139,25 @@ untypedConvert lhs@(Ntrl (CastStuck a b t)) rhs@(Ntrl (CastStuck a' b' t')) = do lift $ doCast _ a b t -- Pi types untypedConvert t@(Cnstr (Lambda s var _)) (Ntrl u) = do - u <- lift $ doApp (Ntrl $ weaken [isSet s] u) (point (var, (s ** Refl)) Here) + 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 [isSet s] t) (point (var, (s ** Refl)) Here) + 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 (isSet s || isSet s') ctx - t'' = rewrite trans (sym $ maxIsSet s s') (soToEq prf) in t' + 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 (isSet s) (isSet s') t'' - u' <- lift $ doSnd (isSet s) (isSet s') t'' + 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 (isSet s || isSet s') ctx - t'' = rewrite trans (sym $ maxIsSet s s') (soToEq prf) in t + 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 (isSet s) (isSet s') t'' - u <- lift $ doSnd (isSet s) (isSet s') t'' + 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 @@ -168,33 +168,33 @@ 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 (Sort s)) t u = do +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 [isSet s] t) (point (var, (s ** Refl)) Here) - u' <- lift $ doApp (Sorted.weaken [isSet s] u) (point (var, (s ** Refl)) Here) + 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 True (isSet s') t - u1 <- lift $ doFst True (isSet s') u + t1 <- lift $ doFst Relevant (relevance s') t + u1 <- lift $ doFst Relevant (relevance s') u t1 <- convert s a t1 u1 - t2 <- lift $ doSnd True (isSet s') t - u2 <- lift $ doSnd True (isSet s') u + 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' Oh t1 t2) + 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 False True t - u2 <- lift $ doSnd False True u + 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' Oh Irrel t2) + 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) |