Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

feat: LCtxSearch abstraction to search the local context in a single pass #189

Merged
merged 16 commits into from
Sep 30, 2024
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 1 addition & 2 deletions Tactics/Common.lean
Original file line number Diff line number Diff line change
Expand Up @@ -242,8 +242,7 @@ def findProgramHyp (state : Expr) : MetaM (LocalDecl × Name) := do
-- Assert that `program` is a(n application of a) constant, and find its name
let program := (← instantiateMVars program).getAppFn
let .const program _ := program
| -- withErrorContext h_run h_run_type <|
throwError "Expected a constant, found:\n\t{program}"
| throwError "Expected a constant, found:\n\t{program}"

return ⟨h_program, program⟩

Expand Down
9 changes: 3 additions & 6 deletions Tactics/Sym.lean
Original file line number Diff line number Diff line change
Expand Up @@ -244,7 +244,7 @@ elab "explode_step" h_step:term " at " state:term : tactic => withMainContext do
let .fvar stateFVar := state
| throwError "Expected fvar, found {state}"
let stateDecl := (← getLCtx).get! stateFVar
let c ← SymContext.fromLocalContext (some stateDecl.userName)
let c ← SymContext.fromMainContext (some stateDecl.userName)
let _ ← SymM.run c <| explodeStep hStep

/--
Expand Down Expand Up @@ -403,11 +403,8 @@ elab "sym_n" whileTac?:(sym_while)? n:num s:(sym_at)? : tactic => do
omega;
))

let c ← withMainContext <| SymContext.fromLocalContext s
SymM.run' c <| do
-- Context preparation
canonicalizeHypothesisTypes

let c ← SymContext.fromMainContext s
SymM.run' c <| withMainContext' <| do
-- Check pre-conditions
assertStepTheoremsGenerated
let n ← ensureAtMostRunSteps n.getNat
Expand Down
27 changes: 26 additions & 1 deletion Tactics/Sym/AxEffects.lean
Original file line number Diff line number Diff line change
Expand Up @@ -231,11 +231,36 @@ def getField (eff : AxEffects) (fld : StateField) : MetaM FieldEffect :=
let proof ← eff.mkAppNonEffect (toExpr fld)
pure { value, proof }

variable {m} [Monad m] [MonadReaderOf AxEffects m] [MonadLiftT MetaM m] in
section Monad
variable {m} [Monad m] [MonadLiftT MetaM m]

variable [MonadReaderOf AxEffects m] in
@[inherit_doc getField]
def getFieldM (field : StateField) : m FieldEffect := do
(← read).getField field

variable [MonadStateOf AxEffects m]

/-- Set the effect of a specific field in the monad state, overwriting any
previous value for that field.

NOTE: the proof in `effect` is assumed to be valid for the current state,
this is not eagerly checked (but the kernel will of course eventually reject
a proof if it used a malformed field-effect; a mallformed proof does not
compromise soundness, but it will cause obscure errors) -/
def setFieldEffect (field : StateField) (effect : FieldEffect) : m Unit :=
modify fun eff => { eff with
fields := eff.fields.insert field effect }

/-- Given a proof that `r .ERR <currentState> = None`, set the effect of the
`ERR` field accordingly.

This is a specialization of `setFieldEffect`. -/
def setErrorProof (proof : Expr) : m Unit :=
setFieldEffect .ERR { value := mkConst ``StateError.None, proof }

end Monad

/-! ## Update a Reflected State -/

/-- Execute `write_mem <n> <addr> <val>` against the state stored in `eff`
Expand Down
Loading
Loading