diff --git a/src/Lib/Parser.idr b/src/Lib/Parser.idr index 501b095..2fd45e2 100644 --- a/src/Lib/Parser.idr +++ b/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: - kw 'let' $ indentedSome assignment +parseSig : Parser Decl +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 -current indentation level. - -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" +parseDef : Parser Decl +parseDef = Def <$> ident <* keyword "=" <*> term -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 diff --git a/src/Main.idr b/src/Main.idr index 6286c46..44645be 100644 --- a/src/Main.idr +++ b/src/Main.idr @@ -7,8 +7,8 @@ import Lib.Parser.Impl import Lib.Parser import Syntax -check : Show a => Parser a -> String -> IO () -check pa src = do +test : Show a => Parser a -> String -> IO () +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" - check term "let x = 1 in x + 2" + test letExpr "let x = 1\n y = 2\n in x + y" + 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" - check term "x + y * z + w" - check term "y * z + w" - check term "x -> y -> z" - check term "x y z" + test term "case x of\n True => something\n False => let\n x = 1\n y = 2\n in x + y" + test term "x + y * z + w" + test term "y * z + w" + test term "x -> y -> z" + test term "x y z" + test parseMod "module Foo\nfoo : Int -> Int\nfoo = \\ x . x" + test lamExpr "\\ x . x" diff --git a/src/Syntax.idr b/src/Syntax.idr index c4c8019..9ba4f19 100644 --- a/src/Syntax.idr +++ b/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"