fromMaybe is working, but stuff feels a little messy/fragile

README.md

@@ -1,4 +1,5 @@
-
+- [ ] case tree building favors the right size, reverse the list
+- [ ] see note in Zoo1.newt - fix the FC in that situation
 - [x] Support primitives
 - [ ] Make DCon/TCon separate from Ref? (Or add flavor to VRef/Ref? If processing is often the same. I think I want arity though. I don't think a checked DCon can be overapplied, but it could be underapplied without special form. And special form is possibly difficult if not collecting a stack on the way down...
 

newt/Zoo1.newt

@@ -48,8 +48,26 @@ length (Define env _) = S (length env)
 
 lookup : Env -> Nat -> Maybe Val
 lookup (Define env v) Z = Just v
-lookup (Define env _) (S k) = Just (lookup env k)
+-- If I write "Just (lookup env k)" on RHS, it's wrong, but the error message is unusable (mainly due to FC)
--- bug in unify? are the meta args backwards? It seems to quote back right..
+-- The FC is fine if I write lookup {Val} env k
--- we're getting `Maybe Val` as meta3, and comparing:
+lookup (Define env _) (S k) = lookup env k
--- Maybe ?m3  =?= Maybe Val
 lookup (ENil) x = Nothing
+
+eval : Env -> Tm -> Val
+
+cApp : Closure -> Val -> Val
+-- If I put Closure instead of MkClosure, it reports missing case, fix that (should be bad constructor or something)
+cApp (MkClosure env t) u = eval (Define env u) t
+
+eval env (Var x) =
+  case lookup env x of
+    -- case doesn't use the new code.  We've got a wildcard here that
+    -- is forced to {Val}, but we don't have forcing/dotting
+    -- I guess we see what Jesper says about dotting
+    Just x => x
+
+eval env (App t u) =
+  let tv = eval env t
+      tu = eval env u
+  in ?
+

newt/testcase3.newt

@@ -0,0 +1,25 @@
+module Scratch2
+
+data Nat : U where
+  Z : Nat
+  S : Nat -> Nat
+
+data Maybe : U -> U where
+  Just : {a : U} -> a -> Maybe a
+  Nothing : {a : U} -> Maybe a
+
+
+-- failed to unify _:1 with Val
+-- Legit on RHS, IMO. On LHS, we should be dotting?
+-- I either need to unify and collect constraints or figure out how
+-- other systems manage this.
+
+-- Note that an unused
+-- variable may stand for either a wildcard or a forced pattern. In the latter case our algorithm
+-- treats it as a let-bound variable in the right-hand side of the clause.
+
+-- we need let-bound in environment but we do have define.
+
+fromMaybe : Maybe Nat -> Nat
+fromMaybe (Just x) = x
+fromMaybe Nothing = Z

src/Lib/CaseTree.idr

@@ -14,6 +14,31 @@ import Lib.Check
 import Lib.TT
 import Lib.Syntax
 
+
+-- ok, so new idea:
+
+-- we make a meta for each patvar
+-- then "solve" the meta when we match stuff up.
+-- a meta is something we can change
+
+-- but the solutions vary per branch. n is S k in one branch and Z in another.
+-- and metas are essentially global.
+
+-- NEXT So on LHS, I think we need to collect constraints pat$0 = Val and change
+-- the entry in the environment to a let?
+
+-- Except I think the let might reference something not bound yet? For RHS (a raw), we
+-- can shadow. For expected type, we might have to mess with the Val?
+
+-- On RHS I don't think unification can assign a value to a name.
+
+-- exempli gratia
+-- fromMaybe : Maybe Nat -> Nat
+-- fromMaybe (Just x) = x
+--                      ^- currently
+-- fromMaybe Nothing = Z
+
+
 -- LHSProblem
 -- List of [ E ] qbar --> rhs
 -- E is bag of constraints:
@@ -86,9 +111,11 @@ fresh base = base ++ "$" ++ show (length ctx.env)
 export
 buildTree : Context -> Problem -> M Tm
 
-introClause : String -> Clause -> M Clause
+introClause : String -> Icit -> Clause -> M Clause
-introClause nm (MkClause fc cons [] expr) = error fc "Clause size doesn't match"
+-- I don't think this makes a difference?
-introClause nm (MkClause fc cons (pat :: pats) expr) = pure $ MkClause fc ((nm, pat) :: cons) pats expr
+introClause nm Implicit (MkClause fc cons pats expr) = pure $ MkClause fc ((nm, PatWild fc) :: cons) pats expr
+introClause nm icit (MkClause fc cons [] expr) = error fc "Clause size doesn't match"
+introClause nm icit (MkClause fc cons (pat :: pats) expr) = pure $ MkClause fc ((nm, pat) :: cons) pats expr
 
 -- A split candidate looks like x /? Con ...
 -- we need a type here. I pulled if off of the
@@ -109,7 +136,7 @@ findSplit (_ :: xs) = findSplit xs
 
 -- TODO, we may need to filter these for the situation.
 getConstructors : Context -> Val -> M (List (String, Nat, Tm))
-getConstructors ctx (VRef fc nm _ sc) = do
+getConstructors ctx (VRef fc nm _ _) = do
   names <- lookupTCon nm
   traverse lookupDCon names
   where
@@ -140,15 +167,61 @@ extendPi ctx ty nms = pure (ctx, ty, nms <>> [])
 
 -- FIXME - I don't think we're properly noticing
 
+updateContext : Context -> List (Nat, Val) -> M Context
+updateContext ctx [] = pure ctx
+updateContext ctx ((k, val) :: cs) = let ix = (length ctx.env `minus` k) `minus` 1 in
+  pure $ {env $= makeLet ix} ctx
+  where
+    makeLet : Nat -> Env -> Env
+    makeLet _ [] = ?nothing_to_update
+    makeLet 0 ((VVar fc j [<]) :: xs) = val :: xs
+    makeLet 0 (_ :: xs) = ?not_a_var
+    makeLet (S k) (x :: xs) = x :: makeLet k xs
 
 -- 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 -> (String, Nat, Tm) -> M CaseAlt
+buildCase : Context -> Problem -> String -> Val -> (String, Nat, Tm) -> M CaseAlt
-buildCase ctx prob scnm (dcName, _, ty) = do
+buildCase ctx prob scnm scty (dcName, _, ty) = do
+  debug "CASE \{scnm} \{dcName} \{pprint (names ctx) ty}"
   vty <- eval [] CBN ty
   (ctx', ty', vars) <- extendPi ctx (vty) [<]
 
+  -- what is the goal?
+  -- we have something here that informs what happens in the casealt, possibly tweaking
+  -- context or goal
+  -- e.g. we get to end of Just {a} x  and goal is Maybe Val, we want `let a = Val` in context.
+  -- likewise if the constructor says `Foo String` and goal is `Foo x` we know x is String in this branch.
+
+  -- we need unify to hand constraints back...
+  -- we may need to walk through the case alt constraint and discharge or drop things?
+
+  -- should I somehow make those holes? It would be nice to not make the user dot it.
+  -- And we don't _need_ a solution, just if it's unified against
+
+  -- I think I'm going down a different road than Idris..
+
+
+  -- do this or see how other people manage?
+  -- this puts the failure on the LHS
+  -- unifying these should say say VVar 1 is Nat.
+  -- ERROR at (23, 0): unify failed (%var 1 [< ]) =?= (%ref Nat [< ]) [no Fn]
+  res <- unify ctx' (length ctx.env) ty' scty
+  debug "scty \{show scty}"
+  debug "UNIFY results \{show res.constraints}"
+  debug "before types: \{show ctx'.types}"
+  debug "before env: \{show ctx'.env}"
+
+  -- So we go and stuff stuff into the environment, which I guess gets it into the RHS,
+  -- but doesn't touch goal...
+  ctx' <- updateContext ctx' res.constraints
+  debug "context types: \{show ctx'.types}"
+  debug "context env: \{show ctx'.env}"
+  -- This doesn't really update existing val... including types in the context.
+
+  -- What if all of the pattern vars are defined to meta
+
+  debug "(dcon \{show dcName} ty \{show ty'} scty \{show scty}"
   debug "(dcon \{show dcName}) (vars \{show vars}) clauses were"
   for_ prob.clauses $ (\x => debug "    \{show x}")
   let clauses = mapMaybe (rewriteClause vars) prob.clauses
@@ -223,7 +296,13 @@ lookupName ctx name = go 0 ctx.types
       -- error fc "Stuck, no splits \{show constraints}"
 
 checkDone : Context -> List (String, Pattern) -> Raw -> Val -> M Tm
-checkDone ctx [] body ty = check ctx body ty
+checkDone ctx [] body ty = do
+  debug "DONE-> check body \{show body} at \{show ty}"
+  debug "\{show ctx.env}"
+  debug "\{show ctx.types}"
+  got <- check ctx body ty
+  debug "DONE<- got \{pprint (names ctx) got}"
+  pure got
 checkDone ctx ((x, PatWild _) :: xs) body ty = checkDone ctx xs body ty
 checkDone ctx ((nm, (PatVar _ nm')) :: xs) body ty = checkDone ({ types $= rename } ctx) xs body ty
   where
@@ -239,26 +318,18 @@ checkDone ctx ((x, pat) :: xs) body ty = error emptyFC "stray constraint \{x} /?
 -- 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 Implicit a b)) = do
-  let l = length ctx.env
-  let nm = fresh "pat"
-  let ctx' = extend ctx nm a
-  -- type of the rest
-  -- clauses <- traverse (introClause nm) prob.clauses
-  vb <- b $$ VVar fc l [<]
-  Lam fc nm <$> buildTree ctx' ({ ty := vb } prob)
 buildTree ctx prob@(MkProb ((MkClause fc cons (x :: xs) expr) :: cs) (VPi _ str icit a b)) = do
   let l = length ctx.env
   let nm = fresh "pat"
   let ctx' = extend ctx nm a
   -- type of the rest
-  clauses <- traverse (introClause nm) prob.clauses
+  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)
 buildTree ctx prob@(MkProb ((MkClause fc cons pats@(x :: xs) expr) :: cs) ty) =
   error fc "Extra pattern variables \{show pats}"
-buildTree ctx prob@(MkProb ((MkClause fc [] [] expr) :: cs) ty) = check ctx expr ty
+buildTree ctx prob@(MkProb ((MkClause fc [] [] expr) :: cs) ty) = check (withPos ctx fc) expr ty
 -- need to find some name we can split in (x :: xs)
 -- so LHS of constraint is name (or VVar - if we do Val)
 -- then run the split
@@ -267,11 +338,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}"
-  let Just (sctm, ty') := lookupName ctx scnm
+  let Just (sctm, scty) := lookupName ctx scnm
     | _ => error fc "Internal Error: can't find \{scnm} in environment"
 
-  cons <- getConstructors ctx ty'
+  cons <- getConstructors ctx scty
-  alts <- traverse (buildCase ctx prob scnm) cons
+  alts <- traverse (buildCase ctx prob scnm scty) cons
 
   pure $ Case fc sctm alts

src/Lib/Check.idr

@@ -38,6 +38,18 @@ forceType (VMeta fc ix sp) = case !(lookupMeta ix) of
 forceType x = pure x
 
 
+public export
+record UnifyResult where
+  constructor MkResult
+  -- wild guess here - lhs is a VVar
+  constraints : List (Nat, Val)
+
+Semigroup UnifyResult where
+  (MkResult cs) <+> (MkResult cs') = MkResult (cs ++ cs')
+
+Monoid UnifyResult where
+  neutral = MkResult []
+
 parameters (ctx: Context)
   -- return renaming, the position is the new VVar
   invert : Nat -> SnocList Val -> M (List Nat)
@@ -98,12 +110,13 @@ parameters (ctx: Context)
     solveMeta top m soln
     pure ()
 
-  unify : (l : Nat) -> Val -> Val  -> M  ()
+  export
+  unify : (l : Nat) -> Val -> Val  -> M UnifyResult
 
-  unifySpine : Nat -> Bool -> SnocList Val -> SnocList Val  -> M  ()
+  unifySpine : Nat -> Bool -> SnocList Val -> SnocList Val  -> M UnifyResult
   unifySpine l False _ _ = error emptyFC "unify failed at head" -- unreachable now
-  unifySpine l True [<] [<] = pure ()
+  unifySpine l True [<] [<] = pure (MkResult [])
-  unifySpine l True (xs :< x) (ys :< y) = unify l x y >> unifySpine l True xs ys
+  unifySpine l True (xs :< x) (ys :< y) = [| unify l x y <+> (unifySpine l True xs ys) |]
   unifySpine l True _ _ = error emptyFC "meta spine length mismatch"
 
   unify l t u = do
@@ -115,26 +128,36 @@ parameters (ctx: Context)
     debug "forced \{show t'}"
     debug "  =?= \{show u'}"
     debug "env \{show ctx.env}"
+    debug "types \{show $ ctx.types}"
     case (t',u') of
       (VLam _ _ t,  VLam _ _ t') => unify (l + 1) !(t $$ VVar emptyFC l [<]) !(t' $$ VVar emptyFC l [<])
       (t,         VLam fc' _ t') => unify (l + 1) !(t `vapp` VVar emptyFC l [<]) !(t' $$ VVar emptyFC l [<])
       (VLam fc _ t,  t'       ) => unify (l + 1) !(t $$ VVar emptyFC l [<]) !(t' `vapp` VVar emptyFC l [<])
-      (VPi fc _ _ a b, VPi fc' _ _ a' b') => unify l a a' >> unify (S l) !(b $$ VVar emptyFC l [<]) !(b' $$ VVar emptyFC l [<])
+      (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'
         else error emptyFC "vvar mismatch \{show k} \{show k'}"
+
+      -- attempt at building constraints
+      -- and using them
+      (VVar fc k sp, u) => case lookupVar k of
+        Just v => unify l v u
+        Nothing => pure $ MkResult[(k, u)]
+      (t, VVar fc k sp) => pure $ MkResult[(k, t)]
+
       (VRef fc k def sp,   VRef fc' k' def' sp'  ) =>
         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'}"
+
       (VMeta fc k sp,  VMeta fc' k' sp' ) =>
         if k == k' then unifySpine l (k == k') sp sp'
-        else solve l k sp (VMeta fc' k' sp')
+        else solve l k sp (VMeta fc' k' sp') >> pure neutral
-      (t,           VMeta fc' i' sp') => solve l i' sp' t
+      (t,           VMeta fc' i' sp') => solve l i' sp' t >> pure neutral
-      (VMeta fc i sp, t'           ) => solve l i sp t'
+      (VMeta fc i sp, t'           ) => solve l i sp t' >> pure neutral
-      (VU _, VU _) => pure ()
+      (VU _, VU _) => pure neutral
       -- Lennart.newt cursed type references itself
       -- We _could_ look up the ref, eval against [] and vappSpine...
       (t,         VRef fc' k' def sp') => do
@@ -144,15 +167,29 @@ parameters (ctx: Context)
           _ => error ctx.fc "unify failed \{show t'} =?= \{show u'} [no Fn]\n  env is \{show ctx.env} \{show $ map fst ctx.types}"
       -- REVIEW I'd like to quote this back, but we have l that aren't in the environment.
       _ => error ctx.fc "unify failed \{show t'} =?= \{show u'} \n  env is \{show ctx.env} \{show $ map fst ctx.types}"
+    where
+      lookupVar : Nat -> Maybe Val
+      lookupVar k = let l = length ctx.env in
+        if k > l
+          then Nothing
+          else case getAt ((l `minus` k) `minus` 1) ctx.env of
+            Just (VVar{}) => Nothing
+            Just v => Just v
+            Nothing => Nothing
+
 
 unifyCatch : FC -> Context -> Val -> Val -> M ()
-unifyCatch fc ctx ty' ty = catchError (unify ctx ctx.lvl ty' ty) $ \(E x str) => do
+unifyCatch fc ctx ty' ty = do
+    res <- catchError (unify ctx ctx.lvl ty' ty) $ \(E x str) => do
       let names = toList $ map fst ctx.types
       debug "fail \{show ty'} \{show ty}"
       a <- quote ctx.lvl ty'
       b <- quote ctx.lvl ty
       let msg = "\n  failed to unify \{pprint names a}\n    with \{pprint names b}\n  " <+> str
       throwError (E fc msg)
+    case res of
+      MkResult [] => pure ()
+      cs => error fc "Unification yields constraints \{show cs.constraints}"
 
 insert : (ctx : Context) -> Tm -> Val -> M (Tm, Val)
 insert ctx tm ty = do
@@ -379,7 +416,7 @@ infer ctx (RApp fc t u icit) = do
       debug "unify PI for \{show tty}"
       a <- eval ctx.env CBN !(freshMeta ctx fc)
       b <- MkClosure ctx.env <$> freshMeta (extend ctx ":ins" a) fc
-      unify ctx 0 tty (VPi fc ":ins" icit a b)
+      unifyCatch fc ctx tty (VPi fc ":ins" icit a b)
       pure (a,b)
 
   u <- check ctx u a

src/Lib/Types.idr

@@ -367,6 +367,9 @@ record Context where
   metas : IORef MetaContext
   fc : FC
 
+export withPos : Context -> FC -> Context
+withPos ctx fc = { fc := fc } ctx
+
 export
 names : Context -> List String
 names ctx = toList $ map fst ctx.types