diff --git a/src/Lib/Parser.newt b/src/Lib/Parser.newt index 9883ff7..ab8d8c6 100644 --- a/src/Lib/Parser.newt +++ b/src/Lib/Parser.newt @@ -615,9 +615,10 @@ parseData = do -- commit when we hit ":" name <- try $ (keyword "data" *> (uident <|> ident <|> token MixFix) <* keyword ":") ty <- typeExpr - keyword "where" + Just _ <- optional (keyword "where") + | _ => pure $ Data fc name ty Nothing decls <- startBlock $ manySame $ parseSig - pure $ Data fc name ty decls + pure $ Data fc name ty (Just decls) nakedBind : Parser Telescope nakedBind = do diff --git a/src/Lib/ProcessDecl.newt b/src/Lib/ProcessDecl.newt index fc86566..ea0a4a1 100644 --- a/src/Lib/ProcessDecl.newt +++ b/src/Lib/ProcessDecl.newt @@ -229,7 +229,7 @@ processClass ns classFC nm tele decls = do log 1 $ \ _ => "tcon type \{render 90 $ pretty tcType}" log 1 $ \ _ => "dcon type \{render 90 $ pretty dcType}" - let decl = Data classFC nm tcType (TypeSig classFC (dcName :: Nil) dcType :: Nil) + let decl = Data classFC nm tcType (Just $ TypeSig classFC (dcName :: Nil) dcType :: Nil) log 1 $ \ _ => "Decl:" log 1 $ \ _ => render 90 $ pretty decl processDecl ns decl @@ -381,7 +381,7 @@ processShortData ns fc lhs sigs = do (nm,args) <- getArgs lhs Nil let ty = foldr mkPi (RU fc) args cons <- traverse (mkDecl args Nil) sigs - let dataDecl = Data fc nm ty cons + let dataDecl = Data fc nm ty (Just cons) log 1 $ \ _ => "SHORTDATA" log 1 $ \ _ => "\{render 90 $ pretty dataDecl}" processDecl ns dataDecl @@ -504,7 +504,7 @@ processRecord ns recordFC nm tele cname decls = do log 1 $ \ _ => "tcon type \{render 90 $ pretty tcType}" log 1 $ \ _ => "dcon type \{render 90 $ pretty dcType}" - let decl = Data recordFC nm tcType (TypeSig recordFC (dcName :: Nil) dcType :: Nil) + let decl = Data recordFC nm tcType (Just $ TypeSig recordFC (dcName :: Nil) dcType :: Nil) log 1 $ \ _ => "Decl:" log 1 $ \ _ => render 90 $ pretty decl processDecl ns decl @@ -544,5 +544,7 @@ processDecl ns (DCheck fc tm ty) = processCheck ns fc tm ty processDecl ns (Class classFC nm tele decls) = processClass ns classFC nm tele decls processDecl ns (Instance instfc ty decls) = processInstance ns instfc ty decls processDecl ns (ShortData fc lhs sigs) = processShortData ns fc lhs sigs -processDecl ns (Data fc nm ty cons) = processData ns fc nm ty cons +processDecl ns (Data fc nm ty (Just cons)) = processData ns fc nm ty cons +-- TODO distinguish from function signatures +processDecl ns (Data fc nm ty Nothing) = processTypeSig ns fc (nm :: Nil) ty processDecl ns (Record recordFC nm tele cname decls) = processRecord ns recordFC nm tele cname decls diff --git a/src/Lib/Syntax.newt b/src/Lib/Syntax.newt index eeaf275..47388c9 100644 --- a/src/Lib/Syntax.newt +++ b/src/Lib/Syntax.newt @@ -76,17 +76,15 @@ instance HasFC Raw where data Import = MkImport FC Name - - Telescope : U Telescope = List (BindInfo × Raw) - data Decl = TypeSig FC (List Name) Raw | FunDef FC Name (List (Raw × Maybe Raw)) | DCheck FC Raw Raw - | Data FC Name Raw (List Decl) + -- TODO maybe add Telescope (before `:`) and auto-add to constructors... + | Data FC Name Raw (Maybe $ List Decl) | ShortData FC Raw (List Raw) | PType FC Name (Maybe Raw) | PFunc FC Name (List String) Raw String @@ -247,7 +245,8 @@ instance Pretty Decl where prettyPair : Raw × Maybe Raw → Doc prettyPair (a, Nothing) = pretty a prettyPair (a, Just b) = pretty a <+> text "=" <+> pretty b - pretty (Data _ nm x xs) = text "data" <+> text nm <+> text ":" <+> pretty x <+> (nest 2 $ text "where" stack (map pretty xs)) + pretty (Data _ nm x Nothing) = text "data" <+> text nm <+> text ":" <+> pretty x + pretty (Data _ nm x (Just xs)) = text "data" <+> text nm <+> text ":" <+> pretty x <+> (nest 2 $ text "where" stack (map pretty xs)) pretty (DCheck _ x y) = text "#check" <+> pretty x <+> text ":" <+> pretty y pretty (PType _ nm ty) = text "ptype" <+> text nm <+> (maybe empty (\ty => text ":" <+> pretty ty) ty) pretty (PFunc _ nm Nil ty src) = text "pfunc" <+> text nm <+> text ":" <+> nest 2 (pretty ty <+> text ":=" <+/> text (show src))