diff --git a/src/Lib/Parser.idr b/src/Lib/Parser.idr index 619ca1c..1c04c73 100644 --- a/src/Lib/Parser.idr +++ b/src/Lib/Parser.idr @@ -20,7 +20,6 @@ import Data.List ident = token Ident - parens : Parser a -> Parser a parens pa = do sym "(" @@ -33,12 +32,9 @@ lit = do t <- token Number pure $ Lit (LInt (cast t)) - - export term : (Parser Term) - -- ( t : ty ), (t , u) (t) -- Or do we want (x : ty) I think we may need to annotate any term parenThinger : Parser Term @@ -77,7 +73,6 @@ parseApp = do rest <- many atom pure $ foldl App hd rest - parseOp : Lazy (Parser Term) parseOp = parseApp >>= go 0 where @@ -96,7 +91,6 @@ parseOp = parseApp >>= go 0 go prec (App (App (Var op) left) right) <|> pure left - export letExpr : Parser Term letExpr = do @@ -173,9 +167,21 @@ export parseDef : Parser Decl parseDef = Def <$> ident <* keyword "=" <*> term +export +parseData : Parser Decl +parseData = do + keyword "data" + name <- ident + keyword ":" + ty <- term + keyword "where" + decls <- startBlock $ someSame $ parseSig + -- TODO - turn decls into something more useful + pure $ Data name ty decls + export parseDecl : Parser Decl -parseDecl = parseImport <|> parseSig <|> parseDef +parseDecl = parseImport <|> parseSig <|> parseDef <|> parseData export parseMod : Parser Module diff --git a/src/Syntax.idr b/src/Syntax.idr index 604d999..f35bb2a 100644 --- a/src/Syntax.idr +++ b/src/Syntax.idr @@ -55,7 +55,7 @@ data Decl = TypeSig Name TyTerm | Def Name Term | DImport Name - | Data Name Telescope (List ConstrDef) + | Data Name Term (List Decl) public export record Module where