Add more program structure to type universes.

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)