summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSon Ho2024-06-17 06:26:43 +0200
committerSon Ho2024-06-17 06:26:43 +0200
commit007c9024c0c3b549049a55243b391ae2337ad616 (patch)
tree45a941bee7e7bce03154b10b303910942f1328ed
parente57e6f08e5cc34bf4e9237650f5ecbab440b9ea2 (diff)
Make a minor cleanup
Diffstat (limited to '')
-rw-r--r--backends/lean/Base/Arith/Int.lean20
1 files changed, 11 insertions, 9 deletions
diff --git a/backends/lean/Base/Arith/Int.lean b/backends/lean/Base/Arith/Int.lean
index ab6dd4ab..068d6f2f 100644
--- a/backends/lean/Base/Arith/Int.lean
+++ b/backends/lean/Base/Arith/Int.lean
@@ -112,9 +112,10 @@ def collectInstancesFromMainCtx (k : Expr → MetaM (Option Expr)) : Tactic.Tact
-- Explore the declarations
let decls ← ctx.getDecls
let hs ← decls.foldlM (fun hs d => do
- -- Collect instances over all subexpressions
- -- of the inferred type rather than the declaration expression
- -- which is often just a name.
+ -- Collect instances over all subexpressions in the context.
+ -- Note that we explore the *type* of the local declarations: if we have
+ -- for instance `h : A ∧ B` in the context, the expression itself is simply
+ -- `h`; the information we are interested in is its type.
let ty ← Lean.Meta.inferType d.toExpr
collectInstances k hs ty
) hs
@@ -122,26 +123,27 @@ def collectInstancesFromMainCtx (k : Expr → MetaM (Option Expr)) : Tactic.Tact
collectInstances k hs (← Tactic.getMainTarget)
-- Helper
-def lookupProp (fName : String) (className : Name) (e : Expr) (instantiateClassFn : Expr → Expr → Array Expr) (instantiateProjectionFn : Expr → Array Expr) : MetaM (Option Expr) := do
+def lookupProp (fName : String) (className : Name) (e : Expr)
+ (instantiateClassFn : Expr → MetaM (Array Expr))
+ (instantiateProjectionFn : Expr → MetaM (Array Expr)) : MetaM (Option Expr) := do
trace[Arith] fName
-- TODO: do we need Lean.observing?
-- This actually eliminates the error messages
trace[Arith] m!"{fName}: {e}"
Lean.observing? do
trace[Arith] m!"{fName}: observing: {e}"
- let ty ← Lean.Meta.inferType e
- let hasProp ← mkAppM className (instantiateClassFn ty e)
+ let hasProp ← mkAppM className (← instantiateClassFn e)
let hasPropInst ← trySynthInstance hasProp
match hasPropInst with
| LOption.some i =>
trace[Arith] "Found {fName} instance"
let i_prop ← mkProjection i (Name.mkSimple "prop")
- some (← mkAppM' i_prop (instantiateProjectionFn e))
+ some (← mkAppM' i_prop (← instantiateProjectionFn e))
| _ => none
-- Return an instance of `HasIntProp` for `e` if it has some
def lookupHasIntProp (e : Expr) : MetaM (Option Expr) :=
- lookupProp "lookupHasIntProp" ``HasIntProp e (fun ty _ => #[ty]) (fun e => #[e])
+ lookupProp "lookupHasIntProp" ``HasIntProp e (fun e => do pure #[← Lean.Meta.inferType e]) (fun e => pure #[e])
-- Collect the instances of `HasIntProp` for the subexpressions in the context
def collectHasIntPropInstancesFromMainCtx : Tactic.TacticM (HashSet Expr) := do
@@ -149,7 +151,7 @@ def collectHasIntPropInstancesFromMainCtx : Tactic.TacticM (HashSet Expr) := do
-- Return an instance of `HasIntPred` for `e` if it has some
def lookupHasIntPred (e : Expr) : MetaM (Option Expr) :=
- lookupProp "lookupHasIntPred" ``HasIntPred e (fun _ term => #[term]) (fun _ => #[])
+ lookupProp "lookupHasIntPred" ``HasIntPred e (fun term => pure #[term]) (fun _ => pure #[])
-- Collect the instances of `HasIntPred` for the subexpressions in the context
def collectHasIntPredInstancesFromMainCtx : Tactic.TacticM (HashSet Expr) := do