From 2ae92340efd6174b97876883236ee514bb2a1184 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 5 Dec 2019 10:57:48 -0800 Subject: [PATCH] feat: add `intro` and `assumption` --- src/Init/Lean/Meta.lean | 1 + src/Init/Lean/Meta/Tactic.lean | 8 +++ src/Init/Lean/Meta/Tactic/Assumption.lean | 27 +++++++++ src/Init/Lean/Meta/Tactic/Intro.lean | 73 +++++++++++++++++++++++ src/Init/Lean/Meta/Tactic/Util.lean | 27 +++++++++ tests/lean/run/tactic.lean | 21 +++++++ 6 files changed, 157 insertions(+) create mode 100644 src/Init/Lean/Meta/Tactic.lean create mode 100644 src/Init/Lean/Meta/Tactic/Assumption.lean create mode 100644 src/Init/Lean/Meta/Tactic/Intro.lean create mode 100644 src/Init/Lean/Meta/Tactic/Util.lean create mode 100644 tests/lean/run/tactic.lean diff --git a/src/Init/Lean/Meta.lean b/src/Init/Lean/Meta.lean index 659031cdec..a0ba448e37 100644 --- a/src/Init/Lean/Meta.lean +++ b/src/Init/Lean/Meta.lean @@ -16,3 +16,4 @@ import Init.Lean.Meta.Instances import Init.Lean.Meta.AbstractMVars import Init.Lean.Meta.SynthInstance import Init.Lean.Meta.AppBuilder +import Init.Lean.Meta.Tactic diff --git a/src/Init/Lean/Meta/Tactic.lean b/src/Init/Lean/Meta/Tactic.lean new file mode 100644 index 0000000000..9d200763a3 --- /dev/null +++ b/src/Init/Lean/Meta/Tactic.lean @@ -0,0 +1,8 @@ +/- +Copyright (c) 2019 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Leonardo de Moura +-/ +prelude +import Init.Lean.Meta.Tactic.Intro +import Init.Lean.Meta.Tactic.Assumption diff --git a/src/Init/Lean/Meta/Tactic/Assumption.lean b/src/Init/Lean/Meta/Tactic/Assumption.lean new file mode 100644 index 0000000000..134e256b64 --- /dev/null +++ b/src/Init/Lean/Meta/Tactic/Assumption.lean @@ -0,0 +1,27 @@ +/- +Copyright (c) 2019 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Leonardo de Moura +-/ +prelude +import Init.Lean.Meta.ExprDefEq +import Init.Lean.Meta.Tactic.Util + +namespace Lean +namespace Meta + +def assumptionAux (mvarId : MVarId) : MetaM Bool := +withMVarContext mvarId $ do + checkNotAssigned mvarId "assumption"; + mvarType ← getMVarType mvarId; + lctx ← getLCtx; + h? ← lctx.findDeclRevM $ fun decl => condM (isDefEq mvarType decl.type) (pure (some decl.toExpr)) (pure none); + match h? with + | some h => do assignExprMVar mvarId h; pure true + | none => pure false + +def assumption (mvarId : MVarId) : MetaM Unit := +unlessM (assumptionAux mvarId) $ throw $ Exception.other "`assumption` failed" + +end Meta +end Lean diff --git a/src/Init/Lean/Meta/Tactic/Intro.lean b/src/Init/Lean/Meta/Tactic/Intro.lean new file mode 100644 index 0000000000..d8cbbc054d --- /dev/null +++ b/src/Init/Lean/Meta/Tactic/Intro.lean @@ -0,0 +1,73 @@ +/- +Copyright (c) 2019 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Leonardo de Moura +-/ +prelude +import Init.Lean.Meta.Tactic.Util + +namespace Lean +namespace Meta + +@[specialize] +def introNCoreAux {σ} (mvarId : MVarId) (mkName : LocalContext → Name → σ → Name × σ) + : Nat → LocalContext → Array Expr → Nat → σ → Expr → MetaM (Array Expr × MVarId) +| 0, lctx, fvars, j, _, type => + let type := type.instantiateRevRange j fvars.size fvars; + adaptReader (fun (ctx : Context) => { lctx := lctx, .. ctx }) $ + withNewLocalInstances isClassExpensive fvars j $ do + newMVar ← mkFreshExprSyntheticMVar type; + lctx ← getLCtx; + modify $ fun s => { mctx := s.mctx.assignDelayed mvarId lctx fvars newMVar, .. s }; + pure $ (fvars, newMVar.mvarId!) +| (i+1), lctx, fvars, j, s, Expr.letE n type val body _ => do + let type := type.instantiateRevRange j fvars.size fvars; + let val := val.instantiateRevRange j fvars.size fvars; + fvarId ← mkFreshId; + let (n, s) := mkName lctx n s; + let lctx := lctx.mkLetDecl fvarId n type val; + let fvar := mkFVar fvarId; + let fvars := fvars.push fvar; + introNCoreAux i lctx fvars j s body +| (i+1), lctx, fvars, j, s, Expr.forallE n type body c => do + let type := type.instantiateRevRange j fvars.size fvars; + fvarId ← mkFreshId; + let (n, s) := mkName lctx n s; + let lctx := lctx.mkLocalDecl fvarId n type c.binderInfo; + let fvar := mkFVar fvarId; + let fvars := fvars.push fvar; + introNCoreAux i lctx fvars j s body +| (i+1), lctx, fvars, j, s, type => + let type := type.instantiateRevRange j fvars.size fvars; + adaptReader (fun (ctx : Context) => { lctx := lctx, .. ctx }) $ + withNewLocalInstances isClassExpensive fvars j $ do + newType ← whnf type; + if newType.isForall then + introNCoreAux i lctx fvars fvars.size s newType + else + throw $ Exception.other "`introN` failed insufficient number of binders" + +@[specialize] def introNCore {σ} (mvarId : MVarId) (n : Nat) (mkName : LocalContext → Name → σ → Name × σ) (s : σ) : MetaM (Array Expr × MVarId) := +withMVarContext mvarId $ do + checkNotAssigned mvarId "introN"; + mvarType ← getMVarType mvarId; + lctx ← getLCtx; + introNCoreAux mvarId mkName n lctx #[] 0 s mvarType + +def mkAuxName (lctx : LocalContext) (defaultName : Name) : List Name → Name × List Name +| [] => (lctx.getUnusedName defaultName, []) +| n :: rest => (if n == "_" then lctx.getUnusedName defaultName else n, rest) + +def introN (mvarId : MVarId) (n : Nat) (givenNames : List Name := []) : MetaM (Array Expr × MVarId) := +introNCore mvarId n mkAuxName givenNames + +def intro (mvarId : MVarId) (name : Name) : MetaM (Expr × MVarId) := +do (fvars, mvarid) ← introN mvarId 1 [name]; + pure (fvars.get! 0, mvarId) + +def intro1 (mvarId : MVarId) : MetaM (Expr × MVarId) := +do (fvars, mvarid) ← introN mvarId 1 []; + pure (fvars.get! 0, mvarId) + +end Meta +end Lean diff --git a/src/Init/Lean/Meta/Tactic/Util.lean b/src/Init/Lean/Meta/Tactic/Util.lean new file mode 100644 index 0000000000..d9fbc3ed9f --- /dev/null +++ b/src/Init/Lean/Meta/Tactic/Util.lean @@ -0,0 +1,27 @@ +/- +Copyright (c) 2019 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Leonardo de Moura +-/ +prelude +import Init.Lean.Meta.Basic + +namespace Lean +namespace Meta + +def mkFreshExprSyntheticMVar (type : Expr) (userName : Name := Name.anonymous) : MetaM Expr := +mkFreshExprMVar type userName true + +def checkNotAssigned (mvarId : MVarId) (tacticName : String) : MetaM Unit := +whenM (isExprMVarAssigned mvarId) $ + throw $ Exception.other ("`" ++ tacticName ++ "` failed, metavariable has already been assigned") + +def getMVarType (mvarId : MVarId) : MetaM Expr := +do mvarDecl ← getMVarDecl mvarId; + pure mvarDecl.type + +@[init] private def regTraceClasses : IO Unit := +registerTraceClass `Meta.Tactic + +end Meta +end Lean diff --git a/tests/lean/run/tactic.lean b/tests/lean/run/tactic.lean new file mode 100644 index 0000000000..5f95557887 --- /dev/null +++ b/tests/lean/run/tactic.lean @@ -0,0 +1,21 @@ +import Init.Lean.Meta +open Lean +open Lean.Meta + +axiom simple : forall {p q : Prop}, p → q → p + +def print (msg : MessageData) : MetaM Unit := +trace! `Meta.Tactic msg + +set_option trace.Meta.Tactic true + +def tst1 : MetaM Unit := +do cinfo ← getConstInfo `simple; + mvar ← mkFreshExprSyntheticMVar cinfo.type; + let mvarId := mvar.mvarId!; + (_, mvarId) ← introN mvarId 4; + assumption mvarId; + result ← instantiateMVars mvar; + print result + +#eval tst1