parsing!

app/Repl.hs

@@ -23,6 +23,7 @@ data ReplCommand
     | WeakNormalize String
     | Input String
     | LoadFile String
+    | DumpDebug String
     deriving (Show)
 
 parseCommand :: Maybe String -> Maybe ReplCommand
@@ -35,6 +36,7 @@ parseCommand (Just input)
     | ":n " `isPrefixOf` input = Normalize <$> stripPrefix ":n " input
     | ":w " `isPrefixOf` input = WeakNormalize <$> stripPrefix ":w " input
     | ":l " `isPrefixOf` input = LoadFile <$> stripPrefix ":l " input
+    | ":d " `isPrefixOf` input = DumpDebug <$> stripPrefix ":d " input
     | otherwise = Just $ Input input
 
 handleInput :: Env -> String -> InputT IO Env
@@ -46,9 +48,7 @@ handleInput env input =
             Right env' -> pure env'
 
 actOnParse :: String -> (Expr -> InputT IO ()) -> InputT IO ()
-actOnParse input action = case parseExpr "repl" (pack input) of
+actOnParse input action = either outputStrLn (action . elaborate) $ parseExpr "repl" (pack input)
-    Left err -> outputStrLn err
-    Right expr -> action $ elaborate expr
 
 printErrorOrResult :: Env -> (Expr -> ReaderT Env Result Expr) -> Expr -> InputT IO ()
 printErrorOrResult env action expr = putTextLn $ either toText pretty $ runReaderT (action expr) env
@@ -78,5 +78,6 @@ repl = do
             Just (ValueQuery input) -> lookupAct env input (putTextLn . pretty . _val) >> loop env
             Just (Normalize input) -> parseActPrint env input normalize >> loop env
             Just (WeakNormalize input) -> parseActPrint env input whnf >> loop env
+            Just (DumpDebug input) -> either outputStrLn (outputStrLn . show) (parseDef "repl" (pack input)) >> loop env
             Just (LoadFile filename) -> lift (runExceptT $ handleAndParseFile env filename) >>= either ((>> loop env) . outputStrLn) loop
             Just (Input input) -> handleInput env input >>= loop

examples/algebra.pg

@@ -131,6 +131,14 @@ def inv_lg (G : *) (op : binop G) (e : G) (i : unop G) (Hgroup : group G op e i)
 def inv_rg (G : *) (op : binop G) (e : G) (i : unop G) (Hgroup : group G op e i) (a : G) : inv_r G op e a (i a) :=
     and_elim_r (inv_l G op e a (i a)) (inv_r G op e a (i a)) (inv_g G op e i Hgroup a);
 
+section Groups
+    variable G : *;
+    variable op : binop G;
+    hypothesis Hgroup : group G op e i;
+
+    def left_inv_unique 
+end Groups
+
 def left_inv_unique (G : *) (op : binop G) (e : G) (i : unop G) (Hgroup : group G op e i) (a b : G) (h : inv_l G op e a b) : eq G b (i a) :=
     -- b = b * e
     --   = b * (a * a^-1)

lib/IR.hs

@@ -40,5 +40,14 @@ data IRDef
         { axiomName :: Text
         , axiomAscription :: IRExpr
         }
+    | Section
+        { sectionName :: Text
+        , sectionContents :: [IRDef]
+        }
+    | Variable
+        { variableName :: Text
+        , variableType :: IRExpr
+        }
+    deriving (Show, Eq, Ord)
 
 type IRProgram = [IRDef]

lib/Parser.hs

@@ -34,10 +34,7 @@ eat :: Text -> Parser ()
 eat = void . lexeme . chunk
 
 keywords :: [Text]
-keywords = ["forall", "let", "in", "end", "fun", "def", "axiom"]
+keywords = ["forall", "let", "in", "end", "fun", "def", "axiom", "section", "variable", "hypothesis", "variables", "hypotheses"]
-
-reservedChars :: [Char]
-reservedChars = "();:"
 
 pIdentifier :: Parser Text
 pIdentifier = try $ label "identifier" $ lexeme $ do
@@ -158,6 +155,18 @@ pNumSort = lexeme $ pSquare >> Level <$> (L.decimal <|> subscriptInt)
 pSort :: Parser IRExpr
 pSort = lexeme $ pStar <|> try pNumSort <|> pSquare
 
+pTerm :: Parser IRExpr
+pTerm = lexeme $ label "term" $ choice [pSort, pVar, between (char '(') (char ')') pIRExpr]
+
+pAppTerm :: Parser IRExpr
+pAppTerm = lexeme $ choice [pLAbs, pPAbs, pLet, pApp]
+
+pIRExpr :: Parser IRExpr
+pIRExpr = lexeme $ try pArrow <|> pAppTerm
+
+pAscription :: Parser IRExpr
+pAscription = lexeme $ try $ eat ":" >> label "type" pIRExpr
+
 pAxiom :: Parser IRDef
 pAxiom = lexeme $ label "axiom" $ do
     eat "axiom"
@@ -167,6 +176,15 @@ pAxiom = lexeme $ label "axiom" $ do
     eat ";"
     pure $ Axiom ident ascription
 
+pVariable :: Parser IRDef
+pVariable = lexeme $ label "variable declaration" $ do
+    eat "variable" <|> eat "hypothesis"
+    ident <- pIdentifier
+    params <- pManyParams
+    ascription <- fmap (flip (foldr (mkPi Nothing)) params) pAscription
+    eat ";"
+    pure $ Variable ident ascription
+
 pDef :: Parser IRDef
 pDef = lexeme $ label "definition" $ do
     eat "def"
@@ -178,20 +196,17 @@ pDef = lexeme $ label "definition" $ do
     eat ";"
     pure $ Def ident ascription $ foldr (mkAbs Nothing) body params
 
+pSection :: Parser IRDef
+pSection = lexeme $ label "section" $ do
+    eat "section"
+    secLabel <- pIdentifier
+    body <- many pIRDef
+    eat "end"
+    void $ lexeme $ chunk secLabel
+    pure $ Section secLabel body
+
 pIRDef :: Parser IRDef
-pIRDef = pAxiom <|> pDef
+pIRDef = pAxiom <|> pDef <|> pVariable <|> pSection
-
-pTerm :: Parser IRExpr
-pTerm = lexeme $ label "term" $ choice [pSort, pVar, between (char '(') (char ')') pIRExpr]
-
-pAppTerm :: Parser IRExpr
-pAppTerm = lexeme $ choice [pLAbs, pPAbs, pLet, pApp]
-
-pIRExpr :: Parser IRExpr
-pIRExpr = lexeme $ try pArrow <|> pAppTerm
-
-pAscription :: Parser IRExpr
-pAscription = lexeme $ try $ eat ":" >> label "type" pIRExpr
 
 pIRProgram :: Parser IRProgram
 pIRProgram = skipSpace >> some pIRDef

lib/Program.hs

@@ -36,6 +36,8 @@ handleDef (Def name (Just irTy) irBody) = do
   where
     body = elaborate irBody
     ty = elaborate irTy
+handleDef (Variable name ty) = undefined
+handleDef (Section name contents) = undefined
 
 evalDef :: Env -> IRDef -> Result Env
 evalDef = flip (execStateT . handleDef)