diff --git a/eg/ex.newt b/eg/ex.newt index 0dcbafd..0263270 100644 --- a/eg/ex.newt +++ b/eg/ex.newt @@ -1,5 +1,5 @@ module Ex - +-- comment data Bool : Type where True : Bool False : Bool diff --git a/src/Lib/Tokenizer.idr b/src/Lib/Tokenizer.idr index 68ecf27..6bfd699 100644 --- a/src/Lib/Tokenizer.idr +++ b/src/Lib/Tokenizer.idr @@ -26,8 +26,8 @@ rawTokens : Tokenizer (Token Kind) rawTokens = match (alpha <+> many identMore) checkKW <|> match (some digit) (Tok Number) - <|> match (some opChar) (\s => Tok Oper s) <|> match (lineComment (exact "--")) (Tok Space) + <|> match (some opChar) (\s => Tok Oper s) <|> match symbol (Tok Symbol) <|> match spaces (Tok Space) diff --git a/src/Main.idr b/src/Main.idr index be94e82..379e359 100644 --- a/src/Main.idr +++ b/src/Main.idr @@ -71,4 +71,4 @@ main = do Right files <- listDir "eg" | Left err => printLn err traverse_ testFile (filter (".newt" `isSuffixOf`) files) - + diff --git a/src/Syntax.idr b/src/Syntax.idr index 34436a5..82c9812 100644 --- a/src/Syntax.idr +++ b/src/Syntax.idr @@ -12,6 +12,7 @@ public export data Literal = LString String | LInt Int | LBool Bool public export data RigCount = Rig0 | RigW +-- I think I got Eq from pi-forall, it uses it for equality args (which are kinda like Prop/Rig0?) public export data Plicity = Implicit | Explicit | Eq @@ -30,7 +31,7 @@ data CaseAlt = MkAlt Pattern Raw public export data Raw - = RVar Name + = RVar Name | RLam Pattern Raw | RApp Raw Raw | RU