chore: move to new frontend
This commit is contained in:
Leonardo de Moura
parent
152f275aac
commit
728ff419c7
1 changed files with 63 additions and 66 deletions
|
|
@ -1,3 +1,4 @@
|
|||
#lang lean4
|
||||
/-
|
||||
Copyright (c) 2019 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
|
|
@ -5,90 +6,86 @@ Authors: Leonardo de Moura
|
|||
-/
|
||||
import Lean.Meta.Tactic.Util
|
||||
|
||||
namespace Lean
|
||||
namespace Meta
|
||||
namespace Lean.Meta
|
||||
|
||||
@[specialize]
|
||||
private partial def introNImpAux {σ} (mvarId : MVarId) (mkName : LocalContext → Name → σ → MetaM (Name × σ))
|
||||
: Nat → LocalContext → Array Expr → Nat → σ → Expr → MetaM (Array Expr × MVarId)
|
||||
| 0, lctx, fvars, j, _, type =>
|
||||
let type := type.instantiateRevRange j fvars.size fvars;
|
||||
withReader (fun ctx => { ctx with lctx := lctx }) $
|
||||
withNewLocalInstances fvars j $ do
|
||||
tag ← getMVarTag mvarId;
|
||||
let type := type.headBeta;
|
||||
newMVar ← mkFreshExprSyntheticOpaqueMVar type tag;
|
||||
lctx ← getLCtx;
|
||||
newVal ← mkLambdaFVars fvars newMVar;
|
||||
assignExprMVar mvarId newVal;
|
||||
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 type := type.headBeta;
|
||||
let val := val.instantiateRevRange j fvars.size fvars;
|
||||
fvarId ← mkFreshId;
|
||||
(n, s) ← mkName lctx n s;
|
||||
let lctx := lctx.mkLetDecl fvarId n type val;
|
||||
let fvar := mkFVar fvarId;
|
||||
let fvars := fvars.push fvar;
|
||||
introNImpAux 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;
|
||||
let type := type.headBeta;
|
||||
fvarId ← mkFreshId;
|
||||
(n, s) ← mkName lctx n s;
|
||||
let lctx := lctx.mkLocalDecl fvarId n type c.binderInfo;
|
||||
let fvar := mkFVar fvarId;
|
||||
let fvars := fvars.push fvar;
|
||||
introNImpAux i lctx fvars j s body
|
||||
| (i+1), lctx, fvars, j, s, type =>
|
||||
let type := type.instantiateRevRange j fvars.size fvars;
|
||||
withReader (fun ctx => { ctx with lctx := lctx }) $
|
||||
withNewLocalInstances fvars j $ do
|
||||
newType ← whnf type;
|
||||
if newType.isForall then
|
||||
introNImpAux (i+1) lctx fvars fvars.size s newType
|
||||
else
|
||||
throwTacticEx `introN mvarId "insufficient number of binders"
|
||||
|
||||
@[specialize] private def introNImp {σ} (mvarId : MVarId) (n : Nat) (mkName : LocalContext → Name → σ → MetaM (Name × σ)) (s : σ) : MetaM (Array FVarId × MVarId) :=
|
||||
withMVarContext mvarId $ do
|
||||
checkNotAssigned mvarId `introN;
|
||||
mvarType ← getMVarType mvarId;
|
||||
lctx ← getLCtx;
|
||||
(fvars, mvarId) ← introNImpAux mvarId mkName n lctx #[] 0 s mvarType;
|
||||
@[inline] private partial def introNImp {σ} (mvarId : MVarId) (n : Nat) (mkName : LocalContext → Name → σ → MetaM (Name × σ)) (s : σ)
|
||||
: MetaM (Array FVarId × MVarId) :=
|
||||
withMVarContext mvarId do
|
||||
checkNotAssigned mvarId `introN
|
||||
let mvarType ← getMVarType mvarId
|
||||
let lctx ← getLCtx
|
||||
let rec @[specialize] loop : Nat → LocalContext → Array Expr → Nat → σ → Expr → MetaM (Array Expr × MVarId)
|
||||
| 0, lctx, fvars, j, _, type =>
|
||||
let type := type.instantiateRevRange j fvars.size fvars
|
||||
withReader (fun ctx => { ctx with lctx := lctx }) $
|
||||
withNewLocalInstances fvars j $ do
|
||||
let tag ← getMVarTag mvarId
|
||||
let type := type.headBeta
|
||||
let newMVar ← mkFreshExprSyntheticOpaqueMVar type tag
|
||||
let lctx ← getLCtx
|
||||
let newVal ← mkLambdaFVars fvars newMVar
|
||||
assignExprMVar mvarId newVal
|
||||
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 type := type.headBeta
|
||||
let val := val.instantiateRevRange j fvars.size fvars
|
||||
let 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
|
||||
loop 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
|
||||
let type := type.headBeta
|
||||
let 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
|
||||
loop i lctx fvars j s body
|
||||
| (i+1), lctx, fvars, j, s, type =>
|
||||
let type := type.instantiateRevRange j fvars.size fvars
|
||||
withReader (fun ctx => { ctx with lctx := lctx }) $
|
||||
withNewLocalInstances fvars j do
|
||||
let newType ← whnf type
|
||||
if newType.isForall then
|
||||
loop (i+1) lctx fvars fvars.size s newType
|
||||
else
|
||||
throwTacticEx `introN mvarId "insufficient number of binders"
|
||||
let (fvars, mvarId) ← loop n lctx #[] 0 s mvarType
|
||||
pure (fvars.map Expr.fvarId!, mvarId)
|
||||
|
||||
def hygienicIntroDef := true
|
||||
|
||||
def hygienicIntroDefault := true
|
||||
def getHygienicIntro : MetaM Bool := do
|
||||
o ← getOptions;
|
||||
pure $ o.get `hygienicIntro hygienicIntroDef
|
||||
let o ← getOptions
|
||||
pure $ o.get `hygienicIntro hygienicIntroDefault
|
||||
|
||||
@[init] def registerHygienicIntro : IO Unit :=
|
||||
registerOption `hygienicIntro { defValue := hygienicIntroDef, group := "tactic", descr := "make sure 'intro'-like tactics are hygienic" }
|
||||
initialize registerOption `hygienicIntro { defValue := hygienicIntroDefault, group := "tactic", descr := "make sure 'intro'-like tactics are hygienic" }
|
||||
|
||||
private def mkAuxNameImp (preserveBinderNames : Bool) (hygienic : Bool) (lctx : LocalContext) (binderName : Name) : List Name → MetaM (Name × List Name)
|
||||
| [] =>
|
||||
| [] => do
|
||||
if preserveBinderNames then
|
||||
pure (binderName, [])
|
||||
else if hygienic then do
|
||||
binderName ← mkFreshUserName binderName;
|
||||
let binderName ← mkFreshUserName binderName;
|
||||
pure (binderName, [])
|
||||
else
|
||||
pure (lctx.getUnusedName binderName, [])
|
||||
| n :: rest =>
|
||||
if n != "_" then pure (n, rest)
|
||||
| n :: rest => do
|
||||
if n != mkNameSimple "_" then
|
||||
pure (n, rest)
|
||||
else if preserveBinderNames then
|
||||
pure (binderName, rest)
|
||||
else if hygienic then do
|
||||
binderName ← mkFreshUserName binderName;
|
||||
else if hygienic then
|
||||
let binderName ← mkFreshUserName binderName
|
||||
pure (binderName, rest)
|
||||
else
|
||||
pure (lctx.getUnusedName binderName, rest)
|
||||
|
||||
def introNCore (mvarId : MVarId) (n : Nat) (givenNames : List Name) (preserveBinderNames : Bool) : MetaM (Array FVarId × MVarId) := do
|
||||
hygienic ← getHygienicIntro;
|
||||
let hygienic ← getHygienicIntro
|
||||
if n == 0 then pure (#[], mvarId)
|
||||
else introNImp mvarId n (mkAuxNameImp preserveBinderNames hygienic) givenNames
|
||||
|
||||
|
|
@ -99,11 +96,11 @@ abbrev introNP (mvarId : MVarId) (n : Nat) : MetaM (Array FVarId × MVarId) :=
|
|||
introNCore mvarId n [] true
|
||||
|
||||
def intro (mvarId : MVarId) (name : Name) : MetaM (FVarId × MVarId) := do
|
||||
(fvarIds, mvarId) ← introN mvarId 1 [name];
|
||||
let (fvarIds, mvarId) ← introN mvarId 1 [name]
|
||||
pure (fvarIds.get! 0, mvarId)
|
||||
|
||||
def intro1Core (mvarId : MVarId) (preserveBinderNames : Bool) : MetaM (FVarId × MVarId) := do
|
||||
(fvarIds, mvarId) ← introNCore mvarId 1 [] preserveBinderNames;
|
||||
let (fvarIds, mvarId) ← introNCore mvarId 1 [] preserveBinderNames
|
||||
pure (fvarIds.get! 0, mvarId)
|
||||
|
||||
abbrev intro1 (mvarId : MVarId) : MetaM (FVarId × MVarId) := do
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue