systemqfw

commit d9f8021abfe73b38a5de9e93cc2bf5152baf5098
parent 28f3bc9cd70267578af66975c8216ca595fcc2e3
Author: Robert Russell <robert@rr3.xyz>
Date:   Thu, 29 Aug 2024 00:10:11 -0700

Add means to declare types

Diffstat:
M
Main.hs
 | 
75
++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++-------------
M
Parser.hs
 | 
10
++++++++--

2 files changed, 70 insertions(+), 15 deletions(-)
diff --git a/Main.hs b/Main.hs
@@ -3,10 +3,13 @@ import Control.Monad
 import Control.Monad.Except
 import Control.Monad.Reader
 import Data.ByteString (ByteString)
+import Data.Foldable (foldlM)
 import qualified Data.ByteString as ByteString
 import Sparsec
+import System.Exit
 
 import Algebra
+import Qul (Qul)
 import Ledger (Ledger)
 import qualified Ledger as L
 import Common
@@ -252,20 +255,66 @@ checkTerm t q a = case (t, a) of
 
 --------------------------------------------------------------------------------
 
-input :: ByteString
+type Q = Qul
+pQ :: Parse P.Err Q
+pQ = P.pQul
+
+data Decl = Decl ByteString ByteString ByteString
+
+data Prog = Prog {
+    decls :: [Decl],
+    body :: ByteString
+}
+
+parseKind :: ByteString -> IO Kind
+parseKind k =
+    case P.runP P.pTopKind pQ k of
+        Ok k _ _ -> pure k
+        result -> print result *> exitFailure
+
+parseType :: ByteString -> IO (S.Type Q)
+parseType a =
+    case P.runP P.pTopType pQ a of
+        Ok a _ _ -> pure a
+        result -> print result *> exitFailure
+
+parseTerm :: ByteString -> IO (S.Term Q)
+parseTerm t =
+    case P.runP P.pTopTerm pQ t of
+        Ok t _ _ -> pure t
+        result -> print result *> exitFailure
+
+declare :: TypeCtx Q -> Decl -> IO (TypeCtx Q)
+declare typeCtx (Decl x k a) = do
+    let x' = S.TypeName x
+    k' <- parseKind k
+    a' <- parseType a
+    a'' <- case checkType a' k' `runElab` BothCtx typeCtx Ctx.empty of
+        Left e -> print e *> exitFailure
+        Right a -> pure a
+    let a''' = V.evalType typeCtx.env a''
+    let (lvl, typeCtx') = Ctx.bindAndAssign x' k' typeCtx
+    pure $ Ctx.define lvl a''' typeCtx'
+
+input :: Prog
 input =
-    ByteString.intercalate "\n" [
-        "let zero : @M:* -> M -> (M -> M) -> M = \\[M] z s => z;",
-        "\\[M] z s => z : @M:* -> M -> (M -> M) -> M"
+    Prog [
+        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);",
+        "succ (succ zero)"
     ]
 
 main :: IO ()
-main =
-    case P.runP P.pSrc P.pQul input of
-        Ok t _ _ ->
-            case inferTerm t one `runElab` bothCtxEmpty of
-                Left e -> print e
-                Right (t, a, _) -> do
-                    print t
-                    print $ V.quoteType Env.empty a
-        result -> print result
+main = do
+    typeCtx <- foldlM declare Ctx.empty input.decls
+    t <- parseTerm input.body
+    case inferTerm t one `runElab` BothCtx typeCtx Ctx.empty of
+        Left e -> print e
+        Right (t, a, _) -> do
+            putStrLn "term:"
+            print t
+            putStrLn "----------------------------"
+            putStrLn "type:"
+            print $ V.quoteType Env.empty a
diff --git a/Parser.hs b/Parser.hs
@@ -98,6 +98,9 @@ pKind = \case
         <|> pDelim "(" (pKind 0) ")"
     _ -> error "pKind: invalid precedence"
 
+pTopKind :: P q Kind
+pTopKind = pWs *> pKind 0 <* eof
+
 pTypeAnnot :: Type q -> P q (Type q)
 pTypeAnnot a = pSym ":" *> (TypeAnnot a <$> pKind 0) `cut` Err
 
@@ -144,6 +147,9 @@ pType = \case
         <|> pDelim "(" (pType 0) ")"
     _ -> error "pType: invalid precedence"
 
+pTopType :: P q (Type q)
+pTopType = pWs *> pType 0 <* eof
+
 pTermAnnot :: Term q -> P q (Term q)
 pTermAnnot t = pSym ":" *> (TermAnnot t <$> pType 0) `cut` Err
 
@@ -180,5 +186,5 @@ pTerm = \case
         <|> pDelim "(" (pTerm 0) ")"
     _ -> error "pTerm: invalid precedence"
 
-pSrc :: P q (Term q)
-pSrc = pWs *> pTerm 0 <* eof
+pTopTerm :: P q (Term q)
+pTopTerm = pWs *> pTerm 0 <* eof