chore: add abbreviations MVarId and FVarId
This commit is contained in:
Leonardo de Moura
parent
f8fb195719
commit
f701683388
10 changed files with 115 additions and 111 deletions
|
|
@ -160,12 +160,15 @@ Expr.mkDataCore h looseBVarRange hasFVar hasExprMVar hasLevelMVar hasLevelParam
|
|||
|
||||
open Expr
|
||||
|
||||
abbrev MVarId := Name
|
||||
abbrev FVarId := Name
|
||||
|
||||
/- We use the `E` suffix (short for `Expr`) to avoid collision with keywords.
|
||||
We considered using «...», but it is too inconvenient to use. -/
|
||||
inductive Expr
|
||||
| bvar : Nat → Data → Expr -- bound variables
|
||||
| fvar : Name → Data → Expr -- free variables
|
||||
| mvar : Name → Data → Expr -- meta variables
|
||||
| fvar : FVarId → Data → Expr -- free variables
|
||||
| mvar : MVarId → Data → Expr -- meta variables
|
||||
| sort : Level → Data → Expr -- Sort
|
||||
| const : Name → List Level → Data → Expr -- constants
|
||||
| app : Expr → Expr → Data → Expr -- application
|
||||
|
|
@ -261,10 +264,10 @@ Expr.bvar idx $ mkData (mixHash 7 $ hash idx) (idx+1)
|
|||
def mkSort (lvl : Level) : Expr :=
|
||||
Expr.sort lvl $ mkData (mixHash 11 $ hash lvl) 0 false false lvl.hasMVar lvl.hasParam
|
||||
|
||||
def mkFVar (fvarId : Name) : Expr :=
|
||||
def mkFVar (fvarId : FVarId) : Expr :=
|
||||
Expr.fvar fvarId $ mkData (mixHash 13 $ hash fvarId) 0 true
|
||||
|
||||
def mkMVar (fvarId : Name) : Expr :=
|
||||
def mkMVar (fvarId : MVarId) : Expr :=
|
||||
Expr.mvar fvarId $ mkData (mixHash 17 $ hash fvarId) 0 false true
|
||||
|
||||
def mkMData (d : MData) (e : Expr) : Expr :=
|
||||
|
|
@ -309,12 +312,13 @@ Expr.letE x t v b $ mkDataForLet (mixHash 41 $ mixHash (hash t) $ mixHash (hash
|
|||
(t.hasLevelParam || v.hasLevelParam || b.hasLevelParam)
|
||||
nonDep
|
||||
|
||||
-- TODO: delete
|
||||
def mkLocal (x u : Name) (t : Expr) (bi : BinderInfo) : Expr :=
|
||||
Expr.localE x u t $ mkDataForBinder (mixHash 43 $ hash t) t.looseBVarRange true t.hasExprMVar t.hasLevelMVar t.hasLevelParam bi
|
||||
|
||||
@[export lean_expr_mk_bvar] def mkBVarEx : Nat → Expr := mkBVar
|
||||
@[export lean_expr_mk_fvar] def mkFVarEx : Name → Expr := mkFVar
|
||||
@[export lean_expr_mk_mvar] def mkMVarEx : Name → Expr := mkMVar
|
||||
@[export lean_expr_mk_fvar] def mkFVarEx : FVarId → Expr := mkFVar
|
||||
@[export lean_expr_mk_mvar] def mkMVarEx : MVarId → Expr := mkMVar
|
||||
@[export lean_expr_mk_sort] def mkSortEx : Level → Expr := mkSort
|
||||
@[export lean_expr_mk_const] def mkConstEx (c : Name) (lvls : List Level) : Expr := mkConst c lvls
|
||||
@[export lean_expr_mk_app] def mkAppEx : Expr → Expr → Expr := mkApp
|
||||
|
|
@ -507,11 +511,11 @@ def bvarIdx! : Expr → Nat
|
|||
| bvar idx _ => idx
|
||||
| _ => panic! "bvar expected"
|
||||
|
||||
def fvarId! : Expr → Name
|
||||
def fvarId! : Expr → FVarId
|
||||
| fvar n _ => n
|
||||
| _ => panic! "fvar expected"
|
||||
|
||||
def mvarId! : Expr → Name
|
||||
def mvarId! : Expr → MVarId
|
||||
| mvar n _ => n
|
||||
| _ => panic! "mvar expected"
|
||||
|
||||
|
|
|
|||
|
|
@ -11,8 +11,8 @@ import Init.Lean.Expr
|
|||
namespace Lean
|
||||
|
||||
inductive LocalDecl
|
||||
| cdecl (index : Nat) (name : Name) (userName : Name) (type : Expr) (bi : BinderInfo)
|
||||
| ldecl (index : Nat) (name : Name) (userName : Name) (type : Expr) (value : Expr)
|
||||
| cdecl (index : Nat) (fvarId : FVarId) (userName : Name) (type : Expr) (bi : BinderInfo)
|
||||
| ldecl (index : Nat) (fvarId : FVarId) (userName : Name) (type : Expr) (value : Expr)
|
||||
|
||||
namespace LocalDecl
|
||||
instance : Inhabited LocalDecl := ⟨ldecl (arbitrary _) (arbitrary _) (arbitrary _) (arbitrary _) (arbitrary _)⟩
|
||||
|
|
@ -25,9 +25,9 @@ def index : LocalDecl → Nat
|
|||
| cdecl idx _ _ _ _ => idx
|
||||
| ldecl idx _ _ _ _ => idx
|
||||
|
||||
def name : LocalDecl → Name
|
||||
| cdecl _ n _ _ _ => n
|
||||
| ldecl _ n _ _ _ => n
|
||||
def fvarId : LocalDecl → FVarId
|
||||
| cdecl _ id _ _ _ => id
|
||||
| ldecl _ id _ _ _ => id
|
||||
|
||||
def userName : LocalDecl → Name
|
||||
| cdecl _ _ n _ _ => n
|
||||
|
|
@ -50,17 +50,17 @@ def value : LocalDecl → Expr
|
|||
| ldecl _ _ _ _ v => v
|
||||
|
||||
def updateUserName : LocalDecl → Name → LocalDecl
|
||||
| cdecl index name _ type bi, userName => cdecl index name userName type bi
|
||||
| ldecl index name _ type val, userName => ldecl index name userName type val
|
||||
| cdecl index id _ type bi, userName => cdecl index id userName type bi
|
||||
| ldecl index id _ type val, userName => ldecl index id userName type val
|
||||
|
||||
def toExpr (decl : LocalDecl) : Expr :=
|
||||
mkFVar decl.name
|
||||
mkFVar decl.fvarId
|
||||
|
||||
end LocalDecl
|
||||
|
||||
structure LocalContext :=
|
||||
(nameToDecl : PersistentHashMap Name LocalDecl := {})
|
||||
(decls : PersistentArray (Option LocalDecl) := {})
|
||||
(fvarIdToDecl : PersistentHashMap Name LocalDecl := {})
|
||||
(decls : PersistentArray (Option LocalDecl) := {})
|
||||
|
||||
namespace LocalContext
|
||||
instance : Inhabited LocalContext := ⟨{}⟩
|
||||
|
|
@ -74,34 +74,34 @@ def empty : LocalContext :=
|
|||
|
||||
@[export lean_local_ctx_is_empty]
|
||||
def isEmpty (lctx : LocalContext) : Bool :=
|
||||
lctx.nameToDecl.isEmpty
|
||||
lctx.fvarIdToDecl.isEmpty
|
||||
|
||||
/- Low level API for creating local declarations. It is used to implement actions in the monads `Elab` and `Tactic`. It should not be used directly since the argument `(name : Name)` is assumed to be "unique". -/
|
||||
@[export lean_local_ctx_mk_local_decl]
|
||||
def mkLocalDecl (lctx : LocalContext) (fvarId : Name) (userName : Name) (type : Expr) (bi : BinderInfo := BinderInfo.default) : LocalContext :=
|
||||
def mkLocalDecl (lctx : LocalContext) (fvarId : FVarId) (userName : Name) (type : Expr) (bi : BinderInfo := BinderInfo.default) : LocalContext :=
|
||||
match lctx with
|
||||
| { nameToDecl := map, decls := decls } =>
|
||||
| { fvarIdToDecl := map, decls := decls } =>
|
||||
let idx := decls.size;
|
||||
let decl := LocalDecl.cdecl idx fvarId userName type bi;
|
||||
{ nameToDecl := map.insert fvarId decl, decls := decls.push decl }
|
||||
{ fvarIdToDecl := map.insert fvarId decl, decls := decls.push decl }
|
||||
|
||||
@[export lean_local_ctx_mk_let_decl]
|
||||
def mkLetDecl (lctx : LocalContext) (fvarId : Name) (userName : Name) (type : Expr) (value : Expr) : LocalContext :=
|
||||
def mkLetDecl (lctx : LocalContext) (fvarId : FVarId) (userName : Name) (type : Expr) (value : Expr) : LocalContext :=
|
||||
match lctx with
|
||||
| { nameToDecl := map, decls := decls } =>
|
||||
| { fvarIdToDecl := map, decls := decls } =>
|
||||
let idx := decls.size;
|
||||
let decl := LocalDecl.ldecl idx fvarId userName type value;
|
||||
{ nameToDecl := map.insert fvarId decl, decls := decls.push decl }
|
||||
{ fvarIdToDecl := map.insert fvarId decl, decls := decls.push decl }
|
||||
|
||||
@[export lean_local_ctx_find]
|
||||
def find (lctx : LocalContext) (fvarId : Name) : Option LocalDecl :=
|
||||
lctx.nameToDecl.find fvarId
|
||||
def find (lctx : LocalContext) (fvarId : FVarId) : Option LocalDecl :=
|
||||
lctx.fvarIdToDecl.find fvarId
|
||||
|
||||
def findFVar (lctx : LocalContext) (e : Expr) : Option LocalDecl :=
|
||||
lctx.find e.fvarId!
|
||||
|
||||
def contains (lctx : LocalContext) (fvarId : Name) : Bool :=
|
||||
lctx.nameToDecl.contains fvarId
|
||||
def contains (lctx : LocalContext) (fvarId : FVarId) : Bool :=
|
||||
lctx.fvarIdToDecl.contains fvarId
|
||||
|
||||
def containsFVar (lctx : LocalContext) (e : Expr) : Bool :=
|
||||
lctx.contains e.fvarId!
|
||||
|
|
@ -114,21 +114,21 @@ private partial def popTailNoneAux : PArray (Option LocalDecl) → PArray (Optio
|
|||
| some _ => a
|
||||
|
||||
@[export lean_local_ctx_erase]
|
||||
def erase (lctx : LocalContext) (fvarId : Name) : LocalContext :=
|
||||
def erase (lctx : LocalContext) (fvarId : FVarId) : LocalContext :=
|
||||
match lctx with
|
||||
| { nameToDecl := map, decls := decls } =>
|
||||
| { fvarIdToDecl := map, decls := decls } =>
|
||||
match map.find fvarId with
|
||||
| none => lctx
|
||||
| some decl => { nameToDecl := map.erase fvarId, decls := popTailNoneAux (decls.set decl.index none) }
|
||||
| some decl => { fvarIdToDecl := map.erase fvarId, decls := popTailNoneAux (decls.set decl.index none) }
|
||||
|
||||
@[export lean_local_ctx_pop]
|
||||
def pop (lctx : LocalContext): LocalContext :=
|
||||
match lctx with
|
||||
| { nameToDecl := map, decls := decls } =>
|
||||
| { fvarIdToDecl := map, decls := decls } =>
|
||||
if decls.size == 0 then lctx
|
||||
else match decls.get! (decls.size - 1) with
|
||||
| none => lctx -- unreachable
|
||||
| some decl => { nameToDecl := map.erase decl.name, decls := popTailNoneAux decls.pop }
|
||||
| some decl => { fvarIdToDecl := map.erase decl.fvarId, decls := popTailNoneAux decls.pop }
|
||||
|
||||
@[export lean_local_ctx_find_from_user_name]
|
||||
def findFromUserName (lctx : LocalContext) (userName : Name) : Option LocalDecl :=
|
||||
|
|
@ -159,13 +159,13 @@ lctx.decls.get! (lctx.decls.size - 1)
|
|||
@[export lean_local_ctx_rename_user_name]
|
||||
def renameUserName (lctx : LocalContext) (fromName : Name) (toName : Name) : LocalContext :=
|
||||
match lctx with
|
||||
| { nameToDecl := map, decls := decls } =>
|
||||
| { fvarIdToDecl := map, decls := decls } =>
|
||||
match lctx.findFromUserName fromName with
|
||||
| none => lctx
|
||||
| some decl =>
|
||||
let decl := decl.updateUserName toName;
|
||||
{ nameToDecl := map.insert decl.name decl,
|
||||
decls := decls.set decl.index decl }
|
||||
{ fvarIdToDecl := map.insert decl.fvarId decl,
|
||||
decls := decls.set decl.index decl }
|
||||
|
||||
@[export lean_local_ctx_num_indices]
|
||||
def numIndices (lctx : LocalContext) : Nat :=
|
||||
|
|
@ -231,7 +231,7 @@ partial def isSubPrefixOfAux (a₁ a₂ : PArray (Option LocalDecl)) : Nat → N
|
|||
match a₂.get! j with
|
||||
| none => isSubPrefixOfAux i (j+1)
|
||||
| some decl₂ =>
|
||||
if decl₁.name == decl₂.name then isSubPrefixOfAux (i+1) (j+1) else isSubPrefixOfAux i (j+1)
|
||||
if decl₁.fvarId == decl₂.fvarId then isSubPrefixOfAux (i+1) (j+1) else isSubPrefixOfAux i (j+1)
|
||||
else false
|
||||
else true
|
||||
|
||||
|
|
|
|||
|
|
@ -257,38 +257,38 @@ adaptReader
|
|||
{ config := { transparency := mode, .. ctx.config }, .. ctx })
|
||||
x
|
||||
|
||||
def isSyntheticExprMVar (mvarId : Name) : MetaM Bool :=
|
||||
def isSyntheticExprMVar (mvarId : MVarId) : MetaM Bool :=
|
||||
do mctx ← getMCtx;
|
||||
match mctx.findDecl mvarId with
|
||||
| some d => pure $ d.synthetic
|
||||
| _ => throwEx $ Exception.unknownExprMVar mvarId
|
||||
|
||||
def isReadOnlyExprMVar (mvarId : Name) : MetaM Bool :=
|
||||
def isReadOnlyExprMVar (mvarId : MVarId) : MetaM Bool :=
|
||||
do mctx ← getMCtx;
|
||||
match mctx.findDecl mvarId with
|
||||
| some d => pure $ d.depth != mctx.depth
|
||||
| _ => throwEx $ Exception.unknownExprMVar mvarId
|
||||
|
||||
def isReadOnlyOrSyntheticExprMVar (mvarId : Name) : MetaM Bool :=
|
||||
def isReadOnlyOrSyntheticExprMVar (mvarId : MVarId) : MetaM Bool :=
|
||||
do mctx ← getMCtx;
|
||||
match mctx.findDecl mvarId with
|
||||
| some d => pure $ d.synthetic || d.depth != mctx.depth
|
||||
| _ => throwEx $ Exception.unknownExprMVar mvarId
|
||||
|
||||
def isReadOnlyLevelMVar (mvarId : Name) : MetaM Bool :=
|
||||
def isReadOnlyLevelMVar (mvarId : MVarId) : MetaM Bool :=
|
||||
do mctx ← getMCtx;
|
||||
match mctx.findLevelDepth mvarId with
|
||||
| some depth => pure $ depth != mctx.depth
|
||||
| _ => throwEx $ Exception.unknownLevelMVar mvarId
|
||||
|
||||
@[inline] def isExprMVarAssigned (mvarId : Name) : MetaM Bool :=
|
||||
@[inline] def isExprMVarAssigned (mvarId : MVarId) : MetaM Bool :=
|
||||
do mctx ← getMCtx;
|
||||
pure $ mctx.isExprAssigned mvarId
|
||||
|
||||
@[inline] def getExprMVarAssignment (mvarId : Name) : MetaM (Option Expr) :=
|
||||
@[inline] def getExprMVarAssignment (mvarId : MVarId) : MetaM (Option Expr) :=
|
||||
do mctx ← getMCtx; pure (mctx.getExprAssignment mvarId)
|
||||
|
||||
def assignExprMVar (mvarId : Name) (val : Expr) : MetaM Unit :=
|
||||
def assignExprMVar (mvarId : MVarId) (val : Expr) : MetaM Unit :=
|
||||
do whenDebugging $ whenM (isExprMVarAssigned mvarId) $ throwBug $ Bug.overwritingExprMVar mvarId;
|
||||
modify $ fun s => { mctx := s.mctx.assignExpr mvarId val, .. s }
|
||||
|
||||
|
|
@ -329,7 +329,7 @@ getConstAux constName true
|
|||
@[inline] def getConstNoEx (constName : Name) : MetaM (Option ConstantInfo) :=
|
||||
getConstAux constName false
|
||||
|
||||
def getLocalDecl (fvarId : Name) : MetaM LocalDecl :=
|
||||
def getLocalDecl (fvarId : FVarId) : MetaM LocalDecl :=
|
||||
do lctx ← getLCtx;
|
||||
match lctx.find fvarId with
|
||||
| some d => pure d
|
||||
|
|
@ -635,10 +635,10 @@ fun _ s =>
|
|||
def instantiateLevelMVars (lvl : Level) : MetaM Level :=
|
||||
liftStateMCtx $ MetavarContext.instantiateLevelMVars lvl
|
||||
|
||||
def assignLevelMVar (mvarId : Name) (lvl : Level) : MetaM Unit :=
|
||||
def assignLevelMVar (mvarId : MVarId) (lvl : Level) : MetaM Unit :=
|
||||
modify $ fun s => { mctx := MetavarContext.assignLevel s.mctx mvarId lvl, .. s }
|
||||
|
||||
def mkFreshLevelMVarId : MetaM Name :=
|
||||
def mkFreshLevelMVarId : MetaM MVarId :=
|
||||
do mvarId ← mkFreshId;
|
||||
modify $ fun s => { mctx := s.mctx.addLevelMVarDecl mvarId, .. s };
|
||||
pure mvarId
|
||||
|
|
|
|||
|
|
@ -53,7 +53,7 @@ namespace DiscrTree
|
|||
|
||||
inductive Key
|
||||
| const : Name → Nat → Key
|
||||
| fvar : Name → Nat → Key
|
||||
| fvar : FVarId → Nat → Key
|
||||
| lit : Literal → Key
|
||||
| star : Key
|
||||
| other : Key
|
||||
|
|
@ -127,7 +127,7 @@ def empty {α} : DiscrTree α := { root := {} }
|
|||
|
||||
/- The discrimination tree ignores implicit arguments and proofs.
|
||||
We use the following auxiliary id as a "mark". -/
|
||||
private def tmpMVarId : Name := `_discr_tree_tmp
|
||||
private def tmpMVarId : MVarId := `_discr_tree_tmp
|
||||
private def tmpStar := mkMVar tmpMVarId
|
||||
|
||||
instance {α} : Inhabited (DiscrTree α) := ⟨{}⟩
|
||||
|
|
|
|||
|
|
@ -19,18 +19,18 @@ inductive Bug
|
|||
|
||||
inductive Exception
|
||||
| unknownConst (constName : Name) (ctx : ExceptionContext)
|
||||
| unknownFVar (fvarId : Name) (ctx : ExceptionContext)
|
||||
| unknownExprMVar (mvarId : Name) (ctx : ExceptionContext)
|
||||
| unknownLevelMVar (mvarId : Name) (ctx : ExceptionContext)
|
||||
| unknownFVar (fvarId : FVarId) (ctx : ExceptionContext)
|
||||
| unknownExprMVar (mvarId : MVarId) (ctx : ExceptionContext)
|
||||
| unknownLevelMVar (mvarId : MVarId) (ctx : ExceptionContext)
|
||||
| unexpectedBVar (bvarIdx : Nat)
|
||||
| functionExpected (f a : Expr) (ctx : ExceptionContext)
|
||||
| typeExpected (type : Expr) (ctx : ExceptionContext)
|
||||
| incorrectNumOfLevels (constName : Name) (constLvls : List Level) (ctx : ExceptionContext)
|
||||
| invalidProjection (structName : Name) (idx : Nat) (s : Expr) (ctx : ExceptionContext)
|
||||
| revertFailure (toRevert : Array Expr) (decl : LocalDecl) (ctx : ExceptionContext)
|
||||
| readOnlyMVar (mvarId : Name) (ctx : ExceptionContext)
|
||||
| readOnlyMVar (mvarId : MVarId) (ctx : ExceptionContext)
|
||||
| isDefEqStuck (t s : Expr) (ctx : ExceptionContext)
|
||||
| letTypeMismatch (fvarId : Name) (ctx : ExceptionContext)
|
||||
| letTypeMismatch (fvarId : FVarId) (ctx : ExceptionContext)
|
||||
| appTypeMismatch (f a : Expr) (ctx : ExceptionContext)
|
||||
| bug (b : Bug) (ctx : ExceptionContext)
|
||||
| other (msg : String)
|
||||
|
|
|
|||
|
|
@ -339,7 +339,7 @@ namespace CheckAssignment
|
|||
|
||||
structure Context :=
|
||||
(lctx : LocalContext)
|
||||
(mvarId : Name)
|
||||
(mvarId : MVarId)
|
||||
(mvarDecl : MetavarDecl)
|
||||
(fvars : Array Expr)
|
||||
(ctxApprox : Bool)
|
||||
|
|
@ -348,10 +348,10 @@ structure Context :=
|
|||
inductive Exception
|
||||
| occursCheck
|
||||
| useFOApprox
|
||||
| outOfScopeFVar (fvarId : Name)
|
||||
| readOnlyMVarWithBiggerLCtx (mvarId : Name)
|
||||
| mvarTypeNotWellFormedInSmallerLCtx (mvarId : Name)
|
||||
| unknownExprMVar (mvarId : Name)
|
||||
| outOfScopeFVar (fvarId : FVarId)
|
||||
| readOnlyMVarWithBiggerLCtx (mvarId : MVarId)
|
||||
| mvarTypeNotWellFormedInSmallerLCtx (mvarId : MVarId)
|
||||
| unknownExprMVar (mvarId : MVarId)
|
||||
|
||||
structure State :=
|
||||
(mctx : MetavarContext)
|
||||
|
|
@ -435,7 +435,7 @@ partial def check : Expr → CheckAssignmentM Expr
|
|||
|
||||
end CheckAssignment
|
||||
|
||||
private def checkAssignmentFailure (mvarId : Name) (fvars : Array Expr) (v : Expr) (ex : CheckAssignment.Exception) : MetaM (Option Expr) :=
|
||||
private def checkAssignmentFailure (mvarId : MVarId) (fvars : Array Expr) (v : Expr) (ex : CheckAssignment.Exception) : MetaM (Option Expr) :=
|
||||
match ex with
|
||||
| CheckAssignment.Exception.occursCheck => do
|
||||
trace `Meta.isDefEq.assign.occursCheck $ fun _ => mkMVar mvarId ++ fvars ++ " := " ++ v;
|
||||
|
|
@ -462,7 +462,7 @@ if !e.hasExprMVar && !e.hasFVar then true else f e
|
|||
|
||||
partial def check
|
||||
(hasCtxLocals ctxApprox : Bool)
|
||||
(mctx : MetavarContext) (lctx : LocalContext) (mvarDecl : MetavarDecl) (mvarId : Name) (fvars : Array Expr) : Expr → Bool
|
||||
(mctx : MetavarContext) (lctx : LocalContext) (mvarDecl : MetavarDecl) (mvarId : MVarId) (fvars : Array Expr) : Expr → Bool
|
||||
| e@(Expr.mdata _ b _) => check b
|
||||
| e@(Expr.proj _ _ s _) => check s
|
||||
| e@(Expr.app f a _) => visit check f && visit check a
|
||||
|
|
@ -506,7 +506,7 @@ end CheckAssignmentQuick
|
|||
The result is `none` if the assignment can't be performed.
|
||||
The result is `some newV` where `newV` is a possibly updated `v`. This method may need
|
||||
to unfold let-declarations. -/
|
||||
def checkAssignment (mvarId : Name) (fvars : Array Expr) (v : Expr) : MetaM (Option Expr) :=
|
||||
def checkAssignment (mvarId : MVarId) (fvars : Array Expr) (v : Expr) : MetaM (Option Expr) :=
|
||||
fun ctx s => if !v.hasExprMVar && !v.hasFVar then EStateM.Result.ok (some v) s else
|
||||
let mvarDecl := s.mctx.getDecl mvarId;
|
||||
let hasCtxLocals := fvars.any $ fun fvar => mvarDecl.lctx.containsFVar fvar;
|
||||
|
|
@ -885,7 +885,7 @@ match t.etaExpanded? with
|
|||
| some t => t == s
|
||||
| none => false
|
||||
|
||||
private def isLetFVar (fvarId : Name) : MetaM Bool :=
|
||||
private def isLetFVar (fvarId : FVarId) : MetaM Bool :=
|
||||
do decl ← getLocalDecl fvarId;
|
||||
pure decl.isLet
|
||||
|
||||
|
|
|
|||
|
|
@ -104,13 +104,13 @@ savingCache $ do
|
|||
adaptReader (fun (ctx : Context) => { lctx := ctx.lctx.mkLocalDecl fvarId name type bi, .. ctx }) $
|
||||
x (mkFVar fvarId)
|
||||
|
||||
private def inferMVarType (mvarId : Name) : MetaM Expr :=
|
||||
private def inferMVarType (mvarId : MVarId) : MetaM Expr :=
|
||||
do mctx ← getMCtx;
|
||||
match mctx.findDecl mvarId with
|
||||
| some d => pure d.type
|
||||
| none => throwEx $ Exception.unknownExprMVar mvarId
|
||||
|
||||
private def inferFVarType (fvarId : Name) : MetaM Expr :=
|
||||
private def inferFVarType (fvarId : FVarId) : MetaM Expr :=
|
||||
do lctx ← getLCtx;
|
||||
match lctx.find fvarId with
|
||||
| some d => pure d.type
|
||||
|
|
|
|||
|
|
@ -21,7 +21,7 @@ private def strictOccursMax (lvl : Level) : Level → Bool
|
|||
| _ => false
|
||||
|
||||
/-- `mkMaxArgsDiff mvarId (max u_1 ... (mvar mvarId) ... u_n) v` => `max v u_1 ... u_n` -/
|
||||
private def mkMaxArgsDiff (mvarId : Name) : Level → Level → Level
|
||||
private def mkMaxArgsDiff (mvarId : MVarId) : Level → Level → Level
|
||||
| Level.max u v _, acc => mkMaxArgsDiff v $ mkMaxArgsDiff u acc
|
||||
| l@(Level.mvar id _), acc => if id != mvarId then mkLevelMax acc l else acc
|
||||
| l, acc => mkLevelMax acc l
|
||||
|
|
@ -29,9 +29,9 @@ private def mkMaxArgsDiff (mvarId : Name) : Level → Level → Level
|
|||
/--
|
||||
Solve `?m =?= max ?m v` by creating a fresh metavariable `?n`
|
||||
and assigning `?m := max ?n v` -/
|
||||
private def solveSelfMax (mId : Name) (v : Level) : MetaM Unit :=
|
||||
private def solveSelfMax (mvarId : MVarId) (v : Level) : MetaM Unit :=
|
||||
do n ← mkFreshLevelMVar;
|
||||
assignLevelMVar mId $ mkMaxArgsDiff mId v n
|
||||
assignLevelMVar mvarId $ mkMaxArgsDiff mvarId v n
|
||||
|
||||
private def postponeIsLevelDefEq (lhs : Level) (rhs : Level) : MetaM Unit :=
|
||||
modify $ fun s => { postponed := s.postponed.push { lhs := lhs, rhs := rhs }, .. s }
|
||||
|
|
|
|||
|
|
@ -222,11 +222,11 @@ structure DelayedMetavarAssignment :=
|
|||
|
||||
structure MetavarContext :=
|
||||
(depth : Nat := 0)
|
||||
(lDepth : PersistentHashMap Name Nat := {})
|
||||
(decls : PersistentHashMap Name MetavarDecl := {})
|
||||
(lAssignment : PersistentHashMap Name Level := {})
|
||||
(eAssignment : PersistentHashMap Name Expr := {})
|
||||
(dAssignment : PersistentHashMap Name DelayedMetavarAssignment := {})
|
||||
(lDepth : PersistentHashMap MVarId Nat := {})
|
||||
(decls : PersistentHashMap MVarId MetavarDecl := {})
|
||||
(lAssignment : PersistentHashMap MVarId Level := {})
|
||||
(eAssignment : PersistentHashMap MVarId Expr := {})
|
||||
(dAssignment : PersistentHashMap MVarId DelayedMetavarAssignment := {})
|
||||
|
||||
namespace MetavarContext
|
||||
|
||||
|
|
@ -238,10 +238,10 @@ fun _ => {}
|
|||
|
||||
/- Low level API for adding/declaring metavariable declarations.
|
||||
It is used to implement actions in the monads `MetaM`, `ElabM` and `TacticM`.
|
||||
It should not be used directly since the argument `(mvarId : Name)` is assumed to be "unique". -/
|
||||
It should not be used directly since the argument `(mvarId : MVarId)` is assumed to be "unique". -/
|
||||
@[export lean_metavar_ctx_mk_decl]
|
||||
def addExprMVarDecl (mctx : MetavarContext)
|
||||
(mvarId : Name)
|
||||
(mvarId : MVarId)
|
||||
(userName : Name)
|
||||
(lctx : LocalContext)
|
||||
(localInstances : LocalInstances)
|
||||
|
|
@ -257,74 +257,74 @@ def addExprMVarDecl (mctx : MetavarContext)
|
|||
|
||||
/- Low level API for adding/declaring universe level metavariable declarations.
|
||||
It is used to implement actions in the monads `MetaM`, `ElabM` and `TacticM`.
|
||||
It should not be used directly since the argument `(mvarId : Name)` is assumed to be "unique". -/
|
||||
def addLevelMVarDecl (mctx : MetavarContext) (mvarId : Name) : MetavarContext :=
|
||||
It should not be used directly since the argument `(mvarId : MVarId)` is assumed to be "unique". -/
|
||||
def addLevelMVarDecl (mctx : MetavarContext) (mvarId : MVarId) : MetavarContext :=
|
||||
{ lDepth := mctx.lDepth.insert mvarId mctx.depth,
|
||||
.. mctx }
|
||||
|
||||
@[export lean_metavar_ctx_find_decl]
|
||||
def findDecl (mctx : MetavarContext) (mvarId : Name) : Option MetavarDecl :=
|
||||
def findDecl (mctx : MetavarContext) (mvarId : MVarId) : Option MetavarDecl :=
|
||||
mctx.decls.find mvarId
|
||||
|
||||
def getDecl (mctx : MetavarContext) (mvarId : Name) : MetavarDecl :=
|
||||
def getDecl (mctx : MetavarContext) (mvarId : MVarId) : MetavarDecl :=
|
||||
match mctx.decls.find mvarId with
|
||||
| some decl => decl
|
||||
| none => panic! "unknown metavariable"
|
||||
|
||||
def findLevelDepth (mctx : MetavarContext) (mvarId : Name) : Option Nat :=
|
||||
def findLevelDepth (mctx : MetavarContext) (mvarId : MVarId) : Option Nat :=
|
||||
mctx.lDepth.find mvarId
|
||||
|
||||
def getLevelDepth (mctx : MetavarContext) (mvarId : Name) : Nat :=
|
||||
def getLevelDepth (mctx : MetavarContext) (mvarId : MVarId) : Nat :=
|
||||
match mctx.findLevelDepth mvarId with
|
||||
| some d => d
|
||||
| none => panic! "unknown metavariable"
|
||||
|
||||
@[export lean_metavar_ctx_assign_level]
|
||||
def assignLevel (m : MetavarContext) (mvarId : Name) (val : Level) : MetavarContext :=
|
||||
def assignLevel (m : MetavarContext) (mvarId : MVarId) (val : Level) : MetavarContext :=
|
||||
{ lAssignment := m.lAssignment.insert mvarId val, .. m }
|
||||
|
||||
@[export lean_metavar_ctx_assign_expr]
|
||||
def assignExpr (m : MetavarContext) (mvarId : Name) (val : Expr) : MetavarContext :=
|
||||
def assignExpr (m : MetavarContext) (mvarId : MVarId) (val : Expr) : MetavarContext :=
|
||||
{ eAssignment := m.eAssignment.insert mvarId val, .. m }
|
||||
|
||||
@[export lean_metavar_ctx_assign_delayed]
|
||||
def assignDelayed (m : MetavarContext) (mvarId : Name) (lctx : LocalContext) (fvars : Array Expr) (val : Expr) : MetavarContext :=
|
||||
def assignDelayed (m : MetavarContext) (mvarId : MVarId) (lctx : LocalContext) (fvars : Array Expr) (val : Expr) : MetavarContext :=
|
||||
{ dAssignment := m.dAssignment.insert mvarId { lctx := lctx, fvars := fvars, val := val }, .. m }
|
||||
|
||||
@[export lean_metavar_ctx_get_level_assignment]
|
||||
def getLevelAssignment (m : MetavarContext) (mvarId : Name) : Option Level :=
|
||||
def getLevelAssignment (m : MetavarContext) (mvarId : MVarId) : Option Level :=
|
||||
m.lAssignment.find mvarId
|
||||
|
||||
@[export lean_metavar_ctx_get_expr_assignment]
|
||||
def getExprAssignment (m : MetavarContext) (mvarId : Name) : Option Expr :=
|
||||
def getExprAssignment (m : MetavarContext) (mvarId : MVarId) : Option Expr :=
|
||||
m.eAssignment.find mvarId
|
||||
|
||||
@[export lean_metavar_ctx_get_delayed_assignment]
|
||||
def getDelayedAssignment (m : MetavarContext) (mvarId : Name) : Option DelayedMetavarAssignment :=
|
||||
def getDelayedAssignment (m : MetavarContext) (mvarId : MVarId) : Option DelayedMetavarAssignment :=
|
||||
m.dAssignment.find mvarId
|
||||
|
||||
@[export lean_metavar_ctx_is_level_assigned]
|
||||
def isLevelAssigned (m : MetavarContext) (mvarId : Name) : Bool :=
|
||||
def isLevelAssigned (m : MetavarContext) (mvarId : MVarId) : Bool :=
|
||||
m.lAssignment.contains mvarId
|
||||
|
||||
@[export lean_metavar_ctx_is_expr_assigned]
|
||||
def isExprAssigned (m : MetavarContext) (mvarId : Name) : Bool :=
|
||||
def isExprAssigned (m : MetavarContext) (mvarId : MVarId) : Bool :=
|
||||
m.eAssignment.contains mvarId
|
||||
|
||||
@[export lean_metavar_ctx_is_delayed_assigned]
|
||||
def isDelayedAssigned (m : MetavarContext) (mvarId : Name) : Bool :=
|
||||
def isDelayedAssigned (m : MetavarContext) (mvarId : MVarId) : Bool :=
|
||||
m.dAssignment.contains mvarId
|
||||
|
||||
@[export lean_metavar_ctx_erase_delayed]
|
||||
def eraseDelayed (m : MetavarContext) (mvarId : Name) : MetavarContext :=
|
||||
def eraseDelayed (m : MetavarContext) (mvarId : MVarId) : MetavarContext :=
|
||||
{ dAssignment := m.dAssignment.erase mvarId, .. m }
|
||||
|
||||
def isLevelAssignable (mctx : MetavarContext) (mvarId : Name) : Bool :=
|
||||
def isLevelAssignable (mctx : MetavarContext) (mvarId : MVarId) : Bool :=
|
||||
match mctx.lDepth.find mvarId with
|
||||
| some d => d == mctx.depth
|
||||
| _ => panic! "unknown universe metavariable"
|
||||
|
||||
def isExprAssignable (mctx : MetavarContext) (mvarId : Name) : Bool :=
|
||||
def isExprAssignable (mctx : MetavarContext) (mvarId : MVarId) : Bool :=
|
||||
let decl := mctx.getDecl mvarId;
|
||||
decl.depth == mctx.depth
|
||||
|
||||
|
|
@ -424,7 +424,7 @@ modify $ fun s => { state := f s.state, .. s }
|
|||
instantiateDelayedAux i (mkLet n ty val b)
|
||||
|
||||
/-- Try to instantiate a delayed assignment. Return `none` (i.e., fail) if assignment still contains variables. -/
|
||||
@[inline] private def instantiateDelayed (main : Expr → M Expr) (mvarId : Name) : DelayedMetavarAssignment → M (Option Expr)
|
||||
@[inline] private def instantiateDelayed (main : Expr → M Expr) (mvarId : MVarId) : DelayedMetavarAssignment → M (Option Expr)
|
||||
| { lctx := lctx, fvars := fvars, val := val } => do
|
||||
newVal ← visit main val;
|
||||
let fail : M (Option Expr) := do {
|
||||
|
|
@ -504,7 +504,7 @@ else do
|
|||
@[inline] private def visit (main : Expr → M Bool) (e : Expr) : M Bool :=
|
||||
condM (visit? e) (main e) (pure false)
|
||||
|
||||
@[specialize] private partial def dep (mctx : MetavarContext) (p : Name → Bool) : Expr → M Bool
|
||||
@[specialize] private partial def dep (mctx : MetavarContext) (p : FVarId → Bool) : Expr → M Bool
|
||||
| e@(Expr.proj _ _ s _) => visit dep s
|
||||
| e@(Expr.forallE _ d b _) => visit dep d <||> visit dep b
|
||||
| e@(Expr.lam _ d b _) => visit dep d <||> visit dep b
|
||||
|
|
@ -516,11 +516,11 @@ condM (visit? e) (main e) (pure false)
|
|||
| some a => visit dep a
|
||||
| none =>
|
||||
let lctx := (mctx.getDecl mvarId).lctx;
|
||||
pure $ lctx.any $ fun decl => p decl.name
|
||||
pure $ lctx.any $ fun decl => p decl.fvarId
|
||||
| e@(Expr.fvar fvarId _) => pure $ p fvarId
|
||||
| e => pure false
|
||||
|
||||
@[inline] partial def main (mctx : MetavarContext) (p : Name → Bool) (e : Expr) : M Bool :=
|
||||
@[inline] partial def main (mctx : MetavarContext) (p : FVarId → Bool) (e : Expr) : M Bool :=
|
||||
if !e.hasFVar && !e.hasMVar then pure false else dep mctx p e
|
||||
|
||||
end DependsOn
|
||||
|
|
@ -531,13 +531,13 @@ end DependsOn
|
|||
1- If `?m := t`, then we visit `t` looking for `x`
|
||||
2- If `?m` is unassigned, then we consider the worst case and check whether `x` is in the local context of `?m`.
|
||||
This case is a "may dependency". That is, we may assign a term `t` to `?m` s.t. `t` contains `x`. -/
|
||||
@[inline] def exprDependsOn (mctx : MetavarContext) (p : Name → Bool) (e : Expr) : Bool :=
|
||||
@[inline] def exprDependsOn (mctx : MetavarContext) (p : FVarId → Bool) (e : Expr) : Bool :=
|
||||
(DependsOn.main mctx p e).run' {}
|
||||
|
||||
/--
|
||||
Similar to `exprDependsOn`, but checks the expressions in the given local declaration
|
||||
depends on a free variable `x` s.t. `p x` is `true`. -/
|
||||
@[inline] def localDeclDependsOn (mctx : MetavarContext) (p : Name → Bool) : LocalDecl → Bool
|
||||
@[inline] def localDeclDependsOn (mctx : MetavarContext) (p : FVarId → Bool) : LocalDecl → Bool
|
||||
| LocalDecl.cdecl _ _ _ type _ => exprDependsOn mctx p type
|
||||
| LocalDecl.ldecl _ _ _ type value => (DependsOn.main mctx p type <||> DependsOn.main mctx p value).run' {}
|
||||
|
||||
|
|
@ -545,7 +545,7 @@ namespace MkBinding
|
|||
|
||||
inductive Exception
|
||||
| revertFailure (mctx : MetavarContext) (lctx : LocalContext) (toRevert : Array Expr) (decl : LocalDecl)
|
||||
| readOnlyMVar (mctx : MetavarContext) (mvarId : Name)
|
||||
| readOnlyMVar (mctx : MetavarContext) (mvarId : MVarId)
|
||||
|
||||
def Exception.toString : Exception → String
|
||||
| Exception.revertFailure _ lctx toRevert decl =>
|
||||
|
|
@ -632,7 +632,7 @@ else
|
|||
let minDecl := getLocalDeclWithSmallestIdx lctx toRevert;
|
||||
lctx.foldlFromM
|
||||
(fun newToRevert decl =>
|
||||
if toRevert.any (fun x => decl.name == x.fvarId!) then
|
||||
if toRevert.any (fun x => decl.fvarId == x.fvarId!) then
|
||||
pure (newToRevert.push decl.toExpr)
|
||||
else if localDeclDependsOn mctx (fun fvarId => newToRevert.any $ fun x => x.fvarId! == fvarId) decl then
|
||||
if decl.binderInfo.isAuxDecl then
|
||||
|
|
@ -689,7 +689,7 @@ mkForall
|
|||
private def mkMVarApp (lctx : LocalContext) (mvar : Expr) (xs : Array Expr) : Expr :=
|
||||
xs.foldl (fun e x => if (lctx.findFVar x).get!.isLet then e else mkApp e x) mvar
|
||||
|
||||
private def mkAuxMVar (lctx : LocalContext) (localInsts : LocalInstances) (type : Expr) (synthetic : Bool) : M Name :=
|
||||
private def mkAuxMVar (lctx : LocalContext) (localInsts : LocalInstances) (type : Expr) (synthetic : Bool) : M MVarId :=
|
||||
do s ← get;
|
||||
let mvarId := s.ngen.curr;
|
||||
modify $ fun s => { mctx := s.mctx.addExprMVarDecl mvarId Name.anonymous lctx localInsts type synthetic, ngen := s.ngen.next, .. s };
|
||||
|
|
|
|||
|
|
@ -277,8 +277,8 @@ else
|
|||
(whnf : Expr → m Expr)
|
||||
(inferType : Expr → m Expr)
|
||||
(isDefEq : Expr → Expr → m Bool)
|
||||
(getLocalDecl : Name → m LocalDecl)
|
||||
(getMVarAssignment : Name → m (Option Expr)) : Expr → m Expr
|
||||
(getLocalDecl : FVarId → m LocalDecl)
|
||||
(getMVarAssignment : MVarId → m (Option Expr)) : Expr → m Expr
|
||||
| e => whnfEasyCases getLocalDecl getMVarAssignment e $ fun e =>
|
||||
match e with
|
||||
| e@(Expr.const _ _ _) => pure e
|
||||
|
|
@ -321,8 +321,8 @@ else
|
|||
(inferType : Expr → m Expr)
|
||||
(isDefEq : Expr → Expr → m Bool)
|
||||
(synthesizePending : Expr → m Bool)
|
||||
(getLocalDecl : Name → m LocalDecl)
|
||||
(getMVarAssignment : Name → m (Option Expr))
|
||||
(getLocalDecl : FVarId → m LocalDecl)
|
||||
(getMVarAssignment : MVarId → m (Option Expr))
|
||||
: Expr → m Expr
|
||||
| e => do
|
||||
e ← whnfCore getConst isAuxDef? whnf inferType isDefEq getLocalDecl getMVarAssignment e;
|
||||
|
|
@ -338,8 +338,8 @@ else
|
|||
(inferType : Expr → m Expr)
|
||||
(isDefEq : Expr → Expr → m Bool)
|
||||
(synthesizePending : Expr → m Bool)
|
||||
(getLocalDecl : Name → m LocalDecl)
|
||||
(getMVarAssignment : Name → m (Option Expr))
|
||||
(getLocalDecl : FVarId → m LocalDecl)
|
||||
(getMVarAssignment : MVarId → m (Option Expr))
|
||||
(e : Expr) : m (Option Expr) :=
|
||||
match e with
|
||||
| Expr.app f _ _ =>
|
||||
|
|
@ -380,8 +380,8 @@ match e with
|
|||
(inferType : Expr → m Expr)
|
||||
(isDefEq : Expr → Expr → m Bool)
|
||||
(synthesizePending : Expr → m Bool)
|
||||
(getLocalDecl : Name → m LocalDecl)
|
||||
(getMVarAssignment : Name → m (Option Expr))
|
||||
(getLocalDecl : FVarId → m LocalDecl)
|
||||
(getMVarAssignment : MVarId → m (Option Expr))
|
||||
: Expr → m Expr
|
||||
| e => do
|
||||
e ← whnfCore getConst isAuxDef? whnfMain inferType isDefEq getLocalDecl getMVarAssignment e;
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue