systemqfw

commit 7f47d266632f566073389743af7edc0c6500dce9
parent 7f339c58c6d34e9ecb44725e74b78bdb1ea8110c
Author: Robert Russell <robert@rr3.xyz>
Date:   Mon, 23 Dec 2024 13:24:54 -0800

Add stuff

I have no idea what these changes are. I'm just putting them in VC
so I have access to them while I'm away from home. I really ought
to do a better job of using git in the future.

Diffstat:
M
Main.hs
 | 
4
++--
M
Value.hs
 | 
23
++++++++++++++---------

2 files changed, 16 insertions(+), 11 deletions(-)
diff --git a/Main.hs b/Main.hs
@@ -34,7 +34,7 @@ a `orThrowError` e =
 -- Elaboration monad
 
 type TypeCtx q = Ctx S.TypeName C.TypeIdx (V.Type q) Kind
-type TermCtx q = Ctx S.TermName C.TermIdx V.Term (V.Type q)
+type TermCtx q = Ctx S.TermName C.TermIdx (V.Term q) (V.Type q)
 data BothCtx q = BothCtx {
     typeCtx :: TypeCtx q,
     termCtx :: TermCtx q
@@ -308,7 +308,7 @@ declare typeCtx (Decl x k a) = do
 input :: Prog
 input =
     Prog [
-        Decl "Nat" "*" "@M:* -> M -> (M -> M) -> M"
+        Decl "Nat" "%" "@M:% -> M -> (M -> M) -> M"
     ] $ ByteString.intercalate "\n" [
         "let zero : Nat = \\[M] z s => z;",
         "let succ : Nat -> Nat = \\n => \\[M] z s => s (n [M] z s);",
diff --git a/Value.hs b/Value.hs
@@ -14,10 +14,7 @@ newtype TypeLvl = TypeLvl Int deriving (Eq, Show, IsInt)
 
 type TypeEnv q = Env C.TypeIdx (Type q)
 
-data TypeClosure q = TypeClosure {
-    env :: TypeEnv q,
-    abs :: C.Type q
-}
+data TypeClosure q = TypeClosure (TypeEnv q) (C.Type q)
 
 data Type q
     = TypeGeneric TypeLvl
@@ -148,11 +145,19 @@ convTypeClosure env xclo yclo =
 
 newtype TermLvl = TermLvl Int deriving (Eq, Show, IsInt)
 
-type TermEnv q = Env C.TermIdx Term
+type TermEnv q = Env C.TermIdx (Term q)
 
--- During elaboration, we only need to "evaluate" term variables.
-newtype Term = TermGeneric TermLvl
+data TermClosure q = TermClosure (TypeEnv q) (C.Term q)
 
-instance Value Term where
-    type Level Term = TermLvl
+data Term q
+   = TermGeneric TermLvl
+ 
+   | TermArrowAbs (TermClosure q)
+   | TermArrowApp (Term q) (Term q)
+
+   | TermForallAbs (TermClosure q)
+   | TermForallApp (Term q) (Type q)
+
+instance Value (Term q) where
+    type Level (Term q) = TermLvl
     generic = TermGeneric