Merge pull request leanprover#189 from leanprover/refactor-state-mona…

…ds-5

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

Tactics/Common.lean

@@ -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⟩
 

Tactics/Sym.lean

@@ -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
 
 /--
@@ -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

Tactics/Sym/AxEffects.lean

@@ -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`