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

chore: move to new frontend

Browse source
This commit is contained in:
Leonardo de Moura 2020-10-17 07:24:10 -07:00
parent c75d0350ec
commit ced9d88cc6
1 changed files with 45 additions and 48 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

93
src/Lean/Meta/Tactic/Assert.lean
View file

@ -1,3 +1,4 @@
#lang lean4
/-
Copyright (c) 2020 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
@ -8,20 +9,19 @@ import Lean.Meta.Tactic.FVarSubst
import Lean.Meta.Tactic.Intro
import Lean.Meta.Tactic.Revert
namespace Lean
namespace Meta
namespace Lean.Meta
/--
Convert the given goal `Ctx |- target` into `Ctx |- type -> target`.
It assumes `val` has type `type` -/
def assert (mvarId : MVarId) (name : Name) (type : Expr) (val : Expr) : MetaM MVarId := do
withMVarContext mvarId $ do
checkNotAssigned mvarId `assert;
tag ← getMVarTag mvarId;
target ← getMVarType mvarId;
let newType := Lean.mkForall name BinderInfo.default type target;
newMVar ← mkFreshExprSyntheticOpaqueMVar newType tag;
assignExprMVar mvarId (mkApp newMVar val);
def assert (mvarId : MVarId) (name : Name) (type : Expr) (val : Expr) : MetaM MVarId :=
withMVarContext mvarId do
checkNotAssigned mvarId `assert
let tag ← getMVarTag mvarId
let target ← getMVarType mvarId
let newType := Lean.mkForall name BinderInfo.default type target
let newMVar ← mkFreshExprSyntheticOpaqueMVar newType tag
assignExprMVar mvarId (mkApp newMVar val)
pure newMVar.mvarId!
/--
@ -29,12 +29,12 @@ withMVarContext mvarId $ do
It assumes `val` has type `type` -/
def define (mvarId : MVarId) (name : Name) (type : Expr) (val : Expr) : MetaM MVarId := do
withMVarContext mvarId $ do
checkNotAssigned mvarId `define;
tag ← getMVarTag mvarId;
target ← getMVarType mvarId;
let newType := Lean.mkLet name type val target;
newMVar ← mkFreshExprSyntheticOpaqueMVar newType tag;
assignExprMVar mvarId newMVar;
checkNotAssigned mvarId `define
let tag ← getMVarTag mvarId
let target ← getMVarType mvarId
let newType := Lean.mkLet name type val target
let newMVar ← mkFreshExprSyntheticOpaqueMVar newType tag
assignExprMVar mvarId newMVar
pure newMVar.mvarId!
/--
@ -42,15 +42,15 @@ withMVarContext mvarId $ do
It assumes `val` has type `type` -/
def assertExt (mvarId : MVarId) (name : Name) (type : Expr) (val : Expr) (hName : Name := `h) : MetaM MVarId := do
withMVarContext mvarId $ do
checkNotAssigned mvarId `assert;
tag ← getMVarTag mvarId;
target ← getMVarType mvarId;
u ← getLevel type;
let hType := mkApp3 (mkConst `Eq [u]) type (mkBVar 0) val;
let newType := Lean.mkForall name BinderInfo.default type $ Lean.mkForall hName BinderInfo.default hType target;
newMVar ← mkFreshExprSyntheticOpaqueMVar newType tag;
rflPrf ← mkEqRefl val;
assignExprMVar mvarId (mkApp2 newMVar val rflPrf);
checkNotAssigned mvarId `assert
let tag ← getMVarTag mvarId
let target ← getMVarType mvarId
let u ← getLevel type
let hType := mkApp3 (mkConst `Eq [u]) type (mkBVar 0) val
let newType := Lean.mkForall name BinderInfo.default type $ Lean.mkForall hName BinderInfo.default hType target
let newMVar ← mkFreshExprSyntheticOpaqueMVar newType tag
let rflPrf ← mkEqRefl val
assignExprMVar mvarId (mkApp2 newMVar val rflPrf)
pure newMVar.mvarId!
structure AssertAfterResult :=
@ -64,28 +64,25 @@ structure AssertAfterResult :=
Note that `val` does not need to be well-formed after `fvarId`. That is, it may contain variables that are defined after `fvarId`. -/
def assertAfter (mvarId : MVarId) (fvarId : FVarId) (userName : Name) (type : Expr) (val : Expr) : MetaM AssertAfterResult := do
withMVarContext mvarId $ do
checkNotAssigned mvarId `assertAfter;
tag ← getMVarTag mvarId;
target ← getMVarType mvarId;
localDecl ← getLocalDecl fvarId;
lctx ← getLCtx;
localInsts ← getLocalInstances;
let fvarIds := lctx.foldlFrom (fun (fvarIds : Array FVarId) decl => fvarIds.push decl.fvarId) #[] (localDecl.index+1);
let xs := fvarIds.map mkFVar;
targetNew ← mkForallFVars xs target;
let targetNew := Lean.mkForall userName BinderInfo.default type targetNew;
let lctxNew := fvarIds.foldl (fun (lctxNew : LocalContext) fvarId => lctxNew.erase fvarId) lctx;
let localInstsNew := localInsts.filter fun inst => fvarIds.contains inst.fvar.fvarId!;
mvarNew ← mkFreshExprMVarAt lctxNew localInstsNew targetNew MetavarKind.syntheticOpaque tag;
let args := (fvarIds.filter fun fvarId => !(lctx.get! fvarId).isLet).map mkFVar;
let args := #[val] ++ args;
assignExprMVar mvarId (mkAppN mvarNew args);
(fvarIdNew, mvarIdNew) ← intro1P mvarNew.mvarId!;
(fvarIdsNew, mvarIdNew) ← introNP mvarIdNew fvarIds.size;
let subst := fvarIds.size.fold
(fun i (subst : FVarSubst) => subst.insert (fvarIds.get! i) (mkFVar (fvarIdsNew.get! i)))
{};
checkNotAssigned mvarId `assertAfter
let tag ← getMVarTag mvarId
let target ← getMVarType mvarId
let localDecl ← getLocalDecl fvarId
let lctx ← getLCtx
let localInsts ← getLocalInstances
let fvarIds := lctx.foldlFrom (fun (fvarIds : Array FVarId) decl => fvarIds.push decl.fvarId) #[] (localDecl.index+1)
let xs := fvarIds.map mkFVar
let targetNew ← mkForallFVars xs target
let targetNew := Lean.mkForall userName BinderInfo.default type targetNew
let lctxNew := fvarIds.foldl (fun (lctxNew : LocalContext) fvarId => lctxNew.erase fvarId) lctx
let localInstsNew := localInsts.filter fun inst => fvarIds.contains inst.fvar.fvarId!
let mvarNew ← mkFreshExprMVarAt lctxNew localInstsNew targetNew MetavarKind.syntheticOpaque tag
let args := (fvarIds.filter fun fvarId => !(lctx.get! fvarId).isLet).map mkFVar
let args := #[val] ++ args
assignExprMVar mvarId (mkAppN mvarNew args)
let (fvarIdNew, mvarIdNew) ← intro1P mvarNew.mvarId!
let (fvarIdsNew, mvarIdNew) ← introNP mvarIdNew fvarIds.size
let subst := fvarIds.size.fold (init := {}) fun i subst => subst.insert fvarIds[i] (mkFVar fvarIdsNew[i])
pure { fvarId := fvarIdNew, mvarId := mvarIdNew, subst := subst }
end Meta
end Lean
end Lean.Meta