dunham/newt
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

Forward declaration syntax for data

Browse Source 
Allow:
```newt
data Foo : U
```
as a forward declaration for data. (The `Foo : U` syntax still works for
now.)
This commit is contained in:
Steve Dunham
2026-02-07 07:52:00 -08:00
parent 79ab29f090
commit 0c206a94ab
3 changed files with 13 additions and 11 deletions
Download Patch File Download Diff File Expand all files Collapse all files

5
src/Lib/Parser.newt
View File

@@ -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

10
src/Lib/ProcessDecl.newt
View File

@@ -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

9
src/Lib/Syntax.newt
View File

@@ -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))