Track HLevels of Sets and Theories

packages/coln-compiler/src/Coln/Core/Layout.hs

@@ -49,7 +49,7 @@ bind sc x a =
 
 layout :: Path -> Scope -> V.Ty N -> (Trie Generator, M.El N)
 layout p sc a
-  | levelOf a == Theory = case V.behavior a of
+  | (levelOf a).mlevel == Theory = case V.behavior a of
       V.LikeFunction ft -> do
         let x = argName sc.usedNames ft.cod
         let (v, sc') = bind sc x ft.dom
@@ -65,13 +65,14 @@ layout p sc a
         let (gts, ms) = go rt.capture (toList rt.fieldTypes)
         let m = M.cons (Dict rt.fieldTypes.head (Vector.fromList ms))
         (Node $ Dict rt.fieldTypes.head (Vector.fromList gts), m)
-      V.LikeU SetU -> do
+      V.LikeU (SetU; PropU) -> do
+        -- TODO: layout Prop correctly
         let gt = Leaf (Rel (toList sc.names) (toList sc.ctx))
         let a = V.EltOf (TableName sc.realm p) (fromList $ zip (toList sc.names) (toList sc.bound))
         (gt, M.code (M.fromVTy sc.len a))
       V.NoRules -> panic "cannot layout type with no rules"
       V.LikeBuiltinTy _; V.LikeU _ -> panic "non-theory type"
-  | levelOf a == Set = do
+  | (levelOf a).mlevel == Set = do
       let gt = Leaf (Fun (toList sc.names) (toList sc.ctx) (readb sc.len a))
       let v = V.Lookup (TableName sc.realm p) (fromList $ zip (toList sc.names) (toList sc.bound))
       (gt, M.fromVEl sc.len v)

packages/coln-compiler/src/Coln/Core/Params.hs

@@ -12,75 +12,126 @@ import Prettyprinter
 -- Level stuff (levels, universes, function variants)
 --------------------------------------------------------------------------------
 
-data Level
+data MLevel
   = Set
   | Theory
   | Top
   deriving (Eq, Show)
 
-instance DPretty Level where
+instance DPretty MLevel where
   dpretty = pretty . show
 
-instance PartialOrd Level where
+instance PartialOrd MLevel where
   leq l1 l2 = case (l1, l2) of
     (Set, _) -> True
     (Theory, Set) -> False
     (Theory, _) -> True
     (Top, Top) -> True
     (Top, _) -> False
 
-maxLevel :: Level -> Level -> Level
-maxLevel l1 l2
+maxMLevel :: MLevel -> MLevel -> MLevel
+maxMLevel l1 l2
   | leq l1 l2 = l2
   | otherwise = l1
 
+data HLevel
+  = HUnit
+  | HProp
+  | HSet
+  | HTop
+  deriving (Eq, Show, Ord)
+
+instance PartialOrd HLevel where
+  leq l1 l2 = l1 <= l2
+
+equalityHLevelOf :: HLevel -> HLevel
+equalityHLevelOf = \case
+  HUnit -> HUnit
+  HProp -> HUnit
+  HSet -> HProp
+  HTop -> HTop
+
+data Level = Level
+  { mlevel :: MLevel
+  , hlevel :: HLevel
+  }
+  deriving (Eq, Show)
+
+instance PartialOrd Level where
+  leq (Level s1 h1) (Level s2 h2) = s1 `leq` s2 && h1 `leq` h2
+
+maxLevel :: Level -> Level -> Level
+maxLevel l1 l2 = Level (maxMLevel l1.mlevel l2.mlevel) (max l1.hlevel l2.hlevel)
+
 class LevelOf a where
   levelOf :: a -> Level
 
 data Universe
-  = SetU
+  = PropU
+  | SetU
   | TheoryU
+  | PropTheoryU -- TODO: better name?
   deriving (Eq, Show)
 
 decodesInto :: Universe -> Level
 decodesInto = \case
-  SetU -> Set
-  TheoryU -> Theory
+  PropU -> Level Set HProp
+  SetU -> Level Set HSet
+  PropTheoryU -> Level Theory HProp
+  TheoryU -> Level Theory HSet
 
 codesInto :: Universe -> Level
 codesInto = \case
-  SetU -> Theory
-  TheoryU -> Top
+  PropU -> Level Theory HSet
+  SetU -> Level Theory HSet
+  TheoryU -> Level Top HSet
+  PropTheoryU -> Level Top HSet
 
 instance Pretty Universe where
   pretty = \case
+    PropU -> "Prop"
     SetU -> "Set"
     TheoryU -> "Theory"
+    PropTheoryU -> "PropTheory"
 
 universeFor :: Level -> Maybe Universe
 universeFor = \case
-  Set -> Just SetU
-  Theory -> Just TheoryU
-  Top -> Nothing
+  Level Set (HUnit; HProp) -> Just PropU
+  Level Set HSet -> Just SetU
+  Level Theory (HUnit; HProp) -> Just PropTheoryU
+  Level Theory HSet -> Just TheoryU
+  Level _ _ -> Nothing
 
-data FunctionVariant
+data FunctionVariantMLevel
   = SetTheory
   | TheoryTop
   deriving (Eq, Show)
 
+functionMLevelFor :: MLevel -> MLevel -> Maybe FunctionVariantMLevel
+functionMLevelFor v1 v2 = case (v1, v2) of
+  (Set, (Set; Theory)) -> pure SetTheory
+  (Set, Top) -> pure TheoryTop
+  (Theory, _) -> pure TheoryTop
+  (Top, _) -> Nothing
+
+data FunctionVariant = FunctionVariant {mlevel :: FunctionVariantMLevel, hlevel :: HLevel}
+  deriving (Eq, Show)
+
 instance Pretty FunctionVariant where
   pretty = pretty . show
 
 instance LevelOf FunctionVariant where
-  levelOf = \case
-    SetTheory -> Theory
-    TheoryTop -> Top
+  levelOf v = Level mlevel v.hlevel
+   where
+    mlevel = case v.mlevel of
+      SetTheory -> Theory
+      TheoryTop -> Top
 
 class HasCodomain a b | a -> b where
   codOf :: a -> b
 
-instance HasCodomain FunctionVariant Level where
-  codOf = \case
+instance HasCodomain FunctionVariant MLevel where
+  codOf v = case v.mlevel of
     SetTheory -> Theory
     TheoryTop -> Top
 

packages/coln-compiler/src/Coln/Core/Print.hs

@@ -69,7 +69,7 @@ nbinding x n = N.Infix (N.Ident x ()) (N.Keyword ":" ()) n
 
 instance ToNotation (Ty e) where
   toNotation xs = \case
-    U u -> N.Keyword (fromString $ show $ decodesInto u) ()
+    U u -> N.Keyword (fromString $ show $ pretty u) ()
     Decode t -> toNotation xs t
     Function f -> case f.cod of
       Abs x b ->

packages/coln-compiler/src/Coln/Core/Value.hs

@@ -225,9 +225,9 @@ instance LevelOf (Ty c) where
     Decode n -> decodesInto n.universe
     Function ft -> levelOf ft.variant
     Record rt -> rt.level
-    Eq ety -> levelOf ety.at
-    BuiltinTy _ -> Set
-    EltOf _ _ -> Set
+    Eq ety -> Level (levelOf ety.at).mlevel (equalityHLevelOf (levelOf ety.at).hlevel)
+    BuiltinTy _ -> Level Set HSet -- Only Int/String so far
+    EltOf _ _ -> Level Set HSet -- TODO
 
 behavior :: Ty c -> TypeBehavior
 behavior = \case

packages/coln-compiler/src/Coln/Elaborator/Debug.hs

@@ -22,6 +22,7 @@ import Coln.Report
 data DebugCommand
   = ShowType Span (Syn N)
   | ShowTypeBehavior Span (Syn N)
+  | ShowLevel Span (Typ N)
   | Expand Span (Syn N)
 
 runDebug :: ElabEnv N -> DebugCommand -> IO ()
@@ -31,6 +32,9 @@ runDebug e (ShowType sp s) = do
 runDebug e (ShowTypeBehavior sp s) = do
   (a, m) <- s.elab e
   report e.diagEnv sp DebugMisc ("value" <+> prtIn e m.val <+> "has type" <+> prtIn e a <+> "with behavior" <+> prtIn e (V.behavior a))
+runDebug e (ShowLevel sp s) = do
+  ty <- s.elab e
+  report e.diagEnv sp DebugMisc ("type" <+> prtIn e ty <+> "has level" <+> (pretty $ show $ levelOf ty))
 runDebug e (Expand sp s) = do
   (_, m) <- s.elab e
   report e.diagEnv sp DebugMisc ("expands to:" <+> prtIn e (canon m.val))

packages/coln-compiler/src/Coln/Elaborator/Rules/Equality.hs

@@ -28,7 +28,7 @@ formation sp lhs rhs = Typ \e -> do
       let msg = "types" <+> prtIn e lty <+> "and" <+> prtIn e rty <+> "of compared terms differ"
       let note = Just $ dpretty err
       failWithNote e.diagEnv sp TypeMismatch msg note
-    Right _ -> case levelOf lty of
+    Right _ -> case (levelOf lty).mlevel of
       Set -> pure $ equality $ S.EqualityType (fromVTy e.scope.len lty) elhs erhs
       _ -> do
         let msg = "equality requires data types, but" <+> prtIn e lty <+> "is a schema-level type"

packages/coln-compiler/src/Coln/Elaborator/Rules/Function.hs

@@ -16,12 +16,12 @@ import Coln.Elaborator.Judgment
 import Coln.Report
 
 variantFor :: Ty N -> Ty N -> Span -> ElabEnv c -> IO FunctionVariant
-variantFor dom cod sp e = case (levelOf dom, levelOf cod) of
-  ((Set, Set); (Set, Theory)) -> pure SetTheory
-  ((Set, Top); (Theory, _)) -> pure TheoryTop
-  (Top, _) -> do
-    let msg = "higher-order theories are not supported"
-    failWith e.diagEnv sp FunctionDomainTooLarge msg
+variantFor dom cod sp e =
+  case functionMLevelFor (levelOf dom).mlevel (levelOf cod).mlevel of
+    Just l -> pure (FunctionVariant l (levelOf cod).hlevel)
+    Nothing -> do
+      let msg = "higher-order theories are not supported"
+      failWith e.diagEnv sp FunctionDomainTooLarge msg
 
 data Binder = Anonymous (Typ N) | Named Name (Typ N)
 

packages/coln-compiler/src/Coln/Elaborator/Rules/Record.hs

@@ -27,7 +27,7 @@ data FieldDeclaration
 
 formation :: [FieldDeclaration] -> Typ D
 formation fieldTyps = Typ $ \e -> do
-  let go _ [] = pure (Set, [])
+  let go _ [] = pure (Level Set HUnit, [])
       go e' ((FieldDeclaration x typ) : rest) = do
         ty <- typ.elab e'
         (l, fieldTys) <- go (e'{scope = bind x ty.val e'.scope}) rest

packages/coln-compiler/src/Coln/Frontend/Driver.hs

@@ -80,8 +80,11 @@ debugCommand e _ "showtype" n = do
   s <- syn e "argument to showtype" n
   pure $ ShowType (N.span n) s
 debugCommand e _ "showtypeb" n = do
-  s <- syn e "argument to showtype" n
+  s <- syn e "argument to showtypeb" n
   pure $ ShowTypeBehavior (N.span n) s
+debugCommand e _ "showlevel" n = do
+  ty <- typ e n
+  pure $ ShowLevel (N.span n) ty
 debugCommand e _ "expand" n = do
   s <- syn e "argument to expand" n
   pure $ Expand (N.span n) s
@@ -194,7 +197,7 @@ expr e n = case n of
     s <- syn e "target of elimination" n0
     fromSynN <$> elim e s n1
   N.Keyword "Set" _ -> pure $ fromTypN $ Universe.formation SetU
-  N.Keyword "Prop" _ -> pure $ fromTypN $ Universe.formation SetU
+  N.Keyword "Prop" _ -> pure $ fromTypN $ Universe.formation PropU
   N.Keyword "Int" _ -> pure $ fromTypN $ Builtin.formation BuiltinInt
   N.Keyword "String" _ -> pure $ fromTypN $ Builtin.formation BuiltinString
   N.Infix arg n@(N.Keyword "->" _) body ->

packages/coln-compiler/src/Coln/Frontend/Notation.hs

@@ -20,6 +20,7 @@ lexConfig =
     , ("import", K.Decl)
     , ("showtypeb", K.Decl)
     , ("showtype", K.Decl)
+    , ("showlevel", K.Decl)
     , ("expand", K.Decl)
     , ("end", K.End)
     , ("Set", K.AKeyword)

packages/coln-compiler/test/ancestor.output

@@ -3,7 +3,7 @@ global entry named Family
 type: Theory
 value: sig
   person : Set
-  is-parent : person -> person -> Set
+  is-parent : person -> person -> Prop
 end
 
 -- messages

packages/coln-compiler/test/hlevel.glog

@@ -0,0 +1,52 @@
+theory Family := sig
+  person : Set
+  is-parent : person -> person -> Prop
+
+  happy : Prop
+
+  showtype happy
+  showlevel happy
+  showtype is-parent
+  showtype happy -> person
+  showtype person -> happy
+end
+
+theory Q (F : Family) := sig
+  son : F.person
+  father : F.person
+
+  showtype F.is-parent
+  showtype F.is-parent father son
+end
+
+# Family analogies getting a bit risky
+theory HP := sig
+  person : Set
+
+  voldemort : person
+  tomriddle : person
+
+  showlevel voldemort = tomriddle
+
+  reveal : voldemort = tomriddle
+
+  showtype reveal
+  showlevel (reveal = reveal)
+end
+
+def Unit : Prop := sig
+end
+
+theory P := sig
+  showtype Unit
+  showlevel Unit
+
+  u : Unit
+  showtype u = u
+  showlevel u = u
+end
+
+def LevelJoinRecordIsNotSet (A : Set) (P : Prop) : Set := sig
+  f : A -> P
+  a : A
+end