restructure Raw to separate import directives

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

src/Lib/Parser.idr

@@ -242,8 +242,8 @@ export
 parseSig : Parser Decl
 parseSig = TypeSig <$> getPos <*> (ident <|> uident) <* keyword ":" <*> typeExpr
 
-parseImport : Parser Decl
+parseImport : Parser Import
-parseImport = DImport <$> getPos <* keyword "import" <*> uident
+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
+  startBlock $ do
-  pure $ MkModule name decls
+    imports <- manySame $ parseImport
+    decls <- manySame $ parseDecl
+    pure $ MkModule name imports decls
 
 public export
 data ReplCmd =

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)

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) =
+  pretty (MkModule name imports decls) =
-    text "module" <+> text name </> stack (map doDecl 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

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 
+  -- TODO separate imports and detect loops / redundant
-  for_ res.decls $ \ decl => case decl of
+  for_ res.imports $ \ (MkImport fc name) => loadModule base name
-    (DImport x str) => loadModule base str
-    _ => pure ()
-
 
+  -- 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)