From 30cc85ca0e68363fe359bd8f3881d98c84639cbb Mon Sep 17 00:00:00 2001
From: Steve Dunham <dunhamsteve@gmail.com>
Date: Thu, 2 Jan 2025 13:48:16 -0800
Subject: [PATCH] move auto solver to elab

---
 src/Lib/Elab.idr        | 145 ++++++++++++++++++++++++++++++++++++++--
 src/Lib/ProcessDecl.idr | 105 -----------------------------
 src/Lib/Types.idr       |  15 -----
 3 files changed, 139 insertions(+), 126 deletions(-)

diff --git a/src/Lib/Elab.idr b/src/Lib/Elab.idr
index 76e1f10..923d018 100644
--- a/src/Lib/Elab.idr
+++ b/src/Lib/Elab.idr
@@ -11,6 +11,9 @@ import Lib.Eval
 import Lib.TopContext
 import Lib.Syntax
 
+
+
+
 ||| collectDecl collects multiple Def for one function into one
 export
 collectDecl : List Decl -> List Decl
@@ -92,6 +95,124 @@ Monoid UnifyResult where
 
 data UnifyMode = Normal | Pattern
 
+
+export
+check : Context -> Raw -> Val -> M Tm
+
+export
+unifyCatch : FC -> Context -> Val -> Val -> M ()
+
+-- Check that the arguments are not explicit and the type constructor in codomain matches
+-- Later we will build a table of codomain type, and maybe make the user tag the candidates
+-- like Idris does with %hint
+isCandidate : Val -> Tm -> Bool
+isCandidate ty (Pi fc nm Explicit rig t u) = False
+isCandidate ty (Pi fc nm icit rig t u) = isCandidate ty u
+isCandidate (VRef _ nm _ _) (Ref fc nm' def) = nm == nm'
+isCandidate ty (App fc t u) = isCandidate ty t
+isCandidate _ _ = False
+
+-- This is a crude first pass
+export
+findMatches : Context -> Val -> List TopEntry -> M (List (Tm, MetaContext))
+findMatches ctx ty [] = pure []
+findMatches ctx ty ((MkEntry _ name type def) :: xs) = do
+  let True = isCandidate ty type | False => findMatches ctx ty xs
+  top <- get
+  -- let ctx = mkCtx (getFC ty)
+  -- FIXME we're restoring state, but the INFO logs have already been emitted
+  -- Also redo this whole thing to run during elab, recheck constraints, etc.
+  mc <- readIORef top.metaCtx
+  catchError(do
+      -- TODO sort out the FC here
+      let fc = getFC ty
+      debug "TRY \{name} : \{pprint [] type} for \{show ty}"
+      -- This check is solving metas, so we save mc below in case we want this solution
+      -- tm <- check (mkCtx fc) (RVar fc name) ty
+      -- FIXME RVar should optionally have qualified names
+      let (QN ns nm) = name
+      tm <- check ctx (RVar fc nm) ty
+      debug "Found \{pprint [] tm} for \{show ty}"
+      mc' <- readIORef top.metaCtx
+      writeIORef top.metaCtx mc
+      ((tm, mc') ::) <$> findMatches ctx ty xs)
+    (\ err => do
+      debug "No match \{show ty} \{pprint [] type} \{showError "" err}"
+      writeIORef top.metaCtx mc
+      findMatches ctx ty xs)
+
+export
+contextMatches : Context -> Val -> M (List (Tm, MetaContext))
+contextMatches ctx ty = go (zip ctx.env (toList ctx.types))
+  where
+    go : List (Val, String, Val) -> M (List (Tm, MetaContext))
+    go [] = pure []
+    go ((tm, nm, vty) :: xs) = do
+      type <- quote ctx.lvl vty
+      let True = isCandidate ty type | False => go xs
+      top <- get
+      mc <- readIORef top.metaCtx
+      catchError(do
+          debug "TRY context \{nm} : \{pprint (names ctx) type} for \{show ty}"
+          unifyCatch (getFC ty) ctx ty vty
+          mc' <- readIORef top.metaCtx
+          writeIORef top.metaCtx mc
+          tm <- quote ctx.lvl tm
+          ((tm, mc') ::) <$> go xs)
+        (\ err => do
+          debug "No match \{show ty} \{pprint (names ctx) type} \{showError "" err}"
+          writeIORef top.metaCtx mc
+          go xs)
+
+export
+getArity : Tm -> Nat
+getArity (Pi x str icit rig t u) = S (getArity u)
+-- Ref or App (of type constructor) are valid
+getArity _ = Z
+
+-- Can metas live in context for now?
+-- We'll have to be able to add them, which might put gamma in a ref
+
+
+
+-- Makes the arg for `solve` when we solve an auto
+makeSpine : Nat -> Vect k BD -> SnocList Val
+makeSpine k [] = [<]
+makeSpine (S k) (Defined :: xs) = makeSpine k xs
+makeSpine (S k) (Bound :: xs) = makeSpine k xs :< VVar emptyFC k [<]
+makeSpine 0 xs = ?fixme
+
+export
+solve : Env -> (k : Nat) -> SnocList Val -> Val -> M ()
+
+export
+solveAutos : Nat -> List MetaEntry -> M ()
+solveAutos mstart [] = pure ()
+solveAutos mstart ((Unsolved fc k ctx ty AutoSolve _) :: es) = do
+      debug "AUTO solving \{show k} : \{show ty}"
+      -- fill in solved metas in type
+      x <- quote ctx.lvl ty
+      ty <- eval ctx.env CBN x
+      debug "AUTO ---> \{show ty}"
+      -- we want the context here too.
+      top <- get
+      [(tm, mc)] <- case !(contextMatches ctx ty) of
+            [] => findMatches ctx ty $ toList top.defs
+            xs => pure xs
+        | res => do
+          debug "FAILED to solve \{show ty}, matches: \{commaSep $ map (pprint [] . fst) res}"
+          solveAutos mstart es
+      writeIORef top.metaCtx mc
+      val <- eval ctx.env CBN tm
+      debug "SOLUTION \{pprint [] tm} evaled to \{show val}"
+      let sp = makeSpine ctx.lvl ctx.bds
+      solve ctx.env k sp val
+      mc <- readIORef top.metaCtx
+      let mlen = length mc.metas `minus` mstart
+      solveAutos mstart (take mlen mc.metas)
+solveAutos mstart (_ :: es) = solveAutos mstart es
+
+
 -- We need to switch to SortedMap here
 export
 updateMeta : Nat -> (MetaEntry -> M MetaEntry) -> M ()
@@ -191,8 +312,6 @@ unify : Env -> UnifyMode -> Val -> Val  -> M UnifyResult
 (.boundNames) : Context -> List String
 ctx.boundNames = map snd $ filter (\x => fst x == Bound) $ toList $ zip ctx.bds (map fst ctx.types)
 
-export
-solve : Env -> (k : Nat) -> SnocList Val -> Val -> M ()
 solve env m sp t = do
   meta@(Unsolved metaFC ix ctx_ ty kind cons) <- lookupMeta m
     | _ => error (getFC t) "Meta \{show m} already solved! [solve]"
@@ -361,8 +480,7 @@ unify env mode t u = do
     unifyPattern t (VVar fc k [<]) = pure $ MkResult [(k, t)]
     unifyPattern t u = unifyMeta t u
 
-export
-unifyCatch : FC -> Context -> Val -> Val -> M ()
+
 unifyCatch fc ctx ty' ty = do
     res <- catchError (unify ctx.env Normal ty' ty) $ \err => do
       let names = toList $ map fst ctx.types
@@ -385,6 +503,23 @@ unifyCatch fc ctx ty' ty = do
         throwError (E fc msg)
         -- error fc "Unification yields constraints \{show cs.constraints}"
 
+export
+freshMeta : Context -> FC -> Val -> MetaKind -> M Tm
+freshMeta ctx fc ty kind = do
+  top <- get
+  mc <- readIORef top.metaCtx
+  debug "fresh meta \{show mc.next} : \{show ty} (\{show kind})"
+  let newmeta = Unsolved fc mc.next ctx ty kind []
+  writeIORef top.metaCtx $ { next $= S, metas $= (newmeta ::) } mc
+  pure $ applyBDs 0 (Meta fc mc.next) ctx.bds
+  where
+    -- hope I got the right order here :)
+    applyBDs : Nat -> Tm -> Vect k BD -> Tm
+    applyBDs k t [] = t
+    -- review the order here
+    applyBDs k t (Bound :: xs) = App emptyFC (applyBDs (S k) t xs) (Bnd emptyFC k)
+    applyBDs k t (Defined :: xs) = applyBDs (S k) t xs
+
 insert : (ctx : Context) -> Tm -> Val -> M (Tm, Val)
 insert ctx tm ty = do
   case !(forceMeta ty) of
@@ -410,8 +545,6 @@ primType fc nm = case lookup nm !(get) of
 export
 infer : Context -> Raw  -> M (Tm, Val)
 
-export
-check : Context -> Raw -> Val -> M Tm
 
 data Bind = MkBind String Icit Val
 
diff --git a/src/Lib/ProcessDecl.idr b/src/Lib/ProcessDecl.idr
index e88666a..72a0232 100644
--- a/src/Lib/ProcessDecl.idr
+++ b/src/Lib/ProcessDecl.idr
@@ -15,111 +15,6 @@ import Lib.Types
 import Lib.Util
 import Lib.Erasure
 
--- Check that the arguments are not explicit and the type constructor in codomain matches
--- Later we will build a table of codomain type, and maybe make the user tag the candidates
--- like Idris does with %hint
-isCandidate : Val -> Tm -> Bool
-isCandidate ty (Pi fc nm Explicit rig t u) = False
-isCandidate ty (Pi fc nm icit rig t u) = isCandidate ty u
-isCandidate (VRef _ nm _ _) (Ref fc nm' def) = nm == nm'
-isCandidate ty (App fc t u) = isCandidate ty t
-isCandidate _ _ = False
-
--- This is a crude first pass
--- TODO consider ctx
-findMatches : Context -> Val -> List TopEntry -> M (List (Tm, MetaContext))
-findMatches ctx ty [] = pure []
-findMatches ctx ty ((MkEntry _ name type def) :: xs) = do
-  let True = isCandidate ty type | False => findMatches ctx ty xs
-  top <- get
-  -- let ctx = mkCtx (getFC ty)
-  -- FIXME we're restoring state, but the INFO logs have already been emitted
-  -- Also redo this whole thing to run during elab, recheck constraints, etc.
-  mc <- readIORef top.metaCtx
-  catchError(do
-      -- TODO sort out the FC here
-      let fc = getFC ty
-      debug "TRY \{name} : \{pprint [] type} for \{show ty}"
-      -- This check is solving metas, so we save mc below in case we want this solution
-      -- tm <- check (mkCtx fc) (RVar fc name) ty
-      -- FIXME RVar should optionally have qualified names
-      let (QN ns nm) = name
-      tm <- check ctx (RVar fc nm) ty
-      debug "Found \{pprint [] tm} for \{show ty}"
-      mc' <- readIORef top.metaCtx
-      writeIORef top.metaCtx mc
-      ((tm, mc') ::) <$> findMatches ctx ty xs)
-    (\ err => do
-      debug "No match \{show ty} \{pprint [] type} \{showError "" err}"
-      writeIORef top.metaCtx mc
-      findMatches ctx ty xs)
-
-contextMatches : Context -> Val -> M (List (Tm, MetaContext))
-contextMatches ctx ty = go (zip ctx.env (toList ctx.types))
-  where
-    go : List (Val, String, Val) -> M (List (Tm, MetaContext))
-    go [] = pure []
-    go ((tm, nm, vty) :: xs) = do
-      type <- quote ctx.lvl vty
-      let True = isCandidate ty type | False => go xs
-      top <- get
-      mc <- readIORef top.metaCtx
-      catchError(do
-          debug "TRY context \{nm} : \{pprint (names ctx) type} for \{show ty}"
-          unifyCatch (getFC ty) ctx ty vty
-          mc' <- readIORef top.metaCtx
-          writeIORef top.metaCtx mc
-          tm <- quote ctx.lvl tm
-          ((tm, mc') ::) <$> go xs)
-        (\ err => do
-          debug "No match \{show ty} \{pprint (names ctx) type} \{showError "" err}"
-          writeIORef top.metaCtx mc
-          go xs)
-
--- FIXME - decide if we want to count Zero here
-getArity : Tm -> Nat
-getArity (Pi x str icit rig t u) = S (getArity u)
--- Ref or App (of type constructor) are valid
-getArity _ = Z
-
--- Can metas live in context for now?
--- We'll have to be able to add them, which might put gamma in a ref
-
-
-
--- Makes the arg for `solve` when we solve an auto
-makeSpine : Nat -> Vect k BD -> SnocList Val
-makeSpine k [] = [<]
-makeSpine (S k) (Defined :: xs) = makeSpine k xs
-makeSpine (S k) (Bound :: xs) = makeSpine k xs :< VVar emptyFC k [<]
-makeSpine 0 xs = ?fixme
-
-solveAutos : Nat -> List MetaEntry -> M ()
-solveAutos mstart [] = pure ()
-solveAutos mstart ((Unsolved fc k ctx ty AutoSolve _) :: es) = do
-      debug "AUTO solving \{show k} : \{show ty}"
-      -- fill in solved metas in type
-      x <- quote ctx.lvl ty
-      ty <- eval ctx.env CBN x
-      debug "AUTO ---> \{show ty}"
-      -- we want the context here too.
-      top <- get
-      [(tm, mc)] <- case !(contextMatches ctx ty) of
-            [] => findMatches ctx ty $ toList top.defs
-            xs => pure xs
-        | res => do
-          debug "FAILED to solve \{show ty}, matches: \{commaSep $ map (pprint [] . fst) res}"
-          solveAutos mstart es
-      writeIORef top.metaCtx mc
-      val <- eval ctx.env CBN tm
-      debug "SOLUTION \{pprint [] tm} evaled to \{show val}"
-      let sp = makeSpine ctx.lvl ctx.bds
-      solve ctx.env k sp val
-      mc <- readIORef top.metaCtx
-      let mlen = length mc.metas `minus` mstart
-      solveAutos mstart (take mlen mc.metas)
-solveAutos mstart (_ :: es) = solveAutos mstart es
-
 dumpEnv : Context -> M String
 dumpEnv ctx =
   unlines . reverse <$> go (names ctx) 0 (reverse $ zip ctx.env (toList ctx.types)) []
diff --git a/src/Lib/Types.idr b/src/Lib/Types.idr
index 8a1dd89..06d3cd2 100644
--- a/src/Lib/Types.idr
+++ b/src/Lib/Types.idr
@@ -572,21 +572,6 @@ export
 error' : String -> M a
 error' msg = throwError $ E emptyFC msg
 
-export
-freshMeta : Context -> FC -> Val -> MetaKind -> M Tm
-freshMeta ctx fc ty kind = do
-  top <- get
-  mc <- readIORef top.metaCtx
-  debug "fresh meta \{show mc.next} : \{show ty} (\{show kind})"
-  writeIORef top.metaCtx $ { next $= S, metas $= (Unsolved fc mc.next ctx ty kind [] ::) } mc
-  pure $ applyBDs 0 (Meta fc mc.next) ctx.bds
-  where
-    -- hope I got the right order here :)
-    applyBDs : Nat -> Tm -> Vect k BD -> Tm
-    applyBDs k t [] = t
-    -- review the order here
-    applyBDs k t (Bound :: xs) = App emptyFC (applyBDs (S k) t xs) (Bnd emptyFC k)
-    applyBDs k t (Defined :: xs) = applyBDs (S k) t xs
 
 export
 lookupMeta : Nat -> M MetaEntry