From 8d8078f9681947b3ff6df04c91077d15a5f83f68 Mon Sep 17 00:00:00 2001 From: Steve Dunham Date: Fri, 6 Dec 2024 20:34:40 -0800 Subject: [PATCH] improvements to erasure checking --- TODO.md | 5 +++-- aoc2023/Day3.newt | 2 -- aoc2024/SortedMap.newt | 4 ++-- newt-vscode/syntaxes/newt.tmLanguage.json | 2 +- newt/Prelude.newt | 11 +++++----- playground/samples/Tour.newt | 9 ++++---- playground/src/monarch.ts | 2 +- src/Lib/Compile.idr | 2 +- src/Lib/CompileExp.idr | 6 +++--- src/Lib/Elab.idr | 25 ++++++++++++----------- src/Lib/Erasure.idr | 20 ++++++++++-------- src/Lib/Eval.idr | 10 ++++----- src/Lib/Syntax.idr | 2 +- src/Lib/Types.idr | 22 ++++++++++---------- tests/black/TypeClass.newt | 4 ++-- 15 files changed, 63 insertions(+), 63 deletions(-) diff --git a/TODO.md b/TODO.md index 09fdf46..99aeba6 100644 --- a/TODO.md +++ b/TODO.md @@ -13,11 +13,12 @@ - [x] Put worker in iframe on safari - [ ] Warnings or errors for missing definitions - [ ] Warnings or errors for unused cases - - Important when misspelled constructors become pattern vars + - This is important when misspelled constructors become pattern vars - [ ] if we're staying with this version of auto, we might need to list candidates and why they're rejected. e.g. I had a bifunctor fail to solve because the right answer unblocked a Foo vs IO Foo mismatch - [ ] literals for double - [ ] add default failing case for constructor matching to catch errors -- [ ] Add icit to Lam (see `check` for details) +- [x] Add icit to Lam (see `check` for details) + - [ ] make change to `check` - [ ] add jump to definition magic to vscode extension - [ ] TCO? Probably needed in browser, since v8 doesn't do it. bun and JavaScriptCore do support it. - [x] deconstructing `let` (and do arrows) diff --git a/aoc2023/Day3.newt b/aoc2023/Day3.newt index f632338..652b04a 100644 --- a/aoc2023/Day3.newt +++ b/aoc2023/Day3.newt @@ -22,9 +22,7 @@ numbers arr = go arr Z where go : List Char → Nat → List Number go (c :: cs) start = if isDigit c - -- then let (front,back) = span isDigit (c :: cs) in ? then case span isDigit (c :: cs) of - -- NOW FC on app is now broken, need the fc of the left (front,back) => let stop = start + length front in MkNumber start stop (stringToInt $ pack front) :: go back stop else go cs (S start) diff --git a/aoc2024/SortedMap.newt b/aoc2024/SortedMap.newt index 88f7abf..e54b3f3 100644 --- a/aoc2024/SortedMap.newt +++ b/aoc2024/SortedMap.newt @@ -57,7 +57,7 @@ updateMap k v (MapOf map) = case insertT23 k v map of Left map' => MapOf map' Right (a, b, c) => MapOf (Node2 a b c) --- FIXME this doesn't work in a `where` because the erased args are un-erased +-- FIXME this doesn't work in a `where` because Letrec doesn't have the type toList' : ∀ k v h. T23 h k v → List (k × v) → List (k × v) toList' (Leaf k v) acc = (k, v) :: acc toList' (Node2 t1 k1 t2) acc = toList' t2 (toList' t1 acc) @@ -65,7 +65,7 @@ toList' (Node3 t1 k1 t2 k2 t3) acc = toList' t3 $ toList' t2 $ toList' t1 acc toList : ∀ k v. SortedMap k v → List (k × v) toList {k} {v} (MapOf smap) = reverse $ toList' smap Nil - -- FIXME erasure checking false positive - maybe because I'm not handling the top level args yet + -- FIXME erasure checking false positive (need type on foo in env when processing Letrec) -- where -- foo : ∀ k v h. T23 h k v → List (k × v) → List (k × v) -- foo (Leaf k v) acc = (k, v) :: acc diff --git a/newt-vscode/syntaxes/newt.tmLanguage.json b/newt-vscode/syntaxes/newt.tmLanguage.json index 05b9886..f0d17ee 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|uses|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/newt/Prelude.newt b/newt/Prelude.newt index c8ddff1..78ace48 100644 --- a/newt/Prelude.newt +++ b/newt/Prelude.newt @@ -98,13 +98,13 @@ class Monad (m : U → U) where pure : {0 a} → a → m a infixl 1 _>>=_ _>>_ -_>>=_ : {0 m} {{Monad m}} {0 a b} -> (m a) -> (a -> m b) -> m b +_>>=_ : ∀ m a b. {{Monad m}} -> (m a) -> (a -> m b) -> m b ma >>= amb = bind ma amb -_>>_ : {0 m} {{Monad m}} {0 a b} -> m a -> m b -> m b +_>>_ : ∀ m a b. {{Monad m}} -> m a -> m b -> m b ma >> mb = ma >>= (\ _ => mb) -join : ∀ m. {{Monad m}} {0 a} → m (m a) → m a +join : ∀ m a. {{Monad m}} → m (m a) → m a join mma = mma >>= id -- Equality @@ -295,7 +295,7 @@ pfunc replicate : Nat -> Char → String := `(n,c) => c.repeat(natToInt(n))` ptype World data IORes : U -> U where - MkIORes : {a : U} -> a -> World -> IORes a + MkIORes : ∀ a. a -> World -> IORes a IO : U -> U IO a = World -> IORes a @@ -303,8 +303,7 @@ IO a = World -> IORes a instance Monad IO where bind ma mab = \ w => case ma w of MkIORes a w => mab a w - pure a = \ w => MkIORes a w - + pure x = \ w => MkIORes x w bindList : ∀ a b. List a → (a → List b) → List b diff --git a/playground/samples/Tour.newt b/playground/samples/Tour.newt index 5880a76..15bf366 100644 --- a/playground/samples/Tour.newt +++ b/playground/samples/Tour.newt @@ -64,8 +64,8 @@ infixl 2 _≡_ -- Here is an equality, like Idris, everything goes to the right of the colon -- Implicits are denoted with braces `{ }` -- unlike idris, you have to declare all of your implicits -data _≡_ : {A : U} -> A -> A -> U where - Refl : {A : U} {a : A} -> a ≡ a +data _≡_ : {0 A : U} -> A -> A -> U where + Refl : {0 A : U} {0 a : A} -> a ≡ a -- And now the compiler can verify that 1 + 1 = 2 test : plus (S Z) (S Z) ≡ S (S Z) @@ -124,7 +124,6 @@ pfunc plusString : String -> String -> String := `(x,y) => x + y` -- We can make them Plus instances: - instance Add Int where _+_ = plusInt @@ -159,10 +158,10 @@ bind {m} {{MkMonad pure bind}} = bind -- we can declare multiple infix operators at once infixl 1 _>>=_ _>>_ -_>>=_ : {m} {{Monad m}} {a b} -> m a -> (a -> m b) -> m b +_>>=_ : ∀ m a b. {{Monad m}} -> m a -> (a -> m b) -> m b _>>=_ ma amb = bind ma amb -_>>_ : {m} {{Monad m}} {a b} -> m a -> m b -> m b +_>>_ : ∀ m a b. {{Monad m}} -> m a -> m b -> m b ma >> mb = ma >>= (λ _ => mb) -- Now we define list and show it is a monad. At the moment, I don't diff --git a/playground/src/monarch.ts b/playground/src/monarch.ts index 71bab5c..e5ece23 100644 --- a/playground/src/monarch.ts +++ b/playground/src/monarch.ts @@ -87,7 +87,7 @@ export let newtTokens: monaco.languages.IMonarchLanguage = { "infixr", "infix", ], - specialOps: ["=>", "->", ":", "=", ":="], + specialOps: ["=>", "->", ":", "=", ":=", "<-"], tokenizer: { root: [ [ diff --git a/src/Lib/Compile.idr b/src/Lib/Compile.idr index 2b57220..2958fb9 100644 --- a/src/Lib/Compile.idr +++ b/src/Lib/Compile.idr @@ -324,7 +324,7 @@ process (done,docs) nm = do 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 (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) diff --git a/src/Lib/CompileExp.idr b/src/Lib/CompileExp.idr index 60d580e..e5eda9c 100644 --- a/src/Lib/CompileExp.idr +++ b/src/Lib/CompileExp.idr @@ -47,7 +47,7 @@ data CExp : Type where ||| code gen. export lamArity : Tm -> Nat -lamArity (Lam _ _ t) = S (lamArity t) +lamArity (Lam _ _ _ _ t) = S (lamArity t) lamArity _ = Z export @@ -114,7 +114,7 @@ compileTerm t@(Ref fc nm _) = do 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 (Lam _ nm _ _ t) = pure $ CLam nm !(compileTerm t) compileTerm tm@(App _ _ _) with (funArgs tm) _ | (Meta _ k, args) = do -- this will be undefined, should only happen for use metas @@ -151,7 +151,7 @@ compileFun : Tm -> M CExp compileFun tm = go tm [<] where go : Tm -> SnocList String -> M CExp - go (Lam _ nm t) acc = go t (acc :< nm) + go (Lam _ nm _ _ t) acc = go t (acc :< nm) go tm [<] = compileTerm tm go tm args = pure $ CFun (args <>> []) !(compileTerm tm) diff --git a/src/Lib/Elab.idr b/src/Lib/Elab.idr index 9f8f1b0..ac81c38 100644 --- a/src/Lib/Elab.idr +++ b/src/Lib/Elab.idr @@ -172,7 +172,7 @@ rename meta ren lvl v = go ren lvl v _ => do 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 (VLam fc n icit rig t) = pure (Lam fc n icit rig !(go (lvl :: ren) (S lvl) !(t $$ VVar fc 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) go ren lvl (VErased fc) = pure (Erased fc) @@ -186,8 +186,9 @@ rename meta ren lvl v = go ren lvl v lams : Nat -> List String -> Tm -> Tm lams 0 _ tm = tm -lams (S k) [] tm = Lam emptyFC "arg_\{show k}" (lams k [] tm) -lams (S k) (x :: xs) tm = Lam emptyFC x (lams k xs tm) +-- REVIEW do we want a better FC, icity?, rig? +lams (S k) [] tm = Lam emptyFC "arg_\{show k}" Explicit Many (lams k [] tm) +lams (S k) (x :: xs) tm = Lam emptyFC x Explicit Many (lams k xs tm) export unify : Env -> UnifyMode -> Val -> Val -> M UnifyResult @@ -284,14 +285,14 @@ unify env mode t u = do [| unify env mode a a' <+> unify (fresh :: env) mode !(b $$ fresh) !(b' $$ fresh) |] -- we don't eta expand on LHS - unify' (VLam fc _ t) (VLam _ _ t') = do + unify' (VLam fc _ _ _ t) (VLam _ _ _ _ t') = do let fresh = VVar fc (length env) [<] unify (fresh :: env) mode !(t $$ fresh) !(t' $$ fresh) - unify' t (VLam fc' _ t') = do + unify' t (VLam fc' _ _ _ t') = do debug "ETA \{show t}" let fresh = VVar fc' (length env) [<] unify (fresh :: env) mode !(t `vapp` fresh) !(t' $$ fresh) - unify' (VLam fc _ t) t' = do + unify' (VLam fc _ _ _ t) t' = do debug "ETA' \{show t'}" let fresh = VVar fc (length env) [<] unify (fresh :: env) mode !(t $$ fresh) !(t' `vapp` fresh) @@ -853,7 +854,7 @@ buildTree ctx prob@(MkProb ((MkClause fc cons (x :: xs) expr) :: cs) (VPi _ str clauses <- traverse (introClause nm icit) prob.clauses -- REVIEW fc from a pat? vb <- b $$ VVar fc l [<] - Lam fc nm <$> buildTree ctx' ({ clauses := clauses, ty := vb } prob) + Lam fc nm icit rig <$> buildTree ctx' ({ clauses := clauses, ty := vb } prob) buildTree ctx prob@(MkProb ((MkClause fc cons pats@(x :: xs) expr) :: cs) ty) = error fc "Extra pattern variables \{show pats}" -- need to find some name we can split in (x :: xs) @@ -949,13 +950,13 @@ check ctx tm ty = case (tm, !(forceType ctx.env ty)) of let var = VVar fc (length ctx.env) [<] let ctx' = extend ctx nm a tm' <- check ctx' tm !(b $$ var) - pure $ Lam fc nm tm' + pure $ Lam fc nm icit rig tm' else if icit' /= Explicit then do let var = VVar fc (length ctx.env) [<] ty' <- b $$ var -- use nm' here if we want them automatically in scope sc <- check (extend ctx nm' a) t ty' - pure $ Lam fc nm' sc + pure $ Lam fc nm' icit rig sc else error fc "Icity issue checking \{show t} at \{show ty}" (t@(RLam _ (BI fc nm icit quant) tm), ty) => @@ -980,7 +981,7 @@ check ctx tm ty = case (tm, !(forceType ctx.env ty)) of ty' <- b $$ var debugM $ pure "XXX ty' is \{!(prvalCtx {ctx=(extend ctx nm' a)} ty')}" sc <- check (extend ctx nm' a) tm ty' - pure $ Lam (getFC tm) nm' sc + pure $ Lam (getFC tm) nm' Implicit rig sc (tm, ty@(VPi fc nm' Auto rig a b)) => do let names = toList $ map fst ctx.types @@ -989,7 +990,7 @@ check ctx tm ty = case (tm, !(forceType ctx.env ty)) of ty' <- b $$ var debugM $ pure "XXX ty' is \{!(prvalCtx {ctx=(extend ctx nm' a)} ty')}" sc <- check (extend ctx nm' a) tm ty' - pure $ Lam (getFC tm) nm' sc + pure $ Lam (getFC tm) nm' Auto rig sc (tm,ty) => do -- We need to insert if tm is not an Implicit Lam @@ -1080,7 +1081,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 quant a $ MkClosure ctx.env !(quote (S ctx.lvl) b)) + pure $ (Lam fc nm icit quant 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/Erasure.idr b/src/Lib/Erasure.idr index 2659e5f..22bfdcd 100644 --- a/src/Lib/Erasure.idr +++ b/src/Lib/Erasure.idr @@ -4,7 +4,7 @@ import Lib.Types import Data.SnocList import Lib.TopContext -EEnv = List (String, Quant) +EEnv = List (String, Quant, Maybe Tm) -- check App at type @@ -43,7 +43,7 @@ doAlt env (CaseCons name args t) = do CaseCons name args <$> erase env' t [] where piEnv : EEnv -> Tm -> List String -> EEnv - piEnv env (Pi fc nm icit rig t u) (arg :: args) = piEnv ((arg,rig) :: env) u args + piEnv env (Pi fc nm icit rig t u) (arg :: args) = piEnv ((arg, rig, Just t) :: env) u args piEnv env _ _ = env doAlt env (CaseLit lit t) = CaseLit lit <$> erase env t [] @@ -51,6 +51,7 @@ doAlt env (CaseLit lit t) = CaseLit lit <$> erase env t [] -- Check erasure and insert "Erased" value -- We have a solution for Erased values, so important thing here is checking. -- build stack, see what to do when we hit a non-app +-- This is a little fuzzy because we don't have all of the types. erase env t sp = case t of (App fc u v) => erase env u ((fc,v) :: sp) (Ref fc nm x) => do @@ -58,11 +59,12 @@ erase env t sp = case t of case lookup nm top of Nothing => eraseSpine env t sp Nothing (Just (MkEntry name type def)) => eraseSpine env t sp (Just type) - (Lam fc nm u) => Lam fc nm <$> erase ((nm, Many) :: env) u [] + (Lam fc nm icit rig u) => Lam fc nm icit rig <$> erase ((nm, rig, Nothing) :: env) u [] + (Lam fc nm icit rig u) => Lam fc nm icit rig <$> erase ((nm, rig, Nothing) :: env) u [] -- If we get here, we're looking at a runtime pi type (Pi fc nm icit rig u v) => do u' <- erase env u [] - v' <- erase ((nm, Many) :: env) v [] + v' <- erase ((nm, Many, Just u) :: env) v [] eraseSpine env (Pi fc nm icit rig u' v') sp Nothing -- leaving as-is for now, we don't know the quantity of the apps (Meta fc k) => pure t @@ -73,18 +75,18 @@ erase env t sp = case t of eraseSpine env (Case fc u' alts') sp Nothing (Let fc nm u v) => do u' <- erase env u [] - v' <- erase ((nm, Many) :: env) v [] + v' <- erase ((nm, Many, Nothing) :: env) v [] eraseSpine env (Let fc nm u' v') sp Nothing (LetRec fc nm u v) => do - u' <- erase ((nm, Many) :: env) u [] - v' <- erase ((nm, Many) :: env) v [] + u' <- erase ((nm, Many, Nothing) :: env) u [] + v' <- erase ((nm, Many, Nothing) :: env) v [] eraseSpine env (LetRec fc nm u' v') sp Nothing (Bnd fc k) => do case getAt k env of Nothing => error fc "bad index \{show k}" -- This is working, but empty FC - Just (nm, Zero) => error fc "used erased value \{show nm} (FIXME FC may be wrong here)" - Just (nm, Many) => eraseSpine env t sp Nothing + Just (nm, Zero, ty) => error fc "used erased value \{show nm} (FIXME FC may be wrong here)" + Just (nm, Many, ty) => eraseSpine env t sp ty (U fc) => eraseSpine env t sp Nothing (Lit fc lit) => eraseSpine env t sp Nothing Erased fc => eraseSpine env t sp Nothing diff --git a/src/Lib/Eval.idr b/src/Lib/Eval.idr index 4386d8a..a69d82e 100644 --- a/src/Lib/Eval.idr +++ b/src/Lib/Eval.idr @@ -34,7 +34,7 @@ infixl 8 $$ export vapp : Val -> Val -> M Val -vapp (VLam _ _ t) u = t $$ u +vapp (VLam _ _ _ _ t) u = t $$ u vapp (VVar fc k sp) u = pure $ VVar fc k (sp :< u) vapp (VRef fc nm def sp) u = pure $ VRef fc nm def (sp :< u) vapp (VMeta fc k sp) u = pure $ VMeta fc k (sp :< u) @@ -150,7 +150,7 @@ eval env mode (Meta fc i) = case !(lookupMeta i) of (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 (Lam fc x icit rig t) = pure $ VLam fc x icit rig (MkClosure env t) 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) @@ -186,7 +186,7 @@ quote l (VMeta fc i sp) = case !(lookupMeta i) of (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 (VLam fc x icit rig t) = pure $ Lam fc x icit rig !(quote (S l) !(t $$ 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) @@ -244,7 +244,7 @@ tweakFC fc (Bnd fc1 k) = Bnd fc k tweakFC fc (Ref fc1 nm x) = Ref fc nm x tweakFC fc (U fc1) = U fc tweakFC fc (Meta fc1 k) = Meta fc k -tweakFC fc (Lam fc1 nm t) = Lam fc nm t +tweakFC fc (Lam fc1 nm icit rig t) = Lam fc nm icit rig t tweakFC fc (App fc1 t u) = App fc t u tweakFC fc (Pi fc1 nm icit x t u) = Pi fc nm icit x t u tweakFC fc (Case fc1 t xs) = Case fc t xs @@ -278,7 +278,7 @@ zonkAlt top l env (CaseCons name args t) = CaseCons name args <$> go l env args 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) + (Lam fc nm icit rig u) => Lam fc nm icit rig <$> (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 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 diff --git a/src/Lib/Syntax.idr b/src/Lib/Syntax.idr index e67ac55..f10a5e9 100644 --- a/src/Lib/Syntax.idr +++ b/src/Lib/Syntax.idr @@ -255,7 +255,7 @@ Pretty Raw where asDoc p (RU _) = text "U" asDoc p (RPi _ (BI _ "_" Explicit Many) ty scope) = par p 1 $ asDoc p ty <+> text "->" <+/> asDoc p scope asDoc p (RPi _ (BI _ nm icit quant) ty scope) = - par p 1 $ wrap icit (text "_" <+> text ":" <+> asDoc p ty ) <+> text "->" <+/> asDoc 1 scope + par p 1 $ wrap icit (text (show quant ++ nm) <+> text ":" <+> asDoc p ty ) <+> text "->" <+/> asDoc 1 scope asDoc p (RLet _ x v ty scope) = par p 0 $ text "let" <+> text x <+> text ":" <+> asDoc p ty <+> text "=" <+> asDoc p v diff --git a/src/Lib/Types.idr b/src/Lib/Types.idr index 5b48205..8d95b81 100644 --- a/src/Lib/Types.idr +++ b/src/Lib/Types.idr @@ -117,7 +117,7 @@ data Tm : Type where Meta : FC -> Nat -> Tm -- kovacs optimization, I think we can App out meta instead -- InsMeta : Nat -> List BD -> Tm - Lam : FC -> Name -> Tm -> Tm + Lam : FC -> Name -> Icit -> Quant -> Tm -> Tm App : FC -> Tm -> Tm -> Tm U : FC -> Tm Pi : FC -> Name -> Icit -> Quant -> Tm -> Tm -> Tm @@ -136,7 +136,7 @@ HasFC Tm where getFC (Bnd fc k) = fc getFC (Ref fc str x) = fc getFC (Meta fc k) = fc - getFC (Lam fc str t) = fc + getFC (Lam fc str _ _ t) = fc getFC (App fc t u) = fc getFC (U fc) = fc getFC (Pi fc str icit quant t u) = fc @@ -159,14 +159,14 @@ public export covering Show Tm where show (Bnd _ k) = "(Bnd \{show k})" show (Ref _ str _) = "(Ref \{show str})" - show (Lam _ nm t) = "(\\ \{nm} => \{show t})" + show (Lam _ nm icit rig t) = "(\\ \{show rig}\{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 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 (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})" @@ -192,7 +192,7 @@ Eq (Tm) where -- (Local x) == (Local y) = x == y (Bnd _ x) == (Bnd _ y) = x == y (Ref _ x _) == Ref _ y _ = x == y - (Lam _ n t) == Lam _ n' t' = t == t' + (Lam _ n _ _ t) == Lam _ n' _ _ t' = t == t' (App _ t u) == App _ t' u' = t == t' && u == u' (U _) == (U _) = True (Pi _ n icit rig t u) == (Pi _ n' icit' rig' t' u') = icit == icit' && rig == rig' && t == t' && u == u' @@ -229,7 +229,7 @@ pprint names tm = go 0 names tm Just nm => text "\{nm}:\{show k}" go p names (Ref _ str mt) = text str go p names (Meta _ k) = text "?m:\{show k}" - go p names (Lam _ nm t) = parens 0 p $ nest 2 $ text "\\ \{nm} =>" <+/> go 0 (nm :: names) t + go p names (Lam _ nm icit quant t) = parens 0 p $ nest 2 $ text "\\ \{show quant}\{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 rig t u) = parens 0 p $ @@ -274,7 +274,7 @@ data Val : Type where VCase : FC -> (sc : Val) -> List CaseAlt -> Val -- we'll need to look this up in ctx with IO VMeta : FC -> (ix : Nat) -> (sp : SnocList Val) -> Val - VLam : FC -> Name -> Closure -> Val + VLam : FC -> Name -> Icit -> Quant -> 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 @@ -288,7 +288,7 @@ getValFC (VVar fc _ _) = fc getValFC (VRef fc _ _ _) = fc getValFC (VCase fc _ _) = fc getValFC (VMeta fc _ _) = fc -getValFC (VLam fc _ _) = fc +getValFC (VLam fc _ _ _ _) = fc getValFC (VPi fc _ _ _ a b) = fc getValFC (VU fc) = fc getValFC (VErased fc) = fc @@ -309,7 +309,7 @@ Show Val where show (VRef _ nm _ [<]) = nm 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 (VLam _ str icit quant x) = "(%lam \{show quant}\{str} \{show x})" 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} ...)" diff --git a/tests/black/TypeClass.newt b/tests/black/TypeClass.newt index 194fb2e..ec5335a 100644 --- a/tests/black/TypeClass.newt +++ b/tests/black/TypeClass.newt @@ -2,7 +2,7 @@ module TypeClass data Monad : (U -> U) -> U where MkMonad : { M : U -> U } -> - (bind : {A B : U} -> (M A) -> (A -> M B) -> M B) -> + (bind : ∀ A B. (M A) -> (A -> M B) -> M B) -> (pure : ∀ A. A -> M A) -> Monad M @@ -24,7 +24,7 @@ bindEither : ∀ A B C. (Either A B) -> (B -> Either A C) -> Either A C bindEither (Left a) amb = Left a bindEither (Right b) amb = amb b -EitherMonad : ∀ A. Monad (Either A) +EitherMonad : {A : U} -> Monad (Either A) EitherMonad = MkMonad {Either A} bindEither Right data Maybe : U -> U where