From 94ffbdb3a2288d06a071d58e50a35c597b13d968 Mon Sep 17 00:00:00 2001 From: Steve Dunham Date: Sat, 28 Sep 2024 11:14:44 -0700 Subject: [PATCH] fixes to casetree --- TODO.md | 6 +++- src/Lib/Check.idr | 82 +++++++++++++++++++++++++++++------------- src/Lib/TT.idr | 5 ++- tests/black/case3.newt | 41 +++++++++++++++++++-- 4 files changed, 105 insertions(+), 29 deletions(-) diff --git a/TODO.md b/TODO.md index a0ba410..67fe578 100644 --- a/TODO.md +++ b/TODO.md @@ -3,8 +3,12 @@ I may be done with `U` - I keep typing `Type`. +TT.idr should be Eval.idr, utilities up front belong elsewhere + +- [ ] consider making meta application implicit in term, so its more readable when printed + - Currently we have explicit `App` surrounding `Meta` when inserting metas. Some people + leave that implicit for efficiency. I think it would also make printing more readable. - [ ] eval for case (see order.newt) -- [ ] fix `ite.newt` - [ ] dynamic pattern unification (add test case first) - [x] switch from commit/mustWork to checking progress - [x] type constructors are no longer generated? And seem to have 0 arity. diff --git a/src/Lib/Check.idr b/src/Lib/Check.idr index a1377c4..577e488 100644 --- a/src/Lib/Check.idr +++ b/src/Lib/Check.idr @@ -18,6 +18,18 @@ import Lib.Syntax -- dom gamma ren data Pden = PR Nat Nat (List Nat) +pprint : Context -> Val -> M String +pprint ctx v = pure $ pprint (names ctx) !(quote (length ctx.env) v) + +export +lookupName : Context -> String -> Maybe (Tm, Val) +lookupName ctx name = go 0 ctx.types + where + go : Nat -> Vect n (String, Val) -> Maybe (Tm, Val) + go ix [] = Nothing + -- FIXME - we should stuff a Binder of some sort into "types" + go ix ((nm, ty) :: xs) = if nm == name then Just (Bnd emptyFC ix, ty) else go (S ix) xs + -- IORef for metas needs IO export forceMeta : Val -> M Val @@ -167,9 +179,9 @@ parameters (ctx: Context) (VMeta fc k sp, VMeta fc' k' sp' ) => if k == k' then unifySpine l (k == k') sp sp' -- TODO, might want to try the other way, too. - else trySolve l k sp (VMeta fc' k' sp') >> pure neutral - (t, VMeta fc' i' sp') => trySolve l i' sp' t >> pure neutral - (VMeta fc i sp, t' ) => trySolve l i sp t' >> pure neutral + else solve l k sp (VMeta fc' k' sp') >> pure neutral + (t, VMeta fc' i' sp') => solve l i' sp' t >> pure neutral + (VMeta fc i sp, t' ) => solve l i sp t' >> pure neutral (VPi fc _ _ a b, VPi fc' _ _ a' b') => [| unify l a a' <+> unify (S l) !(b $$ VVar emptyFC l [<]) !(b' $$ VVar emptyFC l [<]) |] (VVar fc k sp, (VVar fc' k' sp') ) => if k == k' then unifySpine l (k == k') sp sp' @@ -225,7 +237,16 @@ unifyCatch fc ctx ty' ty = do throwError (E fc msg) case res of MkResult [] => pure () - cs => error fc "Unification yields constraints \{show cs.constraints}" + cs => do + -- probably want a unification mode that throws instead of returning constraints + -- TODO need a normalizeHoles, maybe on quote? + debug "fail with constraints \{show cs.constraints}" + a <- quote ctx.lvl ty' + b <- quote ctx.lvl ty + let names = toList $ map fst ctx.types + let msg = "\n failed to unify \{pprint names a}\n with \{pprint names b}" + throwError (E fc msg) + -- error fc "Unification yields constraints \{show cs.constraints}" insert : (ctx : Context) -> Tm -> Val -> M (Tm, Val) insert ctx tm ty = do @@ -300,22 +321,22 @@ findSplit (_ :: xs) = findSplit xs -- TODO, we may need to filter these against the type to rule out -- impossible cases -getConstructors : Context -> Val -> M (List (String, Nat, Tm)) -getConstructors ctx (VRef fc nm _ _) = do +getConstructors : Context -> FC -> Val -> M (List (String, Nat, Tm)) +getConstructors ctx scfc (VRef fc nm _ _) = do names <- lookupTCon nm traverse lookupDCon names where lookupTCon : String -> M (List String) lookupTCon str = case lookup nm !get of (Just (MkEntry name type (TCon names))) => pure names - _ => error fc "Not a type constructor \{nm}" + _ => error scfc "Not a type constructor \{nm}" lookupDCon : String -> M (String, Nat, Tm) lookupDCon nm = do case lookup nm !get of (Just (MkEntry name type (DCon k str))) => pure (name, k, type) Just _ => error fc "Internal Error: \{nm} is not a DCon" Nothing => error fc "Internal Error: DCon \{nm} not found" -getConstructors ctx tm = error (getValFC tm) "Not a type constructor \{show tm}" +getConstructors ctx scfc tm = error scfc "Can't split on type: \{!(pprint ctx tm)}" -- Extend environment with fresh variables from a pi-type -- the pi-type here is the telescope of a constructor @@ -346,9 +367,15 @@ updateContext ctx ((k, val) :: cs) = let ix = (length ctx.env `minus` k) `minus` replaceV 0 x (y :: xs) = x :: xs replaceV (S k) x (y :: xs) = y :: replaceV k x xs +forcedName : Context -> String -> Maybe Name +forcedName ctx nm = case lookupName ctx nm of + Just (Bnd fc ix, ty) => case getAt ix ctx.env of + (Just (VRef x nm y sp)) => -- TODO verify is constructor? + Just nm + _ => Nothing + _ => Nothing + -- ok, so this is a single constructor, CaseAlt --- since we've gotten here, we assume it's possible and we better have at least --- one valid clause -- return Nothing if dcon doesn't unify with scrut buildCase : Context -> Problem -> String -> Val -> (String, Nat, Tm) -> M (Maybe CaseAlt) buildCase ctx prob scnm scty (dcName, arity, ty) = do @@ -365,10 +392,17 @@ buildCase ctx prob scnm scty (dcName, arity, ty) = do -- We get unification constraints from matching the data constructors -- codomain with the scrutinee type - debug "unify dcon dom with scrut" + debug "unify dcon dom with scrut\n \{show ty'}\n \{show scty}" Just res <- catchError {e = Error} (Just <$> unify ctx' (length ctx'.env) ty' scty) (\_ => pure Nothing) | _ => pure Nothing + -- if the value is already constrained to a different constructor, return Nothing + debug "scrut \{scnm} constrained to \{show $ forcedName ctx scnm}" + let True = (case forcedName ctx scnm of + Just nm => nm == scnm + _ => True) + | _ => pure Nothing + -- Additionally, we constrain the scrutinee's variable to be -- dcon applied to args let Just x = findIndex ((==scnm) . fst) ctx'.types @@ -477,15 +511,6 @@ makeClause top (lhs, rhs) = do pats <- traverse (mkPat top) args pure $ MkClause (getFC lhs) [] pats rhs - -lookupName : Context -> String -> Maybe (Tm, Val) -lookupName ctx name = go 0 ctx.types - where - go : Nat -> Vect n (String, Val) -> Maybe (Tm, Val) - go ix [] = Nothing - -- FIXME - we should stuff a Binder of some sort into "types" - go ix ((nm, ty) :: xs) = if nm == name then Just (Bnd emptyFC ix, ty) else go (S ix) xs - checkDone : Context -> List (String, Pattern) -> Raw -> Val -> M Tm checkDone ctx [] body ty = do debug "DONE-> check body \{show body} at \{show ty}" @@ -529,11 +554,11 @@ buildTree ctx prob@(MkProb ((MkClause fc constraints [] expr) :: cs) ty) = do let Just (scnm, pat) := findSplit constraints | _ => checkDone ctx constraints expr ty - debug "SPLIT on \{scnm} because \{show pat}" + debug "SPLIT on \{scnm} because \{show pat} \{show $ getFC pat}" let Just (sctm, scty) := lookupName ctx scnm | _ => error fc "Internal Error: can't find \{scnm} in environment" - cons <- getConstructors ctx scty + cons <- getConstructors ctx (getFC pat) scty alts <- traverse (buildCase ctx prob scnm scty) cons -- TODO check for empty somewhere? @@ -561,7 +586,7 @@ check ctx tm ty = case (tm, !(forceType ty)) of -- it's compared against the first part of Constraint. We could switch -- to a level and only let if the scrutinee is not a var. let ctx' = extend ctx scnm scty - cons <- getConstructors ctx' scty + cons <- getConstructors ctx' fc scty alts <- traverse (buildCase ctx' (MkProb clauses ty) scnm scty) cons pure $ Let fc scnm sc $ Case fc (Bnd fc 0) (catMaybes alts) @@ -605,10 +630,19 @@ check ctx tm ty = case (tm, !(forceType ty)) of debug "XXX edge add implicit lambda to \{show tm}" let var = VVar fc (length ctx.env) [<] ty' <- b $$ var - debug "XXX ty' is \{!(prvalCtx {ctx=(extend ctx nm' a)} ty')}" + 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 + (RLet fc nm ty v sc, rty) => do + ty' <- check ctx ty (VU emptyFC) + vty <- eval ctx.env CBN ty' + v' <- check ctx v vty + vv <- eval ctx.env CBN v' + let ctx' = define ctx nm vv vty + sc' <- check ctx' sc rty + pure $ Let fc nm v' sc' + (tm,ty) => do -- We need to insert if tm is not an Implicit Lam -- assuming all of the implicit ty have been handled above diff --git a/src/Lib/TT.idr b/src/Lib/TT.idr index a12a781..b2e773a 100644 --- a/src/Lib/TT.idr +++ b/src/Lib/TT.idr @@ -194,7 +194,10 @@ quoteSp lvl t (xs :< x) = quote l (VVar fc k sp) = if k < l then quoteSp l (Bnd emptyFC ((l `minus` k) `minus` 1)) sp -- level to index else ?borken -quote l (VMeta fc i sp) = quoteSp l (Meta fc i) sp +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 (VPi fc x icit a b) = pure $ Pi fc x icit !(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 $$ VVar emptyFC l [<])) diff --git a/tests/black/case3.newt b/tests/black/case3.newt index 8e1f721..913f473 100644 --- a/tests/black/case3.newt +++ b/tests/black/case3.newt @@ -13,6 +13,41 @@ infixr 5 _::_ head : {a : U} {k : Nat} -> Vect (S k) a -> a head (x :: xs) = x -zapp : {s t: U} {k : Nat} -> Vect k (s -> t) -> Vect k s -> Vect k t -zapp (f :: fs) (t :: ts) = f t :: zapp fs ts -zapp Nil Nil = Nil +-- These came from a Conor McBride lecture where they use SHE + +vapp : {s t: U} {k : Nat} -> Vect k (s -> t) -> Vect k s -> Vect k t +vapp (f :: fs) (t :: ts) = f t :: vapp fs ts +vapp Nil Nil = Nil + +vec : { a : U } -> (n : Nat) -> a -> Vect n a +vec Z x = Nil +vec (S k) x = x :: vec k x + +-- And then typeclass, which I don't have yet. I'll add a few underlying functions + +fmap : {a b : U} {n : Nat} -> (a -> b) -> Vect n a -> Vect n b +fmap f Nil = Nil +fmap f (x :: xs) = (f x :: fmap f xs) + +pure : {a : U} {n : Nat} -> a -> Vect n a +pure {a} {n} = vec n + +_<*>_ : {s t: U} {k : Nat} -> Vect k (s -> t) -> Vect k s -> Vect k t +_<*>_ = vapp + +-- and idiom brackets (maybe someday) + +-- I'll add foldl + +foldl : {acc el : U} {n : Nat} -> (acc -> el -> acc) -> acc -> Vect n el -> acc +foldl f acc Nil = acc +foldl f acc (x :: xs) = foldl f (f acc x) xs + +zipWith : {a b c : U} {m : Nat} -> (a -> b -> c) -> Vect m a -> Vect m b -> Vect m c +zipWith f Nil Nil = Nil +zipWith f (x :: xs) (y :: ys) = f x y :: zipWith f xs ys + +transpose : {a : U} {m n : Nat} -> Vect m (Vect n a) -> Vect n (Vect m a) +-- TODO Doesn't work without the (forced) Z, investigate +transpose {a} {Z} {n} Nil = vec n Nil +transpose {a} {S k} {n} (x :: xs) = zipWith (_::_) x (transpose xs)