From 5c294850a8cff06e4f5cf1bcf4bb0ae4b2fab79c Mon Sep 17 00:00:00 2001 From: Steve Dunham Date: Mon, 10 Apr 2023 21:24:07 -0700 Subject: [PATCH] Checkpoint some existing changes. --- src/Lib/Parser.idr | 21 +++++--- src/Lib/Parser/Impl.idr | 5 +- src/Lib/Token.idr | 4 ++ src/Lib/Tokenizer.idr | 18 ++----- src/Main.idr | 47 ++++++++++++++-- src/Syntax.idr | 115 ++++++++++++++++++++++------------------ 6 files changed, 130 insertions(+), 80 deletions(-) diff --git a/src/Lib/Parser.idr b/src/Lib/Parser.idr index 2fd45e2..619ca1c 100644 --- a/src/Lib/Parser.idr +++ b/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 diff --git a/src/Lib/Parser/Impl.idr b/src/Lib/Parser/Impl.idr index 07ad1f8..5b9b29a 100644 --- a/src/Lib/Parser/Impl.idr +++ b/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 diff --git a/src/Lib/Token.idr b/src/Lib/Token.idr index 94a36d4..092421b 100644 --- a/src/Lib/Token.idr +++ b/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 diff --git a/src/Lib/Tokenizer.idr b/src/Lib/Tokenizer.idr index 90ed60c..68ecf27 100644 --- a/src/Lib/Tokenizer.idr +++ b/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 --- tmap : TokenMap (Token Kind) --- 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) --- ] +identMore : Lexer +identMore = alphaNum <|> exact "." 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 - - diff --git a/src/Main.idr b/src/Main.idr index 44645be..12d201e 100644 --- a/src/Main.idr +++ b/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 () -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. +testFile : String -> IO () +testFile fn = do + putStrLn ("***" ++ fn) + Right text <- readFile $ "eg/" ++ fn + | 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) + diff --git a/src/Syntax.idr b/src/Syntax.idr index 9ba4f19..750ed43 100644 --- a/src/Syntax.idr +++ b/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 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 Literal where + show (LString str) = foo [ "LString", show str] + show (LInt i) = foo [ "LInt", show i] + show (LBool x) = foo [ "LBool", show x] + + +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 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" - - 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"] - + 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", 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 (ParseError str) = foo [ "ParseError", "str"] + show _ = "woo"