Checkpoint some existing changes.

src/Lib/Parser.idr

@@ -107,7 +107,6 @@ letExpr = do
   scope <- term
   pure $ Let alts scope
   -- Let <$ keyword "let" <*> ident <* keyword "=" <*> term <* keyword "in" <*> term
-
   where
     letAssign : Parser (Name,Term)
     letAssign = do
@@ -127,7 +126,7 @@ lamExpr = do
   keyword "\\"
   commit
   name <- pPattern
-  keyword "."
+  keyword "=>"
   scope <- term
   pure $ Lam name scope
 
@@ -150,25 +149,33 @@ caseExpr = do
   alts <- startBlock $ someSame $ caseAlt
   pure $ Case sc alts
 
-
 term = defer $ \_ => 
         caseExpr
     <|> letExpr
     <|> lamExpr
     <|> parseOp
 
-
 -- And top level stuff
 
+optional : Parser a -> Parser (Maybe a)
+optional pa = Just <$> pa <|> pure Nothing
+
+export
 parseSig : Parser Decl
 parseSig = TypeSig <$> ident <* keyword ":" <*> term
 
+parseImport : Parser Decl
+parseImport = DImport <$ keyword "import" <*> ident
+
+-- Do we do pattern stuff now? or just name = lambda?
+
+export
 parseDef : Parser Decl
 parseDef = Def <$> ident <* keyword "=" <*> term
 
-
+export
 parseDecl : Parser Decl
-parseDecl = parseSig <|> parseDef
+parseDecl = parseImport <|> parseSig <|> parseDef
 
 export
 parseMod : Parser Module
@@ -176,7 +183,7 @@ parseMod = do
   keyword "module"
   name <- ident
   -- probably should be manySame, and we want to start with col -1
-  -- if we enforce blocks indent
+  -- if we enforce blocks indent more than parent
   decls <- startBlock $ someSame $ parseDecl
   pure $ MkModule name [] decls
 

src/Lib/Parser/Impl.idr

@@ -44,6 +44,7 @@ parse pa toks = case runP pa toks False (0,0) of
   OK a [] _ => Right a
   OK a ts _ => Left "Extra toks \{show ts}"
 
+-- I think I want to drop the typeclasses for v1
 
 export
 fail : String -> Parser a
@@ -147,11 +148,9 @@ indented (P p) = P $ \toks,com,(l,c) => case toks of
     in if tc > c || tl == l then p toks com (l,c)
     else Fail (E "unexpected outdent") toks com
 
-
-
 export
 token' : Kind -> Parser String
-token' k = pred (\t => t.val.kind == k) "Expected a \{show k}"
+token' k = pred (\t => t.val.kind == k) "Expected a \{show k} token"
 
 
 export

src/Lib/Token.idr

@@ -10,10 +10,12 @@ data Kind
   | Number 
   | Symbol
   | Space
+  | Comment
   -- not doing Layout.idr
   | LBrace
   | Semi
   | RBrace
+  | EOI
 
 export
 Show Kind where
@@ -26,6 +28,8 @@ Show Kind where
   show LBrace  = "LBrace"
   show Semi    = "Semi"
   show RBrace  = "RBrace"
+  show Comment = "Comment"
+  show EOI     = "EOI"
 
 export
 Eq Kind where

src/Lib/Tokenizer.idr

@@ -8,7 +8,7 @@ keywords : List String
 keywords = ["let", "in", "where", "case", "of", "data"]
 
 specialOps : List String
-specialOps = ["->", ":"]
+specialOps = ["->", ":", "=>"]
 
 checkKW : String -> Token Kind
 checkKW s = if elem s keywords then Tok Keyword s else Tok Ident s
@@ -19,20 +19,12 @@ isOpChar c = c `elem` (unpack ":!#$%&*+./<=>?@\\^|-~")
 opChar : Lexer
 opChar = pred isOpChar
 
--- so Text.Lexer.Core.lex is broken
+identMore : Lexer
--- tmap : TokenMap (Token Kind)
+identMore = alphaNum <|> exact "."
--- tmap = [
---   (alpha <+> many alphaNum, checkKW),
---   (some digit, Tok Number),
---   (some opChar, \s => Tok Oper s),
---   (lineComment (exact "--"), Tok Space),
---   (symbol, Tok Symbol),
---   (spaces, Tok Space)
--- ]
 
 rawTokens : Tokenizer (Token Kind)
 rawTokens
-   =  match (alpha <+> many alphaNum) checkKW
+   =  match (alpha <+> many identMore) checkKW
   <|> match (some digit) (Tok Number)
   <|> match (some opChar) (\s => Tok Oper s)
   <|> match (lineComment (exact "--")) (Tok Space)
@@ -46,5 +38,3 @@ notSpace _ = True
 export
 tokenise : String -> List BTok
 tokenise = filter notSpace . fst . lex rawTokens 
-
-

src/Main.idr

@@ -1,18 +1,35 @@
 module Main
 
+import Data.String
 import Lib.Tokenizer
 import Lib.Layout
 import Lib.Token
 import Lib.Parser.Impl
 import Lib.Parser
 import Syntax
+import System
+import System.File
+import System.Directory
+import Control.App
+
+-- Put stuff in attic
+-- Error printing
+-- Review surface syntax
+-- Prettier printer
+-- First pass at typecheck
+-- Just do it in zoo order
+
+
+-- showPError : String -> 
 
 test : Show a => Parser a -> String -> IO ()
 test pa src = do
   _ <- putStrLn "--"
   _ <- putStrLn $ src
   let toks = tokenise src
+  putStrLn "- Toks"
   printLn $ toks
+  putStrLn "- Parse"
   let res = parse pa toks
   printLn res
   -- let toks2 = layout toks
@@ -20,11 +37,15 @@ test pa src = do
 
 -- gotta fix up error messages. Show it with some source
 
-main : IO ()
+testFile : String -> IO ()
-main = do
+testFile fn = do
-  -- this stuff is working with layout, should I bother with col.
+  putStrLn ("***" ++ fn)
-  -- downside is that it will be somewhat picky about the indentation of `in`
+  Right text <- readFile $ "eg/" ++ fn
-  -- The sixty stuff looks promising.  I might want my own tokenizer though.
+    | Left err => printLn err
+  test parseMod text
+
+olderTests : IO ()
+olderTests = do
   test letExpr "let x = 1\n    y = 2\n in x + y"
   test term "let x = 1 in x + 2"
   printLn "BREAK"
@@ -35,3 +56,19 @@ main = do
   test term "x y z"
   test parseMod "module Foo\nfoo : Int -> Int\nfoo = \\ x . x"
   test lamExpr "\\ x . x"
+  test parseMod "module Foo\nimport Foo.Bar\nfoo = 1\n"
+  test parseDef "foo = 1"
+  test parseSig "foo : Bar -> Int"
+  test parseMod "module Test\nid : a -> a\nid = \\ x => x\n"
+
+foo : Maybe Int -> Int
+foo Nothing = ?foo_rhs_0
+foo (Just x) = ?foo_rhs_1
+
+
+main : IO ()
+main = do
+  Right files <- listDir "eg"
+    | Left err => printLn err
+  traverse_ testFile (filter (".newt" `isSuffixOf`) files)
+  

src/Syntax.idr

@@ -3,7 +3,6 @@ module Syntax
 import Data.String
 import Derive
 
-
 -- Good enough start, lets parse
 -- This is informed by pi-forall and others and is somewhat low level
 -- %language ElabReflection
@@ -64,6 +63,7 @@ public export
 data Decl
   = TypeSig Name TyTerm
   | Def Name Term
+  | DImport Name
   | Data Name Telescope (List ConstrDef)
 
 public export
@@ -76,55 +76,68 @@ record Module where
 foo : List String -> String
 foo ts = "(" ++ unwords ts ++ ")"
 
-mutual
-  Show ConstrDef where
-    show x = ?holex
 
-  covering
+Show Literal where
-  Show Decl where
+  show (LString str) = foo [ "LString", show str]
-    show (TypeSig str x) = foo ["TypeSig", show str, show x]
+  show (LInt i) = foo [ "LInt", show i]
-    show (Def str x) = foo ["Def", show str, show x]
+  show (LBool x) = foo [ "LBool", show x]
-    show (Data str xs ys) = foo ["Data", show str, show xs, show ys]
+
+
+export
+covering
+implementation Show Term
+
+export
+implementation Show Decl
+
+covering
+Show ConstrDef where
+  show (MkCDef str xs) = foo ["MkCDef", show str, show xs]
+
+
+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]
+  show (DImport str) = foo ["DImport", show str]
+
+
+export covering
+Show Module where
+  show (MkModule name imports decls) = foo ["MkModule", show name, show imports, show decls]
+
+Show RigCount where
+  show Rig0 = "Rig0"
+  show RigW = "RigW"
+
+Show Pattern where
+  show (PatVar str) = foo ["PatVar", show str]
+  show (PatCon str xs) = foo ["PatCon", show str, assert_total $ show xs]
+  show PatWild = "PatWild"
+  show (PatLit x) = foo ["PatLit" , show x]
+
+Show CaseAlt where
+  show (MkAlt x y)= foo ["MkAlt", show x, assert_total $ show y]
+
+Show Plicity where
+  show Implicit = "Implicit"
+  show Explicit = "Explicit"
+  show Eq = "Eq"
+
+covering
+Show Term where
+  show (Ann t ty) = "Ann" ++ " " ++ show t ++ " " ++ show ty
+  show Wildcard = "Wildcard"
   
-  export covering
+  show (Var name) = foo ["Var", show name]
-  Show Module where
+  show (Ann t ty) = foo [ "Ann", show t, show ty]
-    show (MkModule name imports decls) = foo ["MkModule", show name, show imports, show decls]
+  show (Lit x) = foo [ "Lit", show x]
-
+  show (Let alts y) = foo [ "Let", show alts, show y]
-  Show RigCount where
+  show (Pi str x y z) = foo [ "Pi", show str, show x, show y, show z]
-    show Rig0 = "Rig0"
+  show (App x y) = foo [ "App", show x, show y]
-    show RigW = "RigW"
+  show (Lam x y) = foo [ "Lam", show x, show y]
-
+  show (Case x xs) = foo [ "Case", show x, show xs]
-  Show Pattern where
+  
-    show (PatVar str) = foo ["PatVar", show str]
+  show (ParseError str) = foo [ "ParseError", "str"]
-    show (PatCon str xs) = foo ["PatCon", show str, assert_total $ show xs]
+  show _ = "woo"
-    show PatWild = "PatWild"
-    show (PatLit x) = foo ["PatLit" , show x]
-
-
-  Show CaseAlt where
-    show (MkAlt x y)= foo ["MkAlt", show x, assert_total $ show y]
-
-  Show Plicity where
-    show Implicit = "Implicit"
-    show Explicit = "Explicit"
-    show Eq = "Eq"
-
-  Show Literal where
-    show (LString str) = foo [ "LString", show str]
-    show (LInt i) = foo [ "LInt", show i]
-    show (LBool x) = foo [ "LBool", show x]
-
-
-  export
-  Show Term where
-    show (Var name) = foo ["Var", show name]
-    show (Ann t ty) = foo [ "Ann", show t, show ty]
-    show (Lit x) = foo [ "Lit", show x]
-    show (Let alts y) = foo [ "Let", assert_total $ show alts, show y]
-    show (Pi str x y z) = foo [ "Pi", show str, show x, show y, show z]
-    show (App x y) = foo [ "App", show x, show y]
-    show (Lam x y) = foo [ "Lam", show x, show y]
-    show (Case x xs) = foo [ "Case", show x, show xs]
-    show Wildcard = "Wildcard"
-    show (ParseError str) = foo [ "ParseError", "str"]
-