From eb281fa3b3fec3219a9d4cdbbac70c96b3708822 Mon Sep 17 00:00:00 2001 From: Steve Dunham Date: Fri, 27 Sep 2024 20:21:23 -0700 Subject: [PATCH] Drop incompatible constructors in case --- TODO.md | 3 +++ newt/order.newt | 29 +++++++++++++++++++++++++++ newt/typeclass.newt | 44 ++++++++++++++++++++++++++++++++++++++++- src/Lib/Check.idr | 33 ++++++++++++++++++++----------- src/Lib/Parser.idr | 2 +- src/Lib/ProcessDecl.idr | 9 ++++++--- tests/black/case3.newt | 18 +++++++++++++++++ 7 files changed, 121 insertions(+), 17 deletions(-) create mode 100644 newt/order.newt create mode 100644 tests/black/case3.newt diff --git a/TODO.md b/TODO.md index ecfe60d..a0ba410 100644 --- a/TODO.md +++ b/TODO.md @@ -3,6 +3,9 @@ I may be done with `U` - I keep typing `Type`. +- [ ] 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. - [x] raw let is not yet implemented (although define used by case tree building) diff --git a/newt/order.newt b/newt/order.newt new file mode 100644 index 0000000..2a5fc5f --- /dev/null +++ b/newt/order.newt @@ -0,0 +1,29 @@ +module Order + +data Nat : U where + Z : Nat + S : Nat -> Nat + +plus : Nat -> Nat -> Nat +plus Z y = y +plus (S x) y = S (plus x y) + +data Pair : U -> U -> U where + _,_ : {A B : U} -> A -> B -> Pair A B + +infix 1 _,_ + +foo : Pair Nat Nat +foo = (Z , S Z) + +-- So I was going to force a (a + b, a) =?= (3,0) unification problem +-- as an example of needing _dynamic_ pattern unification +data Eq : {A : U} -> A -> A -> U where + Refl : {A : U} -> {x : A} -> Eq x x + +-- but hold up here. This doesn't solve either. +-- Oh, because I can't reduce case. +-- And the FC is useless. +two : Eq (plus Z (S (S Z))) (S (S Z)) +two = Refl {Nat} {S (S Z)} + diff --git a/newt/typeclass.newt b/newt/typeclass.newt index bfedee9..71db267 100644 --- a/newt/typeclass.newt +++ b/newt/typeclass.newt @@ -4,6 +4,13 @@ module TypeClass -- this would be nicer with records and copatterns +-- At this point, for Agda style, I'll probably need to postpone, or collect constraints +-- at lesat. Idris style, I might get away without short term. + +-- So I can read mcbride paper and maybe agda source. + + + -- we need a bit more than this, but data Monad : (U -> U) -> U where MkMonad : { M : U -> U } -> @@ -15,6 +22,17 @@ data Maybe : U -> U where Nothing : {A : U} -> Maybe A +data Either : U -> U -> U where + Left : {A B : U} -> A -> Either A B + Right : {A B : U} -> B -> Either A B + +EitherMonad : {A : U} -> Monad (Either A) +EitherMonad = MkMonad {Either A} (\ ma amb => +-- ^ Need this for scrut type to be non-meta + case ma of + Left a => Left a + Right b => amb b) + -- [instance] MaybeMonad : Monad Maybe -- Agda case lambda might be nice.. @@ -44,5 +62,29 @@ ptype Int -- Idris gets this by specially treating determining arguments of an auto as "invertible". It then unifies -- the last arg on each side and tries the rest, which is now in the pattern fragment. +-- Agda may do this slightly differently from Idris: +-- https://agda.readthedocs.io/en/v2.6.0.1/language/instance-arguments.html#instance-resolution + +-- I think it searches, pulls in all possibilities and tries to unify them into place. +-- We'll want to extend our example to what I have in Foo2.agda to test that it finds the right +-- one. Maybe look at the source to see if there is any invertible trickery going on? + +-- I know that here, if I fill in the instance, everything works out, so finding the instance that works +-- out might be sufficient. That might mean that a instance constraint is a pile of options that get +-- winnowed down? + +-- Putting MaybeMonad in there helps the unification +-- of Maybe Int =?= ?m6 ?m2 (as Monad Maybe (the type) gives ?m6 is Maybe) +-- and MaybeEither would fail after a couple of steps. But it seems expensive/complex +-- to have to run the process down for each candidate. + +-- Agda seems complicated, minting fresh metas for bits of potential solutions (which +-- may be tossed if the solution is ruled out.) + foo : Int -> Maybe Int -foo x = _>>=_ (Just x) (\ x => Just 10) +foo x = _>>=_ {_} {_} {_} {_} (Just x) (\ x => Just 10) +-- ^ +/- +So, agda style we'd guess ?m8 is MonadMaybe or MonadEither - agda's "maybe" case + +-/ diff --git a/src/Lib/Check.idr b/src/Lib/Check.idr index fbc8e25..a1377c4 100644 --- a/src/Lib/Check.idr +++ b/src/Lib/Check.idr @@ -19,7 +19,7 @@ import Lib.Syntax data Pden = PR Nat Nat (List Nat) -- IORef for metas needs IO - +export forceMeta : Val -> M Val forceMeta (VMeta fc ix sp) = case !(lookupMeta ix) of (Unsolved pos k xs _) => pure (VMeta fc ix sp) @@ -102,7 +102,7 @@ parameters (ctx: Context) solve : Nat -> Nat -> SnocList Val -> Val -> M () solve l m sp t = do - debug "solve \{show l} \{show m} \{show sp} \{show t}" + debug "solve \{show m} lvl \{show l} sp \{show sp} is \{show t}" meta <- lookupMeta m debug "meta \{show meta}" ren <- invert l sp @@ -113,6 +113,13 @@ parameters (ctx: Context) solveMeta top m soln pure () + trySolve : Nat -> Nat -> SnocList Val -> Val -> M () + trySolve l m sp t = do + catchError {e=Error} (solve l m sp t) $ (\err => do + debug $ showError "" err + pure ()) + + export unify : (l : Nat) -> Val -> Val -> M UnifyResult @@ -160,9 +167,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 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 + 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 (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' @@ -177,8 +184,7 @@ parameters (ctx: Context) if k == k' then do debug "unify \{show l} spine at \{k} \{show sp} \{show sp'}" unifySpine l (k == k') sp sp' - -- REVIEW - consider forcing? - else error emptyFC "vref mismatch \{show k} \{show k'} -- \{show sp} \{show sp'}" + else error fc "vref mismatch \{show k} \{show k'} -- \{show sp} \{show sp'}" (VU _, VU _) => pure neutral -- Lennart.newt cursed type references itself @@ -343,7 +349,8 @@ updateContext ctx ((k, val) :: cs) = let ix = (length ctx.env `minus` k) `minus` -- 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 -buildCase : Context -> Problem -> String -> Val -> (String, Nat, Tm) -> M CaseAlt +-- 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 debug "CASE \{scnm} \{dcName} \{pprint (names ctx) ty}" vty <- eval [] CBN ty @@ -359,7 +366,8 @@ 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" - res <- unify ctx' (length ctx'.env) ty' scty + Just res <- catchError {e = Error} (Just <$> unify ctx' (length ctx'.env) ty' scty) (\_ => pure Nothing) + | _ => pure Nothing -- Additionally, we constrain the scrutinee's variable to be -- dcon applied to args @@ -397,7 +405,7 @@ buildCase ctx prob scnm scty (dcName, arity, ty) = do when (length clauses == 0) $ error ctx.fc "Missing case for \{dcName} splitting \{scnm}" tm <- buildTree ctx' (MkProb clauses prob.ty) - pure $ CaseCons dcName (map getName vars) tm + pure $ Just $ CaseCons dcName (map getName vars) tm where getName : Bind -> String getName (MkBind nm _ _) = nm @@ -528,7 +536,8 @@ buildTree ctx prob@(MkProb ((MkClause fc constraints [] expr) :: cs) ty) = do cons <- getConstructors ctx scty alts <- traverse (buildCase ctx prob scnm scty) cons - pure $ Case fc sctm alts + -- TODO check for empty somewhere? + pure $ Case fc sctm (catMaybes alts) showDef : Context -> List String -> Nat -> Val -> M String @@ -554,7 +563,7 @@ check ctx tm ty = case (tm, !(forceType ty)) of let ctx' = extend ctx scnm scty cons <- getConstructors ctx' scty alts <- traverse (buildCase ctx' (MkProb clauses ty) scnm scty) cons - pure $ Let fc scnm sc $ Case fc (Bnd fc 0) alts + pure $ Let fc scnm sc $ Case fc (Bnd fc 0) (catMaybes alts) -- Document a hole, pretend it's implemented (RHole fc, ty) => do diff --git a/src/Lib/Parser.idr b/src/Lib/Parser.idr index 4e9975d..a77708b 100644 --- a/src/Lib/Parser.idr +++ b/src/Lib/Parser.idr @@ -95,8 +95,8 @@ parseOp = parseApp >>= go 0 go : Int -> Raw -> Parser Raw go prec left = try (do - op <- token Oper fc <- getPos + op <- token Oper ops <- getOps let op' = "_" ++ op ++ "_" let Just (p,fix) = lookup op' ops diff --git a/src/Lib/ProcessDecl.idr b/src/Lib/ProcessDecl.idr index b1b9b80..f814904 100644 --- a/src/Lib/ProcessDecl.idr +++ b/src/Lib/ProcessDecl.idr @@ -82,12 +82,15 @@ processDecl (Def fc nm clauses) = do for_ mc.metas $ \case (Solved k x) => pure () - (Unsolved (l,c) k xs ty) => do + (Unsolved (l,c) k ctx ty) => do -- should just print, but it's too subtle in the sea of messages -- we'd also need the ability to mark the whole top context as failure if we continue -- put a list of errors in TopContext - putStrLn $ showError "" $ E (l,c) "Unsolved meta \{show k}" - addError $ E (l,c) "Unsolved meta \{show k}" + + -- Something wrong here - bad VVar + tm <- quote ctx.lvl !(forceMeta ty) + -- putStrLn $ showError "" $ E (l,c) "Unsolved meta \{show k} type \{show ty}" + addError $ E (l,c) "Unsolved meta \{show k} type \{pprint (names ctx) tm}" -- throwError $ E (l,c) "Unsolved meta \{show k}" debug "Add def \{nm} \{pprint [] tm'} : \{pprint [] ty}" modify $ setDef nm ty (Fn tm') diff --git a/tests/black/case3.newt b/tests/black/case3.newt new file mode 100644 index 0000000..8e1f721 --- /dev/null +++ b/tests/black/case3.newt @@ -0,0 +1,18 @@ +module Case3 + +data Nat : U where + Z : Nat + S : Nat -> Nat + +data Vect : Nat -> U -> U where + Nil : {a : U} -> Vect Z a + _::_ : {a : U} -> {k : Nat} -> a -> Vect k a -> Vect (S k) a + +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