dunham/newt
1
0
Fork 0
Code Issues Pull Requests Actions 1 Packages Projects Releases Wiki Activity

primitive string and int, primitive functions, codegen fixes

Browse Source
This commit is contained in:
Steve Dunham
2024-08-22 19:41:24 -07:00
parent dfa6b835b0
commit 9db5649446
14 changed files with 142 additions and 29 deletions
Download Patch File Download Diff File Expand all files Collapse all files

16
src/Lib/Check.idr
View File

@@ -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.

13
src/Lib/Compile.idr
View File

@@ -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

16
src/Lib/CompileExp.idr
View File

@@ -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

35
src/Lib/Parser.idr
View File

@@ -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

2
src/Lib/Parser/Impl.idr
View File

@@ -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

10
src/Lib/ProcessDecl.idr
View File

@@ -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}"

11
src/Lib/Syntax.idr
View File

@@ -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))

2
src/Lib/TT.idr
View File

@@ -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:

17
src/Lib/Token.idr
View File

@@ -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

23
src/Lib/Tokenizer.idr
View File

@@ -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)

18
src/Lib/Types.idr
View File

@@ -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