From 8a7edf03caebc844629f5d2069a2148e5f2c58e3 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 16 Aug 2020 10:55:15 -0700 Subject: [PATCH] feat: add `commitWhenSome?` --- src/Lean/Meta/LevelDefEq.lean | 26 ++++++++++++++++++-------- 1 file changed, 18 insertions(+), 8 deletions(-) diff --git a/src/Lean/Meta/LevelDefEq.lean b/src/Lean/Meta/LevelDefEq.lean index 17530f485a..2a6754be18 100644 --- a/src/Lean/Meta/LevelDefEq.lean +++ b/src/Lean/Meta/LevelDefEq.lean @@ -194,25 +194,35 @@ def restore (env : Environment) (mctx : MetavarContext) (postponed : PersistentA modify $ fun s => { s with env := env, mctx := mctx, postponed := postponed } /-- - `commitWhen x` executes `x` and process all postponed universe level constraints produced by `x`. - We keep the modifications only if both return `true`. + `commitWhenSome? x` executes `x` and process all postponed universe level constraints produced by `x`. + We keep the modifications only if `processPostponed` return true and `x` returned `some a`. Remark: postponed universe level constraints must be solved before returning. Otherwise, we don't know whether `x` really succeeded. -/ -@[specialize] def commitWhen (x : MetaM Bool) : MetaM Bool := do +@[specialize] def commitWhenSome? {α} (x? : MetaM (Option α)) : MetaM (Option α) := do s ← get; let env := s.env; let mctx := s.mctx; let postponed := s.postponed; modify $ fun s => { s with postponed := {} }; catch - (condM x - (condM processPostponed - (pure true) - (do restore env mctx postponed; pure false)) - (do restore env mctx postponed; pure false)) + (do + a? ← x?; + match a? with + | some a => + (condM processPostponed + (pure (some a)) + (do restore env mctx postponed; pure none)) + | none => do + restore env mctx postponed; pure none) (fun ex => do restore env mctx postponed; throw ex) +@[specialize] def commitWhen (x : MetaM Bool) : MetaM Bool := do +r? ← commitWhenSome? (condM x (pure $ some ()) (pure none)); +match r? with +| some _ => pure true +| none => pure false + /- Public interface -/ def isLevelDefEq (u v : Level) : MetaM Bool :=