MonadTC: add getInstance + findInstance

Class/MonadTC.agda

@@ -92,6 +92,7 @@ record MonadTC (M : ∀ {f} → Set f → Set f)
     isMacro          : Name → M Bool
     debugPrint       : String → ℕ → List ErrorPart → M ⊤
     runSpeculative   : M (A × Bool) → M A
+    getInstances     : Meta → M (List Term)
 
   instance _ = Functor-M
   open MonadError me
@@ -351,5 +352,19 @@ module _ {M : ∀ {f} → Set f → Set f}
     runWithHole hole tac
     return hole
 
+  -- Finding all instance candidates of a given type.
+  findInstances : Type → M (List Term)
+  findInstances ty = runAndReset $ do
+    just m ← findMeta <$> newMeta ty
+      where _ → error1 "[findInstances] newMeta did not produce meta-variable!"
+    getInstances m
+    where
+      open import Data.Maybe using (_<∣>_)
+      findMeta = λ where
+        (pi (arg _ ty) (abs _ t)) → findMeta ty <∣> findMeta t
+        (lam _ (abs _ t))         → findMeta t
+        (meta m _)                → just m
+        _                         → nothing
+
 MonadTC-TC : MonadTC R.TC ⦃ Monad-TC ⦄ ⦃ MonadError-TC ⦄
-MonadTC-TC = record { R; R' using (quoteωTC; withReconstructed; onlyReduceDefs; dontReduceDefs) }
+MonadTC-TC = record { R; R' using (quoteωTC; withReconstructed; onlyReduceDefs; dontReduceDefs; getInstances) }

Reflection/TCI.agda

@@ -128,5 +128,8 @@ module MonadTCI where
   runSpeculative    : TC (A × Bool) → TC A
   runSpeculative    = R.runSpeculative ∘_
 
+  getInstances      : Meta → TC (List Term)
+  getInstances      = liftTC1 R'.getInstances
+
 MonadTC-TCI : MonadTC TC ⦃ Monad-TC ⦄ ⦃ MonadError-TC ⦄
 MonadTC-TCI = record { MonadTCI }

Reflection/Utils.agda

@@ -170,9 +170,8 @@ module _ (f : ℕ → ℕ) where
 
     mapFreeVarsᶜ : ℕ → (Clause → Clause)
     mapFreeVarsᶜ b = λ where
-      -- clause        : (tel : List (Σ String λ _ → Arg Type)) (ps : List (Arg Pattern)) (t : Term) → Clause
-      (clause tel ps t) → clause (mapFreeVarsᵗ b tel) (mapFreeVarsᵖ∗ b ps) (mapFreeVars (length tel + b) t)
-      -- absurd-clause : (tel : List (Σ String λ _ → Arg Type)) (ps : List (Arg Pattern)) → Clause
+      (clause tel ps t) → clause (mapFreeVarsᵗ b tel) (mapFreeVarsᵖ∗ b ps)
+                                 (mapFreeVars (length tel + b) t)
       (absurd-clause tel ps) → absurd-clause (mapFreeVarsᵗ b tel) (mapFreeVarsᵖ∗ b ps)
     mapFreeVarsᶜ∗ : ℕ → (List Clause → List Clause)
     mapFreeVarsᶜ∗ b = λ where
@@ -240,6 +239,7 @@ apply⋯ is n = def n $ remove-iArgs $
   map (λ{ (n , arg i _) → arg i (♯ (length is ∸ suc (toℕ n)))}) (zip (allFin $ length is) is)
 
 -- ** records
+
 mkRecord : List (Name × Term) → Term
 mkRecord fs = pat-lam (map (λ where (fn , e) → clause [] [ vArg (proj fn) ] e) fs) []