Refactored parser into two: inner + outer

rationalis-petra · Nov 20, 2023 · 943de35 · 943de35
1 parent ff11bfd
commit 943de35
Show file tree

Hide file tree

Showing 13 changed files with 853 additions and 518 deletions.
diff --git a/app/Interactive.hs b/app/Interactive.hs
@@ -89,7 +89,7 @@ interactive (Interpreter {..}) opts = do
       env <- get_env ("repl" :| []) (istate^.imports)
       precs <- get_precs ("repl" :| []) (istate^.imports)
       resolution <- get_resolve ("repl" :| []) (istate^.imports)
-      parsed <- parseToErr (core precs <* eof) "console-in" line 
+      parsed <- core precs "console-in" line  -- TODO: eof??
       resolved <- resolve_closed (("unbound name" <+>) . pretty) resolution parsed
         `catchError` (throwError . (<+>) "Resolution:")
       (term, ty) <- infer (CheckInterp interp_eval interp_eq spretty) env resolved
@@ -127,7 +127,7 @@ interactive (Interpreter {..}) opts = do
 
     check_mod :: Text -> Text -> m InternalModule
     check_mod filename file = do
-      parsed <- parse (mod get_precs <* eof) filename file 
+      parsed <- mod get_precs filename file  -- TODO: eof??
         `catchError` (throwError . (<+>) "Parse:")
 
       resolve_vars <- get_resolve (parsed^.module_header) (parsed^.module_imports)

diff --git a/app/Server.hs b/app/Server.hs
@@ -11,7 +11,6 @@ import Control.Concurrent (forkFinally)
 
 import Data.Bifunctor
 import qualified Data.ByteString as Bs
-import Text.Megaparsec hiding (runParser)
 import Data.List.NonEmpty (NonEmpty(..))
 import Data.Text.IO
 import Data.Text (Text, pack)
@@ -121,7 +120,7 @@ processMessage (Interpreter {..}) state socket = \case
       env <- get_env path imports
       precs <- get_precs path imports
       resolve_vars <- get_resolve path imports
-      parsed <- parseToErr (core precs <* eof) "server-in" line 
+      parsed <- core precs "server-in" line  -- TODO: eof?
       resolved <- resolve_closed (("unbound name" <+>) . pretty) resolve_vars parsed
         `catchError` (throwError . (<+>) "Resolution:")
       (term, ty) <- infer (CheckInterp interp_eval interp_eq spretty) env resolved

diff --git a/src/Sigil/Abstract/Syntax.hs b/src/Sigil/Abstract/Syntax.hs
@@ -88,6 +88,7 @@ type Case b n χ = (Pattern n, Core b n χ)
 data Pattern n
   = PatCtr Text [Pattern n]
   | PatVar n
+  deriving Eq
 
 data Core b n χ
   = Coreχ (Coreχ b n χ)

diff --git a/src/Sigil/Analysis/Typecheck.hs b/src/Sigil/Analysis/Typecheck.hs
@@ -296,7 +296,9 @@ instance Checkable Name ResolvedCore InternalCore where
           anorm <- normalize' env asort a'
           let env' = insert name (Just anorm, asort) env
           ctors' <- forM ctors $ \(label, ty) -> do
-            ty' <- check' env' ty asort -- TODO: is this predicativity??
+            -- TODO: level check
+            -- ty' <- check' env' ty asort -- TODO: is this predicativity??
+            (ty', _) <- infer' env' ty
             pure $ (label, ty')
           pure $ (Ind name a' ctors', a')
         Indχ _ _ Nothing _ -> throwError' "inductive definition should provide sort"
@@ -399,7 +401,9 @@ instance Checkable Name ResolvedCore InternalCore where
           anorm <- normalize' env asort a'
           let env' = insert n (Just anorm, asort) env
           ctors' <- forM ctors $ \(label, ty) -> do
-            ty' <- check' env' ty asort -- TODO: is this predicativity??
+            -- TODO: level check??
+            --ty' <- check' env' ty asort -- TODO: is this predicativity??
+            (ty', _) <- infer' env' ty
             pure $ (label, ty')
           pure $ Ind n a' ctors'
         (Indχ _ _ Nothing _, _) -> do

diff --git a/src/Sigil/Concrete/Parsed.hs b/src/Sigil/Concrete/Parsed.hs
@@ -141,3 +141,6 @@ instance Pretty ParsedEntry where
 instance Pretty ParsedModule where
   pretty =
     pretty_mod_builder pretty
+
+instance Show ParsedCore where
+  show = show . pretty