From 6850725d3b9be1e2b7cb88c849653bb193bff3a0 Mon Sep 17 00:00:00 2001 From: Steve Dunham Date: Sat, 20 May 2023 17:10:58 -0700 Subject: [PATCH] checkpoint --- eg/ex.newt | 16 ++++++++++++++-- src/Lib/Parser.idr | 2 +- 2 files changed, 15 insertions(+), 3 deletions(-) diff --git a/eg/ex.newt b/eg/ex.newt index 0263270..d3ed540 100644 --- a/eg/ex.newt +++ b/eg/ex.newt @@ -1,9 +1,21 @@ +-- comment with double hyphen, takes precedence over operators module Ex --- comment +-- imports not implemented yet +import Foo +-- inductive data type declaration (not supported in language yet) data Bool : Type where True : Bool False : Bool +-- claim id : a -> a -id = \ a => a +-- declaration +id = \ a => a * a + 2 * (3 + x) +-- this is complicated with patterns because we need to group stuff together. +-- I really should make a simple grammar + +-- I want to put this on ice, there is so much to do before patterns.. + +blah : Either a a -> a +blah = \ x => let x = 1 in x * x diff --git a/src/Lib/Parser.idr b/src/Lib/Parser.idr index 91c77c3..89627e6 100644 --- a/src/Lib/Parser.idr +++ b/src/Lib/Parser.idr @@ -189,7 +189,7 @@ parseDecl = parseImport <|> parseSig <|> parseDef <|> parseData export parseMod : Parser Module parseMod = do - keyword "module" + sameLevel $ keyword "module" name <- ident -- probably should be manySame, and we want to start with col -1 -- if we enforce blocks indent more than parent