Parse modules

src/Lib/Parser.idr

@@ -65,7 +65,7 @@ data Fixity = InfixL | InfixR | Infix
 operators : List (String, Int, Fixity)
 operators = [
   ("->", 1, InfixR),
-  ("=", 2, InfixL), -- REVIEW
+  ("=", 2, InfixL), -- REVIEW L R ?
   ("+",4,InfixL),
   ("-",4,InfixL),
   ("*",5,InfixL),
@@ -119,7 +119,7 @@ letExpr = do
 pPattern : Parser Pattern
 pPattern
    = PatWild <$ keyword "_"
-  <|> [| PatVar ident |]
+  <|> PatVar <$> ident
 
 export
 lamExpr : Parser Term
@@ -154,32 +154,29 @@ caseExpr = do
 term = defer $ \_ => 
         caseExpr
     <|> letExpr
+    <|> lamExpr
     <|> parseOp
 
-{-
-so lets say we wanted to do the indent, the hard way. 
 
-what does this look like
+-- And top level stuff
 
-We want to say:
+parseSig : Parser Decl
-   kw 'let' $  indentedSome assignment
+parseSig = TypeSig <$> ident <* keyword ":" <*> term
 
-now assignment is going to be whatever, but we need to make sure the initial token can/must be at
+parseDef : Parser Decl
-current indentation level.
+parseDef = Def <$> ident <* keyword "=" <*> term
-
-Ok idris indent is not Col, it's AnyIndent | AtPos Int | AfterPos Int
-
-The col though is somehow sixty.
-
-sixten is sameCol, dropAnchor, with an "environment"
 
 
-sixty is Position is line and col and either line matches or col < tokenCol.
+parseDecl : Parser Decl
+parseDecl = parseSig <|> parseDef
 
-that's maybe doable..
+export
-
+parseMod : Parser Module
-
+parseMod = do
-
+  keyword "module"
-
+  name <- ident
- -}
+  -- probably should be manySame, and we want to start with col -1
+  -- if we enforce blocks indent
+  decls <- startBlock $ someSame $ parseDecl
+  pure $ MkModule name [] decls
 

src/Main.idr

@@ -7,8 +7,8 @@ import Lib.Parser.Impl
 import Lib.Parser
 import Syntax
 
-check : Show a => Parser a -> String -> IO ()
+test : Show a => Parser a -> String -> IO ()
-check pa src = do
+test pa src = do
   _ <- putStrLn "--"
   _ <- putStrLn $ src
   let toks = tokenise src
@@ -25,11 +25,13 @@ main = do
   -- this stuff is working with layout, should I bother with col.
   -- downside is that it will be somewhat picky about the indentation of `in`
   -- The sixty stuff looks promising.  I might want my own tokenizer though.
-  check letExpr "let x = 1\n    y = 2\n in x + y"
+  test letExpr "let x = 1\n    y = 2\n in x + y"
-  check term "let x = 1 in x + 2"
+  test term "let x = 1 in x + 2"
   printLn "BREAK"
-  check term "case x of\n   True => something\n   False => let\n      x = 1\n      y = 2\n    in x + y"
+  test term "case x of\n   True => something\n   False => let\n      x = 1\n      y = 2\n    in x + y"
-  check term "x + y * z + w"
+  test term "x + y * z + w"
-  check term "y * z + w"
+  test term "y * z + w"
-  check term "x -> y -> z"
+  test term "x -> y -> z"
-  check term "x y z"
+  test term "x y z"
+  test parseMod "module Foo\nfoo : Int -> Int\nfoo = \\ x . x"
+  test lamExpr "\\ x . x"

src/Syntax.idr

@@ -60,11 +60,13 @@ Telescope = List Decl -- pi-forall, always typeSig?
 
 data ConstrDef = MkCDef Name Telescope
 
+public export
 data Decl
-  = TypeSig Name RigCount TyTerm
+  = TypeSig Name TyTerm
   | Def Name Term
   | Data Name Telescope (List ConstrDef)
 
+public export
 record Module where
   constructor MkModule
   name : Name
@@ -75,6 +77,18 @@ foo : List String -> String
 foo ts = "(" ++ unwords ts ++ ")"
 
 mutual
+  Show ConstrDef where
+    show x = ?holex
+
+  covering
+  Show Decl where
+    show (TypeSig str x) = foo ["TypeSig", show str, show x]
+    show (Def str x) = foo ["Def", show str, show x]
+    show (Data str xs ys) = foo ["Data", show str, show xs, show ys]
+  
+  export covering
+  Show Module where
+    show (MkModule name imports decls) = foo ["MkModule", show name, show imports, show decls]
 
   Show RigCount where
     show Rig0 = "Rig0"