diff --git a/Tactics/Common.lean b/Tactics/Common.lean index ac1432ee..1af7140d 100644 --- a/Tactics/Common.lean +++ b/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⟩ diff --git a/Tactics/Sym.lean b/Tactics/Sym.lean index 5a62f834..b0d5621f 100644 --- a/Tactics/Sym.lean +++ b/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 diff --git a/Tactics/Sym/AxEffects.lean b/Tactics/Sym/AxEffects.lean index a0653c11..8c8a6aa5 100644 --- a/Tactics/Sym/AxEffects.lean +++ b/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 = 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 ` against the state stored in `eff` diff --git a/Tactics/Sym/Context.lean b/Tactics/Sym/Context.lean index 39f6f4ed..e38c1ee0 100644 --- a/Tactics/Sym/Context.lean +++ b/Tactics/Sym/Context.lean @@ -11,8 +11,10 @@ import Tactics.Common import Tactics.Attr import Tactics.Sym.ProgramInfo import Tactics.Sym.AxEffects +import Tactics.Sym.LCtxSearch import Tactics.Simp + /-! This files defines the `SymContext` structure, which collects the names of various @@ -218,6 +220,22 @@ def traceSymContext : SymM Unit := let m ← (← getThe SymContext).toMessageData trace[Tactic.sym] m +/-! ## Adding new simp theorems for aggregation -/ + +/-- Add a set of new simp-theorems to the simp-theorems used +for effect aggregation -/ +def addSimpTheorems (c : SymContext) (simpThms : Array SimpTheorem) : SymContext := + let addSimpThms := simpThms.foldl addSimpTheoremEntry + + let oldSimpTheorems := c.aggregateSimpCtx.simpTheorems + let simpTheorems := + if oldSimpTheorems.isEmpty then + oldSimpTheorems.push <| addSimpThms {} + else + oldSimpTheorems.modify (oldSimpTheorems.size - 1) addSimpThms + + { c with aggregateSimpCtx.simpTheorems := simpTheorems } + /-! ## Creating initial contexts -/ /-- Modify a `SymContext` with a monadic action `k : SymM Unit` -/ @@ -225,6 +243,34 @@ def modify (ctxt : SymContext) (k : SymM Unit) : TacticM SymContext := do let ((), ctxt) ← SymM.run ctxt k return ctxt +private def initial (state : Expr) : MetaM SymContext := do + /- Create an mvar for the final state -/ + let finalState ← mkFreshExprMVar mkArmState + /- Get the default simp lemmas & simprocs for aggregation -/ + let (aggregateSimpCtx, aggregateSimprocs) ← + LNSymSimpContext (config := {decide := true, failIfUnchanged := false}) + let aggregateSimpCtx := { aggregateSimpCtx with + -- Create a new discrtree for effect hypotheses to be added to. + -- TODO(@alexkeizer): I put this here, since the previous version kept + -- a seperate discrtree for lemmas. I should run benchmarks to see what + -- happens if we keep everything in one simpset. + simpTheorems := aggregateSimpCtx.simpTheorems.push {} + } + return { + finalState + runSteps? := none + h_run := `dummyValue + programInfo := { + name := `dummyValue + instructions := ∅ + } + pc := 0 + h_sp? := none + aggregateSimpCtx, + aggregateSimprocs, + effects := AxEffects.initial state + } + /-- Infer `state_prefix` and `curr_state_number` from the `state` name as follows: if `state` is `s{i}` for some number `i` and a single character `s`, then `s` is the prefix and `i` the number, @@ -259,16 +305,127 @@ private def withErrorContext (name : Name) (type? : Option Expr) (k : MetaM α) | none => m!"" throwErrorAt e.getRef "{e.toMessageData}\n\nIn {h}{type}" -/-- Build a `SymContext` by searching the local context for hypotheses of the -required types (up-to defeq) . The local context is modified to unfold the types -to be syntactically equal to the expected type. +-- protected def AxEffects.searchFor + +/-- Build the lazy search structure (for use with `searchLCtx`) +to populate the `SymContext` state from the local context. + +NOTE: some search might be performed eagerly. The resulting search structure +is tied to the specific `SymM` state and local context, it's expected that +neither of these change between construction and execution of the search. -/ +protected def searchFor : SearchLCtxForM SymM Unit := do + let c ← getThe SymContext + let currentState ← AxEffects.getCurrentState + + /- We start by doing an eager search for `h_run`, outside the `SearchLCxtForM` + monad. This is needed to instantiate the initial state -/ + let runSteps ← mkFreshExprMVar (Expr.const ``Nat []) + let hRunType := h_run_type c.finalState runSteps currentState + let some hRun ← findLocalDeclOfType? hRunType + | throwNotFound hRunType + + let runSteps? ← reflectNatLiteral? runSteps + if runSteps?.isNone then + trace[Tactic.sym] "failed to reflect {runSteps} \ + (from {hRun.toExpr} : {hRun.type})" + + modifyThe SymContext ({ · with + h_run := hRun.userName + finalState := ←instantiateMVars c.finalState + runSteps? + }) + + /- + From here on out, we're building the lazy search patterns + -/ + -- Find `h_program : .program = ` + let program ← mkFreshExprMVar none + searchLCtxForOnce (h_program_type currentState program) + (whenNotFound := throwNotFound) + (whenFound := fun decl _ => do + -- Register the program proof + modifyThe AxEffects ({· with + programProof := decl.toExpr + }) + -- Assert that `program` is a(n application of a) constant + let program := (← instantiateMVars program).getAppFn + let .const program _ := program + | throwError "Expected a constant, found:\n\t{program}" + -- Retrieve the programInfo from the environment + let some programInfo ← ProgramInfo.lookup? program + | throwError "Could not find program info for `{program}`.\n\ + Did you remember to generate step theorems with:\n \ + #generateStepEqTheorems {program}" + modifyThe SymContext ({· with + programInfo + }) + ) + + -- Find `h_pc : r .PC = ` + let pc ← mkFreshExprMVar (← mkAppM ``BitVec #[toExpr 64]) + searchLCtxForOnce (h_pc_type currentState pc) + (changeType := true) + (whenNotFound := throwNotFound) + (whenFound := fun decl _ => do + let pc ← instantiateMVars pc + -- Set the field effect + AxEffects.setFieldEffect .PC { + value := pc + proof := decl.toExpr + } + -- Then, reflect the value + let pc ← withErrorContext decl.userName decl.type <| + reflectBitVecLiteral 64 pc + modifyThe SymContext ({ · with pc }) + ) + + -- Find `h_err : r .ERR = .None`, or add a new subgoal if it isn't found + searchLCtxForOnce (h_err_type currentState) + (changeType := true) + (whenFound := fun decl _ => + AxEffects.setErrorProof decl.toExpr + ) + (whenNotFound := fun _ => do + let errHyp ← mkFreshExprMVar (h_err_type currentState) + replaceMainGoal [← getMainGoal, errHyp.mvarId!] + AxEffects.setErrorProof errHyp + ) + + -- Find `h_sp : CheckSPAlignment `. + searchLCtxForOnce (h_sp_type currentState) + (changeType := true) + (whenNotFound := traceNotFound `Tactic.sym) + -- ^^ Note that `h_sp` is optional, so there's no need to throw an error, + -- we merely add a message to the trace and move on + (whenFound := fun decl _ => do + modifyThe AxEffects ({ · with + stackAlignmentProof? := some decl.toExpr + }) + modifyThe SymContext ({· with + h_sp? := decl.userName + }) + ) + + /- TODO(@alexkeizer): search for any other hypotheses of the form + `r ?field = _`, and record those. + Keeping in mind that we have to do this search AFTER `h_pc` or `h_err`, to + ensure those field-specific searches take priority. + Also, maybe for memory-reads as well? Or we can hold off on that untill + after the equality refactor -/ + + return () + +/-- Build a `SymContext` by searching the local context of the main goal for +hypotheses of the required types (up-to defeq). +The local context is modified to unfold the types to be syntactically equal to +the expected types. If an hypothesis `h_err : r .ERR = None` is not found, -we create a new subgoal of this type +we create a new subgoal of this type. -/ -def fromLocalContext (state? : Option Name) : TacticM SymContext := do +def fromMainContext (state? : Option Name) : TacticM SymContext := do let msg := m!"Building a `SymContext` from the local context" - withTraceNode `Tactic.sym (fun _ => pure msg) do + withTraceNode `Tactic.sym (fun _ => pure msg) <| withMainContext' do trace[Tactic.Sym] "state? := {state?}" let lctx ← getLCtx @@ -281,131 +438,16 @@ def fromLocalContext (state? : Option Name) : TacticM SymContext := do pure (Expr.fvar decl.fvarId) | none => mkFreshExprMVar (Expr.const ``ArmState []) - -- Find `h_run` - let finalState ← mkFreshExprMVar none - let runSteps ← mkFreshExprMVar (Expr.const ``Nat []) - let h_run ← - findLocalDeclOfTypeOrError <| h_run_type finalState runSteps stateExpr - - -- Unwrap and reflect `runSteps` - let runSteps? ← do - let msg := m!"Reflecting: {runSteps}" - withTraceNode `Tactic.sym (fun _ => pure msg) <| do - let runSteps? ← reflectNatLiteral? runSteps - trace[Tactic.sym] "got: {runSteps?}" - pure runSteps? - let finalState ← instantiateMVars finalState - - -- At this point, `stateExpr` should have been assigned (if it was an mvar), - -- so we can unwrap it to get the underlying name - let stateExpr ← instantiateMVars stateExpr - - -- Try to find `h_program`, and infer `program` from it - let ⟨h_program, program⟩ ← withErrorContext h_run.userName h_run.type <| - findProgramHyp stateExpr - - -- Then, try to find `h_pc` - let pcE ← mkFreshExprMVar (← mkAppM ``BitVec #[toExpr 64]) - let h_pc ← findLocalDeclOfTypeOrError <| h_pc_type stateExpr pcE - - -- Unwrap and reflect `pc` - let pcE ← instantiateMVars pcE - let pc ← withErrorContext h_pc.userName h_pc.type <| - reflectBitVecLiteral 64 pcE - - -- Attempt to find `h_err`, adding a new subgoal if it couldn't be found - let errHyp ← do - let h_err? ← findLocalDeclOfType? (h_err_type stateExpr) - match h_err? with - | some d => pure d.toExpr - | none => do - let errHyp ← mkFreshExprMVar (h_err_type stateExpr) - replaceMainGoal [← getMainGoal, errHyp.mvarId!] - pure errHyp - - let h_sp? ← findLocalDeclOfType? (h_sp_type stateExpr) - if h_sp?.isNone then - trace[Sym] "Could not find local hypothesis of type {h_sp_type stateExpr}" - - -- Finally, retrieve the programInfo from the environment - let some programInfo ← ProgramInfo.lookup? program - | throwError "Could not find program info for `{program}`. - Did you remember to generate step theorems with: - #generateStepEqTheorems {program}" - - -- Initialize the axiomatic hypotheses with hypotheses for the initial state - let axHyps := #[h_program, h_pc] ++ h_sp?.toArray - let (aggregateSimpCtx, aggregateSimprocs) ← - LNSymSimpContext - (config := {decide := true, failIfUnchanged := false}) - (decls := axHyps) - (exprs := #[errHyp]) - (noIndexAtArgs := false) - - -- Build an initial AxEffects - let effects := AxEffects.initial stateExpr - let effects := { effects with - fields := effects.fields - |>.insert .PC { value := pcE, proof := h_pc.toExpr} - |>.insert .ERR { value := mkConst ``StateError.None, proof := errHyp} - programProof := h_program.toExpr - stackAlignmentProof? := h_sp?.map (·.toExpr) - } - let c : SymContext := { - finalState, runSteps?, pc, - h_run := h_run.userName, - h_sp? := (·.userName) <$> h_sp?, - programInfo, - effects, - aggregateSimpCtx, aggregateSimprocs - } - c.modify <| - inferStatePrefixAndNumber -where - findLocalDeclOfType? (expectedType : Expr) : MetaM (Option LocalDecl) := do - let msg := m!"Searching for hypothesis of type: {expectedType}" - withTraceNode `Tactic.sym (fun _ => pure msg) <| do - let decl? ← _root_.findLocalDeclOfType? expectedType - trace[Tactic.sym] "Found: {(·.toExpr) <$> decl?}" - return decl? - findLocalDeclOfTypeOrError (expectedType : Expr) : MetaM LocalDecl := do - let msg := m!"Searching for hypothesis of type: {expectedType}" - withTraceNode `Tactic.sym (fun _ => pure msg) <| do - let decl ← _root_.findLocalDeclOfTypeOrError expectedType - trace[Tactic.sym] "Found: {decl.toExpr}" - return decl - -/-! ## Massaging the local context -/ - -/-- change the type (in the local context of the main goal) -of the hypotheses tracked by the given `SymContext` to be *exactly* of the shape -described in the relevant docstrings. - -That is, (un)fold types which were definitionally, but not syntactically, -equal to the expected shape. -/ -def canonicalizeHypothesisTypes : SymReaderM Unit := withMainContext' do - let c ← readThe SymContext - let lctx ← getLCtx - let mut goal ← getMainGoal - let state := c.effects.currentState - - let mut hyps := #[] - if let some runSteps := c.runSteps? then - hyps := hyps.push (c.h_run, h_run_type c.finalState (toExpr runSteps) state) - if let some h_sp := c.h_sp? then - hyps := hyps.push (h_sp, h_sp_type state) - - let mut hypIds ← hyps.mapM fun ⟨name, type⟩ => do - let some decl := lctx.findFromUserName? name - | throwError "Unknown local hypothesis `{name}`" - pure (decl.fvarId, type) - - let errHyp ← AxEffects.getFieldM .ERR - if let Expr.fvar id := errHyp.proof then - hypIds := hypIds.push (id, h_err_type state) - for ⟨fvarId, type⟩ in hypIds do - goal ← goal.replaceLocalDeclDefEq fvarId type - replaceMainGoal [goal] + -- We create a bogus initial context + let c ← SymContext.initial stateExpr + c.modify <| do + searchLCtx SymContext.searchFor + + withMainContext' <| do + let thms ← (← readThe AxEffects).toSimpTheorems + modifyThe SymContext (·.addSimpTheorems thms) + + inferStatePrefixAndNumber /-! ## Incrementing the context to the next state -/ @@ -431,17 +473,3 @@ def prepareForNextStep : SymM Unit := do runSteps? := (· - 1) <$> c.runSteps? currentStateNumber := c.currentStateNumber + 1 }) - -/-- Add a set of new simp-theorems to the simp-theorems used -for effect aggregation -/ -def addSimpTheorems (c : SymContext) (simpThms : Array SimpTheorem) : SymContext := - let addSimpThms := simpThms.foldl addSimpTheoremEntry - - let oldSimpTheorems := c.aggregateSimpCtx.simpTheorems - let simpTheorems := - if oldSimpTheorems.isEmpty then - oldSimpTheorems.push <| addSimpThms {} - else - oldSimpTheorems.modify (oldSimpTheorems.size - 1) addSimpThms - - { c with aggregateSimpCtx.simpTheorems := simpTheorems } diff --git a/Tactics/Sym/LCtxSearch.lean b/Tactics/Sym/LCtxSearch.lean new file mode 100644 index 00000000..58d4c3ea --- /dev/null +++ b/Tactics/Sym/LCtxSearch.lean @@ -0,0 +1,214 @@ +/- +Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Author(s): Alex Keizer +-/ +import Lean + +open Lean + +/-! +## Local Context Search + +In this module we build an abstraction around searching the local context for +multiple local variables or hypotheses at the same time. + +The main entry point to search is `searchLocalContext`. +`searchFor` is the main way to register which patterns to search for, +and what actions to perform if the variable is found (or not found). +-/ + +variable (m) [Monad m] + +inductive LCtxSearchResult + /-- This occurence of the pattern should be ignored -/ + | skip + /-- This should be counted as a successful occurence, + and we should *continue* matching for more variables -/ + | continu + /-- This should be counted as a successful occurence, + and we can *stop* matching against this particular pattern -/ + | done + deriving DecidableEq + +structure LCtxSearchState.Pattern where + /-- The type to search for (up to def-eq!). + Notice that `expectedType` is stored as a monadic value, + so that we can create fresh metavariables for each search -/ + expectedType : m Expr + /-- A cached result of `expectedType`; + this should be regenerated after every match! -/ + cachedExpectedType : Expr + /-- `whenFound` will be called whenever a match for `pattern` is found, + with the instantiated pattern as an argument. + The returned `LCtxSearchResult` determines if we count this as a successful + occurence of the pattern, which is relevant for if `whenNotFound` is called. + + NOTE: We give the (instantiated) pattern as an arg, *not* the expression that + we matched against. This way, implementors can recover information through + syntactic destructuring. + + An alternative design would have `pattern : MetaM (List Expr × Expr)`, + where the list is intended to be a list of meta-variables, and + `whenFound : List Expr → Expr → m Unit`, where we would call + `whenFound` with the list returned by `pattern` (which has the metavariables + that should now have been instantiated with subexpressions of interest). + -/ + whenFound : LocalDecl → Expr → m LCtxSearchResult + /-- `whenNotFound` will be called if no successful occurence of the pattern + (as determined by the return value of `whenFound`) + could be found in the local context -/ + whenNotFound : Expr → m Unit + /-- Whether to change the type of successful matches -/ + changeType : Bool + /-- How many times have we (successfully) found the pattern -/ + occurences : Nat := 0 + /-- Whether the pattern is active; is `isActive = false`, + then no further matches are attempted -/ + isActive : Bool := true + +structure LCtxSearchState where + patterns : Array (LCtxSearchState.Pattern m) + +abbrev SearchLCtxForM := StateT (LCtxSearchState m) m + +variable {m} + +/-- register a new expression pattern to search for: +- `expectedType` should give an expression, with meta-variables, which is the + type to search for. + + Note that, once a match is found, any meta-variables in `expectedType` will be + assigned, and thus further matches will now need to match those same concrete + values. That is why `expectedType` is a monadic value, which is re-evaluated + after each successful match. + If multiple matches, with distinct instantiations of a meta-variable, are + desired, it's important that meta-variable is created *inside* the + `expectedType` action. + If, on the other hand, a single instantiation accross all variables is + desired, the meta-variable should be created *outside*. +- `whenFound` will be called whenever a local variable whose type is def-eq + to `expectedType` is found, with as argument the instantiated `expectedType`. + The return value of `whenFound` is used to determine if a match is considered + succesful. +- `whenNotFound` will be called if no local variable could be found with a type + def-eq to the pattern, or if `whenFound` returned `skip` for all variables + that were found. For convenience, we pass in the `expectedType` here as well. + See `throwNotFound` for a convenient way to throw an error here. +- If `changeType` is set to true, then we change the type of every successful + match (i.e., `whenFound` returns `continu` or `done`) to be exactly the + `expectedType` + +WARNING: Once a pattern is found for which `whenFound` returns `done`, that +particular variable will not be matched for any other patterns. +In case of overlapping patterns, the pattern which was added first will be +tried first +-/ +def searchLCtxFor + (expectedType : m Expr) + (whenFound : LocalDecl → Expr → m LCtxSearchResult) + (whenNotFound : Expr → m Unit := fun _ => pure ()) + (changeType : Bool := false) + : SearchLCtxForM m Unit := do + let pattern := { + -- Placeholder value, since we can't evaluate `m` inside of `LCtxSearchM` + cachedExpectedType :=← expectedType + expectedType, whenFound, whenNotFound, changeType + } + modify fun state => { state with + patterns := state.patterns.push pattern + } + +/-- A wrapper around `searchLCtxFor`, which is simplified for matching at most +one occurence of `expectedType`. + +See `searchLCtxFor` for an explanation of the arguments -/ +def searchLCtxForOnce + (expectedType : Expr) + (whenFound : LocalDecl → Expr → m Unit) + (whenNotFound : Expr → m Unit := fun _ => pure ()) + (changeType : Bool := false) + : SearchLCtxForM m Unit := do + searchLCtxFor (pure expectedType) + (fun d e => do whenFound d e; return .done) + whenNotFound changeType + +section Run +open Elab.Tactic +open Meta (isDefEq) +variable [MonadLCtx m] [MonadLiftT MetaM m] [MonadLiftT TacticM m] + +/-- +Attempt to match `e` against the given pattern: +- if `e` is def-eq to `pat.cachedExpectedType`, then return + the updated pattern state (with a fresh `cachedExpectedType`), and + the result of `whenFound` +- Otherwise, if `e` is not def-eq, return `none` +-/ +def LCtxSearchState.Pattern.match? (pat : Pattern m) (decl : LocalDecl) : + m (Option (Pattern m × LCtxSearchResult)) := do + if !pat.isActive then + return none + else if !(← isDefEq decl.type pat.cachedExpectedType) then + return none + else + let cachedExpectedType ← pat.expectedType + let res ← pat.whenFound decl pat.cachedExpectedType + let mut occurences := pat.occurences + if res != .skip then + occurences := occurences + 1 + if pat.changeType = true then + let goal ← getMainGoal + let goal ← goal.replaceLocalDeclDefEq decl.fvarId pat.cachedExpectedType + replaceMainGoal [goal] + return some ({pat with cachedExpectedType, occurences}, res) + +/-- Search the local context for variables of certain types, in a single pass. +`k` is a monadic continuation that determines the patterns to search for, +see `searchLCtxFor` to see how to register those patterns +-/ +def searchLCtx (k : SearchLCtxForM m Unit) : m Unit := do + let ((), { patterns }) ← StateT.run k ⟨#[]⟩ + -- We have to keep `patterns` in a Subtype to be able to prove our indexes + -- are valid even after mutation + -- TODO(@alexkeizer): consider using `Batteries.Data.Vector`, if we can + -- justify a batteries dependency + let n := patterns.size + let mut patterns : { as : Array _ // as.size = n} := + ⟨patterns, rfl⟩ + + -- The main search + for decl in ← getLCtx do + for hi : i in [0:n] do + have hi : i < patterns.val.size := by + rw [patterns.property]; get_elem_tactic + let pat := patterns.val[i] + if let some (pat, res) ← pat.match? decl then + patterns := ⟨ + patterns.val.set ⟨i, hi⟩ pat, + by simp[patterns.property] + ⟩ + if res = .done || res = .continu then + break -- break out of the inner loop + + -- Finally, check each pattern and call `whenNotFound` if appropriate + for pat in patterns.val do + if pat.occurences = 0 then + pat.whenNotFound pat.cachedExpectedType + return () + +variable [MonadError m] in +/-- Throw an error complaining that no variable of `expectedType` could +be found -/ +def throwNotFound (expectedType : Expr) : m Unit := + throwError "Expected a local variable of type:\n {expectedType}\n\ + but no such variable was found in the local context" + +/-- Add a message to the trace that we searched for, but couldn't find, +a variable of `expectedType`, and continue execution. -/ +def traceNotFound (cls : Name) (expectedType : Expr) : m Unit := + trace (m:=MetaM) cls fun _ => + m!"Unable to find a variable of type {expectedType} in the local context" + + +end Run