From 9db5649446463fc944f9cc64ec12b27c996c08f2 Mon Sep 17 00:00:00 2001 From: Steve Dunham Date: Thu, 22 Aug 2024 19:41:24 -0700 Subject: [PATCH] primitive string and int, primitive functions, codegen fixes --- Makefile | 4 +++ newt-vscode/src/extension.ts | 2 +- newt-vscode/syntaxes/newt.tmLanguage.json | 2 +- src/Lib/Check.idr | 16 +++++++---- src/Lib/Compile.idr | 13 ++++++++- src/Lib/CompileExp.idr | 16 +++++++++-- src/Lib/Parser.idr | 35 ++++++++++++++++++++--- src/Lib/Parser/Impl.idr | 2 +- src/Lib/ProcessDecl.idr | 10 +++++++ src/Lib/Syntax.idr | 11 ++++--- src/Lib/TT.idr | 2 ++ src/Lib/Token.idr | 17 +++++++---- src/Lib/Tokenizer.idr | 23 +++++++++++++-- src/Lib/Types.idr | 18 +++++++++++- 14 files changed, 142 insertions(+), 29 deletions(-) diff --git a/Makefile b/Makefile index 2a96ce6..b5d1620 100644 --- a/Makefile +++ b/Makefile @@ -10,3 +10,7 @@ build/exec/newt.js: ${SRCS} test: build/exec/newt build/exec/newt newt/*.newt + +vscode: + cd newt-vscode && vsce package && code --install-extension *.vsix + diff --git a/newt-vscode/src/extension.ts b/newt-vscode/src/extension.ts index 73d7a46..5c2b10c 100644 --- a/newt-vscode/src/extension.ts +++ b/newt-vscode/src/extension.ts @@ -47,7 +47,7 @@ export function activate(context: vscode.ExtensionContext) { ) { message += "\n" + lines[++i]; } - const severity = kind === 'ERROR' ? vscode.DiagnosticSeverity.Error : vscode.DiagnosticSeverity.Information + const severity = kind === 'ERROR' ? vscode.DiagnosticSeverity.Error : vscode.DiagnosticSeverity.Information; const diag = new vscode.Diagnostic(range, message, severity); diagnostics.push(diag); } diff --git a/newt-vscode/syntaxes/newt.tmLanguage.json b/newt-vscode/syntaxes/newt.tmLanguage.json index 750cc08..3eca2b0 100644 --- a/newt-vscode/syntaxes/newt.tmLanguage.json +++ b/newt-vscode/syntaxes/newt.tmLanguage.json @@ -16,7 +16,7 @@ }, { "name": "keyword.newt", - "match": "\\b(data|where|case|of|let|in|U|module)\\b" + "match": "\\b(data|where|case|of|let|in|U|module|ptype|pfunc)\\b" } ] } diff --git a/src/Lib/Check.idr b/src/Lib/Check.idr index 6bf3af9..bcfe9fd 100644 --- a/src/Lib/Check.idr +++ b/src/Lib/Check.idr @@ -80,6 +80,7 @@ parameters (ctx: Context) -- Here we have raw Tm so we haven't even done occurs check. I'm thinking -- we don't allow solutions with Case in them -- pure (Case fc !(go ren lvl sc) alts) + go ren lvl (VLit fc lit) = pure (Lit fc lit) lams : Nat -> Tm -> Tm lams 0 tm = tm @@ -168,6 +169,12 @@ lookupName ctx (RVar fc nm) = go 0 ctx.types lookupName ctx _ = pure Nothing +primType : FC -> String -> M Val +primType fc nm = case lookup nm !(get) of + Just (MkEntry name ty PrimTCon) => pure $ VRef fc name PrimTCon [<] + _ => error fc "Primitive type \{show nm} not in scope" + + export infer : Context -> Raw -> M (Tm, Val) @@ -391,13 +398,10 @@ infer ctx (RImplicit fc) = do tm <- freshMeta ctx fc pure (tm, vty) -infer ctx tm = error (getFC tm) "Implement infer \{show tm}" +infer ctx (RLit fc (LString str)) = pure (Lit fc (LString str), !(primType fc "String")) +infer ctx (RLit fc (LInt i)) = pure (Lit fc (LInt i), !(primType fc "Int")) --- I don't have types for these yet... --- infer ctx (RLit (LString str)) = ?rhs_10 --- infer ctx (RLit (LInt i)) = ?rhs_11 --- infer ctx (RLit (LBool x)) = ?rhs_12 --- infer ctx (RCase tm xs) = ?rhs_9 +infer ctx tm = error (getFC tm) "Implement infer \{show tm}" -- The idea here is to insert a hole for a parse error -- but the parser doesn't emit this yet. diff --git a/src/Lib/Compile.idr b/src/Lib/Compile.idr index 739049c..a94ecaa 100644 --- a/src/Lib/Compile.idr +++ b/src/Lib/Compile.idr @@ -20,6 +20,7 @@ data JSExp : Type where LitArray : List JSExp -> JSExp LitObject : List (String, JSExp) -> JSExp LitString : String -> JSExp + LitInt : Int -> JSExp Apply : JSExp -> List JSExp -> JSExp Var : String -> JSExp JLam : List String -> JSStmt Return -> JSExp @@ -88,6 +89,8 @@ termToJS env (CFun nms t) f = in f $ JLam nms' (termToJS env' t JReturn) termToJS env (CRef nm) f = f $ Var nm termToJS env (CMeta k) f = f $ LitString "META \{show k}" +termToJS env (CLit (LString str)) f = f (LitString str) +termToJS env (CLit (LInt i)) f = f (LitInt i) termToJS env (CApp t args) f = termToJS env t (\ t' => argsToJS args [<] (\ args' => f (Apply t' args'))) where argsToJS : List CExp -> SnocList JSExp -> (List JSExp -> JSStmt e) -> JSStmt e @@ -122,6 +125,11 @@ jsString str = text "\"\{str}\"" stmtToDoc : JSStmt e -> Doc +||| separate with space +export +commaSep : List Doc -> Doc +commaSep = folddoc (\a, b => a ++ "," <+> b) + expToDoc : JSExp -> Doc expToDoc (LitArray xs) = ?expToDoc_rhs_0 expToDoc (LitObject xs) = text "{" <+> folddoc (\ a, e => a ++ ", " <+/> e) (map entry xs) <+> text "}" @@ -131,7 +139,8 @@ expToDoc (LitObject xs) = text "{" <+> folddoc (\ a, e => a ++ ", " <+/> e) (map entry (nm, exp) = text nm ++ ":" <+> expToDoc exp expToDoc (LitString str) = jsString str -expToDoc (Apply x xs) = expToDoc x ++ "(" ++ spread (map expToDoc xs) ++ ")" +expToDoc (LitInt i) = text $ show i +expToDoc (Apply x xs) = expToDoc x ++ "(" ++ commaSep (map expToDoc xs) ++ ")" expToDoc (Var nm) = text nm expToDoc (JLam nms (JReturn exp)) = text "(" <+> text (joinBy ", " nms) <+> ") =>" <+> expToDoc exp expToDoc (JLam nms body) = text "(" <+> text (joinBy ", " nms) <+> ") =>" <+> bracket "{" (stmtToDoc body) "}" @@ -176,6 +185,8 @@ entryToDoc (MkEntry name ty (Fn tm)) = do entryToDoc (MkEntry name type Axiom) = pure "" entryToDoc (MkEntry name type (TCon strs)) = pure "" entryToDoc (MkEntry name type (DCon arity str)) = pure $ dcon name arity +entryToDoc (MkEntry name _ PrimTCon) = pure $ text "/* PrimTCon \{name} */" +entryToDoc (MkEntry name _ (PrimFn src)) = pure $ text "const" <+> text name <+> "=" <+> text src export compile : M Doc diff --git a/src/Lib/CompileExp.idr b/src/Lib/CompileExp.idr index 9e90db8..b204b91 100644 --- a/src/Lib/CompileExp.idr +++ b/src/Lib/CompileExp.idr @@ -31,6 +31,7 @@ data CExp : Type where CCase : CExp -> List CAlt -> CExp CRef : Name -> CExp CMeta : Nat -> CExp + CLit : Literal -> CExp ||| I'm counting Lam in the term for arity. This matches what I need in ||| code gen. @@ -39,6 +40,11 @@ getArity : Tm -> Nat getArity (Lam _ _ t) = S (getArity t) getArity _ = Z +export +piArity : Tm -> Nat +piArity (Pi _ _ _ _ b) = S (piArity b) +piArity _ = Z + arityForName : FC -> Name -> M Nat arityForName fc nm = case lookup nm !get of Nothing => error fc "Name \{show nm} not in scope" @@ -46,6 +52,9 @@ arityForName fc nm = case lookup nm !get of (Just (MkEntry name type (TCon strs))) => pure 0 -- FIXME (Just (MkEntry name type (DCon k str))) => pure k (Just (MkEntry name type (Fn t))) => pure $ getArity t + (Just (MkEntry name type (PrimTCon))) => pure 0 + -- Assuming a primitive can't return a function + (Just (MkEntry name type (PrimFn t))) => pure $ piArity type export compileTerm : Tm -> M CExp @@ -84,11 +93,11 @@ compileTerm tm@(App _ _ _) with (funArgs tm) (Solved j tm) => pure $ getArity !(quote 0 tm) apply (CRef "Meta\{show k}") args' [<] arity _ | (t@(Ref fc nm _), args) = do - t' <- compileTerm t args' <- traverse compileTerm args - apply t' args' [<] !(arityForName fc nm) + arity <- arityForName fc nm + apply (CRef nm) args' [<] arity _ | (t, args) = do - debug "apply \{pprint [] t}" + debug "apply other \{pprint [] t}" t' <- compileTerm t args' <- traverse compileTerm args apply t' args' [<] 0 @@ -100,6 +109,7 @@ compileTerm (Case _ t alts) = do CaseDefault tm => pure $ CDefAlt !(compileTerm tm) CaseCons nm args tm => pure $ CConAlt nm args !(compileTerm tm)) alts pure $ CCase t' alts' +compileTerm (Lit _ lit) = pure $ CLit lit export diff --git a/src/Lib/Parser.idr b/src/Lib/Parser.idr index 716db5f..b6f35a0 100644 --- a/src/Lib/Parser.idr +++ b/src/Lib/Parser.idr @@ -48,12 +48,22 @@ braces pa = do optional : Parser a -> Parser (Maybe a) optional pa = Just <$> pa <|> pure Nothing -lit : Parser Raw -lit = do - t <- token Number +stringLit : Parser Raw +stringLit = do fc <- getFC + t <- token StringKind + pure $ RLit fc (LString (cast t)) + +intLit : Parser Raw +intLit = do + fc <- getFC + t <- token Number pure $ RLit fc (LInt (cast t)) + +lit : Parser Raw +lit = intLit <|> stringLit + -- typeExpr is term with arrows. export typeExpr : Parser Raw export term : (Parser Raw) @@ -236,6 +246,23 @@ export parseDef : Parser Decl parseDef = Def <$> getFC <*> ident <* keyword "=" <*> mustWork typeExpr +export +parsePType : Parser Decl +parsePType = PType <$> getFC <* keyword "ptype" <*> ident + +parsePFunc : Parser Decl +parsePFunc = do + fc <- getFC + keyword "pfunc" + nm <- ident + keyword ":" + ty <- typeExpr + keyword ":=" + src <- mustWork (cast <$> token StringKind) + pure $ PFunc fc nm ty src + -- PFunc <$> getFC <* keyword "pfunc" <*> mustWork ident <* keyword ":" <*> mustWork typeExpr <* keyword ":=" <*> (cast <$> token StringKind) + + export parseData : Parser Decl parseData = do @@ -257,7 +284,7 @@ parseNorm = DCheck <$> getFC <* keyword "#check" <*> typeExpr <* keyword ":" <*> export parseDecl : Parser Decl -parseDecl = parseImport <|> parseSig <|> parseDef <|> parseNorm <|> parseData +parseDecl = parsePType <|> parsePFunc <|> parseImport <|> parseNorm <|> parseData <|> parseSig <|> parseDef export parseMod : Parser Module diff --git a/src/Lib/Parser/Impl.idr b/src/Lib/Parser/Impl.idr index 6e0326d..c3c2c9f 100644 --- a/src/Lib/Parser/Impl.idr +++ b/src/Lib/Parser/Impl.idr @@ -138,7 +138,7 @@ Monad Parser where pred : (BTok -> Bool) -> String -> Parser String pred f msg = P $ \toks,com,col => case toks of - (t :: ts) => if f t then OK (value t) ts com else Fail False (error toks "\{msg} vt:\{value t}") toks com + (t :: ts) => if f t then OK (value t) ts com else Fail False (error toks "\{msg} at \{show $ kind t}:\{value t}") toks com [] => Fail False (error toks "\{msg} at EOF") toks com export diff --git a/src/Lib/ProcessDecl.idr b/src/Lib/ProcessDecl.idr index 010ff1b..6a4e3b0 100644 --- a/src/Lib/ProcessDecl.idr +++ b/src/Lib/ProcessDecl.idr @@ -30,6 +30,16 @@ processDecl (TypeSig fc nm tm) = do putStrLn "got \{pprint [] ty'}" modify $ setDef nm ty' Axiom +processDecl (PType fc nm) = do + ctx <- get + modify $ setDef nm (U fc) PrimTCon +processDecl (PFunc fc nm ty src) = do + top <- get + ty <- check (mkCtx top.metas) ty (VU fc) + ty' <- nf [] ty + putStrLn "pfunc \{nm} : \{pprint [] ty'} := \{show src}" + modify $ setDef nm ty' (PrimFn src) + processDecl (Def fc nm raw) = do putStrLn "-----" putStrLn "def \{show nm}" diff --git a/src/Lib/Syntax.idr b/src/Lib/Syntax.idr index 9d4700f..050615c 100644 --- a/src/Lib/Syntax.idr +++ b/src/Lib/Syntax.idr @@ -9,8 +9,6 @@ import Lib.Types public export data Raw : Type where -public export -data Literal = LString String | LInt Int | LBool Bool public export data RigCount = Rig0 | RigW @@ -70,6 +68,9 @@ data Decl | DImport FC Name | DCheck FC Raw Raw | Data FC Name Raw (List Decl) + | PType FC Name + | PFunc FC Name Raw String + public export record Module where @@ -84,7 +85,6 @@ foo ts = "(" ++ unwords ts ++ ")" 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 @@ -101,6 +101,8 @@ Show Decl where show (Data _ str xs ys) = foo ["Data", show str, show xs, show ys] show (DImport _ str) = foo ["DImport", show str] show (DCheck _ x y) = foo ["DCheck", show x, show y] + show (PType _ name) = foo ["PType", name] + show (PFunc _ nm ty src) = foo ["PFunc", nm, show ty, show src] export covering Show Module where @@ -166,7 +168,6 @@ Pretty Raw where asDoc p (RAnn _ x y) = text "TODO - RAnn" asDoc p (RLit _ (LString str)) = text $ interpolate str asDoc p (RLit _ (LInt i)) = text $ show i - asDoc p (RLit _ (LBool x)) = text $ show x asDoc p (RCase _ x xs) = text "TODO - RCase" asDoc p (RImplicit _) = text "_" asDoc p (RHole _) = text "?" @@ -184,3 +185,5 @@ Pretty Module where -- the behavior of nest is kinda weird, I have to do the nest before/around the . doDecl (Data _ nm x xs) = text "data" <+> text nm <+> text ":" <+> pretty x <+> (nest 2 $ text "where" stack (map doDecl xs)) doDecl (DCheck _ x y) = text "#check" <+> pretty x <+> ":" <+> pretty y + doDecl (PType _ nm) = text "ptype" <+> text nm + doDecl (PFunc _ nm ty src) = "pfunc" <+> text nm <+> ":" <+> nest 2 (pretty ty <+> ":=" <+/> text (show src)) diff --git a/src/Lib/TT.idr b/src/Lib/TT.idr index 068b8f3..2029cea 100644 --- a/src/Lib/TT.idr +++ b/src/Lib/TT.idr @@ -180,6 +180,7 @@ eval env mode (Pi fc x icit a b) = pure $ VPi fc x icit !(eval env mode a) (MkCl eval env mode (Bnd fc i) = case getAt i env of Just rval => pure rval Nothing => error' "Bad deBruin index \{show i}" +eval env mode (Lit fc lit) =pure $ VLit fc lit -- We need a neutral and some code to run the case tree @@ -207,6 +208,7 @@ quote l (VPi fc x icit a b) = pure $ Pi fc x icit !(quote l a) !(quote (S l) !(b quote l (VU fc) = pure (U fc) quote l (VRef fc n def sp) = quoteSp l (Ref fc n def) sp quote l (VCase fc sc alts) = pure $ Case fc !(quote l sc) alts +quote l (VLit fc lit) = pure $ Lit fc lit -- Can we assume closed terms? -- ezoo only seems to use it at [], but essentially does this: diff --git a/src/Lib/Token.idr b/src/Lib/Token.idr index c853652..47ba63c 100644 --- a/src/Lib/Token.idr +++ b/src/Lib/Token.idr @@ -5,11 +5,12 @@ module Lib.Token import public Text.Lexer public export -data Kind - = Ident - | Keyword - | Oper - | Number +data Kind + = Ident + | Keyword + | Oper + | Number + | StringKind | Symbol | Space | Comment @@ -34,6 +35,7 @@ Show Kind where show Comment = "Comment" show EOI = "EOI" show Pragma = "Pragma" + show StringKind = "String" export Eq Kind where Ident == Ident = True @@ -45,6 +47,7 @@ Eq Kind where LBrace == LBrace = True Semi == Semi = True RBrace == RBrace = True + StringKind == StringKind = True _ == _ = False export @@ -58,3 +61,7 @@ BTok = WithBounds (Token Kind) export value : BTok -> String value (MkBounded (Tok _ s) _ _) = s + +export +kind : BTok -> Kind +kind (MkBounded (Tok k s) _ _) = k diff --git a/src/Lib/Tokenizer.idr b/src/Lib/Tokenizer.idr index b8858a4..6b868a8 100644 --- a/src/Lib/Tokenizer.idr +++ b/src/Lib/Tokenizer.idr @@ -5,10 +5,10 @@ import Text.Lexer.Tokenizer import Lib.Token keywords : List String -keywords = ["let", "in", "where", "case", "of", "data", "U"] +keywords = ["let", "in", "where", "case", "of", "data", "U", "ptype", "pfunc", "module"] specialOps : List String -specialOps = ["->", ":", "=>"] +specialOps = ["->", ":", "=>", ":="] checkKW : String -> Token Kind checkKW s = if elem s keywords then Tok Keyword s else Tok Ident s @@ -22,11 +22,30 @@ opChar = pred isOpChar identMore : Lexer identMore = alphaNum <|> exact "." <|> exact "'" +quo : Recognise True +quo = is '"' + +esc : Recognise True -> Recognise True +esc l = is '\\' <+> l + +-- REVIEW maybe we can do this faster with the view thinger +unquote : String -> String +unquote str = case unpack str of + ('"' :: xs) => pack $ go xs + imp => pack $ go imp + where + go : List Char -> List Char + go [] = [] + go ['"'] = [] + go ('\\' :: (x :: xs)) = x :: go xs + go (x :: xs) = x :: go xs + rawTokens : Tokenizer (Token Kind) rawTokens = match (alpha <+> many identMore) checkKW <|> match (some digit) (Tok Number) <|> match (is '#' <+> many alpha) (Tok Pragma) + <|> match (quo <+> manyUntil quo ((esc any <+> any) <|> any) <+> opt quo) (Tok StringKind . unquote) <|> match (lineComment (exact "--")) (Tok Space) <|> match (blockComment (exact "/-") (exact "-/")) (Tok Space) <|> match (some opChar) (\s => Tok Oper s) diff --git a/src/Lib/Types.idr b/src/Lib/Types.idr index 422ad56..26741e9 100644 --- a/src/Lib/Types.idr +++ b/src/Lib/Types.idr @@ -64,6 +64,13 @@ data CaseAlt : Type where data Def : Type +public export +data Literal = LString String | LInt Int + +Show Literal where + show (LString str) = show str + show (LInt i) = show i + data Tm : Type where Bnd : FC -> Nat -> Tm -- Maybe Def here instead of Maybe Tm, we'll have DCon, TCon, etc. @@ -77,6 +84,7 @@ data Tm : Type where Pi : FC -> Name -> Icit -> Tm -> Tm -> Tm -- REVIEW - do we want to just push it up like idris? Case : FC -> Tm -> List CaseAlt -> Tm + Lit : FC -> Literal -> Tm %name Tm t, u, v @@ -90,6 +98,7 @@ getFC (App fc t u) = fc getFC (U fc) = fc getFC (Pi fc str icit t u) = fc getFC (Case fc t xs) = fc +getFC (Lit fc _) = fc covering Show Tm @@ -107,6 +116,7 @@ Show Tm where show (Lam _ nm t) = "(\\ \{nm} => \{show t})" show (App _ t u) = "(\{show t} \{show u})" show (Meta _ i) = "(Meta \{show i})" + show (Lit _ l) = "(Lit \{show l})" show (U _) = "U" show (Pi _ str Explicit t u) = "(Pi (\{str} : \{show t}) => \{show u})" show (Pi _ str Implicit t u) = "(Pi {\{str} : \{show t}} => \{show u})" @@ -153,6 +163,7 @@ pprint names tm = render 80 $ go names tm go names (Pi _ nm Explicit t u) = text "((" <+> text nm <+> ":" <+> go names t <+> ")" <+> "=>" <+> go (nm :: names) u <+> ")" go names (Case _ _ _) = "FIXME CASE" + go names (Lit _ lit) = text "\{show lit}" public export Pretty Tm where @@ -164,6 +175,7 @@ Pretty Tm where pretty (U _) = "U" pretty (Pi _ str icit t u) = text "(" <+> text str <+> ":" <+> pretty t <+> ")" <+> "=>" <+> pretty u <+> ")" pretty (Case _ _ _) = text "FIXME PRETTY CASE" + pretty (Lit _ lit) = text (show lit) -- public export -- data Closure : Nat -> Type @@ -198,6 +210,7 @@ data Val : Type where VLam : FC -> Name -> Closure -> Val VPi : FC -> Name -> Icit -> (a : Lazy Val) -> (b : Closure) -> Val VU : FC -> Val + VLit : FC -> Literal -> Val @@ -213,6 +226,7 @@ Show Val where show (VPi fc str Explicit x y) = "(%pi (\{str} : \{show x}). \{show y})" show (VCase fc sc alts) = "(%case \{show sc} ...)" show (VU _) = "U" + show (VLit _ lit) = show lit -- Not used - I was going to change context to have a List Binder -- instead of env, types, bds @@ -282,7 +296,7 @@ record MetaContext where public export -data Def = Axiom | TCon (List String) | DCon Nat String | Fn Tm +data Def = Axiom | TCon (List String) | DCon Nat String | Fn Tm | PrimTCon | PrimFn String public export covering @@ -291,6 +305,8 @@ Show Def where show (TCon strs) = "TCon \{show strs}" show (DCon k tyname) = "DCon \{show k} \{show tyname}" show (Fn t) = "Fn \{show t}" + show (PrimTCon) = "PrimTCon" + show (PrimFn src) = "PrimFn \{show src}" ||| entry in the top level context public export