From 91eec503d1f13eefe4a392d3d24393c803d204fe Mon Sep 17 00:00:00 2001
From: Steve Dunham <dunhamsteve@gmail.com>
Date: Wed, 30 Oct 2024 21:39:26 -0700
Subject: [PATCH] clean up some vscode noise from backtracking

---
 src/Lib/CompileExp.idr  |  2 +-
 src/Lib/Elab.idr        | 26 +++++++-----------------
 src/Lib/Eval.idr        |  6 +++---
 src/Lib/ProcessDecl.idr |  2 +-
 src/Lib/Types.idr       | 44 ++++++++++++++++++++---------------------
 5 files changed, 34 insertions(+), 46 deletions(-)

diff --git a/src/Lib/CompileExp.idr b/src/Lib/CompileExp.idr
index 67a7012..515d455 100644
--- a/src/Lib/CompileExp.idr
+++ b/src/Lib/CompileExp.idr
@@ -94,7 +94,7 @@ compileTerm tm@(App _ _ _) with (funArgs tm)
         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)
+                (Solved _ j tm) => pure $ getArity !(quote 0 tm)
         apply (CRef "Meta\{show k}") args' [<] arity
   _ | (t@(Ref fc nm _), args) = do
         args' <- traverse compileTerm args
diff --git a/src/Lib/Elab.idr b/src/Lib/Elab.idr
index b7192c7..e6b06f3 100644
--- a/src/Lib/Elab.idr
+++ b/src/Lib/Elab.idr
@@ -55,7 +55,7 @@ export
 forceMeta : Val -> M Val
 forceMeta (VMeta fc ix sp) = case !(lookupMeta ix) of
   (Unsolved pos k xs _ _ _) => pure (VMeta fc ix sp)
-  (Solved k t) => vappSpine t sp >>= forceMeta
+  (Solved _ k t) => vappSpine t sp >>= forceMeta
 forceMeta x = pure x
 
 tryEval : String -> SnocList Val -> M (Maybe Val)
@@ -72,7 +72,7 @@ tryEval k sp =
 forceType : Val -> M Val
 forceType (VMeta fc ix sp) = case !(lookupMeta ix) of
   (Unsolved x k xs _ _ _) => pure (VMeta fc ix sp)
-  (Solved k t) => vappSpine t sp >>= forceType
+  (Solved _ k t) => vappSpine t sp >>= forceType
 forceType x@(VRef fc nm _ sp) = fromMaybe x <$> tryEval nm sp
 forceType x = pure x
 
@@ -99,7 +99,7 @@ updateMeta ctx ix f = do
     go : List MetaEntry -> M (List MetaEntry)
     go [] = error' "Meta \{show ix} not found"
     go (x@((Unsolved y k z w v ys)) :: xs) = if k == ix then (::xs) <$> f x else (x ::) <$> go xs
-    go (x@((Solved k y)) :: xs) = if k == ix then (::xs) <$> f x else (x ::) <$> go xs
+    go (x@((Solved _ k y)) :: xs) = if k == ix then (::xs) <$> f x else (x ::) <$> go xs
 
 export
 addConstraint : Context -> Nat -> SnocList Val -> Val -> M ()
@@ -107,9 +107,9 @@ addConstraint ctx ix sp tm = do
   mc <- readIORef ctx.metas
   updateMeta ctx ix $ \case
     (Unsolved pos k a b c cons) => do
-      info (getFC tm) "Add constraint m\{show ix} \{show sp} =?= \{show tm}"
+      debug "Add constraint m\{show ix} \{show sp} =?= \{show tm}"
       pure (Unsolved pos k a b c (MkMc (getFC tm) ctx sp tm :: cons))
-    (Solved k tm) => error' "Meta \{show k} already solved"
+    (Solved _ k tm) => error' "Meta \{show k} already solved"
   pure ()
 
 parameters (ctx: Context)
@@ -191,26 +191,14 @@ parameters (ctx: Context)
     soln <- eval [] CBN tm
 
     updateMeta ctx m $ \case
-      (Unsolved pos k _ _ _ cons) => do
-          putStrLn "INFO at \{show pos}: solve \{show k} as \{pprint [] !(quote 0 soln)}"
-          pure $ Solved k soln
-      (Solved k x) => error' "Meta \{show ix} already solved!"
+      (Unsolved pos k _ _ _ cons) => pure $ Solved pos k soln
+      (Solved _ k x) => error' "Meta \{show ix} already solved!"
     for_ cons $ \case
       MkMc fc ctx sp rhs => do
         val <- vappSpine soln sp
         debug "discharge l=\{show ctx.lvl} \{(show val)} =?= \{(show rhs)}"
         unify ctx.lvl val rhs
 
-    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 ())
-
-
-
   unifySpine : Nat -> Bool -> SnocList Val -> SnocList Val  -> M UnifyResult
   unifySpine l False _ _ = error emptyFC "unify failed at head" -- unreachable now
   unifySpine l True [<] [<] = pure (MkResult [])
diff --git a/src/Lib/Eval.idr b/src/Lib/Eval.idr
index d836324..b41f994 100644
--- a/src/Lib/Eval.idr
+++ b/src/Lib/Eval.idr
@@ -80,7 +80,7 @@ eval env mode (U fc) = pure (VU fc)
 eval env mode (Meta fc i) =
   case !(lookupMeta i) of
         (Unsolved _ k xs _ _ _) => pure $ VMeta fc i [<]
-        (Solved k t) => pure $ t
+        (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 (Let fc nm t u) = pure $ VLet fc nm !(eval env mode t) (MkClosure env u)
@@ -113,7 +113,7 @@ quote l (VVar fc k sp) = if k < l
 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)
+        (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 [<]))
@@ -162,7 +162,7 @@ appSpine t (x :: xs) = appSpine (App (getFC t) t x) xs
 zonkApp : TopContext -> Nat -> Env -> Tm -> List Tm -> M Tm
 zonkApp top l env (App fc t u) sp = zonkApp top l env t (!(zonk top l env u) :: sp)
 zonkApp top l env t@(Meta fc k) sp = case !(lookupMeta k) of
-  (Solved j v) => do
+  (Solved _ j v) => do
     sp' <- traverse (eval env CBN) sp
     debug "zonk \{show k} -> \{show v} spine \{show sp'}"
     foo <- vappSpine v ([<] <>< sp')
diff --git a/src/Lib/ProcessDecl.idr b/src/Lib/ProcessDecl.idr
index a9e531a..a233050 100644
--- a/src/Lib/ProcessDecl.idr
+++ b/src/Lib/ProcessDecl.idr
@@ -159,7 +159,7 @@ processDecl (Def fc nm clauses) = do
 
   mc <- readIORef top.metas
   for_ (take mlen mc.metas) $ \case
-    (Solved k x) => pure ()
+    (Solved fc k soln) => info fc "solve \{show k} as \{pprint [] !(quote 0 soln)}"
     (Unsolved fc k ctx ty User cons) => do
       ty' <- quote ctx.lvl ty
       let names = (toList $ map fst ctx.types)
diff --git a/src/Lib/Types.idr b/src/Lib/Types.idr
index 9481651..00a03ab 100644
--- a/src/Lib/Types.idr
+++ b/src/Lib/Types.idr
@@ -330,7 +330,7 @@ public export
 data MConstraint = MkMc FC Context (SnocList Val) Val
 
 public export
-data MetaEntry = Unsolved FC Nat Context Val MetaKind (List MConstraint) | Solved Nat Val
+data MetaEntry = Unsolved FC Nat Context Val MetaKind (List MConstraint) | Solved FC Nat Val
 
 
 public export
@@ -422,7 +422,7 @@ export
 covering
 Show MetaEntry where
   show (Unsolved pos k ctx ty kind constraints) = "Unsolved \{show pos} \{show k} \{show kind} : \{show ty} \{show ctx.bds} cs \{show $ length constraints}"
-  show (Solved k x) = "Solved \{show k} \{show x}"
+  show (Solved _ k x) = "Solved \{show k} \{show x}"
 
 export withPos : Context -> FC -> Context
 withPos ctx fc = { fc := fc } ctx
@@ -435,6 +435,24 @@ public export
 M : Type -> Type
 M = (StateT TopContext (EitherT Impl.Error IO))
 
+||| Force argument and print if verbose is true
+export
+debug : Lazy String -> M ()
+debug x = do
+  top <- get
+  when top.verbose $ putStrLn x
+
+export
+info : FC -> String -> M ()
+info fc msg = putStrLn "INFO at \{show fc}: \{msg}"
+
+||| Version of debug that makes monadic computation lazy
+export
+debugM : M String -> M ()
+debugM x = do
+  top <- get
+  when top.verbose $ do putStrLn !(x)
+
 export partial
 Show Context where
   show ctx = "Context \{show $ map fst $ ctx.types}"
@@ -451,7 +469,7 @@ export
 freshMeta : Context -> FC -> Val -> MetaKind -> M Tm
 freshMeta ctx fc ty kind = do
   mc <- readIORef ctx.metas
-  putStrLn "INFO at \{show fc}: fresh meta \{show mc.next} : \{show ty}"
+  debug "fresh meta \{show mc.next} : \{show ty}"
   writeIORef ctx.metas $ { next $= S, metas $= (Unsolved fc mc.next ctx ty kind [] ::) } mc
   pure $ applyBDs 0 (Meta emptyFC mc.next) ctx.bds
   where
@@ -477,28 +495,10 @@ lookupMeta ix = do
     go : List MetaEntry -> M MetaEntry
     go [] = error' "Meta \{show ix} not found"
     go (meta@(Unsolved _ k ys _ _ _) :: xs) = if k == ix then pure meta else go xs
-    go (meta@(Solved k x) :: xs) = if k == ix then pure meta else go xs
+    go (meta@(Solved _ k x) :: xs) = if k == ix then pure meta else go xs
 
 -- we need more of topcontext later - Maybe switch it up so we're not passing
 -- around top
 export
 mkCtx : IORef MetaContext -> FC -> Context
 mkCtx metas fc = MkCtx 0 [] [] [] metas fc
-
-||| Force argument and print if verbose is true
-export
-debug : Lazy String -> M ()
-debug x = do
-  top <- get
-  when top.verbose $ putStrLn x
-
-export
-info : FC -> String -> M ()
-info fc msg = putStrLn "INFO at \{show fc}: \{msg}"
-
-||| Version of debug that makes monadic computation lazy
-export
-debugM : M String -> M ()
-debugM x = do
-  top <- get
-  when top.verbose $ do putStrLn !(x)