asdf

lib/Elaborator.hs

@@ -1,50 +1,97 @@
 module Elaborator where
 
+import Control.Monad.Except
 import Data.List (elemIndex)
+import Data.List.NonEmpty ((<|))
+import Errors (Error (..), Result)
 import Expr (Expr)
 import qualified Expr as E
-import IR (IRExpr)
+import IR (IRDef (..), IRExpr)
 import qualified IR as I
+import Relude.Extra.Lens
 
 type Binders = [Text]
 
-saveBinders :: State Binders a -> State Binders a
+data SectionContext = SectionContext
-saveBinders action = do
+    { sectionDefs :: [(Text, [Text])] -- name and list of variables it depends on
-    binders <- get
+    , sectionVars :: [(Text, IRExpr)] -- variables and their types
-    res <- action
+    }
-    put binders
-    pure res
 
-elaborate :: IRExpr -> Expr
+type ElabMonad = StateT (NonEmpty SectionContext) Result
-elaborate ir = evalState (elaborate' ir) []
+
+sectionDefsL :: Lens' SectionContext [(Text, [Text])]
+sectionDefsL = lens sectionDefs setter
   where
-    helper :: (Monad m) => Maybe a -> (a -> m b) -> m (Maybe b)
+    setter ctxt newDefs = ctxt{sectionDefs = newDefs}
-    helper Nothing _ = pure Nothing
-    helper (Just x) f = Just <$> f x
 
-    elaborate' :: IRExpr -> State Binders Expr
+sectionVarsL :: Lens' SectionContext [(Text, IRExpr)]
-    elaborate' (I.Var n) = do
+sectionVarsL = lens sectionVars setter
-        binders <- get
+  where
-        pure $ E.Var n . fromIntegral <$> elemIndex n binders ?: E.Free n
+    setter ctxt newVars = ctxt{sectionVars = newVars}
-    elaborate' I.Star = pure E.Star
+
-    elaborate' (I.Level level) = pure $ E.Level level
+saveState :: ElabMonad a -> ElabMonad a
-    elaborate' (I.App m n) = E.App <$> elaborate' m <*> elaborate' n
+saveState action = get >>= (action <*) . put
-    elaborate' (I.Abs x t a b) = saveBinders $ do
+
-        t' <- elaborate' t
+elabSection :: Text -> [IRDef] -> ElabMonad [IRDef]
-        a' <- helper a elaborate'
+elabSection _name contents = saveState $ do
-        modify (x :)
+    modify (SectionContext [] [] <|)
-        E.Abs x t' a' <$> elaborate' b
+    concat <$> forM contents elabDef
-    elaborate' (I.Pi x t a b) = saveBinders $ do
+
-        t' <- elaborate' t
+pushVariable :: Text -> IRExpr -> NonEmpty SectionContext -> NonEmpty SectionContext
-        a' <- helper a elaborate'
+pushVariable name ty (SectionContext defs vars :| rest) = SectionContext defs ((name, ty) : vars) :| rest
-        modify (x :)
+
-        E.Pi x t' a' <$> elaborate' b
+elabDef :: IRDef -> ElabMonad [IRDef]
-    elaborate' (I.Let name Nothing val body) = saveBinders $ do
+elabDef (Def name ty body) = undefined
-        val' <- elaborate' val
+elabDef (Axiom name ty) = undefined
-        modify (name :)
+elabDef (Section name contents) = elabSection name contents
-        E.Let name Nothing val' <$> elaborate' body
+elabDef (Variable name ty) = [] <$ modify' (pushVariable name ty)
-    elaborate' (I.Let name (Just ty) val body) = saveBinders $ do
+
-        val' <- elaborate' val
+traverseDef :: [Text] -> IRExpr -> ElabMonad [Text]
-        ty' <- elaborate' ty
+traverseDef seen (I.Var _) = pure seen
-        modify (name :)
+traverseDef seen I.Star = pure seen
-        E.Let name (Just ty') val' <$> elaborate' body
+traverseDef seen (I.Level _) = pure seen
+traverseDef seen (I.App m n) = (++) <$> traverseDef seen m <*> traverseDef seen n
+
+-- game plan:
+-- 1. add arguments to section local definitions
+
+-- saveBinders :: State Binders a -> State Binders a
+-- saveBinders action = do
+--     binders <- get
+--     res <- action
+--     put binders
+--     pure res
+--
+-- elaborate :: IRExpr -> Expr
+-- elaborate ir = evalState (elaborate' ir) []
+--   where
+--     helper :: (Monad m) => Maybe a -> (a -> m b) -> m (Maybe b)
+--     helper Nothing _ = pure Nothing
+--     helper (Just x) f = Just <$> f x
+--
+--     elaborate' :: IRExpr -> State Binders Expr
+--     elaborate' (I.Var n) = do
+--         binders <- get
+--         pure $ E.Var n . fromIntegral <$> elemIndex n binders ?: E.Free n
+--     elaborate' I.Star = pure E.Star
+--     elaborate' (I.Level level) = pure $ E.Level level
+--     elaborate' (I.App m n) = E.App <$> elaborate' m <*> elaborate' n
+--     elaborate' (I.Abs x t a b) = saveBinders $ do
+--         t' <- elaborate' t
+--         a' <- helper a elaborate'
+--         modify (x :)
+--         E.Abs x t' a' <$> elaborate' b
+--     elaborate' (I.Pi x t a b) = saveBinders $ do
+--         t' <- elaborate' t
+--         a' <- helper a elaborate'
+--         modify (x :)
+--         E.Pi x t' a' <$> elaborate' b
+--     elaborate' (I.Let name Nothing val body) = saveBinders $ do
+--         val' <- elaborate' val
+--         modify (name :)
+--         E.Let name Nothing val' <$> elaborate' body
+--     elaborate' (I.Let name (Just ty) val body) = saveBinders $ do
+--         val' <- elaborate' val
+--         ty' <- elaborate' ty
+--         modify (name :)
+--         E.Let name (Just ty') val' <$> elaborate' body

lib/Errors.hs

@@ -9,6 +9,7 @@ data Error
     | NotEquivalent Expr Expr Expr
     | PNMissingType Text
     | DuplicateDefinition Text
+    | EmptySection Text
     deriving (Eq, Ord)
 
 instance ToText Error where
@@ -18,6 +19,7 @@ instance ToText Error where
     toText (NotEquivalent a a' e) = "Cannot unify '" <> pretty a <> "' with '" <> pretty a' <> "' when evaluating '" <> pretty e <> "'"
     toText (PNMissingType x) = "Axiom '" <> x <> "' missing type ascription"
     toText (DuplicateDefinition n) = "'" <> n <> "' already defined"
+    toText (EmptySection var) = "Tried to declare variable " <> var <> " without a section"
 
 instance ToString Error where
     toString = toString . toText