systemqfw

commit 4ba1eb6a4f4e8b9ca44327011c419f5eeccfcfbb
parent d23e713b8fd81d2edd633ad3f6554ae88a3c7a07
Author: Robert Russell <robert@rr3.xyz>
Date:   Wed, 28 Aug 2024 23:34:53 -0700

Add let bindings to terms

Diffstat:
M
Main.hs
 | 
20
+++++++++++++++++++-
M
Parser.hs
 | 
16
++++++++++++++--
M
Surface.hs
 | 
1
+

3 files changed, 34 insertions(+), 3 deletions(-)
diff --git a/Main.hs b/Main.hs
@@ -3,6 +3,7 @@ import Control.Monad
 import Control.Monad.Except
 import Control.Monad.Reader
 import Data.ByteString (ByteString)
+import qualified Data.ByteString as ByteString
 import Sparsec
 
 import Algebra
@@ -46,6 +47,7 @@ data Err
     | ErrTypeArrowAppNotArrow
     | ErrTermInferCheckMismatch
     | ErrTermVarUnbound
+    | ErrTermLetQuantityMismatch
     | ErrTermArrowAbsNotInferable
     | ErrTermArrowAbsQuantityMismatch
     | ErrTermArrowAbsNotArrow
@@ -183,6 +185,18 @@ inferTerm t q = case t of
         (t', tLedger) <- checkTerm t q a''
         pure (t', a'', tLedger)
 
+    S.TermLet x arg rb body -> do
+        rb' <- checkType rb KindQT
+        rb'' <- evalType rb'
+        let r = V.qtFst rb''
+        let b = V.qtSnd rb''
+        (arg', argLedger) <- checkTerm arg r b
+        bindAndAssignTerm x b \lvl -> do
+            (body', bodyType, bodyLedger) <- inferTerm body q
+            let (argDemand, letLedger) = L.split lvl bodyLedger
+            unless (r `V.qGeq` argDemand) $ throwError ErrTermLetQuantityMismatch
+            pure (C.TermArrowApp (C.TermArrowAbs body') arg', bodyType, letLedger <+> argLedger)
+
     S.TermArrowAbs _ _ -> throwError ErrTermArrowAbsNotInferable
 
     S.TermArrowApp fun arg -> do
@@ -239,7 +253,11 @@ checkTerm t q a = case (t, a) of
 --------------------------------------------------------------------------------
 
 input :: ByteString
-input = "\\[M] z s => z : @M:* -> M -> (M -> M) -> M"
+input =
+    ByteString.intercalate "\n" [
+        "let zero : @M:* -> M -> (M -> M) -> M = \\[M] z s => z;",
+        "zero"
+    ]
 
 main :: IO ()
 main =
diff --git a/Parser.hs b/Parser.hs
@@ -50,7 +50,7 @@ isIdentCont :: Char -> Bool
 isIdentCont = isWordCont
 
 isReservedIdent :: ByteString -> Bool
-isReservedIdent s = s == "bot" || s == "top"
+isReservedIdent s = s == "bot" || s == "top" || s == "let"
 
 pWs :: Monad m => ParseT Err m ByteString
 pWs = charWhile isSpace
@@ -156,12 +156,24 @@ pTermAbs = do
     body <- pTerm 1 `cut` Err
     pure $ foldr1 (.) binders body
 
+pTermLet :: P q (Term q)
+pTermLet = do
+    pWord "let"
+    x <- pTermName `cut` Err
+    pSym ":" `cut` Err
+    qa <- pType 0 `cut` Err
+    pSym "=" `cut` Err
+    arg <- pTerm 1 `cut` Err
+    pSym ";" `cut` Err
+    body <- pTerm 1 `cut` Err
+    pure $ TermLet x arg qa body
+
 pTerm :: Int -> P q (Term q)
 pTerm = \case
     0 -> do
         t <- pTerm 1
         pTermAnnot t <|> pure t
-    1 -> pTermAbs <|> pTerm 2
+    1 -> pTermAbs <|> pTermLet <|> pTerm 2
     2 -> pTerm 3 >>= iter \t -> TermArrowApp t <$> pTerm 3
         <|> TermForallApp t <$> pDelim "[" (pType 0) "]"
     3 -> TermVar <$> pTermName
diff --git a/Surface.hs b/Surface.hs
@@ -27,6 +27,7 @@ data Type q
 data Term q
     = TermVar TermName
     | TermAnnot (Term q) (Type q)
+    | TermLet TermName (Term q) (Type q) (Term q)
 
     | TermArrowAbs TermName (Term q)
     | TermArrowApp (Term q) (Term q)