From d4bcbc59490cc777f9cb7e8f4f04dfac09c257d1 Mon Sep 17 00:00:00 2001 From: Steve Dunham Date: Tue, 26 Nov 2024 14:08:57 -0800 Subject: [PATCH] primitive erasure implementation, dead code elimination --- TODO.md | 12 ++-- aoc2023/Node.newt | 2 +- newt-vscode/syntaxes/newt.tmLanguage.json | 2 +- playground/src/monarch.ts | 1 + src/Lib/Compile.idr | 63 ++++++++++++++--- src/Lib/CompileExp.idr | 82 ++++++++++++++++------- src/Lib/Elab.idr | 32 ++++----- src/Lib/Eval.idr | 6 +- src/Lib/Parser.idr | 3 +- src/Lib/ProcessDecl.idr | 37 +++++----- src/Lib/Syntax.idr | 9 +-- src/Lib/Types.idr | 47 +++++++------ src/Lib/Util.idr | 6 +- 13 files changed, 196 insertions(+), 106 deletions(-) diff --git a/TODO.md b/TODO.md index f79a16d..900704b 100644 --- a/TODO.md +++ b/TODO.md @@ -2,9 +2,10 @@ ## TODO - [ ] add filenames to FC -- [ ] maybe use backtick for javascript so we don't highlight strings as JS +- [x] maybe use backtick for javascript so we don't highlight strings as JS - [ ] add namespaces -- [ ] imported files leak info messages everywhere +- [x] dead code elimination +- [x] imported files leak info messages everywhere - For now, take the start ix for the file and report at end starting there - [ ] update node shim to include idris2-playground changes - [ ] accepting DCon for another type (skipping case, but should be an error) @@ -97,9 +98,10 @@ - [ ] decide what to do for erasure - I'm going to try explicit annotation, forall/∀ is erased - [x] Parser side - - [ ] push down to value/term - - [ ] check quantity - - [ ] erase in output + - [x] push down to value/term + - [ ] check quantity!! + - [x] erase in output + - [ ] remove erased top level arguments - [ ] type at point in vscode - [ ] repl - [ ] LSP diff --git a/aoc2023/Node.newt b/aoc2023/Node.newt index b255c66..6077b96 100644 --- a/aoc2023/Node.newt +++ b/aoc2023/Node.newt @@ -4,4 +4,4 @@ import Prelude pfunc fs : JSObject := `require('fs')` pfunc getArgs : List String := `arrayToList(String, process.argv)` -pfunc readFile : (fn : String) -> IO String := `(fn) => (w) => MkIORes(Unit, fs.readFileSync(fn, 'utf8'), w)` +pfunc readFile uses (fs) : (fn : String) -> IO String := `(fn) => (w) => MkIORes(Unit, fs.readFileSync(fn, 'utf8'), w)` diff --git a/newt-vscode/syntaxes/newt.tmLanguage.json b/newt-vscode/syntaxes/newt.tmLanguage.json index 05b1d04..077ee80 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|do|class|instance|case|of|let|if|then|else|forall|∀|in|U|module|import|ptype|pfunc|infix|infixl|infixr)\\b" + "match": "\\b(data|where|do|class|uses|instance|case|of|let|if|then|else|forall|∀|in|U|module|import|ptype|pfunc|infix|infixl|infixr)\\b" }, { "name": "string.js", diff --git a/playground/src/monarch.ts b/playground/src/monarch.ts index e97574b..71bab5c 100644 --- a/playground/src/monarch.ts +++ b/playground/src/monarch.ts @@ -77,6 +77,7 @@ export let newtTokens: monaco.languages.IMonarchLanguage = { "ptype", "pfunc", "if", + "uses", "then", "else", "class", diff --git a/src/Lib/Compile.idr b/src/Lib/Compile.idr index 57eadb3..621c6f9 100644 --- a/src/Lib/Compile.idr +++ b/src/Lib/Compile.idr @@ -4,6 +4,7 @@ module Lib.Compile import Lib.Types import Lib.Prettier import Lib.CompileExp +import Lib.TopContext import Data.String import Data.Maybe import Data.Nat @@ -94,6 +95,7 @@ termToJS : JSEnv -> CExp -> Cont e -> JSStmt e termToJS env (CBnd k) f = case getAt k env.env of (Just e) => f e Nothing => ?bad_bounds +termToJS env CErased f = f JUndefined termToJS env (CLam nm t) f = let nm' = fresh nm env -- "\{nm}$\{show $ length env}" env' = push env (Var nm') @@ -206,6 +208,8 @@ expToDoc (LitObject xs) = text "{" <+> folddoc (\ a, e => a ++ ", " <+/> e) (map expToDoc (LitString str) = jsString str expToDoc (LitInt i) = text $ show i +-- TODO add precedence +expToDoc (Apply x@(JLam{}) xs) = text "(" ++ expToDoc x ++ ")" ++ "(" ++ nest 2 (commaSep (map expToDoc xs)) ++ ")" expToDoc (Apply x xs) = expToDoc x ++ "(" ++ nest 2 (commaSep (map expToDoc xs)) ++ ")" expToDoc (Var nm) = jsIdent nm expToDoc (JLam nms (JReturn exp)) = text "(" <+> commaSep (map jsIdent nms) <+> ") =>" <+> "(" ++ expToDoc exp ++ ")" @@ -247,25 +251,64 @@ dcon nm arity = obj := ("tag", LitString nm) :: map (\x => (x, Var x)) args in stmtToDoc $ JConst nm (JLam args (JReturn (LitObject obj))) +-- use iife to turn stmts into expr +maybeWrap : JSStmt Return -> JSExp +maybeWrap (JReturn exp) = exp +maybeWrap stmt = Apply (JLam [] stmt) [] entryToDoc : TopEntry -> M Doc entryToDoc (MkEntry name ty (Fn tm)) = do - -- so this has a bunch of lambdas on it now, which we want to consolidate - -- and we might need betas? It seems like a mirror of what happens in CExp debug "compileFun \{pprint [] tm}" ct <- compileFun tm - -- If ct has zero arity and is a compount expression, this fails.. - let body@(JPlain {}) = termToJS empty ct JPlain - | js => error (getFC tm) "Not a plain expression: \{render 80 $ stmtToDoc js}" - pure (text "const" <+> jsIdent name <+> text "=" <+/> stmtToDoc body) + let exp = maybeWrap $ termToJS empty ct JReturn + pure $ text "const" <+> jsIdent name <+> text "=" <+/> expToDoc exp ++ ";" entryToDoc (MkEntry name type Axiom) = pure "" entryToDoc (MkEntry name type (TCon strs)) = pure $ dcon name (piArity type) entryToDoc (MkEntry name type (DCon arity str)) = pure $ dcon name arity entryToDoc (MkEntry name type PrimTCon) = pure $ dcon name (piArity type) -entryToDoc (MkEntry name _ (PrimFn src)) = pure $ text "const" <+> jsIdent name <+> "=" <+> text src +entryToDoc (MkEntry name _ (PrimFn src _)) = pure $ text "const" <+> jsIdent name <+> "=" <+> text src + +||| This version (call `reverse . snd <$> process "main" ([],[])`) will do dead +||| code elimination, but the Prelude js primitives are reaching for +||| stuff like True, False, MkUnit, fs which get eliminated +process : (List String, List Doc) -> String -> M (List String, List Doc) +process (done,docs) nm = do + let False = nm `elem` done | _ => pure (done,docs) + top <- get + case TopContext.lookup nm top of + Nothing => error emptyFC "\{nm} not in scope" + Just entry@(MkEntry name ty (PrimFn src uses)) => do + (done,docs) <- foldlM process (nm :: done, docs) uses + pure (done, !(entryToDoc entry) :: docs) + Just (MkEntry name ty (Fn tm)) => do + debug "compileFun \{pprint [] tm}" + ct <- compileFun tm + -- If ct has zero arity and is a compount expression, this fails.. + let exp = maybeWrap $ termToJS empty ct JReturn + let doc = text "const" <+> jsIdent name <+> text "=" <+/> expToDoc exp ++ ";" + (done,docs) <- walkTm tm (nm :: done, docs) + pure (done, doc :: docs) + + Just entry => pure (nm :: done, !(entryToDoc entry) :: docs) + where + walkTm : Tm -> (List String, List Doc) -> M (List String, List Doc) + walkAlt : (List String, List Doc) -> CaseAlt -> M (List String, List Doc) + walkAlt acc (CaseDefault t) = pure acc + walkAlt acc (CaseCons name args t) = walkTm t acc + walkAlt acc (CaseLit lit t) = walkTm t acc + + walkTm (Ref x nm y) acc = process acc nm + walkTm (Lam x str t) acc = walkTm t acc + walkTm (App x t u) acc = walkTm t !(walkTm u acc) + walkTm (Pi x str icit y t u) acc = walkTm t !(walkTm u acc) + walkTm (Let x str t u) acc = walkTm t !(walkTm u acc) + walkTm (LetRec x str t u) acc = walkTm t !(walkTm u acc) + walkTm (Case x t alts) acc = foldlM walkAlt acc alts + walkTm _ acc = pure acc export compile : M (List Doc) -compile = do - top <- get - traverse entryToDoc top.defs +-- compile = do +-- top <- get +-- traverse entryToDoc top.defs +compile = reverse . snd <$> process ([],[]) "main" diff --git a/src/Lib/CompileExp.idr b/src/Lib/CompileExp.idr index 138eeac..833dfa6 100644 --- a/src/Lib/CompileExp.idr +++ b/src/Lib/CompileExp.idr @@ -1,5 +1,5 @@ ||| First pass of compilation -||| - work out arities and fully apply functions / constructors +||| - work out arities and fully apply functions / constructors (currying) ||| - expand metas ||| I could make names unique (e.q. on lambdas), but I might want that to vary per backend? module Lib.CompileExp @@ -36,41 +36,48 @@ data CExp : Type where CLit : Literal -> CExp CLet : Name -> CExp -> CExp -> CExp CLetRec : Name -> CExp -> CExp -> CExp + CErased : CExp ||| I'm counting Lam in the term for arity. This matches what I need in ||| code gen. export -getArity : Tm -> Nat -getArity (Lam _ _ t) = S (getArity t) -getArity _ = Z +lamArity : Tm -> Nat +lamArity (Lam _ _ t) = S (lamArity t) +lamArity _ = Z export piArity : Tm -> Nat -piArity (Pi _ _ _ _ b) = S (piArity b) +piArity (Pi _ _ _ quant _ b) = S (piArity b) piArity _ = Z +||| This is how much we want to curry at top level +||| leading lambda Arity is used for function defs and metas +||| TODO - figure out how this will work with erasure arityForName : FC -> Name -> M Nat arityForName fc nm = case lookup nm !get of -- let the magic hole through for now (will generate bad JS) - Nothing => if nm == "?" then pure 0 else error fc "Name \{show nm} not in scope" + Nothing => error fc "Name \{show nm} not in scope" (Just (MkEntry name type Axiom)) => pure 0 (Just (MkEntry name type (TCon strs))) => pure $ piArity type (Just (MkEntry name type (DCon k str))) => pure k - (Just (MkEntry name type (Fn t))) => pure $ getArity t + (Just (MkEntry name type (Fn t))) => pure $ lamArity t (Just (MkEntry name type (PrimTCon))) => pure $ piArity type -- Assuming a primitive can't return a function - (Just (MkEntry name type (PrimFn t))) => pure $ piArity type + (Just (MkEntry name type (PrimFn t uses))) => pure $ piArity type export compileTerm : Tm -> M CExp -- need to eta out extra args, fill in the rest of the apps -apply : CExp -> List CExp -> SnocList CExp -> Nat -> M CExp --- out of args, make one up -apply t [] acc (S k) = pure $ - CLam "eta\{show k}" !(apply t [] (acc :< CBnd k) k) -apply t (x :: xs) acc (S k) = apply t xs (acc :< x) k -apply t ts acc 0 = go (CApp t (acc <>> [])) ts +apply : CExp -> List CExp -> SnocList CExp -> Nat -> Tm -> M CExp +-- out of args, make one up (fix that last arg) +apply t [] acc (S k) ty = pure $ + CLam "eta\{show k}" !(apply t [] (acc :< CBnd k) k ty) +apply t (x :: xs) acc (S k) (Pi y str icit Zero a b) = apply t xs (acc :< CErased) k b +apply t (x :: xs) acc (S k) (Pi y str icit Many a b) = apply t xs (acc :< x) k b +-- see if there is anything we have to handle here +apply t (x :: xs) acc (S k) ty = error (getFC ty) "Expected pi \{showTm ty}" +apply t ts acc 0 ty = go (CApp t (acc <>> [])) ts where go : CExp -> List CExp -> M CExp -- drop zero arg call @@ -78,37 +85,60 @@ apply t ts acc 0 = go (CApp t (acc <>> [])) ts go t [] = pure t go t (arg :: args) = go (CApp t [arg]) args +-- apply : CExp -> List CExp -> SnocList CExp -> Nat -> M CExp +-- -- out of args, make one up +-- apply t [] acc (S k) = pure $ +-- CLam "eta\{show k}" !(apply t [] (acc :< CBnd k) k) +-- apply t (x :: xs) acc (S k) = apply t xs (acc :< x) k +-- apply t ts acc 0 = go (CApp t (acc <>> [])) ts +-- where +-- go : CExp -> List CExp -> M CExp +-- -- drop zero arg call +-- go (CApp t []) args = go t args +-- go t [] = pure t +-- go t (arg :: args) = go (CApp t [arg]) args + compileTerm (Bnd _ k) = pure $ CBnd k -- need to eta expand to arity -compileTerm t@(Ref fc nm _) = apply (CRef nm) [] [<] !(arityForName fc nm) +compileTerm t@(Ref fc nm _) = do + top <- get + let Just (MkEntry _ type _) = lookup nm top + | Nothing => error fc "Undefined name \{nm}" + apply (CRef nm) [] [<] !(arityForName fc nm) type compileTerm (Meta _ k) = pure $ CRef "meta$\{show k}" -- FIXME compileTerm (Lam _ nm t) = pure $ CLam nm !(compileTerm t) compileTerm tm@(App _ _ _) with (funArgs tm) _ | (Meta _ k, args) = do -- FIXME get arity or zonk? + -- let's see if this happens after zonking + error (getFC tm) "Lambda in CompileExp" -- Maybe we should be storing the Term without the lambdas... -- we don't have a lot here, but JS has an "environment" with names and -- we can assume fully applied. - meta <- lookupMeta k - args' <- traverse compileTerm args - -- apply (CRef "Meta\{show k}") args' [<] 0 - arity <- case meta of - -- maybe throw - (Unsolved x j ctx _ _ _) => pure 0 -- FIXME # of Bound in ctx.bds - (Solved _ j tm) => pure $ getArity !(quote 0 tm) - apply (CRef "Meta\{show k}") args' [<] arity + -- meta <- lookupMeta k + -- args' <- traverse compileTerm args + -- -- apply (CRef "Meta\{show k}") args' [<] 0 + -- arity <- case meta of + -- -- maybe throw + -- (Unsolved x j ctx _ _ _) => pure 0 -- FIXME # of Bound in ctx.bds + -- (Solved _ j tm) => pure $ lamArity !(quote 0 tm) + -- apply (CRef "Meta\{show k}") args' [<] arity _ | (t@(Ref fc nm _), args) = do args' <- traverse compileTerm args arity <- arityForName fc nm - apply (CRef nm) args' [<] arity + top <- get + let Just (MkEntry _ type _) = lookup nm top + | Nothing => error fc "Undefined name \{nm}" + apply (CRef nm) args' [<] arity type _ | (t, args) = do debug "apply other \{pprint [] t}" t' <- compileTerm t args' <- traverse compileTerm args - apply t' args' [<] 0 + apply t' args' [<] 0 (U emptyFC) + -- error (getFC t) "Don't know how to apply \{showTm t}" compileTerm (U _) = pure $ CRef "U" -compileTerm (Pi _ nm icit t u) = pure $ CApp (CRef "PiType") [ !(compileTerm t), CLam nm !(compileTerm u)] +compileTerm (Pi _ nm icit rig t u) = pure $ CApp (CRef "PiType") [ !(compileTerm t), CLam nm !(compileTerm u)] compileTerm (Case _ t alts) = do t' <- compileTerm t alts' <- traverse (\case diff --git a/src/Lib/Elab.idr b/src/Lib/Elab.idr index f9cb2c4..2bd91e1 100644 --- a/src/Lib/Elab.idr +++ b/src/Lib/Elab.idr @@ -173,7 +173,7 @@ rename meta ren lvl v = go ren lvl v debug "rename: \{show ix} is unsolved" catchError {e=Error} (goSpine ren lvl (Meta fc ix) sp) (\err => throwError $ Postpone fc ix (errorMsg err)) go ren lvl (VLam fc n t) = pure (Lam fc n !(go (lvl :: ren) (S lvl) !(t $$ VVar fc lvl [<]))) - go ren lvl (VPi fc n icit ty tm) = pure (Pi fc n icit !(go ren lvl ty) !(go (lvl :: ren) (S lvl) !(tm $$ VVar emptyFC lvl [<]))) + go ren lvl (VPi fc n icit rig ty tm) = pure (Pi fc n icit rig !(go ren lvl ty) !(go (lvl :: ren) (S lvl) !(tm $$ VVar emptyFC lvl [<]))) go ren lvl (VU fc) = pure (U fc) -- for now, we don't do solutions with case in them. go ren lvl (VCase fc sc alts) = error fc "Case in solution" @@ -278,7 +278,7 @@ unify env mode t u = do else solve env k sp (VMeta fc' k' sp') >> pure neutral unify' t (VMeta fc' i' sp') = solve env i' sp' t >> pure neutral unify' (VMeta fc i sp) t' = solve env i sp t' >> pure neutral - unify' (VPi fc _ _ a b) (VPi fc' _ _ a' b') = do + unify' (VPi fc _ _ _ a b) (VPi fc' _ _ _ a' b') = do let fresh = VVar fc (length env) [<] [| unify env mode a a' <+> unify (fresh :: env) mode !(b $$ fresh) !(b' $$ fresh) |] @@ -378,14 +378,14 @@ unifyCatch fc ctx ty' ty = do insert : (ctx : Context) -> Tm -> Val -> M (Tm, Val) insert ctx tm ty = do case !(forceMeta ty) of - VPi fc x Auto a b => do + VPi fc x Auto rig a b => do -- FIXME mark meta as auto, maybe try to solve here? m <- freshMeta ctx (getFC tm) a AutoSolve debug "INSERT Auto \{pprint (names ctx) m} : \{show a}" debug "TM \{pprint (names ctx) tm}" mv <- eval ctx.env CBN m insert ctx (App (getFC tm) tm m) !(b $$ mv) - VPi fc x Implicit a b => do + VPi fc x Implicit rig a b => do m <- freshMeta ctx (getFC tm) a Normal debug "INSERT \{pprint (names ctx) m} : \{show a}" debug "TM \{pprint (names ctx) tm}" @@ -482,7 +482,7 @@ getConstructors ctx scfc tm = error scfc "Can't split - not VRef: \{!(pprint ctx -- the pi-type here is the telescope of a constructor -- return context, remaining type, and list of names extendPi : Context -> Val -> SnocList Bind -> SnocList Val -> M (Context, Val, List Bind, SnocList Val) -extendPi ctx (VPi x str icit a b) nms sc = do +extendPi ctx (VPi x str icit rig a b) nms sc = do let nm = fresh str -- "pat" let ctx' = extend ctx nm a let v = VVar emptyFC (length ctx.env) [<] @@ -499,7 +499,7 @@ substVal k v tm = go tm go : Val -> Val go (VVar fc j sp) = if j == k then v else (VVar fc j (map go sp)) go (VLet fc nm a b) = VLet fc nm (go a) b - go (VPi fc nm icit a b) = VPi fc nm icit (go a) b + go (VPi fc nm icit rig a b) = VPi fc nm icit rig (go a) b go (VMeta fc ix sp) = VMeta fc ix (map go sp) go (VRef fc nm y sp) = VRef fc nm y (map go sp) go tm = tm @@ -850,7 +850,7 @@ buildLitCases ctx prob fc scnm scty = do -- This process is similar to extendPi, but we need to stop -- if one clause is short on patterns. buildTree ctx (MkProb [] ty) = error emptyFC "no clauses" -buildTree ctx prob@(MkProb ((MkClause fc cons (x :: xs) expr) :: cs) (VPi _ str icit a b)) = do +buildTree ctx prob@(MkProb ((MkClause fc cons (x :: xs) expr) :: cs) (VPi _ str icit rig a b)) = do let l = length ctx.env let nm = fresh str -- "pat" let ctx' = extend ctx nm a @@ -934,7 +934,7 @@ check ctx tm ty = case (tm, !(forceType ctx.env ty)) of -- rendered in ProcessDecl (RHole fc, ty) => freshMeta ctx fc ty User - (t@(RLam fc (BI _ nm icit _) tm), ty@(VPi fc' nm' icit' a b)) => do + (t@(RLam fc (BI _ nm icit _) tm), ty@(VPi fc' nm' icit' rig a b)) => do debug "icits \{nm} \{show icit} \{nm'} \{show icit'}" if icit == icit' then do let var = VVar fc (length ctx.env) [<] @@ -952,7 +952,7 @@ check ctx tm ty = case (tm, !(forceType ctx.env ty)) of (t@(RLam _ (BI fc nm icit quant) tm), ty) => error fc "Expected pi type, got \{!(prvalCtx ty)}" - (tm, ty@(VPi fc nm' Implicit a b)) => do + (tm, ty@(VPi fc nm' Implicit rig a b)) => do let names = toList $ map fst ctx.types debug "XXX edge case add implicit lambda {\{nm'} : \{show a}} to \{show tm} " let var = VVar fc (length ctx.env) [<] @@ -980,8 +980,8 @@ check ctx tm ty = case (tm, !(forceType ctx.env ty)) of -- Kovacs doesn't insert on tm = Implicit Lam, we don't have Plicity in Lam -- so I'll check the inferred type for an implicit pi -- This seems wrong, the ty' is what insert runs on, so we're just short circuiting here - (tm'@(Lam{}), ty'@(VPi _ _ Implicit _ _)) => do debug "CheckMe 1"; pure (tm', ty') - (tm'@(Lam{}), ty'@(VPi _ _ Auto _ _)) => do debug "CheckMe 2"; pure (tm', ty') + (tm'@(Lam{}), ty'@(VPi _ _ Implicit rig _ _)) => do debug "CheckMe 1"; pure (tm', ty') + (tm'@(Lam{}), ty'@(VPi _ _ Auto rig _ _)) => do debug "CheckMe 2"; pure (tm', ty') (tm', ty') => do debug "RUN INSERT ON \{pprint names tm'} at \{show ty'}" insert ctx tm' ty' @@ -1016,7 +1016,7 @@ infer ctx (RApp fc t u icit) = do pure (Auto, t, tty) (a,b) <- case !(forceMeta tty) of - (VPi fc str icit' a b) => if icit' == icit then pure (a,b) + (VPi fc str icit' rig a b) => if icit' == icit then pure (a,b) else error fc "IcitMismatch \{show icit} \{show icit'}" -- If it's not a VPi, try to unify it with a VPi @@ -1025,7 +1025,8 @@ infer ctx (RApp fc t u icit) = do debug "unify PI for \{show tty}" a <- eval ctx.env CBN !(freshMeta ctx fc (VU emptyFC) Normal) b <- MkClosure ctx.env <$> freshMeta (extend ctx ":ins" a) fc (VU emptyFC) Normal - unifyCatch fc ctx tty (VPi fc ":ins" icit a b) + -- FIXME - I had to guess Many here. What are the side effects? + unifyCatch fc ctx tty (VPi fc ":ins" icit Many a b) pure (a,b) u <- check ctx u a @@ -1036,7 +1037,7 @@ infer ctx (RPi _ (BI fc nm icit quant) ty ty2) = do ty' <- check ctx ty (VU fc) vty' <- eval ctx.env CBN ty' ty2' <- check (extend ctx nm vty') ty2 (VU fc) - pure (Pi fc nm icit ty' ty2', (VU fc)) + pure (Pi fc nm icit quant ty' ty2', (VU fc)) infer ctx (RLet fc nm ty v sc) = do ty' <- check ctx ty (VU emptyFC) vty <- eval ctx.env CBN ty' @@ -1057,8 +1058,7 @@ infer ctx (RLam _ (BI fc nm icit quant) tm) = do let ctx' = extend ctx nm a (tm', b) <- infer ctx' tm debug "make lam for \{show nm} scope \{pprint (names ctx) tm'} : \{show b}" - pure $ (Lam fc nm tm', VPi fc nm icit a $ MkClosure ctx.env !(quote (S ctx.lvl) b)) - -- error {ctx} [DS "can't infer lambda"] + pure $ (Lam fc nm tm', VPi fc nm icit quant a $ MkClosure ctx.env !(quote (S ctx.lvl) b)) infer ctx (RImplicit fc) = do ty <- freshMeta ctx fc (VU emptyFC) Normal diff --git a/src/Lib/Eval.idr b/src/Lib/Eval.idr index 28b3be1..871a7f0 100644 --- a/src/Lib/Eval.idr +++ b/src/Lib/Eval.idr @@ -150,7 +150,7 @@ eval env mode (Meta fc i) = (Unsolved _ k xs _ _ _) => pure $ VMeta fc i [<] (Solved _ k t) => pure $ t eval env mode (Lam fc x t) = pure $ VLam fc x (MkClosure env t) -eval env mode (Pi fc x icit a b) = pure $ VPi fc x icit !(eval env mode a) (MkClosure env b) +eval env mode (Pi fc x icit rig a b) = pure $ VPi fc x icit rig !(eval env mode a) (MkClosure env b) eval env mode (Let fc nm t u) = pure $ VLet fc nm !(eval env mode t) !(eval (VVar fc (length env) [<] :: env) mode u) eval env mode (LetRec fc nm t u) = pure $ VLetRec fc nm !(eval (VVar fc (length env) [<] :: env) mode t) !(eval (VVar fc (length env) [<] :: env) mode u) -- Here, we assume env has everything. We push levels onto it during type checking. @@ -186,7 +186,7 @@ quote l (VMeta fc i sp) = (Unsolved _ k xs _ _ _) => quoteSp l (Meta fc i) sp (Solved _ k t) => quote l !(vappSpine t sp) quote l (VLam fc x t) = pure $ Lam fc x !(quote (S l) !(t $$ VVar emptyFC l [<])) -quote l (VPi fc x icit a b) = pure $ Pi fc x icit !(quote l a) !(quote (S l) !(b $$ VVar emptyFC l [<])) +quote l (VPi fc x icit rig a b) = pure $ Pi fc x icit rig !(quote l a) !(quote (S l) !(b $$ VVar emptyFC l [<])) quote l (VLet fc nm t u) = pure $ Let fc nm !(quote l t) !(quote (S l) u) quote l (VLetRec fc nm t u) = pure $ LetRec fc nm !(quote (S l) t) !(quote (S l) u) quote l (VU fc) = pure (U fc) @@ -260,7 +260,7 @@ zonk top l env t = case t of (Meta fc k) => zonkApp top l env t [] (Lam fc nm u) => Lam fc nm <$> (zonk top (S l) (VVar fc l [<] :: env) u) (App fc t u) => zonkApp top l env t [!(zonk top l env u)] - (Pi fc nm icit a b) => Pi fc nm icit <$> zonk top l env a <*> zonkBind top l env b + (Pi fc nm icit rig a b) => Pi fc nm icit rig <$> zonk top l env a <*> zonkBind top l env b (Let fc nm t u) => Let fc nm <$> zonk top l env t <*> zonkBind top l env u (LetRec fc nm t u) => LetRec fc nm <$> zonkBind top l env t <*> zonkBind top l env u (Case fc sc alts) => Case fc <$> zonk top l env sc <*> traverse (zonkAlt top l env) alts diff --git a/src/Lib/Parser.idr b/src/Lib/Parser.idr index b4eca45..66d5035 100644 --- a/src/Lib/Parser.idr +++ b/src/Lib/Parser.idr @@ -396,11 +396,12 @@ parsePFunc = do fc <- getPos keyword "pfunc" nm <- ident + uses <- optional (keyword "uses" >> parens (many $ uident <|> ident <|> token MixFix)) keyword ":" ty <- typeExpr keyword ":=" src <- cast <$> token JSLit - pure $ PFunc fc nm ty src + pure $ PFunc fc nm (fromMaybe [] uses) ty src export parseData : Parser Decl diff --git a/src/Lib/ProcessDecl.idr b/src/Lib/ProcessDecl.idr index 48feff6..dab1dc8 100644 --- a/src/Lib/ProcessDecl.idr +++ b/src/Lib/ProcessDecl.idr @@ -18,8 +18,8 @@ import Lib.Util -- Later we will build a table of codomain type, and maybe make the user tag the candidates -- like Idris does with %hint isCandidate : Val -> Tm -> Bool -isCandidate ty (Pi fc nm Explicit t u) = False -isCandidate ty (Pi fc nm icit t u) = isCandidate ty u +isCandidate ty (Pi fc nm Explicit rig t u) = False +isCandidate ty (Pi fc nm icit rig t u) = isCandidate ty u isCandidate (VRef _ nm _ _) (Ref fc nm' def) = nm == nm' isCandidate ty (App fc t u) = isCandidate ty t isCandidate _ _ = False @@ -73,8 +73,9 @@ contextMatches ctx ty = go (zip ctx.env (toList ctx.types)) writeIORef top.metas mc go xs) +-- FIXME - decide if we want to count Zero here getArity : Tm -> Nat -getArity (Pi x str icit t u) = S (getArity u) +getArity (Pi x str icit rig t u) = S (getArity u) -- Ref or App (of type constructor) are valid getArity _ = Z @@ -181,12 +182,16 @@ processDecl (PType fc nm ty) = do ty' <- check (mkCtx fc) (maybe (RU fc) id ty) (VU fc) setDef nm fc ty' PrimTCon -processDecl (PFunc fc nm ty src) = do +processDecl (PFunc fc nm uses ty src) = do top <- get ty <- check (mkCtx fc) ty (VU fc) ty' <- nf [] ty putStrLn "pfunc \{nm} : \{pprint [] ty'} := \{show src}" - setDef nm fc ty' (PrimFn src) + -- TODO wire through fc? + for_ uses $ \ name => case lookup name top of + Nothing => error fc "\{name} not in scope" + _ => pure () + setDef nm fc ty' (PrimFn src uses) processDecl (Def fc nm clauses) = do putStrLn "-----" @@ -274,7 +279,7 @@ processDecl (Class classFC nm tele decls) = do getSigs (_:: xs) = getSigs xs impTele : Telescope - impTele = map (\(BI fc nm _ quant, ty) => (BI fc nm Implicit quant, ty)) tele + impTele = map (\(BI fc nm _ quant, ty) => (BI fc nm Implicit Zero, ty)) tele teleToPi : Telescope -> Raw -> Raw teleToPi [] end = end @@ -309,7 +314,7 @@ processDecl (Instance instfc ty decls) = do | _ => error tyFC "\{tconName} has multiple constructors \{show cons}" let (Just (MkEntry _ dcty (DCon _ _))) = lookup con top | _ => error tyFC "can't find constructor \{show con}" - vdcty@(VPi _ nm icit a b) <- eval [] CBN dcty + vdcty@(VPi _ nm icit rig a b) <- eval [] CBN dcty | x => error (getFC x) "dcty not Pi" debug "dcty \{pprint [] dcty}" let (_,args) = funArgs codomain @@ -322,8 +327,8 @@ processDecl (Instance instfc ty decls) = do conTele <- getFields !(apply vdcty args') env [] -- declare individual functions, collect their defs defs <- for conTele $ \case - (MkBind fc nm Explicit ty) => do - let ty' = foldr (\(MkBind fc nm' icit ty'), acc => Pi fc nm' icit ty' acc) ty tele + (MkBind fc nm Explicit rig ty) => do + let ty' = foldr (\(MkBind fc nm' icit rig ty'), acc => Pi fc nm' icit rig ty' acc) ty tele let nm' = "\{instname},\{nm}" -- we're working with a Tm, so we define directly instead of processDecl setDef nm' fc ty' Axiom @@ -353,10 +358,10 @@ processDecl (Instance instfc ty decls) = do -- try to extract types of individual fields from the typeclass dcon -- We're assuming they don't depend on each other. getFields : Val -> Env -> List Binder -> M (List Binder) - getFields tm@(VPi fc nm Explicit ty sc) env bnds = do - bnd <- MkBind fc nm Explicit <$> quote (length env) ty + getFields tm@(VPi fc nm Explicit rig ty sc) env bnds = do + bnd <- MkBind fc nm Explicit rig <$> quote (length env) ty getFields !(sc $$ VVar fc (length env) [<]) env (bnd :: bnds) - getFields tm@(VPi fc nm _ ty sc) env bnds = getFields !(sc $$ VVar fc (length env) [<]) env bnds + getFields tm@(VPi fc nm _ rig ty sc) env bnds = getFields !(sc $$ VVar fc (length env) [<]) env bnds getFields tm xs bnds = pure $ reverse bnds tenv : Nat -> Env @@ -364,13 +369,13 @@ processDecl (Instance instfc ty decls) = do tenv (S k) = (VVar emptyFC k [<] :: tenv k) mkRHS : String -> List Binder -> Raw -> Raw - mkRHS instName (MkBind fc nm Explicit ty :: bs) tm = mkRHS instName bs (RApp fc tm (RVar fc "\{instName},\{nm}") Explicit) + mkRHS instName (MkBind fc nm Explicit rig ty :: bs) tm = mkRHS instName bs (RApp fc tm (RVar fc "\{instName},\{nm}") Explicit) mkRHS instName (b :: bs) tm = mkRHS instName bs tm mkRHS instName [] tm = tm apply : Val -> List Val -> M Val apply x [] = pure x - apply (VPi fc nm icit a b) (x :: xs) = apply !(b $$ x) xs + apply (VPi fc nm icit rig a b) (x :: xs) = apply !(b $$ x) xs apply x (y :: xs) = error instfc "expected pi type \{show x}" processDecl (Data fc nm ty cons) = do @@ -395,7 +400,7 @@ processDecl (Data fc nm ty cons) = do -- We know it's in U because it's part of a checked Pi type let (codomain, tele) = splitTele dty -- for printing - let tnames = reverse $ map (\(MkBind _ nm _ _) => nm) tele + let tnames = reverse $ map (\(MkBind _ nm _ _ _) => nm) tele let (Ref _ hn _, args) := funArgs codomain | (tm, _) => error (getFC tm) "expected \{nm} got \{pprint tnames tm}" when (hn /= nm) $ @@ -411,5 +416,5 @@ processDecl (Data fc nm ty cons) = do where checkDeclType : Tm -> M () checkDeclType (U _) = pure () - checkDeclType (Pi _ str icit t u) = checkDeclType u + checkDeclType (Pi _ str icit rig t u) = checkDeclType u checkDeclType _ = error fc "data type doesn't return U" diff --git a/src/Lib/Syntax.idr b/src/Lib/Syntax.idr index 56981fe..10900b2 100644 --- a/src/Lib/Syntax.idr +++ b/src/Lib/Syntax.idr @@ -120,7 +120,7 @@ data Decl | DCheck FC Raw Raw | Data FC Name Raw (List Decl) | PType FC Name (Maybe Raw) - | PFunc FC Name Raw String + | PFunc FC Name (List String) Raw String | PMixFix FC (List Name) Nat Fixity | Class FC Name Telescope (List Decl) | Instance FC Raw (List Decl) @@ -132,7 +132,7 @@ HasFC Decl where getFC (DCheck x tm tm1) = x getFC (Data x str tm xs) = x getFC (PType x str mtm) = x - getFC (PFunc x str tm str1) = x + getFC (PFunc x str _ tm str1) = x getFC (PMixFix x strs k y) = x getFC (Class x str xs ys) = x getFC (Instance x tm xs) = x @@ -176,7 +176,7 @@ Show Decl where show (Data _ str xs ys) = foo ["Data", show str, show xs, show ys] show (DCheck _ x y) = foo ["DCheck", show x, show y] show (PType _ name ty) = foo ["PType", name, show ty] - show (PFunc _ nm ty src) = foo ["PFunc", nm, show ty, show src] + show (PFunc _ nm uses ty src) = foo ["PFunc", nm, show uses, show ty, show src] show (PMixFix _ nms prec fix) = foo ["PMixFix", show nms, show prec, show fix] show (Class _ nm tele decls) = foo ["Class", nm, "...", show $ map show decls] show (Instance _ nm decls) = foo ["Instance", show nm, show $ map show decls] @@ -278,7 +278,8 @@ Pretty Decl where pretty (Data _ nm x xs) = text "data" <+> text nm <+> text ":" <+> pretty x <+> (nest 2 $ text "where" stack (map pretty xs)) pretty (DCheck _ x y) = text "#check" <+> pretty x <+> ":" <+> pretty y pretty (PType _ nm ty) = text "ptype" <+> text nm <+> (maybe empty (\ty => ":" <+> pretty ty) ty) - pretty (PFunc _ nm ty src) = "pfunc" <+> text nm <+> ":" <+> nest 2 (pretty ty <+> ":=" <+/> text (show src)) + pretty (PFunc _ nm [] ty src) = "pfunc" <+> text nm <+> ":" <+> nest 2 (pretty ty <+> ":=" <+/> text (show src)) + pretty (PFunc _ nm uses ty src) = "pfunc" <+> text nm <+> "uses" <+> spread (map text uses) <+> ":" <+> nest 2 (pretty ty <+> ":=" <+/> text (show src)) pretty (PMixFix _ names prec fix) = text (show fix) <+> text (show prec) <+> spread (map text names) pretty (Class _ _ _ _) = text "TODO pretty Class" pretty (Instance _ _ _) = text "TODO pretty Instance" diff --git a/src/Lib/Types.idr b/src/Lib/Types.idr index 58fc09a..e58ef85 100644 --- a/src/Lib/Types.idr +++ b/src/Lib/Types.idr @@ -50,9 +50,15 @@ data Quant = Zero | Many public export Show Quant where - show Zero = "0" + show Zero = "0 " show Many = "" +Eq Quant where + Zero == Zero = True + Many == Many = True + _ == _ = False + +-- We could make this polymorphic and use for environment... public export data BindInfo : Type where BI : (fc : FC) -> (name : Name) -> (icit : Icit) -> (quant : Quant) -> BindInfo @@ -114,7 +120,7 @@ data Tm : Type where Lam : FC -> Name -> Tm -> Tm App : FC -> Tm -> Tm -> Tm U : FC -> Tm - Pi : FC -> Name -> Icit -> Tm -> Tm -> Tm + Pi : FC -> Name -> Icit -> Quant -> Tm -> Tm -> Tm Case : FC -> Tm -> List CaseAlt -> Tm -- need type? Let : FC -> Name -> Tm -> Tm -> Tm @@ -132,7 +138,7 @@ HasFC Tm where getFC (Lam fc str t) = fc getFC (App fc t u) = fc getFC (U fc) = fc - getFC (Pi fc str icit t u) = fc + getFC (Pi fc str icit quant t u) = fc getFC (Case fc t xs) = fc getFC (Lit fc _) = fc getFC (Let fc _ _ _) = fc @@ -156,9 +162,9 @@ Show Tm where 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})" - show (Pi _ str Auto t u) = "(Pi {{\{str} : \{show t}}} => \{show u})" + show (Pi _ str Explicit rig t u) = "(Pi (\{show rig} \{str} : \{show t}) => \{show u})" + show (Pi _ str Implicit rig t u) = "(Pi {\{show rig} \{str} : \{show t}} => \{show u})" + show (Pi _ str Auto rig t u) = "(Pi {{\{show rig} \{str} : \{show t}}} => \{show u})" show (Case _ sc alts) = "(Case \{show sc} \{show alts})" show (Let _ nm t u) = "(Let \{nm} \{show t} \{show u})" show (LetRec _ nm t u) = "(LetRec \{nm} \{show t} \{show u})" @@ -186,7 +192,7 @@ Eq (Tm) where (Lam _ n t) == Lam _ n' t' = t == t' (App _ t u) == App _ t' u' = t == t' && u == u' (U _) == (U _) = True - (Pi _ n icit t u) == (Pi _ n' icit' t' u') = icit == icit' && t == t' && u == u' + (Pi _ n icit rig t u) == (Pi _ n' icit' rig' t' u') = icit == icit' && rig == rig' && t == t' && u == u' _ == _ = False @@ -223,14 +229,14 @@ pprint names tm = go 0 names tm go p names (Lam _ nm t) = parens 0 p $ nest 2 $ text "\\ \{nm} =>" <+/> go 0 (nm :: names) t go p names (App _ t u) = parens 0 p $ go 0 names t <+> go 1 names u go p names (U _) = "U" - go p names (Pi _ nm Auto t u) = parens 0 p $ - text "{{" <+> text nm <+> ":" <+> go 0 names t <+> "}}" <+> "->" <+> go 0 (nm :: names) u - go p names (Pi _ nm Implicit t u) = parens 0 p $ - text "{" <+> text nm <+> ":" <+> go 0 names t <+> "}" <+> "->" <+> go 0 (nm :: names) u - go p names (Pi _ "_" Explicit t u) = + go p names (Pi _ nm Auto rig t u) = parens 0 p $ + text "{{" ++ text (show rig) <+> text nm <+> ":" <+> go 0 names t <+> "}}" <+> "->" <+> go 0 (nm :: names) u + go p names (Pi _ nm Implicit rig t u) = parens 0 p $ + text "{" ++ text (show rig) <+> text nm <+> ":" <+> go 0 names t <+> "}" <+> "->" <+> go 0 (nm :: names) u + go p names (Pi _ "_" Explicit Many t u) = parens 0 p $ go 1 names t <+> "->" <+> go 0 ("_" :: names) u - go p names (Pi _ nm Explicit t u) = parens 0 p $ - text "(" ++ text nm <+> ":" <+> go 0 names t ++ ")" <+> "->" <+> go 0 (nm :: names) u + go p names (Pi _ nm Explicit rig t u) = parens 0 p $ + text "(" ++ text (show rig) <+> text nm <+> ":" <+> go 0 names t ++ ")" <+> "->" <+> go 0 (nm :: names) u -- FIXME - probably way wrong on the names here. There is implicit binding going on go p names (Case _ sc alts) = parens 0 p $ text "case" <+> go 0 names sc <+> text "of" ++ (nest 2 (line ++ stack (map (goAlt 0 names) alts))) go p names (Lit _ lit) = text (show lit) @@ -266,7 +272,7 @@ data Val : Type where -- we'll need to look this up in ctx with IO VMeta : FC -> (ix : Nat) -> (sp : SnocList Val) -> Val VLam : FC -> Name -> Closure -> Val - VPi : FC -> Name -> Icit -> (a : Lazy Val) -> (b : Closure) -> Val + VPi : FC -> Name -> Icit -> Quant -> (a : Lazy Val) -> (b : Closure) -> Val VLet : FC -> Name -> Val -> Val -> Val VLetRec : FC -> Name -> Val -> Val -> Val VU : FC -> Val @@ -279,7 +285,7 @@ getValFC (VRef fc _ _ _) = fc getValFC (VCase fc _ _) = fc getValFC (VMeta fc _ _) = fc getValFC (VLam fc _ _) = fc -getValFC (VPi fc _ _ a b) = fc +getValFC (VPi fc _ _ _ a b) = fc getValFC (VU fc) = fc getValFC (VLit fc _) = fc getValFC (VLet fc _ _ _) = fc @@ -299,8 +305,8 @@ Show Val where show (VRef _ nm _ sp) = "(\{nm} \{unwords $ map show (sp <>> [])})" show (VMeta _ ix sp) = "(%meta \{show ix} [\{show $ length sp} sp])" show (VLam _ str x) = "(%lam \{str} \{show x})" - show (VPi fc str Implicit x y) = "(%pi {\{str} : \{show x}}. \{show y})" - show (VPi fc str Explicit x y) = "(%pi (\{str} : \{show x}). \{show y})" + show (VPi fc str Implicit rig x y) = "(%pi {\{show rig} \{str} : \{show x}}. \{show y})" + show (VPi fc str Explicit rig x y) = "(%pi (\{show rig} \{str} : \{show x}). \{show y})" show (VCase fc sc alts) = "(%case \{show sc} ...)" show (VU _) = "U" show (VLit _ lit) = show lit @@ -375,7 +381,8 @@ record MetaContext where public export -data Def = Axiom | TCon (List String) | DCon Nat String | Fn Tm | PrimTCon | PrimFn String +data Def = Axiom | TCon (List String) | DCon Nat String | Fn Tm | PrimTCon + | PrimFn String (List String) public export covering @@ -385,7 +392,7 @@ Show Def where show (DCon k tyname) = "DCon \{show k} \{show tyname}" show (Fn t) = "Fn \{show t}" show (PrimTCon) = "PrimTCon" - show (PrimFn src) = "PrimFn \{show src}" + show (PrimFn src uses) = "PrimFn \{show src} \{show uses}" ||| entry in the top level context public export diff --git a/src/Lib/Util.idr b/src/Lib/Util.idr index 7f8bf45..e0fc75f 100644 --- a/src/Lib/Util.idr +++ b/src/Lib/Util.idr @@ -13,12 +13,12 @@ funArgs tm = go tm [] public export data Binder : Type where - MkBind : FC -> String -> Icit -> Tm -> Binder + MkBind : FC -> String -> Icit -> Quant -> Tm -> Binder -- I don't have a show for terms without a name list export Show Binder where - show (MkBind _ nm icit t) = "[\{nm} \{show icit} : ...]" + show (MkBind _ nm icit quant t) = "[\{show quant}\{nm} \{show icit} : ...]" data Foo : Type -> Type where MkFoo : Nat -> Foo a @@ -28,5 +28,5 @@ splitTele : Tm -> (Tm, List Binder) splitTele = go [] where go : List Binder -> Tm -> (Tm, List Binder) - go ts (Pi fc nm icit t u) = go (MkBind fc nm icit t :: ts) u + go ts (Pi fc nm icit quant t u) = go (MkBind fc nm icit quant t :: ts) u go ts tm = (tm, reverse ts)