From a05244641472e2f080ebb87010fb867d09ca7638 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 20 Oct 2020 15:08:16 -0700 Subject: [PATCH] feat: simplify `decide!` and `nativeDecide!` macros --- src/Lean/Elab/BuiltinNotation.lean | 30 ++++++++++++------------------ src/Lean/Parser/Term.lean | 4 ++-- tests/lean/run/doNotation3.lean | 4 ++-- tests/lean/run/reduce1.lean | 16 ++++++++-------- tests/lean/run/reduce3.lean | 8 ++++---- 5 files changed, 28 insertions(+), 34 deletions(-) diff --git a/src/Lean/Elab/BuiltinNotation.lean b/src/Lean/Elab/BuiltinNotation.lean index f06e4a7297..f5901af294 100644 --- a/src/Lean/Elab/BuiltinNotation.lean +++ b/src/Lean/Elab/BuiltinNotation.lean @@ -156,25 +156,20 @@ fun stx _ => do let eq ← mkEq e val mkExpectedTypeHint r eq -private def getPropToDecide (arg : Syntax) (expectedType? : Option Expr) : TermElabM Expr := do -if arg.isOfKind `Lean.Parser.Term.hole then - tryPostponeIfNoneOrMVar expectedType? - match expectedType? with - | none => throwError "invalid macro, expected type is not available" - | some expectedType => - synthesizeSyntheticMVars - let expectedType ← instantiateMVars expectedType - if expectedType.hasFVar || expectedType.hasMVar then - throwError! "expected type must not contain free or meta variables{indentExpr expectedType}" - pure expectedType -else - let prop := mkSort levelZero - elabClosedTerm arg prop +private def getPropToDecide (expectedType? : Option Expr) : TermElabM Expr := do +tryPostponeIfNoneOrMVar expectedType? +match expectedType? with +| none => throwError "invalid macro, expected type is not available" +| some expectedType => + synthesizeSyntheticMVars + let expectedType ← instantiateMVars expectedType + if expectedType.hasFVar || expectedType.hasMVar then + throwError! "expected type must not contain free or meta variables{indentExpr expectedType}" + pure expectedType @[builtinTermElab «nativeDecide»] def elabNativeDecide : TermElab := fun stx expectedType? => do - let arg := stx[1] - let p ← getPropToDecide arg expectedType? + let p ← getPropToDecide expectedType? let d ← mkAppM `Decidable.decide #[p] let auxDeclName ← mkNativeReflAuxDecl (Lean.mkConst `Bool) d let rflPrf ← mkEqRefl (toExpr true) @@ -183,8 +178,7 @@ fun stx expectedType? => do @[builtinTermElab Lean.Parser.Term.decide] def elabDecide : TermElab := fun stx expectedType? => do - let arg := stx[1] - let p ← getPropToDecide arg expectedType? + let p ← getPropToDecide expectedType? let d ← mkAppM `Decidable.decide #[p] let d ← instantiateMVars d let s := d.appArg! -- get instance from `d` diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean index d2c832d64b..655faa2675 100644 --- a/src/Lean/Parser/Term.lean +++ b/src/Lean/Parser/Term.lean @@ -170,8 +170,8 @@ def letRecDecls := sepBy1 (group (optional «attributes» >> letDecl)) ", " parser!:leadPrec withPosition (group ("let " >> nonReservedSymbol "rec ") >> letRecDecls) >> optSemicolon termParser @[builtinTermParser] def nativeRefl := parser! "nativeRefl! " >> termParser maxPrec -@[builtinTermParser] def nativeDecide := parser! "nativeDecide! " >> termParser maxPrec -@[builtinTermParser] def decide := parser! "decide! " >> termParser maxPrec +@[builtinTermParser] def nativeDecide := parser! "nativeDecide!" +@[builtinTermParser] def decide := parser! "decide!" @[builtinTermParser] def typeOf := parser! "typeOf! " >> termParser maxPrec @[builtinTermParser] def ensureTypeOf := parser! "ensureTypeOf! " >> termParser maxPrec >> strLit >> termParser diff --git a/tests/lean/run/doNotation3.lean b/tests/lean/run/doNotation3.lean index 7f5178bcee..ab7754776d 100644 --- a/tests/lean/run/doNotation3.lean +++ b/tests/lean/run/doNotation3.lean @@ -11,7 +11,7 @@ let rec loop : (i : Nat) → i ≤ as.size → β → m β | 0, h, b => b | i+1, h, b => do have h' : i < as.size from Nat.ltOfLtOfLe (Nat.ltSuccSelf i) h - have as.size - 1 < as.size from Nat.subLt (zeroLtOfLt h') (decide! (0 < 1)) + have as.size - 1 < as.size from Nat.subLt (zeroLtOfLt h') (decide! : (0:Nat) < 1) have as.size - 1 - i < as.size from Nat.ltOfLeOfLt (Nat.subLe (as.size - 1) i) this let b ← f (as.get ⟨as.size - 1 - i, this⟩) b loop i (Nat.leOfLt h') b @@ -28,7 +28,7 @@ let rec loop (i : Nat) (h : i ≤ as.size) (b : β) : m β := do | 0, h => return b | i+1, h => have h' : i < as.size from Nat.ltOfLtOfLe (Nat.ltSuccSelf i) h - have as.size - 1 < as.size from Nat.subLt (zeroLtOfLt h') (decide! (0 < 1)) + have as.size - 1 < as.size from Nat.subLt (zeroLtOfLt h') (decide! : (0:Nat) < 1) have as.size - 1 - i < as.size from Nat.ltOfLeOfLt (Nat.subLe (as.size - 1) i) this let b ← f (as.get ⟨as.size - 1 - i, this⟩) b loop i (Nat.leOfLt h') b diff --git a/tests/lean/run/reduce1.lean b/tests/lean/run/reduce1.lean index 99215eabf1..3a71e6b462 100644 --- a/tests/lean/run/reduce1.lean +++ b/tests/lean/run/reduce1.lean @@ -20,23 +20,23 @@ theorem tst4 : 10000000000000000 < 200000000000000000000 := ofDecideEqTrue (nativeRefl! (decide (10000000000000000 < 200000000000000000000))) theorem tst5 : 10000000000000000 < 200000000000000000000 := -nativeDecide! (10000000000000000 < 200000000000000000000) +nativeDecide! theorem tst6 : 10000000000000000 < 200000000000000000000 := -let h₁ := nativeDecide! (10000000000000000 < 10000000000000010); -let h₂ := nativeDecide! (10000000000000010 < 200000000000000000000); +let h₁ := (nativeDecide! : (10000000000000000:Nat) < 10000000000000010) +let h₂ := (nativeDecide! : (10000000000000010:Nat) < 200000000000000000000) Nat.ltTrans h₁ h₂ theorem tst7 : 10000000000000000 < 200000000000000000000 := -decide! (10000000000000000 < 200000000000000000000) +decide! theorem tst8 : 10000000000000000 < 200000000000000000000 := -let h₁ := decide! (10000000000000000 < 10000000000000010); -let h₂ := decide! (10000000000000010 < 200000000000000000000); +let h₁ := (decide! : (10000000000000000:Nat) < 10000000000000010) +let h₂ := (decide! : (10000000000000010:Nat) < 200000000000000000000) Nat.ltTrans h₁ h₂ theorem tst9 : 10000000000000000 < 200000000000000000000 := -decide! _ +decide! theorem tst10 : 10000000000000000 < 200000000000000000000 := -nativeDecide! _ +nativeDecide! diff --git a/tests/lean/run/reduce3.lean b/tests/lean/run/reduce3.lean index 5e5bb21cff..161d2fc09a 100644 --- a/tests/lean/run/reduce3.lean +++ b/tests/lean/run/reduce3.lean @@ -32,15 +32,15 @@ theorem tst8 : "hello" ++ "world" = "helloworld" := rfl theorem tst9 : "abc" ≠ "cde" := -decide! _ +decide! theorem tst10 : "helloWorld" ≠ "helloworld" := -decide! _ +decide! theorem tst11 : "helloWorld" = "helloWorld" := -decide! _ +decide! theorem tst12 : 'a' ≠ 'c' := -decide! _ +decide! #check tst10