Lean.MetavarContext

Lean.LocalInstances.erase localInsts fvarId = match Array.findIdx? localInsts fun inst => Lean.Expr.fvarId! inst.fvar == fvarId with | some idx => Array.eraseIdx localInsts idx | x => localInsts

source

inductive Lean.MetavarKind :

Type

natural: Lean.MetavarKind
synthetic: Lean.MetavarKind
syntheticOpaque: Lean.MetavarKind

source

instance Lean.instReprMetavarKind :

Repr Lean.MetavarKind

Equations

Lean.instReprMetavarKind = { reprPrec := [anonymous] }

source

instance Lean.instInhabitedMetavarKind :

Inhabited Lean.MetavarKind

Equations

Lean.instInhabitedMetavarKind = { default := Lean.MetavarKind.natural }

source

def Lean.MetavarKind.isSyntheticOpaque :

Lean.MetavarKind → Bool

Equations

Lean.MetavarKind.isSyntheticOpaque x = match x with | Lean.MetavarKind.syntheticOpaque => true | x => false

source

def Lean.MetavarKind.isNatural :

Lean.MetavarKind → Bool

Equations

Lean.MetavarKind.isNatural x = match x with | Lean.MetavarKind.natural => true | x => false

source

structure Lean.MetavarDecl :

Type

userName : Lean.Name
lctx : Lean.LocalContext
type : Lean.Expr
depth : Nat
localInstances : Lean.LocalInstances
kind : Lean.MetavarKind
numScopeArgs : Nat
index : Nat

source

instance Lean.instInhabitedMetavarDecl :

Inhabited Lean.MetavarDecl

Equations

Lean.instInhabitedMetavarDecl = { default := { userName := default, lctx := default, type := default, depth := default, localInstances := default, kind := default, numScopeArgs := default, index := default } }

source

structure Lean.DelayedMetavarAssignment :

Type

source

structure Lean.MetavarContext :

Type

depth : Nat
mvarCounter : Nat
lDepth : Std.PersistentHashMap Lean.MVarId Nat
decls : Std.PersistentHashMap Lean.MVarId Lean.MetavarDecl
userNames : Std.PersistentHashMap Lean.Name Lean.MVarId
lAssignment : Std.PersistentHashMap Lean.MVarId Lean.Level
eAssignment : Std.PersistentHashMap Lean.MVarId Lean.Expr
dAssignment : Std.PersistentHashMap Lean.MVarId Lean.DelayedMetavarAssignment

source

class Lean.MonadMCtx (m : Type → Type) :

Type

getMCtx : m Lean.MetavarContext
modifyMCtx : (Lean.MetavarContext → Lean.MetavarContext) → m Unit

Instances

source

instance Lean.instMonadMCtx (m : Type → Type) (n : Type → Type) [inst : MonadLift m n] [inst : Lean.MonadMCtx m] :

Lean.MonadMCtx n

Equations

Lean.instMonadMCtx m n = { getMCtx := liftM Lean.getMCtx, modifyMCtx := fun f => liftM (Lean.modifyMCtx f) }

source

instance Lean.MetavarContext.instInhabitedMetavarContext :

Inhabited Lean.MetavarContext

Equations

Lean.MetavarContext.instInhabitedMetavarContext = { default := { depth := 0, mvarCounter := 0, lDepth := { root := Std.PersistentHashMap.Node.entries Std.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, decls := { root := Std.PersistentHashMap.Node.entries Std.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, userNames := { root := Std.PersistentHashMap.Node.entries Std.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, lAssignment := { root := Std.PersistentHashMap.Node.entries Std.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, eAssignment := { root := Std.PersistentHashMap.Node.entries Std.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, dAssignment := { root := Std.PersistentHashMap.Node.entries Std.PersistentHashMap.mkEmptyEntriesArray, size := 0 } } }

source

def Lean.MetavarContext.mkMetavarContext :

Unit → Lean.MetavarContext

Equations

Lean.MetavarContext.mkMetavarContext x = { depth := 0, mvarCounter := 0, lDepth := { root := Std.PersistentHashMap.Node.entries Std.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, decls := { root := Std.PersistentHashMap.Node.entries Std.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, userNames := { root := Std.PersistentHashMap.Node.entries Std.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, lAssignment := { root := Std.PersistentHashMap.Node.entries Std.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, eAssignment := { root := Std.PersistentHashMap.Node.entries Std.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, dAssignment := { root := Std.PersistentHashMap.Node.entries Std.PersistentHashMap.mkEmptyEntriesArray, size := 0 } }

source

def Lean.MetavarContext.addExprMVarDecl (mctx : Lean.MetavarContext) (mvarId : Lean.MVarId) (userName : Lean.Name) (lctx : Lean.LocalContext) (localInstances : Lean.LocalInstances) (type : Lean.Expr) (kind : optParam Lean.MetavarKind Lean.MetavarKind.natural) (numScopeArgs : optParam Nat 0) :

Lean.MetavarContext

Equations

Lean.MetavarContext.addExprMVarDecl mctx mvarId userName lctx localInstances type kind numScopeArgs = { depth := mctx.depth, mvarCounter := mctx.mvarCounter + 1, lDepth := mctx.lDepth, decls := Std.PersistentHashMap.insert mctx.decls mvarId { userName := userName, lctx := lctx, type := type, depth := mctx.depth, localInstances := localInstances, kind := kind, numScopeArgs := numScopeArgs, index := mctx.mvarCounter }, userNames := if Lean.Name.isAnonymous userName = true then mctx.userNames else Std.PersistentHashMap.insert mctx.userNames userName mvarId, lAssignment := mctx.lAssignment, eAssignment := mctx.eAssignment, dAssignment := mctx.dAssignment }

source

def Lean.MetavarContext.addExprMVarDeclExp (mctx : Lean.MetavarContext) (mvarId : Lean.MVarId) (userName : Lean.Name) (lctx : Lean.LocalContext) (localInstances : Lean.LocalInstances) (type : Lean.Expr) (kind : Lean.MetavarKind) :

Lean.MetavarContext

Equations

Lean.MetavarContext.addExprMVarDeclExp mctx mvarId userName lctx localInstances type kind = Lean.MetavarContext.addExprMVarDecl mctx mvarId userName lctx localInstances type kind

source

def Lean.MetavarContext.addLevelMVarDecl (mctx : Lean.MetavarContext) (mvarId : Lean.MVarId) :

Lean.MetavarContext

Equations

Lean.MetavarContext.addLevelMVarDecl mctx mvarId = { depth := mctx.depth, mvarCounter := mctx.mvarCounter, lDepth := Std.PersistentHashMap.insert mctx.lDepth mvarId mctx.depth, decls := mctx.decls, userNames := mctx.userNames, lAssignment := mctx.lAssignment, eAssignment := mctx.eAssignment, dAssignment := mctx.dAssignment }

source

def Lean.MetavarContext.findDecl? (mctx : Lean.MetavarContext) (mvarId : Lean.MVarId) :

Option Lean.MetavarDecl

Equations

Lean.MetavarContext.findDecl? mctx mvarId = Std.PersistentHashMap.find? mctx.decls mvarId

source

def Lean.MetavarContext.getDecl (mctx : Lean.MetavarContext) (mvarId : Lean.MVarId) :

Lean.MetavarDecl

Equations

Lean.MetavarContext.getDecl mctx mvarId = match Std.PersistentHashMap.find? mctx.decls mvarId with | some decl => decl | none => panicWithPosWithDecl "Lean.MetavarContext" "Lean.MetavarContext.getDecl" 343 17 "unknown metavariable"

source

def Lean.MetavarContext.findUserName? (mctx : Lean.MetavarContext) (userName : Lean.Name) :

Option Lean.MVarId

Equations

Lean.MetavarContext.findUserName? mctx userName = Std.PersistentHashMap.find? mctx.userNames userName

source

def Lean.MetavarContext.setMVarKind (mctx : Lean.MetavarContext) (mvarId : Lean.MVarId) (kind : Lean.MetavarKind) :

Lean.MetavarContext

Equations

Lean.MetavarContext.setMVarKind mctx mvarId kind = let decl := Lean.MetavarContext.getDecl mctx mvarId; { depth := mctx.depth, mvarCounter := mctx.mvarCounter, lDepth := mctx.lDepth, decls := Std.PersistentHashMap.insert mctx.decls mvarId { userName := decl.userName, lctx := decl.lctx, type := decl.type, depth := decl.depth, localInstances := decl.localInstances, kind := kind, numScopeArgs := decl.numScopeArgs, index := decl.index }, userNames := mctx.userNames, lAssignment := mctx.lAssignment, eAssignment := mctx.eAssignment, dAssignment := mctx.dAssignment }

source

def Lean.MetavarContext.renameMVar (mctx : Lean.MetavarContext) (mvarId : Lean.MVarId) (userName : Lean.Name) :

Lean.MetavarContext

Equations

Lean.MetavarContext.renameMVar mctx mvarId userName = let decl := Lean.MetavarContext.getDecl mctx mvarId; { depth := mctx.depth, mvarCounter := mctx.mvarCounter, lDepth := mctx.lDepth, decls := Std.PersistentHashMap.insert mctx.decls mvarId { userName := userName, lctx := decl.lctx, type := decl.type, depth := decl.depth, localInstances := decl.localInstances, kind := decl.kind, numScopeArgs := decl.numScopeArgs, index := decl.index }, userNames := let userNames := Std.PersistentHashMap.erase mctx.userNames decl.userName; if Lean.Name.isAnonymous userName = true then userNames else Std.PersistentHashMap.insert userNames userName mvarId, lAssignment := mctx.lAssignment, eAssignment := mctx.eAssignment, dAssignment := mctx.dAssignment }

source

def Lean.MetavarContext.setMVarType (mctx : Lean.MetavarContext) (mvarId : Lean.MVarId) (type : Lean.Expr) :

Lean.MetavarContext

Equations

Lean.MetavarContext.setMVarType mctx mvarId type = let decl := Lean.MetavarContext.getDecl mctx mvarId; { depth := mctx.depth, mvarCounter := mctx.mvarCounter, lDepth := mctx.lDepth, decls := Std.PersistentHashMap.insert mctx.decls mvarId { userName := decl.userName, lctx := decl.lctx, type := type, depth := decl.depth, localInstances := decl.localInstances, kind := decl.kind, numScopeArgs := decl.numScopeArgs, index := decl.index }, userNames := mctx.userNames, lAssignment := mctx.lAssignment, eAssignment := mctx.eAssignment, dAssignment := mctx.dAssignment }

source

def Lean.MetavarContext.findLevelDepth? (mctx : Lean.MetavarContext) (mvarId : Lean.MVarId) :

Option Nat

Equations

Lean.MetavarContext.findLevelDepth? mctx mvarId = Std.PersistentHashMap.find? mctx.lDepth mvarId

source

def Lean.MetavarContext.getLevelDepth (mctx : Lean.MetavarContext) (mvarId : Lean.MVarId) :

Nat

Equations

Lean.MetavarContext.getLevelDepth mctx mvarId = match Lean.MetavarContext.findLevelDepth? mctx mvarId with | some d => d | none => panicWithPosWithDecl "Lean.MetavarContext" "Lean.MetavarContext.getLevelDepth" 372 14 "unknown metavariable"

source

def Lean.MetavarContext.isAnonymousMVar (mctx : Lean.MetavarContext) (mvarId : Lean.MVarId) :

Bool

Equations

Lean.MetavarContext.isAnonymousMVar mctx mvarId = match Lean.MetavarContext.findDecl? mctx mvarId with | none => false | some mvarDecl => Lean.Name.isAnonymous mvarDecl.userName

source

def Lean.MetavarContext.assignLevel (m : Lean.MetavarContext) (mvarId : Lean.MVarId) (val : Lean.Level) :

Lean.MetavarContext

Equations

Lean.MetavarContext.assignLevel m mvarId val = { depth := m.depth, mvarCounter := m.mvarCounter, lDepth := m.lDepth, decls := m.decls, userNames := m.userNames, lAssignment := Std.PersistentHashMap.insert m.lAssignment mvarId val, eAssignment := m.eAssignment, dAssignment := m.dAssignment }

source

def Lean.MetavarContext.assignExpr (m : Lean.MetavarContext) (mvarId : Lean.MVarId) (val : Lean.Expr) :

Lean.MetavarContext

Equations

Lean.MetavarContext.assignExpr m mvarId val = { depth := m.depth, mvarCounter := m.mvarCounter, lDepth := m.lDepth, decls := m.decls, userNames := m.userNames, lAssignment := m.lAssignment, eAssignment := Std.PersistentHashMap.insert m.eAssignment mvarId val, dAssignment := m.dAssignment }

source

def Lean.MetavarContext.assignDelayed (m : Lean.MetavarContext) (mvarId : Lean.MVarId) (lctx : Lean.LocalContext) (fvars : Array Lean.Expr) (val : Lean.Expr) :

Lean.MetavarContext

Equations

Lean.MetavarContext.assignDelayed m mvarId lctx fvars val = { depth := m.depth, mvarCounter := m.mvarCounter, lDepth := m.lDepth, decls := m.decls, userNames := m.userNames, lAssignment := m.lAssignment, eAssignment := m.eAssignment, dAssignment := Std.PersistentHashMap.insert m.dAssignment mvarId { lctx := lctx, fvars := fvars, val := val } }

source

def Lean.MetavarContext.getLevelAssignment? (m : Lean.MetavarContext) (mvarId : Lean.MVarId) :

Option Lean.Level

Equations

Lean.MetavarContext.getLevelAssignment? m mvarId = Std.PersistentHashMap.find? m.lAssignment mvarId

source

def Lean.MetavarContext.getExprAssignment? (m : Lean.MetavarContext) (mvarId : Lean.MVarId) :

Option Lean.Expr

Equations

Lean.MetavarContext.getExprAssignment? m mvarId = Std.PersistentHashMap.find? m.eAssignment mvarId

source

def Lean.MetavarContext.getDelayedAssignment? (m : Lean.MetavarContext) (mvarId : Lean.MVarId) :

Option Lean.DelayedMetavarAssignment

Equations

Lean.MetavarContext.getDelayedAssignment? m mvarId = Std.PersistentHashMap.find? m.dAssignment mvarId

source

def Lean.MetavarContext.isLevelAssigned (m : Lean.MetavarContext) (mvarId : Lean.MVarId) :

Bool

Equations

Lean.MetavarContext.isLevelAssigned m mvarId = Std.PersistentHashMap.contains m.lAssignment mvarId

source

def Lean.MetavarContext.isExprAssigned (m : Lean.MetavarContext) (mvarId : Lean.MVarId) :

Bool

Equations

Lean.MetavarContext.isExprAssigned m mvarId = Std.PersistentHashMap.contains m.eAssignment mvarId

source

def Lean.MetavarContext.isDelayedAssigned (m : Lean.MetavarContext) (mvarId : Lean.MVarId) :

Bool

Equations

Lean.MetavarContext.isDelayedAssigned m mvarId = Std.PersistentHashMap.contains m.dAssignment mvarId

source

def Lean.MetavarContext.eraseDelayed (m : Lean.MetavarContext) (mvarId : Lean.MVarId) :

Lean.MetavarContext

Equations

Lean.MetavarContext.eraseDelayed m mvarId = { depth := m.depth, mvarCounter := m.mvarCounter, lDepth := m.lDepth, decls := m.decls, userNames := m.userNames, lAssignment := m.lAssignment, eAssignment := m.eAssignment, dAssignment := Std.PersistentHashMap.erase m.dAssignment mvarId }

source

partial def Lean.MetavarContext.getDelayedRoot (m : Lean.MetavarContext) :

Lean.MVarId → Lean.MVarId

source

def Lean.MetavarContext.isLevelAssignable (mctx : Lean.MetavarContext) (mvarId : Lean.MVarId) :

Bool

Equations

Lean.MetavarContext.isLevelAssignable mctx mvarId = match Std.PersistentHashMap.find? mctx.lDepth mvarId with | some d => d == mctx.depth | x => panicWithPosWithDecl "Lean.MetavarContext" "Lean.MetavarContext.isLevelAssignable" 427 14 "unknown universe metavariable"

source

def Lean.MetavarContext.isExprAssignable (mctx : Lean.MetavarContext) (mvarId : Lean.MVarId) :

Bool

Equations

Lean.MetavarContext.isExprAssignable mctx mvarId = let decl := Lean.MetavarContext.getDecl mctx mvarId; decl.depth == mctx.depth

source

def Lean.MetavarContext.incDepth (mctx : Lean.MetavarContext) :

Lean.MetavarContext

Equations

Lean.MetavarContext.incDepth mctx = { depth := mctx.depth + 1, mvarCounter := mctx.mvarCounter, lDepth := mctx.lDepth, decls := mctx.decls, userNames := mctx.userNames, lAssignment := mctx.lAssignment, eAssignment := mctx.eAssignment, dAssignment := mctx.dAssignment }

source

def Lean.MetavarContext.hasAssignedLevelMVar (mctx : Lean.MetavarContext) :

Lean.Level → Bool

Equations

Lean.MetavarContext.hasAssignedLevelMVar mctx (Lean.Level.succ lvl x_1) = (Lean.Level.hasMVar lvl && Lean.MetavarContext.hasAssignedLevelMVar mctx lvl)
Lean.MetavarContext.hasAssignedLevelMVar mctx (Lean.Level.max lvl₁ lvl₂ x_1) = (Lean.Level.hasMVar lvl₁ && Lean.MetavarContext.hasAssignedLevelMVar mctx lvl₁ || Lean.Level.hasMVar lvl₂ && Lean.MetavarContext.hasAssignedLevelMVar mctx lvl₂)
Lean.MetavarContext.hasAssignedLevelMVar mctx (Lean.Level.imax lvl₁ lvl₂ x_1) = (Lean.Level.hasMVar lvl₁ && Lean.MetavarContext.hasAssignedLevelMVar mctx lvl₁ || Lean.Level.hasMVar lvl₂ && Lean.MetavarContext.hasAssignedLevelMVar mctx lvl₂)
Lean.MetavarContext.hasAssignedLevelMVar mctx (Lean.Level.mvar mvarId x_1) = Lean.MetavarContext.isLevelAssigned mctx mvarId
Lean.MetavarContext.hasAssignedLevelMVar mctx (Lean.Level.zero x_1) = false
Lean.MetavarContext.hasAssignedLevelMVar mctx (Lean.Level.param x_1 x_2) = false

source

def Lean.MetavarContext.hasAssignedMVar (mctx : Lean.MetavarContext) :

Lean.Expr → Bool

source

def Lean.MetavarContext.hasAssignableLevelMVar (mctx : Lean.MetavarContext) :

Lean.Level → Bool

Equations

Lean.MetavarContext.hasAssignableLevelMVar mctx (Lean.Level.succ lvl x_1) = (Lean.Level.hasMVar lvl && Lean.MetavarContext.hasAssignableLevelMVar mctx lvl)
Lean.MetavarContext.hasAssignableLevelMVar mctx (Lean.Level.max lvl₁ lvl₂ x_1) = (Lean.Level.hasMVar lvl₁ && Lean.MetavarContext.hasAssignableLevelMVar mctx lvl₁ || Lean.Level.hasMVar lvl₂ && Lean.MetavarContext.hasAssignableLevelMVar mctx lvl₂)
Lean.MetavarContext.hasAssignableLevelMVar mctx (Lean.Level.imax lvl₁ lvl₂ x_1) = (Lean.Level.hasMVar lvl₁ && Lean.MetavarContext.hasAssignableLevelMVar mctx lvl₁ || Lean.Level.hasMVar lvl₂ && Lean.MetavarContext.hasAssignableLevelMVar mctx lvl₂)
Lean.MetavarContext.hasAssignableLevelMVar mctx (Lean.Level.mvar mvarId x_1) = Lean.MetavarContext.isLevelAssignable mctx mvarId
Lean.MetavarContext.hasAssignableLevelMVar mctx (Lean.Level.zero x_1) = false
Lean.MetavarContext.hasAssignableLevelMVar mctx (Lean.Level.param x_1 x_2) = false

source

def Lean.MetavarContext.hasAssignableMVar (mctx : Lean.MetavarContext) :

Lean.Expr → Bool

source

partial def Lean.MetavarContext.instantiateLevelMVars {m : Type → Type} [inst : Monad m] [inst : Lean.MonadMCtx m] :

Lean.Level → m Lean.Level

source

partial def Lean.MetavarContext.instantiateExprMVars {m : Type → Type} {ω : outParam Type} [inst : Monad m] [inst : Lean.MonadMCtx m] [inst : STWorld ω m] [inst : MonadLiftT (ST ω) m] (e : Lean.Expr) :

Lean.MonadCacheT Lean.ExprStructEq Lean.Expr m Lean.Expr

source

instance Lean.MetavarContext.instMonadMCtxStateRefT'MetavarContextST {ω : Type} :

Lean.MonadMCtx (StateRefT' ω Lean.MetavarContext (ST ω))

Equations

Lean.MetavarContext.instMonadMCtxStateRefT'MetavarContextST = { getMCtx := get, modifyMCtx := modify }

source

def Lean.MetavarContext.instantiateMVars (mctx : Lean.MetavarContext) (e : Lean.Expr) :

Lean.Expr × Lean.MetavarContext

Equations

Lean.MetavarContext.instantiateMVars mctx e = if (!Lean.Expr.hasMVar e) = true then (e, mctx) else let instantiate := fun {ω} e => Lean.MetavarContext.instantiateExprMVars e; runST fun x => StateRefT'.run (Lean.MonadCacheT.run (instantiate e)) mctx

source

def Lean.MetavarContext.instantiateLCtxMVars (mctx : Lean.MetavarContext) (lctx : Lean.LocalContext) :

Lean.LocalContext × Lean.MetavarContext

Equations

Lean.MetavarContext.instantiateLCtxMVars mctx lctx = Lean.LocalContext.foldl lctx (fun x ldecl => match x with | (lctx, mctx) => match ldecl with | Lean.LocalDecl.cdecl x fvarId userName type bi => let x := Lean.MetavarContext.instantiateMVars mctx type; match x with | (type, mctx) => (Lean.LocalContext.mkLocalDecl lctx fvarId userName type bi, mctx) | Lean.LocalDecl.ldecl x fvarId userName type value nonDep => let x := Lean.MetavarContext.instantiateMVars mctx type; match x with | (type, mctx) => let x := Lean.MetavarContext.instantiateMVars mctx value; match x with | (value, mctx) => (Lean.LocalContext.mkLetDecl lctx fvarId userName type value nonDep, mctx)) ({ fvarIdToDecl := { root := Std.PersistentHashMap.Node.entries Std.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, decls := { root := Std.PersistentArrayNode.node (Array.mkEmpty (USize.toNat Std.PersistentArray.branching)), tail := Array.mkEmpty (USize.toNat Std.PersistentArray.branching), size := 0, shift := Std.PersistentArray.initShift, tailOff := 0 } }, mctx)

source

def Lean.MetavarContext.instantiateMVarDeclMVars (mctx : Lean.MetavarContext) (mvarId : Lean.MVarId) :

Lean.MetavarContext

Equations

Lean.MetavarContext.instantiateMVarDeclMVars mctx mvarId = let mvarDecl := Lean.MetavarContext.getDecl mctx mvarId; let x := Lean.MetavarContext.instantiateLCtxMVars mctx mvarDecl.lctx; match x with | (lctx, mctx) => let x := Lean.MetavarContext.instantiateMVars mctx mvarDecl.type; match x with | (type, mctx) => { depth := mctx.depth, mvarCounter := mctx.mvarCounter, lDepth := mctx.lDepth, decls := Std.PersistentHashMap.insert mctx.decls mvarId { userName := mvarDecl.userName, lctx := lctx, type := type, depth := mvarDecl.depth, localInstances := mvarDecl.localInstances, kind := mvarDecl.kind, numScopeArgs := mvarDecl.numScopeArgs, index := mvarDecl.index }, userNames := mctx.userNames, lAssignment := mctx.lAssignment, eAssignment := mctx.eAssignment, dAssignment := mctx.dAssignment }

source

@[inline]

def Lean.MetavarContext.DependsOn.main (mctx : Lean.MetavarContext) (p : Lean.FVarId → Bool) (e : Lean.Expr) :

Lean.MetavarContext.DependsOn.M Bool

Equations

Lean.MetavarContext.DependsOn.main mctx p e = if (!Lean.Expr.hasFVar e && !Lean.Expr.hasMVar e) = true then pure false else Lean.MetavarContext.DependsOn.dep mctx p e

source

@[inline]

def Lean.MetavarContext.findExprDependsOn (mctx : Lean.MetavarContext) (e : Lean.Expr) (p : Lean.FVarId → Bool) :

Bool

Equations

Lean.MetavarContext.findExprDependsOn mctx e p = StateT.run' (Lean.MetavarContext.DependsOn.main mctx p e) ∅

source

@[inline]

def Lean.MetavarContext.findLocalDeclDependsOn (mctx : Lean.MetavarContext) (localDecl : Lean.LocalDecl) (p : Lean.FVarId → Bool) :

Bool

Equations

Lean.MetavarContext.findLocalDeclDependsOn mctx localDecl p = match localDecl with | Lean.LocalDecl.cdecl x x_1 x_2 t x_3 => Lean.MetavarContext.findExprDependsOn mctx t p | Lean.LocalDecl.ldecl x x_1 x_2 t v x_3 => StateT.run' (Lean.MetavarContext.DependsOn.main mctx p t <||> Lean.MetavarContext.DependsOn.main mctx p v) ∅

source

def Lean.MetavarContext.exprDependsOn (mctx : Lean.MetavarContext) (e : Lean.Expr) (fvarId : Lean.FVarId) :

Bool

Equations

Lean.MetavarContext.exprDependsOn mctx e fvarId = Lean.MetavarContext.findExprDependsOn mctx e fun fvarId' => fvarId == fvarId'

source

def Lean.MetavarContext.localDeclDependsOn (mctx : Lean.MetavarContext) (localDecl : Lean.LocalDecl) (fvarId : Lean.FVarId) :

Bool

Equations

Lean.MetavarContext.localDeclDependsOn mctx localDecl fvarId = Lean.MetavarContext.findLocalDeclDependsOn mctx localDecl fun fvarId' => fvarId == fvarId'

source

inductive Lean.MetavarContext.MkBinding.Exception :

Type

revertFailure: Lean.MetavarContext → Lean.LocalContext → Array Lean.Expr → Lean.LocalDecl → Lean.MetavarContext.MkBinding.Exception

source

instance Lean.MetavarContext.MkBinding.instToStringException :

ToString Lean.MetavarContext.MkBinding.Exception

Equations

Lean.MetavarContext.MkBinding.instToStringException = { toString := fun x => match x with | Lean.MetavarContext.MkBinding.Exception.revertFailure x lctx toRevert decl => "failed to revert " ++ toString (Array.map (fun x => "'" ++ toString (Lean.LocalDecl.userName (Lean.LocalContext.getFVar! lctx x)) ++ "'") toRevert) ++ ", '" ++ toString (Lean.LocalDecl.userName decl) ++ "' depends on them, and it is an auxiliary declaration created by the elaborator" ++ " (possible solution: use tactic 'clear' to remove '" ++ toString (Lean.LocalDecl.userName decl) ++ "' from local context)" }

source

structure Lean.MetavarContext.MkBinding.State :

Type

mctx : Lean.MetavarContext
ngen : Lean.NameGenerator
cache : Std.HashMap Lean.ExprStructEq Lean.Expr

source

@[inline]

abbrev Lean.MetavarContext.MkBinding.MCore (α : Type) :

Type

Equations

Lean.MetavarContext.MkBinding.MCore = EStateM Lean.MetavarContext.MkBinding.Exception Lean.MetavarContext.MkBinding.State

source

@[inline]

abbrev Lean.MetavarContext.MkBinding.M (α : Type) :

Type

Equations

Lean.MetavarContext.MkBinding.M = ReaderT Bool Lean.MetavarContext.MkBinding.MCore

source

def Lean.MetavarContext.MkBinding.preserveOrder :

Lean.MetavarContext.MkBinding.M Bool

Equations

Lean.MetavarContext.MkBinding.preserveOrder = read

source

instance Lean.MetavarContext.MkBinding.instMonadHashMapCacheAdapterExprStructEqExprMInstBEqExprStructEqInstHashableExprStructEq :

Lean.MonadHashMapCacheAdapter Lean.ExprStructEq Lean.Expr Lean.MetavarContext.MkBinding.M

Equations

Lean.MetavarContext.MkBinding.instMonadHashMapCacheAdapterExprStructEqExprMInstBEqExprStructEqInstHashableExprStructEq = { getCache := do let s ← get pure s.cache, modifyCache := fun f => modify fun s => { mctx := s.mctx, ngen := s.ngen, cache := f s.cache } }

source

def Lean.MetavarContext.MkBinding.collectDeps (mctx : Lean.MetavarContext) (lctx : Lean.LocalContext) (toRevert : Array Lean.Expr) (preserveOrder : Bool) :

Except Lean.MetavarContext.MkBinding.Exception (Array Lean.Expr)

Equations

Lean.MetavarContext.MkBinding.collectDeps mctx lctx toRevert preserveOrder = if (Array.size toRevert == 0) = true then pure toRevert else let _do_jp := fun y => let newToRevert := if preserveOrder = true then toRevert else Array.mkEmpty (Array.size toRevert); let firstDeclToVisit := Lean.MetavarContext.MkBinding.getLocalDeclWithSmallestIdx lctx toRevert; let initSize := Array.size newToRevert; Lean.LocalContext.foldlM lctx (fun newToRevert decl => if Nat.any (fun i => Lean.LocalDecl.fvarId decl == Lean.Expr.fvarId! (Array.get! newToRevert i)) initSize = true then pure newToRevert else if Array.any toRevert (fun x => Lean.LocalDecl.fvarId decl == Lean.Expr.fvarId! x) 0 (Array.size toRevert) = true then pure (Array.push newToRevert (Lean.LocalDecl.toExpr decl)) else if (Lean.MetavarContext.findLocalDeclDependsOn mctx decl fun fvarId => Array.any newToRevert (fun x => Lean.Expr.fvarId! x == fvarId) 0 (Array.size newToRevert)) = true then pure (Array.push newToRevert (Lean.LocalDecl.toExpr decl)) else pure newToRevert) newToRevert (Lean.LocalDecl.index firstDeclToVisit); if preserveOrder = true then do let y ← Nat.forM (Array.size toRevert) fun i => let fvar := Array.getOp toRevert i; let decl := Lean.LocalContext.getFVar! lctx fvar; Nat.forM i fun j => let prevFVar := Array.getOp toRevert j; let prevDecl := Lean.LocalContext.getFVar! lctx prevFVar; if Lean.MetavarContext.localDeclDependsOn mctx prevDecl (Lean.Expr.fvarId! fvar) = true then throw (Lean.MetavarContext.MkBinding.Exception.revertFailure mctx lctx toRevert prevDecl) else pure PUnit.unit _do_jp y else do let y ← pure PUnit.unit _do_jp y

source

def Lean.MetavarContext.MkBinding.reduceLocalContext (lctx : Lean.LocalContext) (toRevert : Array Lean.Expr) :

Lean.LocalContext

Equations

Lean.MetavarContext.MkBinding.reduceLocalContext lctx toRevert = Array.foldr (fun x lctx => Lean.LocalContext.erase lctx (Lean.Expr.fvarId! x)) lctx toRevert (Array.size toRevert)

source

def Lean.MetavarContext.MkBinding.elimMVarDeps (xs : Array Lean.Expr) (e : Lean.Expr) :

Lean.MetavarContext.MkBinding.M Lean.Expr

Equations

Lean.MetavarContext.MkBinding.elimMVarDeps xs e = if (!Lean.Expr.hasMVar e) = true then pure e else Lean.MetavarContext.MkBinding.withFreshCache (Lean.MetavarContext.MkBinding.elim xs e)

source

def Lean.MetavarContext.MkBinding.revert (xs : Array Lean.Expr) (mvarId : Lean.MVarId) :

Lean.MetavarContext.MkBinding.M (Lean.Expr × Array Lean.Expr)

Equations

Lean.MetavarContext.MkBinding.revert xs mvarId = Lean.MetavarContext.MkBinding.withFreshCache (Lean.MetavarContext.MkBinding.elimMVar xs mvarId #[])

source

@[inline]

def Lean.MetavarContext.MkBinding.abstractRange (xs : Array Lean.Expr) (i : Nat) (e : Lean.Expr) :

Lean.MetavarContext.MkBinding.M Lean.Expr

Equations

Lean.MetavarContext.MkBinding.abstractRange xs i e = do let e ← Lean.MetavarContext.MkBinding.elimMVarDeps xs e pure (Lean.Expr.abstractRange e i xs)

source

@[specialize]

def Lean.MetavarContext.MkBinding.mkBinding (isLambda : Bool) (lctx : Lean.LocalContext) (xs : Array Lean.Expr) (e : Lean.Expr) (usedOnly : Bool) (usedLetOnly : Bool) :

Lean.MetavarContext.MkBinding.M (Lean.Expr × Nat)

Equations

Lean.MetavarContext.MkBinding.mkBinding isLambda lctx xs e usedOnly usedLetOnly = do let e ← Lean.MetavarContext.MkBinding.abstractRange xs (Array.size xs) e Nat.foldRevM (fun i p => let x := p; match x with | (e, num) => let x := Array.getOp xs i; match Lean.LocalContext.getFVar! lctx x with | Lean.LocalDecl.cdecl x x_1 n type bi => if (!usedOnly || Lean.Expr.hasLooseBVar e 0) = true then let type := Lean.Expr.headBeta type; do let type ← Lean.MetavarContext.MkBinding.abstractRange xs i type if isLambda = true then pure (Lean.mkLambda n bi type e, num + 1) else pure (Lean.mkForall n bi type e, num + 1) else pure (Lean.Expr.lowerLooseBVars e 1 1, num) | Lean.LocalDecl.ldecl x x_1 n type value nonDep => if (!usedLetOnly || Lean.Expr.hasLooseBVar e 0) = true then do let type ← Lean.MetavarContext.MkBinding.abstractRange xs i type let value ← Lean.MetavarContext.MkBinding.abstractRange xs i value pure (Lean.mkLet n type value e nonDep, num + 1) else pure (Lean.Expr.lowerLooseBVars e 1 1, num)) (e, 0) (Array.size xs)

source

@[inline]

abbrev Lean.MetavarContext.MkBindingM (α : Type) :

Type

Equations

Lean.MetavarContext.MkBindingM = ReaderT Lean.LocalContext Lean.MetavarContext.MkBinding.MCore

source

def Lean.MetavarContext.elimMVarDeps (xs : Array Lean.Expr) (e : Lean.Expr) (preserveOrder : Bool) :

Lean.MetavarContext.MkBindingM Lean.Expr

Equations

Lean.MetavarContext.elimMVarDeps xs e preserveOrder x = Lean.MetavarContext.MkBinding.elimMVarDeps xs e preserveOrder

source

def Lean.MetavarContext.revert (xs : Array Lean.Expr) (mvarId : Lean.MVarId) (preserveOrder : Bool) :

Lean.MetavarContext.MkBindingM (Lean.Expr × Array Lean.Expr)

Equations

Lean.MetavarContext.revert xs mvarId preserveOrder x = Lean.MetavarContext.MkBinding.revert xs mvarId preserveOrder

source

def Lean.MetavarContext.mkBinding (isLambda : Bool) (xs : Array Lean.Expr) (e : Lean.Expr) (usedOnly : optParam Bool false) (usedLetOnly : optParam Bool true) :

Lean.MetavarContext.MkBindingM (Lean.Expr × Nat)

Equations

Lean.MetavarContext.mkBinding isLambda xs e usedOnly usedLetOnly lctx = Lean.MetavarContext.MkBinding.mkBinding isLambda lctx xs e usedOnly usedLetOnly false

source

@[inline]

def Lean.MetavarContext.mkLambda (xs : Array Lean.Expr) (e : Lean.Expr) (usedOnly : optParam Bool false) (usedLetOnly : optParam Bool true) :

Lean.MetavarContext.MkBindingM Lean.Expr

Equations

Lean.MetavarContext.mkLambda xs e usedOnly usedLetOnly = do let discr ← Lean.MetavarContext.mkBinding true xs e usedOnly usedLetOnly let x : Lean.Expr × Nat := discr match x with | (e, x) => pure e

source

@[inline]

def Lean.MetavarContext.mkForall (xs : Array Lean.Expr) (e : Lean.Expr) (usedOnly : optParam Bool false) (usedLetOnly : optParam Bool true) :

Lean.MetavarContext.MkBindingM Lean.Expr

Equations

Lean.MetavarContext.mkForall xs e usedOnly usedLetOnly = do let discr ← Lean.MetavarContext.mkBinding false xs e usedOnly usedLetOnly let x : Lean.Expr × Nat := discr match x with | (e, x) => pure e

source

@[inline]

def Lean.MetavarContext.abstractRange (e : Lean.Expr) (n : Nat) (xs : Array Lean.Expr) :

Lean.MetavarContext.MkBindingM Lean.Expr

Equations

Lean.MetavarContext.abstractRange e n xs x = Lean.MetavarContext.MkBinding.abstractRange xs n e false

source

partial def Lean.MetavarContext.isWellFormed (mctx : Lean.MetavarContext) (lctx : Lean.LocalContext) :

Lean.Expr → Bool

source

structure Lean.MetavarContext.LevelMVarToParam.Context :

Type

paramNamePrefix : Lean.Name
alreadyUsedPred : Lean.Name → Bool

source

structure Lean.MetavarContext.LevelMVarToParam.State :

Type

mctx : Lean.MetavarContext
paramNames : Array Lean.Name
nextParamIdx : Nat
cache : Std.HashMap Lean.ExprStructEq Lean.Expr

source

@[inline]

abbrev Lean.MetavarContext.LevelMVarToParam.M (α : Type) :

Type

Equations

Lean.MetavarContext.LevelMVarToParam.M = ReaderT Lean.MetavarContext.LevelMVarToParam.Context (StateM Lean.MetavarContext.LevelMVarToParam.State)

source

instance Lean.MetavarContext.LevelMVarToParam.instMonadCacheExprStructEqExprM :

Lean.MonadCache Lean.ExprStructEq Lean.Expr Lean.MetavarContext.LevelMVarToParam.M

Equations

Lean.MetavarContext.LevelMVarToParam.instMonadCacheExprStructEqExprM = { findCached? := fun e => do let a ← get pure (Std.HashMap.find? a.cache e), cache := fun e v => modify fun s => { mctx := s.mctx, paramNames := s.paramNames, nextParamIdx := s.nextParamIdx, cache := Std.HashMap.insert s.cache e v } }

source

partial def Lean.MetavarContext.LevelMVarToParam.mkParamName :

Lean.MetavarContext.LevelMVarToParam.M Lean.Name

source

partial def Lean.MetavarContext.LevelMVarToParam.visitLevel (u : Lean.Level) :

Lean.MetavarContext.LevelMVarToParam.M Lean.Level

source

partial def Lean.MetavarContext.LevelMVarToParam.main (e : Lean.Expr) :

Lean.MetavarContext.LevelMVarToParam.M Lean.Expr

source

partial def Lean.MetavarContext.LevelMVarToParam.main.visitApp (f : Lean.Expr) (args : Array Lean.Expr) :

Lean.MetavarContext.LevelMVarToParam.M Lean.Expr

source

structure Lean.MetavarContext.UnivMVarParamResult :

Type

mctx : Lean.MetavarContext
newParamNames : Array Lean.Name
nextParamIdx : Nat
expr : Lean.Expr

source

def Lean.MetavarContext.levelMVarToParam (mctx : Lean.MetavarContext) (alreadyUsedPred : Lean.Name → Bool) (e : Lean.Expr) (paramNamePrefix : optParam Lean.Name `u) (nextParamIdx : optParam Nat 1) :

Lean.MetavarContext.UnivMVarParamResult

Equations

Lean.MetavarContext.levelMVarToParam mctx alreadyUsedPred e paramNamePrefix nextParamIdx = let x := Lean.MetavarContext.LevelMVarToParam.main e { paramNamePrefix := paramNamePrefix, alreadyUsedPred := alreadyUsedPred } { mctx := mctx, paramNames := #[], nextParamIdx := nextParamIdx, cache := ∅ }; match x with | (e, s) => { mctx := s.mctx, newParamNames := s.paramNames, nextParamIdx := s.nextParamIdx, expr := e }

source

def Lean.MetavarContext.getExprAssignmentDomain (mctx : Lean.MetavarContext) :

Array Lean.MVarId

Equations

Lean.MetavarContext.getExprAssignmentDomain mctx = Std.PersistentHashMap.foldl mctx.eAssignment (fun a mvarId x => Array.push a mvarId) #[]