preliminary parser for data

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

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