From 5f41cb69e40f87357f91137b6cacf353996b5cb2 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 30 Oct 2019 14:56:01 -0700 Subject: [PATCH] feat: `TmpMetavarContext` --- library/Init/Lean/TmpMetavarContext.lean | 131 +++++++++++++++++++++++ 1 file changed, 131 insertions(+) create mode 100644 library/Init/Lean/TmpMetavarContext.lean diff --git a/library/Init/Lean/TmpMetavarContext.lean b/library/Init/Lean/TmpMetavarContext.lean new file mode 100644 index 0000000000..71201e3122 --- /dev/null +++ b/library/Init/Lean/TmpMetavarContext.lean @@ -0,0 +1,131 @@ +/- +Copyright (c) 2019 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Leonardo de Moura +-/ +prelude +import Init.Lean.MetavarContext + +namespace Lean +/-- + Several procedures (e.g., type class resolution, simplifier) need + to create metavariables that are needed for a short period of time. + For example, when applying a simplification lemma such as + ``` + forall x, f x x = x + ``` + to a subterm `t`, we need need to check whether the term + `t` is an instance of the pattern `f ?x ?x`, where `?x` is a fresh metavariable. + That is, we need to find an assignment for `?x` such that `t` + and `f ?x ?x` become definitionally equal. If the assignment is found, + we replace the term `t` with the term assigned to `?x`. After that, + we don't need the metavariable `?x` anymore. We don't want to + use regular metavariables for this operation since we don't want + to waste time declaring them at `MetavarContext`, + then creating the term `f ?x ?x` with the newly created metavariable, + and then performing the matching operation, and finally deleting `?x`. + We avoid this overhead by using temporary metavariables. + + `TmpMetavarContext` implements `AbstractMetavarContext` for temporary metavariables. + All temporary metavariables used to solve a particular problem (e.g., matching) + share the same local context (field `mvarLCtx`), the type of a metavariable is stored in the + field `mvarTypes`. The assignments are implemented using small arrays. + We assume the number of temporary metavariables is usually small (< 1000), + and their names store a small integer that is used to read the arrays. + + `TmpMetavarContext` also keeps a reference to the main `MetavarContext` used in the elaborator and + tactic framework. -/ +structure TmpMetavarContext := +(mctx : MetavarContext := {}) +(mvarLCtx : LocalContext := {}) +(mvarTypes : Array Expr := #[]) +(lAssignment : Array (Option Level) := #[]) +(eAssignment : Array (Option Expr) := #[]) + +def mkTmpMVarId (idx : Nat) := +Name.mkNumeral `_tmp idx + +def Name.isTmpMVarId : Name → Bool +| Name.mkNumeral `_tmp _ => true +| _ => false + +def Name.getTmpMVarIdx : Name → Nat +| Name.mkNumeral _ i => i +| _ => panic! "expected a temporary metavariable name" + +def Level.isTmpMVar : Level → Bool +| Level.mvar mvarId => mvarId.isTmpMVarId +| _ => false + +def Expr.isTmpMVar : Expr → Bool +| Expr.mvar mvarId => mvarId.isTmpMVarId +| _ => false + +/-- + Create a temporary metavariable context with the following characteristics: + - It contains `numLevelMVars` temporary `Level` metavariables + - It contains `mvarTypes.size` temporary `Expr` metavariables + - The temporary metavariable `i` has type `mvarTypes[i]` + - All temporary metavariables have local context `mvarLCtx` + + `mctx` is the main metavariable context, and it is used to + retrieve regular metavariable information. -/ +def mkTmpMetavarContext (mctx : MetavarContext) (mvarLCtx : LocalContext) (mvarTypes : Array Expr) (numLevelMVars : Nat) : TmpMetavarContext := +{ mctx := mctx, + mvarLCtx := mvarLCtx, + mvarTypes := mvarTypes, + eAssignment := mkArray mvarTypes.size none, + lAssignment := mkArray numLevelMVars none } + +namespace TmpMetavarContext + +instance : Inhabited TmpMetavarContext := ⟨{}⟩ + +def getLevelAssignment (m : TmpMetavarContext) (mvarId : Name) : Option Level := +if mvarId.isTmpMVarId then + m.lAssignment.get! mvarId.getTmpMVarIdx +else + m.mctx.getLevelAssignment mvarId + +def assignLevel (m : TmpMetavarContext) (mvarId : Name) (val : Level) : TmpMetavarContext := +if mvarId.isTmpMVarId then + { lAssignment := m.lAssignment.set! mvarId.getTmpMVarIdx val, .. m } +else + { mctx := m.mctx.assignLevel mvarId val, .. } + +def getExprAssignment (m : TmpMetavarContext) (mvarId : Name) : Option Expr := +if mvarId.isTmpMVarId then + m.eAssignment.get! mvarId.getTmpMVarIdx +else + m.mctx.getExprAssignment mvarId + +def assignExpr (m : TmpMetavarContext) (mvarId : Name) (val : Expr) : TmpMetavarContext := +if mvarId.isTmpMVarId then + { eAssignment := m.eAssignment.set! mvarId.getTmpMVarIdx val, .. m } +else + { mctx := m.mctx.assignExpr mvarId val, .. } + +def getDecl (m : TmpMetavarContext) (mvarId : Name) : MetavarDecl := +if mvarId.isTmpMVarId then + { userName := Name.anonymous, lctx := m.mvarLCtx, type := m.mvarTypes.get! mvarId.getTmpMVarIdx, synthetic := false } +else + m.mctx.getDecl mvarId + +instance isAbstractMetavarContext : AbstractMetavarContext TmpMetavarContext := +{ empty := {}, + isReadOnlyLevelMVar := fun _ mvarId => !mvarId.isTmpMVarId, + getLevelAssignment := TmpMetavarContext.getLevelAssignment, + assignLevel := TmpMetavarContext.assignLevel, + isReadOnlyExprMVar := fun _ mvarId => !mvarId.isTmpMVarId, + getExprAssignment := TmpMetavarContext.getExprAssignment, + assignExpr := TmpMetavarContext.assignExpr, + getDecl := TmpMetavarContext.getDecl, + -- TmpMetavarContext does not support delayed assignments or the creation of auxiliary metavariables. + mkAuxMVar := fun _ _ _ _ _ => none, + assignDelayed := fun _ _ _ _ _ => panic! "TmpMetavarContex does not support delayed assignments", + eraseDelayed := fun _ _ => panic! "TmpMetavarContex does not support delayed assignments", + getDelayedAssignment := fun _ _ => none } + +end TmpMetavarContext + +end Lean