max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: add hasAssignableMVar

Browse source
This commit is contained in:
Leonardo de Moura 2019-12-01 18:28:04 -08:00
parent a55841aa68
commit 5682c6e33b
2 changed files with 20 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/Init/Lean/Meta/Basic.lean
View file

@ -294,6 +294,10 @@ 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 }
def hasAssignableMVar (e : Expr) : MetaM Bool :=
do mctx ← getMCtx;
pure $ mctx.hasAssignableMVar e
def dbgTrace {α} [HasToString α] (a : α) : MetaM Unit :=
_root_.dbgTrace (toString a) $ fun _ => pure ()

16
src/Init/Lean/MetavarContext.lean
View file

@ -365,6 +365,22 @@ def hasAssignableLevelMVar (mctx : MetavarContext) : Level → Bool
| Level.zero _ => false
| Level.param _ _ => false
/-- Return `true` iff expression contains a metavariable that can be assigned. -/
def hasAssignableMVar (mctx : MetavarContext) : Expr → Bool
| Expr.const _ lvls _ => lvls.any (hasAssignableLevelMVar mctx)
| Expr.sort lvl _ => hasAssignableLevelMVar mctx lvl
| Expr.app f a _ => (f.hasMVar && hasAssignableMVar f) || (a.hasMVar && hasAssignableMVar a)
| Expr.letE _ t v b _ => (t.hasMVar && hasAssignableMVar t) || (v.hasMVar && hasAssignableMVar v) || (b.hasMVar && hasAssignableMVar b)
| Expr.forallE _ d b _ => (d.hasMVar && hasAssignableMVar d) || (b.hasMVar && hasAssignableMVar b)
| Expr.lam _ d b _ => (d.hasMVar && hasAssignableMVar d) || (b.hasMVar && hasAssignableMVar b)
| Expr.fvar _ _ => false
| Expr.bvar _ _ => false
| Expr.lit _ _ => false
| Expr.mdata _ e _ => e.hasMVar && hasAssignableMVar e
| Expr.proj _ _ e _ => e.hasMVar && hasAssignableMVar e
| Expr.mvar mvarId _ => mctx.isExprAssignable mvarId
| Expr.localE _ _ _ _ => unreachable!
partial def instantiateLevelMVars : Level → StateM MetavarContext Level
| lvl@(Level.succ lvl₁ _) => do lvl₁ ← instantiateLevelMVars lvl₁; pure (Level.updateSucc! lvl lvl₁)
| lvl@(Level.max lvl₁ lvl₂ _) => do lvl₁ ← instantiateLevelMVars lvl₁; lvl₂ ← instantiateLevelMVars lvl₂; pure (Level.updateMax! lvl lvl₁ lvl₂)