From 255e21f08a1c5f9064b9cd43e50fbcfe7608c78e Mon Sep 17 00:00:00 2001 From: Steve Dunham Date: Fri, 19 May 2023 21:10:57 -0700 Subject: [PATCH] Checkpoint what I'd previously been working on. --- README.md | 14 +++++ src/Lib/Check.idr | 10 ++++ src/Lib/Parser.idr | 51 +++++++++--------- src/Lib/Parser/Impl.idr | 20 ++++++-- src/Lib/TT.idr | 111 ++++++++++++++++++++++++++++++++++++++++ src/Syntax.idr | 66 +++++++++++++----------- 6 files changed, 215 insertions(+), 57 deletions(-) create mode 100644 README.md create mode 100644 src/Lib/Check.idr create mode 100644 src/Lib/TT.idr diff --git a/README.md b/README.md new file mode 100644 index 0000000..ba9051e --- /dev/null +++ b/README.md @@ -0,0 +1,14 @@ + + +I think we almost have enough of a parser to take another step. + +- [x] import statement +- [x] def +- [x] simple decl +- [ ] type definition +- [ ] read files +- [ ] write tests +- [ ] symbolic execution +- [ ] compilation + + diff --git a/src/Lib/Check.idr b/src/Lib/Check.idr new file mode 100644 index 0000000..9a8b3dd --- /dev/null +++ b/src/Lib/Check.idr @@ -0,0 +1,10 @@ +module Lib.Check + +import Lib.Parser.Impl +import Lib.TT + + +record Cxt where + env : List Val + + pos : SourcePos diff --git a/src/Lib/Parser.idr b/src/Lib/Parser.idr index 1c04c73..91c77c3 100644 --- a/src/Lib/Parser.idr +++ b/src/Lib/Parser.idr @@ -27,17 +27,20 @@ parens pa = do sym ")" pure t -lit : Parser Term +lit : Parser Raw lit = do t <- token Number - pure $ Lit (LInt (cast t)) + pure $ RLit (LInt (cast t)) export -term : (Parser Term) +term : (Parser Raw) + +withPos : Parser Raw -> Parser Raw +withPos p = RSrcPos <$> getPos <*> p -- ( t : ty ), (t , u) (t) --- Or do we want (x : ty) I think we may need to annotate any term -parenThinger : Parser Term +-- Or do we want (x : ty) I think we may need to annotate any Raw +parenThinger : Parser Raw parenThinger = do keyword "(" t <- term @@ -45,12 +48,12 @@ parenThinger = do -- we could do this with backtracing, but it'd kinda suck? fail "todo" --- the inside of term -atom : Parser Term -atom = lit - <|> Var <$> ident +-- the inside of Raw +atom : Parser Raw +atom = lit + <|> withPos (RVar <$> ident) <|> parens term - -- <|> sym "(" *> term <* sym ")" + -- <|> sym "(" *> Raw <* sym ")" -- -- atom is lit or ident @@ -67,16 +70,16 @@ operators = [ ("*",5,InfixL), ("/",5,InfixL) ] -parseApp : Parser Term +parseApp : Parser Raw parseApp = do hd <- atom rest <- many atom - pure $ foldl App hd rest + pure $ foldl RApp hd rest -parseOp : Lazy (Parser Term) +parseOp : Lazy (Parser Raw) parseOp = parseApp >>= go 0 where - go : Int -> Term -> Parser Term + go : Int -> Raw -> Parser Raw go prec left = do op <- token Oper @@ -88,21 +91,21 @@ parseOp = parseApp >>= go 0 let pr = case fix of InfixR => p; _ => p + 1 -- commit? right <- go pr !(parseApp) - go prec (App (App (Var op) left) right) + go prec (RApp (RApp (RVar op) left) right) <|> pure left export -letExpr : Parser Term +letExpr : Parser Raw letExpr = do keyword "let" commit alts <- startBlock $ someSame $ letAssign keyword' "in" scope <- term - pure $ Let alts scope - -- Let <$ keyword "let" <*> ident <* keyword "=" <*> term <* keyword "in" <*> term + pure $ RLet alts scope + -- Let <$ keyword "let" <*> ident <* keyword "=" <*> Raw <* keyword "in" <*> Raw where - letAssign : Parser (Name,Term) + letAssign : Parser (Name,Raw) letAssign = do name <- ident keyword "=" @@ -115,33 +118,33 @@ pPattern <|> PatVar <$> ident export -lamExpr : Parser Term +lamExpr : Parser Raw lamExpr = do keyword "\\" commit name <- pPattern keyword "=>" scope <- term - pure $ Lam name scope + pure $ RLam name scope caseAlt : Parser CaseAlt caseAlt = do - pat <- pPattern -- Term and sort it out later? + pat <- pPattern -- term and sort it out later? keyword "=>" commit t <- term pure $ MkAlt pat t export -caseExpr : Parser Term +caseExpr : Parser Raw caseExpr = do keyword "case" commit sc <- term keyword "of" alts <- startBlock $ someSame $ caseAlt - pure $ Case sc alts + pure $ RCase sc alts term = defer $ \_ => caseExpr diff --git a/src/Lib/Parser/Impl.idr b/src/Lib/Parser/Impl.idr index 5b9b29a..18a40db 100644 --- a/src/Lib/Parser/Impl.idr +++ b/src/Lib/Parser/Impl.idr @@ -6,6 +6,14 @@ public export TokenList : Type TokenList = List BTok +-- I was going to use a record, but we're peeling this off of bounds at the moment. +public export +SourcePos : Type +SourcePos = (Int,Int) + +emptyPos : SourcePos +emptyPos = (0,0) + -- Error of a parse public export data Error = E String @@ -31,15 +39,15 @@ Functor Result where -- dunno why I'm making that a pair.. export -data Parser a = P (TokenList -> Bool -> (lc : (Int,Int)) -> Result a) +data Parser a = P (TokenList -> Bool -> (lc : SourcePos) -> Result a) export -runP : Parser a -> TokenList -> Bool -> (Int,Int) -> Result a +runP : Parser a -> TokenList -> Bool -> SourcePos -> Result a runP (P f) = f export parse : Parser a -> TokenList -> Either String a -parse pa toks = case runP pa toks False (0,0) of +parse pa toks = case runP pa toks False emptyPos of Fail (E msg) toks com => Left "error: \{msg} next at: \{show toks}" OK a [] _ => Right a OK a ts _ => Left "Extra toks \{show ts}" @@ -65,6 +73,7 @@ Applicative Parser where (OK x toks com) => OK (f x) toks com (Fail err toks com) => Fail err toks com +-- REVIEW it would be nice if the second argument was lazy... export Alternative Parser where empty = fail "empty" @@ -112,6 +121,11 @@ mutual -- Lexer.LLet -> PLet <$> blockOfMany let_ <* token Lexer.In <*> term -- withIndentationBlock - sets the col +export +getPos : Parser SourcePos +getPos = P $ \toks,com, (l,c) => case toks of + [] => Fail (E "End of file") toks com -- OK emptyPos toks com + (t :: ts) => OK (start t) toks com ||| Start an indented block and run parser in it export diff --git a/src/Lib/TT.idr b/src/Lib/TT.idr new file mode 100644 index 0000000..15dd751 --- /dev/null +++ b/src/Lib/TT.idr @@ -0,0 +1,111 @@ +module Lib.TT +-- For SourcePos +import Lib.Parser.Impl + +public export +Name : Type +Name = String + +export +data Icit = Implicit | Explicit + +-- Sorta cribbed from Kovacs +Ty : Type + +-- Idris and Kovacs have Icit at this level. +public export +data Tm + = Local Nat -- IsVar + | Ref String + | Lam Name Icit Tm + | App Tm Tm + | U + | Pi Name Ty Ty + | Let Name Ty Tm Tm + +Ty = Tm + +public export +data Closure : Type +VTy : Type + + -- Closure unpacked in the original +public export +data Val + = VVar Nat -- level + | VApp Val (Lazy Val) + | VLam Name Icit Closure + | VPi Name (Lazy VTy) Closure + | VU + +VTy = Val + +public export +Env : Type +Env = List Val + +-- + +lvl2Ix : Nat -> Nat -> Nat + +data Closure : Type where + MkClosure : Env -> Tm -> Closure + +infixl 8 $$ + +eval : Env -> Tm -> Val + +($$) : Closure -> Lazy Val -> Val +(MkClosure env t) $$ u = eval (u :: env) t + +eval env (Local k) = ?hole +eval env (Ref x) = ?hole_1 +eval env (Lam x _ t) = ?hole_2 +eval env (App t u) = case (eval env t, eval env u) of + (VLam _ icit t, u) => t $$ u + (t, u) => VApp t u + +eval env U = VU +eval env (Pi x a b) = VPi x (eval env a) (MkClosure env b) +eval env (Let x _ t u) = eval (eval env t :: env) u + +quote : Nat -> Val -> Tm +quote l (VVar k) = Local (lvl2Ix l k) +quote l (VApp t u) = App (quote l t) (quote l u) +quote l (VLam x icit t) = Lam x icit (quote (l + 1) (t $$ VVar l)) +quote l (VPi x a b) = Pi x (quote l a) (quote (l+1) (b $$ VVar l)) +quote l VU = ?rhs_4 + +nf : Env -> Tm -> Tm +nf env t = quote (length env) (eval env t) + +--- +public export +conv : (lvl : Nat) -> Val -> Val -> Bool + + +-- +public export +Types : Type +Types = List (Name, Lazy VTy) + +public export +record Ctx where + constructor MkCtx + env : Env + types : Types + lvl : Nat + -- For now, we're following Kovacs and using a node for + -- source position. Might switch to FC at some point? + pos : SourcePos + +public export +emptyCtx : Ctx +emptyCtx = MkCtx [] [] 0 (0,0) + +public export +bind : Name -> Lazy VTy -> Ctx -> Ctx +bind x a (MkCtx env types l pos) = + MkCtx (VVar l :: env) ((x,a) :: types) (l+1) pos + + diff --git a/src/Syntax.idr b/src/Syntax.idr index f35bb2a..34436a5 100644 --- a/src/Syntax.idr +++ b/src/Syntax.idr @@ -1,12 +1,12 @@ module Syntax import Data.String +import Lib.Parser.Impl + Name = String -data Term : Type where - -TyTerm = Term +data Raw : Type where public export data Literal = LString String | LInt Int | LBool Bool @@ -26,20 +26,23 @@ data Pattern -- could be a pair, but I suspect stuff will be added? public export -data CaseAlt = MkAlt Pattern Term +data CaseAlt = MkAlt Pattern Raw public export -data Term - = Var Name - | Ann Term TyTerm - | Lit Literal - | Let (List (Name, Term)) Term - | Pi Name Plicity Term Term - | App Term Term - | Lam Pattern Term - | Case Term (List CaseAlt) - | Wildcard - | ParseError String +data Raw + = RVar Name + | RLam Pattern Raw + | RApp Raw Raw + | RU + | RPi Name Plicity Raw Raw + | RLet (List (Name, Raw)) Raw + | RSrcPos SourcePos Raw + + | RAnn Raw Raw + | RLit Literal + | RCase Raw (List CaseAlt) + | RWildcard + | RParseError String -- derive some stuff - I'd like json, eq, show, ... @@ -52,10 +55,10 @@ data ConstrDef = MkCDef Name Telescope public export data Decl - = TypeSig Name TyTerm - | Def Name Term + = TypeSig Name Raw + | Def Name Raw | DImport Name - | Data Name Term (List Decl) + | Data Name Raw (List Decl) public export record Module where @@ -76,7 +79,7 @@ Show Literal where export covering -implementation Show Term +implementation Show Raw export implementation Show Decl @@ -117,15 +120,18 @@ Show Plicity where show Eq = "Eq" covering -Show Term where - show Wildcard = "Wildcard" - 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 Raw where + show RWildcard = "Wildcard" + show (RVar name) = foo ["RVar", show name] + show (RAnn t ty) = foo [ "RAnn", show t, show ty] + show (RLit x) = foo [ "RLit", show x] + show (RLet alts y) = foo [ "Let", show alts, show y] + show (RPi str x y z) = foo [ "Pi", show str, show x, show y, show z] + show (RApp x y) = foo [ "App", show x, show y] + show (RLam x y) = foo [ "Lam", show x, show y] + show (RCase x xs) = foo [ "Case", show x, show xs] + show (RParseError str) = foo [ "ParseError", "str"] + show RU = "U" + show (RSrcPos pos tm) = show tm +