From ec3cf04db49f0fb925e2904d49dc867889f49eff Mon Sep 17 00:00:00 2001 From: Steve Dunham Date: Sat, 20 May 2023 16:20:36 -0700 Subject: [PATCH] fix comment parsing --- eg/ex.newt | 2 +- src/Lib/Tokenizer.idr | 2 +- src/Main.idr | 2 +- src/Syntax.idr | 3 ++- 4 files changed, 5 insertions(+), 4 deletions(-) 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