From fa7d803ebb9eae376d151ddce82d4e3e6377a791 Mon Sep 17 00:00:00 2001 From: Steve Dunham Date: Sun, 29 Sep 2024 09:33:09 -0700 Subject: [PATCH] restructure Raw to separate import directives --- TODO.md | 4 +++- src/Lib/Parser.idr | 12 +++++++----- src/Lib/ProcessDecl.idr | 2 -- src/Lib/Syntax.idr | 29 +++++++++++++++++------------ src/Main.idr | 8 +++----- 5 files changed, 30 insertions(+), 25 deletions(-) diff --git a/TODO.md b/TODO.md index cb22321..153a01b 100644 --- a/TODO.md +++ b/TODO.md @@ -4,7 +4,7 @@ I may be done with `U` - I keep typing `Type`. - [ ] Generate some programs that do stuff -- [ ] import +- [x] import - [ ] consider making meta application implicit in term, so its more readable when printed - Currently we have explicit `App` surrounding `Meta` when inserting metas. Some people leave that implicit for efficiency. I think it would also make printing more readable. @@ -49,3 +49,5 @@ I may be done with `U` - I keep typing `Type`. - [ ] records / copatterns - [ ] Read Ulf Norell thesis + + diff --git a/src/Lib/Parser.idr b/src/Lib/Parser.idr index 29372dc..8366ef0 100644 --- a/src/Lib/Parser.idr +++ b/src/Lib/Parser.idr @@ -242,8 +242,8 @@ export parseSig : Parser Decl parseSig = TypeSig <$> getPos <*> (ident <|> uident) <* keyword ":" <*> typeExpr -parseImport : Parser Decl -parseImport = DImport <$> getPos <* keyword "import" <*> uident +parseImport : Parser Import +parseImport = MkImport <$> getPos <* keyword "import" <*> uident -- Do we do pattern stuff now? or just name = lambda? @@ -335,15 +335,17 @@ parseNorm = DCheck <$> getPos <* keyword "#check" <*> typeExpr <* keyword ":" <* export parseDecl : Parser Decl -parseDecl = parseMixfix <|> parsePType <|> parsePFunc <|> parseImport <|> parseNorm <|> parseData <|> (try $ parseSig) <|> parseDef +parseDecl = parseMixfix <|> parsePType <|> parsePFunc <|> parseNorm <|> parseData <|> (try $ parseSig) <|> parseDef export parseMod : Parser Module parseMod = do keyword "module" name <- uident - decls <- startBlock $ manySame $ parseDecl - pure $ MkModule name decls + startBlock $ do + imports <- manySame $ parseImport + decls <- manySame $ parseDecl + pure $ MkModule name imports decls public export data ReplCmd = diff --git a/src/Lib/ProcessDecl.idr b/src/Lib/ProcessDecl.idr index 13ac4f3..7630b59 100644 --- a/src/Lib/ProcessDecl.idr +++ b/src/Lib/ProcessDecl.idr @@ -107,8 +107,6 @@ processDecl (DCheck fc tm ty) = do putStrLn "norm \{pprint [] norm}" putStrLn "NF " -processDecl (DImport fc str) = pure () - processDecl (Data fc nm ty cons) = do ctx <- get tyty <- check (mkCtx ctx.metas fc) ty (VU fc) diff --git a/src/Lib/Syntax.idr b/src/Lib/Syntax.idr index b7a5fc0..fd95280 100644 --- a/src/Lib/Syntax.idr +++ b/src/Lib/Syntax.idr @@ -12,8 +12,6 @@ data Raw : Type where public export data RigCount = Rig0 | RigW - - public export data Pattern = PatVar FC Icit Name @@ -92,14 +90,16 @@ HasFC Raw where getFC (RParseError fc str) = fc -- derive some stuff - I'd like json, eq, show, ... + + +public export +data Import = MkImport FC Name + -- FIXME - I think I don't want "where" here, but the parser has an issue public export -data Decl : Type where - data Decl = TypeSig FC Name Raw | Def FC Name (List (Raw,Raw)) -- (List Clause) - | DImport FC Name | DCheck FC Raw Raw | Data FC Name Raw (List Decl) | PType FC Name (Maybe Raw) @@ -111,17 +111,16 @@ public export record Module where constructor MkModule name : Name + imports : List Import decls : List Decl foo : List String -> String foo ts = "(" ++ unwords ts ++ ")" - Show Literal where show (LString str) = foo [ "LString", show str] show (LInt i) = foo [ "LInt", show i] - export covering implementation Show Raw @@ -135,12 +134,14 @@ export covering Show Clause where show (MkClause fc cons pats expr) = show (fc, cons, pats, expr) +Show Import where + show (MkImport _ str) = foo ["MkImport", show str] + covering Show Decl where show (TypeSig _ str x) = foo ["TypeSig", show str, show x] show (Def _ str clauses) = foo ["Def", show str, show clauses] show (Data _ str xs ys) = foo ["Data", show str, show xs, show ys] - show (DImport _ str) = foo ["DImport", show str] show (DCheck _ x y) = foo ["DCheck", show x, show y] show (PType _ name ty) = foo ["PType", name, show ty] show (PFunc _ nm ty src) = foo ["PFunc", nm, show ty, show src] @@ -148,7 +149,7 @@ Show Decl where export covering Show Module where - show (MkModule name decls) = foo ["MkModule", show name, show decls] + show (MkModule name imports decls) = foo ["MkModule", show name, show imports, show decls] Show RigCount where show Rig0 = "Rig0" @@ -226,13 +227,17 @@ Pretty Raw where export Pretty Module where - pretty (MkModule name decls) = - text "module" <+> text name stack (map doDecl decls) + pretty (MkModule name imports decls) = + text "module" <+> text name + stack (map doImport imports) + stack (map doDecl decls) where + doImport : Import -> Doc + doImport (MkImport _ nm) = text "import" <+> text nm ++ line + doDecl : Decl -> Doc doDecl (TypeSig _ nm ty) = text nm <+> text ":" <+> nest 2 (pretty ty) doDecl (Def _ nm clauses) = stack $ map (\(a,b) => pretty a <+> "=" <+> pretty b) clauses - doDecl (DImport _ nm) = text "import" <+> text nm ++ line -- the behavior of nest is kinda weird, I have to do the nest before/around the . doDecl (Data _ nm x xs) = text "data" <+> text nm <+> text ":" <+> pretty x <+> (nest 2 $ text "where" stack (map doDecl xs)) doDecl (DCheck _ x y) = text "#check" <+> pretty x <+> ":" <+> pretty y diff --git a/src/Main.idr b/src/Main.idr index 22e7312..e3e02b7 100644 --- a/src/Main.idr +++ b/src/Main.idr @@ -74,12 +74,10 @@ loadModule base name = do putStrLn "module \{res.name}" let True = name == res.name | _ => fail "module name \{show res.name} doesn't match file name \{show fn}" - -- TODO separate imports and detect loops / redundant - for_ res.decls $ \ decl => case decl of - (DImport x str) => loadModule base str - _ => pure () - + -- TODO separate imports and detect loops / redundant + for_ res.imports $ \ (MkImport fc name) => loadModule base name + -- TODO Lift the error exit, so import errors can get a FC in current file putStrLn "process Decls" Right _ <- tryError $ traverse_ processDecl (collectDecl res.decls) | Left y => fail (showError src y)