chore: remove old tests
This commit is contained in:
Leonardo de Moura
parent
2446c64a99
commit
c434e4e096
6 changed files with 0 additions and 334 deletions
|
|
@ -1,104 +0,0 @@
|
|||
import Lean.MetavarContext
|
||||
|
||||
open Lean
|
||||
|
||||
def check (b : Bool) : IO Unit :=
|
||||
unless b do throw $ IO.userError "error"
|
||||
|
||||
def f := mkConst `f []
|
||||
def g := mkConst `g []
|
||||
def a := mkConst `a []
|
||||
def b := mkConst `b []
|
||||
def c := mkConst `c []
|
||||
|
||||
def b0 := mkBVar 0
|
||||
def b1 := mkBVar 1
|
||||
def b2 := mkBVar 2
|
||||
|
||||
def u := mkLevelParam `u
|
||||
|
||||
def typeE := mkSort levelOne
|
||||
def natE := mkConst `Nat []
|
||||
def boolE := mkConst `Bool []
|
||||
def vecE := mkConst `Vec [levelZero]
|
||||
|
||||
instance : Coe Name FVarId where
|
||||
coe n := { name := n }
|
||||
|
||||
instance : Coe Name MVarId where
|
||||
coe n := { name := n }
|
||||
|
||||
def α := mkFVar `α
|
||||
def x := mkFVar `x
|
||||
def y := mkFVar `y
|
||||
def z := mkFVar `z
|
||||
def w := mkFVar `w
|
||||
|
||||
def m1 := mkMVar `m1
|
||||
def m2 := mkMVar `m2
|
||||
def m3 := mkMVar `m3
|
||||
def m4 := mkMVar `m4
|
||||
def m5 := mkMVar `m5
|
||||
def m6 := mkMVar `m6
|
||||
|
||||
def bi := BinderInfo.default
|
||||
def arrow (d b : Expr) := mkForall `_ bi d b
|
||||
def lctx1 : LocalContext := {}
|
||||
def lctx2 := lctx1.mkLocalDecl `α `α typeE
|
||||
def lctx3 := lctx2.mkLocalDecl `x `x natE
|
||||
def lctx4 := lctx3.mkLocalDecl `y `y α
|
||||
def lctx5 := lctx4.mkLocalDecl `z `z (mkAppN vecE #[x])
|
||||
def lctx6 := lctx5.mkLocalDecl `w `w (arrow natE (mkAppN m6 #[α, x, y]))
|
||||
|
||||
def t1 := lctx5.mkLambda #[α, x, y] $ mkAppN f #[α, mkAppN g #[x, y], lctx5.mkLambda #[z] (mkApp f z)]
|
||||
#eval check (!t1.hasFVar)
|
||||
#eval toString t1
|
||||
|
||||
def mctx1 : MetavarContext := {}
|
||||
def mctx2 := mctx1.addExprMVarDecl `m1 `m1 lctx3 #[] natE
|
||||
def mctx3 := mctx2.addExprMVarDecl `m2 `m2 lctx4 #[] α
|
||||
def mctx4 := mctx3.addExprMVarDecl `m3 `m3 lctx4 #[] natE
|
||||
def mctx5 := mctx4.addExprMVarDecl `m4 `m4 lctx1 #[] (arrow typeE (arrow natE (arrow α natE)))
|
||||
def mctx6 := mctx5.addExprMVarDecl `m5 `m5 lctx5 #[] typeE
|
||||
def mctx7 := mctx5.addExprMVarDecl `m6 `m6 lctx5 #[] (arrow typeE (arrow natE (arrow α natE)))
|
||||
def mctx8 := mctx7.assignDelayed `m4 #[α, x, y] m3
|
||||
def mctx9 := mctx8.assignExpr `m3 (mkAppN g #[x, y])
|
||||
def mctx10 := mctx9.assignExpr `m1 a
|
||||
|
||||
def t2 := lctx5.mkLambda #[α, x, y] $ mkAppN f #[mkAppN m4 #[α, x, y], x]
|
||||
|
||||
#eval t2
|
||||
|
||||
#eval check (!t2.hasFVar)
|
||||
#eval toString t2
|
||||
#eval toString (mctx6.instantiateMVars t2).1
|
||||
#eval check (!(mctx9.instantiateMVars t2).1.hasMVar)
|
||||
#eval check (!(mctx9.instantiateMVars t2).1.hasFVar)
|
||||
#eval toString (mctx9.instantiateMVars t2).1
|
||||
|
||||
-- t3 is ill-formed since m3's localcontext contains ‵α`, `x` and `y`
|
||||
def t3 := lctx5.mkLambda #[α, x, y] $ mkAppN f #[m3, x]
|
||||
#eval check (mctx10.instantiateMVars t3).1.hasFVar
|
||||
#eval toString (mctx7.instantiateMVars t3).1
|
||||
|
||||
partial def mkDiamond : Nat → Expr
|
||||
| 0 => m1
|
||||
| (n+1) => mkAppN f #[mkDiamond n, mkDiamond n]
|
||||
|
||||
#eval toString (mctx7.instantiateMVars (mkDiamond 3)).1
|
||||
#eval toString (mctx10.instantiateMVars (mkDiamond 3)).1
|
||||
#eval toString (mctx7.instantiateMVars (mkDiamond 100)).1.getAppFn
|
||||
#eval toString (mctx10.instantiateMVars (mkDiamond 100)).1.getAppFn
|
||||
|
||||
def mctx11 := mctx10.assignDelayed `m6 #[α, x, y] m5
|
||||
def mctx12 := mctx11.assignExpr `m5 (arrow α α)
|
||||
|
||||
def t4 := lctx6.mkLambda #[α, x, y, w] $ mkAppN f #[mkAppN m4 #[α, x, y], x]
|
||||
|
||||
#eval toString t4
|
||||
#eval toString (mctx9.instantiateMVars t4).1
|
||||
#eval toString (mctx12.instantiateMVars t4).1
|
||||
#eval check (mctx9.instantiateMVars t4).1.hasMVar
|
||||
#eval check (!((mctx9.instantiateMVars t4).1.hasFVar))
|
||||
#eval check (!(mctx12.instantiateMVars t4).1.hasMVar)
|
||||
#eval check (!((mctx12.instantiateMVars t4).1.hasFVar))
|
||||
|
|
@ -1,51 +0,0 @@
|
|||
|
||||
"fun (α : Type) (x : Nat) (y : α) => f α (g x y) (fun (z : Vec.{0} x) => f z)"
|
||||
Lean.Expr.lam
|
||||
`α
|
||||
(Lean.Expr.sort
|
||||
(Lean.Level.succ (Lean.Level.zero (Level.mkData 2221)) (Level.mkData 1676277521 (depth := 1)))
|
||||
(Expr.mkData 1469443585 (bi := Lean.BinderInfo.default)))
|
||||
(Lean.Expr.lam
|
||||
`x
|
||||
(Lean.Expr.const `Nat [] (Expr.mkData 607656011 (bi := Lean.BinderInfo.default)))
|
||||
(Lean.Expr.lam
|
||||
`y
|
||||
(Lean.Expr.bvar 1 (Expr.mkData 4280418285 (looseBVarRange := 2) (bi := Lean.BinderInfo.default)))
|
||||
(Lean.Expr.app
|
||||
(Lean.Expr.app
|
||||
(Lean.Expr.const `f [] (Expr.mkData 3992371127 (bi := Lean.BinderInfo.default)))
|
||||
(Lean.Expr.app
|
||||
(Lean.Expr.app
|
||||
(Lean.Expr.app
|
||||
(Lean.Expr.mvar `m4 (Expr.mkData 3167598817 (hasExprMVar := true) (bi := Lean.BinderInfo.default)))
|
||||
(Lean.Expr.bvar 2 (Expr.mkData 4281466863 (looseBVarRange := 3) (bi := Lean.BinderInfo.default)))
|
||||
(Expr.mkData 621598011 (looseBVarRange := 3) (approxDepth := 1) (hasExprMVar := true) (bi := Lean.BinderInfo.default)))
|
||||
(Lean.Expr.bvar 1 (Expr.mkData 4280418285 (looseBVarRange := 2) (bi := Lean.BinderInfo.default)))
|
||||
(Expr.mkData 1373601833 (looseBVarRange := 3) (approxDepth := 2) (hasExprMVar := true) (bi := Lean.BinderInfo.default)))
|
||||
(Lean.Expr.bvar 0 (Expr.mkData 4279369707 (looseBVarRange := 1) (bi := Lean.BinderInfo.default)))
|
||||
(Expr.mkData 237469531 (looseBVarRange := 3) (approxDepth := 3) (hasExprMVar := true) (bi := Lean.BinderInfo.default)))
|
||||
(Expr.mkData 1344847761 (looseBVarRange := 3) (approxDepth := 4) (hasExprMVar := true) (bi := Lean.BinderInfo.default)))
|
||||
(Lean.Expr.bvar 1 (Expr.mkData 4280418285 (looseBVarRange := 2) (bi := Lean.BinderInfo.default)))
|
||||
(Expr.mkData 569884967 (looseBVarRange := 3) (approxDepth := 5) (hasExprMVar := true) (bi := Lean.BinderInfo.default)))
|
||||
(Expr.mkData 2023949564 (looseBVarRange := 2) (approxDepth := 6) (hasExprMVar := true) (bi := Lean.BinderInfo.default)))
|
||||
(Expr.mkData 1948877337 (looseBVarRange := 1) (approxDepth := 7) (hasExprMVar := true) (bi := Lean.BinderInfo.default)))
|
||||
(Expr.mkData 2017358918 (approxDepth := 8) (hasExprMVar := true) (bi := Lean.BinderInfo.default))
|
||||
|
||||
"fun (α : Type) (x : Nat) (y : α) => f (?m4 α x y) x"
|
||||
"fun (α : Type) (x : Nat) (y : α) => f (?m4 α x y) x"
|
||||
|
||||
|
||||
"fun (α : Type) (x : Nat) (y : α) => f (g x y) x"
|
||||
|
||||
"fun (α : Type) (x : Nat) (y : α) => f ?m3 x"
|
||||
"f (f (f ?m1 ?m1) (f ?m1 ?m1)) (f (f ?m1 ?m1) (f ?m1 ?m1))"
|
||||
"f (f (f a a) (f a a)) (f (f a a) (f a a))"
|
||||
"f"
|
||||
"f"
|
||||
"fun (α : Type) (x : Nat) (y : α) (w : Nat -> (?m6 α x y)) => f (?m4 α x y) x"
|
||||
"fun (α : Type) (x : Nat) (y : α) (w : Nat -> (?m6 α x y)) => f (g x y) x"
|
||||
"fun (α : Type) (x : Nat) (y : α) (w : Nat -> α -> α) => f (g x y) x"
|
||||
|
||||
|
||||
|
||||
|
||||
|
|
@ -1,62 +0,0 @@
|
|||
import Lean.MetavarContext
|
||||
|
||||
open Lean
|
||||
|
||||
def check (b : Bool) : IO Unit :=
|
||||
unless b do throw $ IO.userError "error"
|
||||
|
||||
def f := mkConst `f []
|
||||
def g := mkConst `g []
|
||||
def a := mkConst `a []
|
||||
def b := mkConst `b []
|
||||
def c := mkConst `c []
|
||||
|
||||
def b0 := mkBVar 0
|
||||
def b1 := mkBVar 1
|
||||
def b2 := mkBVar 2
|
||||
|
||||
def u := mkLevelParam `u
|
||||
|
||||
def typeE := mkSort levelOne
|
||||
def natE := mkConst `Nat []
|
||||
def boolE := mkConst `Bool []
|
||||
def vecE := mkConst `Vec [levelZero]
|
||||
|
||||
instance : Coe Name FVarId where
|
||||
coe n := { name := n }
|
||||
|
||||
instance : Coe Name MVarId where
|
||||
coe n := { name := n }
|
||||
|
||||
def α := mkFVar `α
|
||||
def x := mkFVar `x
|
||||
def y := mkFVar `y
|
||||
def z := mkFVar `z
|
||||
def w := mkFVar `w
|
||||
|
||||
def m1 := mkMVar `m1
|
||||
def m2 := mkMVar `m2
|
||||
def m3 := mkMVar `m3
|
||||
|
||||
def bi := BinderInfo.default
|
||||
def arrow (d b : Expr) := mkForall `_ bi d b
|
||||
|
||||
def lctx1 : LocalContext := {}
|
||||
def lctx2 := lctx1.mkLocalDecl `α `α typeE
|
||||
def lctx3 := lctx2.mkLocalDecl `x `x m1
|
||||
def lctx4 := lctx3.mkLocalDecl `y `y (arrow natE (mkAppN m3 #[α, x]))
|
||||
|
||||
def mctx1 : MetavarContext := {}
|
||||
def mctx2 := mctx1.addExprMVarDecl `m1 `m1 lctx1 #[] typeE
|
||||
def mctx3 := mctx2.addExprMVarDecl `m2 `m2 lctx3 #[] natE
|
||||
def mctx4 := mctx3.addExprMVarDecl `m3 `m3 lctx1 #[] (arrow typeE (arrow natE natE))
|
||||
def mctx5 := mctx4.assignDelayed `m3 #[α, x] m2
|
||||
def mctx6 := mctx5.assignExpr `m2 (arrow α α)
|
||||
def mctx7 := mctx6.assignExpr `m1 natE
|
||||
|
||||
def t2 := lctx4.mkLambda #[α, x, y] $ mkAppN f #[mkAppN m3 #[α, x], x]
|
||||
|
||||
#eval check (!t2.hasFVar)
|
||||
#eval toString t2
|
||||
#eval toString (mctx6.instantiateMVars t2).1
|
||||
#eval toString (mctx7.instantiateMVars t2).1
|
||||
|
|
@ -1,4 +0,0 @@
|
|||
|
||||
"fun (α : Type) (x : ?m1) (y : Nat -> (?m3 α x)) => f (?m3 α x) x"
|
||||
"fun (α : Type) (x : ?m1) (y : Nat -> α -> α) => f (α -> α) x"
|
||||
"fun (α : Type) (x : Nat) (y : Nat -> α -> α) => f (α -> α) x"
|
||||
|
|
@ -1,103 +0,0 @@
|
|||
import Lean.MetavarContext
|
||||
|
||||
open Lean
|
||||
|
||||
def mkLambdaTest (mctx : MetavarContext) (ngen : NameGenerator) (lctx : LocalContext) (xs : Array Expr) (e : Expr)
|
||||
: Except MetavarContext.MkBinding.Exception (MetavarContext × NameGenerator × Expr) :=
|
||||
match MetavarContext.mkLambda xs e false true BinderInfo.default { lctx, mainModule := `main } { mctx := mctx, ngen := ngen, nextMacroScope := firstFrontendMacroScope + 1 } with
|
||||
| EStateM.Result.ok e s => Except.ok (s.mctx, s.ngen, e)
|
||||
| EStateM.Result.error e s => Except.error e
|
||||
|
||||
def check (b : Bool) : IO Unit :=
|
||||
unless b do throw $ IO.userError "error"
|
||||
|
||||
def f := mkConst `f
|
||||
def g := mkConst `g
|
||||
def a := mkConst `a
|
||||
def b := mkConst `b
|
||||
def c := mkConst `c
|
||||
|
||||
def b0 := mkBVar 0
|
||||
def b1 := mkBVar 1
|
||||
def b2 := mkBVar 2
|
||||
|
||||
def u := mkLevelParam `u
|
||||
|
||||
def typeE := mkSort levelOne
|
||||
def natE := mkConst `Nat
|
||||
def boolE := mkConst `Bool
|
||||
def vecE := mkConst `Vec [levelZero]
|
||||
|
||||
instance : Coe Name FVarId where
|
||||
coe n := { name := n }
|
||||
|
||||
instance : Coe Name MVarId where
|
||||
coe n := { name := n }
|
||||
|
||||
def α := mkFVar `α
|
||||
def x := mkFVar `x
|
||||
def y := mkFVar `y
|
||||
def z := mkFVar `z
|
||||
def w := mkFVar `w
|
||||
|
||||
def m1 := mkMVar `m1
|
||||
def m2 := mkMVar `m2
|
||||
def m3 := mkMVar `m3
|
||||
|
||||
def bi := BinderInfo.default
|
||||
def arrow (d b : Expr) := mkForall `_ bi d b
|
||||
|
||||
def lctx1 : LocalContext := {}
|
||||
def lctx2 := lctx1.mkLocalDecl `α `α typeE
|
||||
def lctx3 := lctx2.mkLocalDecl `x `x m1
|
||||
def lctx4 := lctx3.mkLocalDecl `y `y (arrow natE m2)
|
||||
|
||||
def mctx1 : MetavarContext := {}
|
||||
def mctx2 := mctx1.addExprMVarDecl `m1 `m1 lctx2 #[] typeE
|
||||
def mctx3 := mctx2.addExprMVarDecl `m2 `m2 lctx3 #[] natE
|
||||
def mctx4 := mctx3.addExprMVarDecl `m3 `m3 lctx3 #[] natE
|
||||
def mctx4' := mctx3.addExprMVarDecl `m3 `m3 lctx3 #[] natE MetavarKind.syntheticOpaque
|
||||
|
||||
def R1 :=
|
||||
match mkLambdaTest mctx4 {namePrefix := `n} lctx4 #[α, x, y] $ mkAppN f #[m3, x] with
|
||||
| Except.ok s => s
|
||||
| Except.error e => panic! (toString e)
|
||||
def e1 := R1.2.2
|
||||
def mctx5 := R1.1
|
||||
|
||||
def sortNames (xs : List Name) : List Name :=
|
||||
(xs.toArray.qsort Name.lt).toList
|
||||
|
||||
instance : ToString MVarId where
|
||||
toString m := toString m.name
|
||||
|
||||
def sortNamePairs {α} [Inhabited α] (xs : List (MVarId × α)) : List (MVarId × α) :=
|
||||
(xs.toArray.qsort (fun a b => Name.lt a.1.name b.1.name)).toList
|
||||
|
||||
#eval toString $ sortNames $ mctx5.decls.toList.map (·.1.name)
|
||||
#eval toString $ sortNamePairs $ mctx5.eAssignment.toList
|
||||
#eval toString e1
|
||||
#eval check (!e1.hasFVar)
|
||||
|
||||
def R2 :=
|
||||
match mkLambdaTest mctx4' {namePrefix := `n} lctx4 #[α, x, y] $ mkAppN f #[m3, y] with
|
||||
| Except.ok s => s
|
||||
| Except.error e => panic! (toString e)
|
||||
def e2 := R2.2.2
|
||||
def mctx6 := R2.1
|
||||
|
||||
#eval toString $ sortNames $ mctx6.decls.toList.map (·.1.name)
|
||||
#eval toString $ sortNamePairs $ mctx6.eAssignment.toList
|
||||
-- ?n.2 was delayed assigned because ?m.3 is synthetic
|
||||
#eval toString $ sortNames $ mctx6.dAssignment.toList.map (·.1.name)
|
||||
#eval toString e2
|
||||
|
||||
#print "assigning ?m1 and ?n.1"
|
||||
def R3 :=
|
||||
let mctx := mctx6.assignExpr `m3 x;
|
||||
let mctx := mctx.assignExpr (Name.mkNum `n 1) (mkLambda `_ bi typeE natE);
|
||||
-- ?n.2 is instantiated because we have the delayed assignment `?n.2 α x := ?m1`
|
||||
(mctx.instantiateMVars e2)
|
||||
def e3 := R3.1
|
||||
def mctx7 := R3.2
|
||||
#eval toString e3
|
||||
|
|
@ -1,10 +0,0 @@
|
|||
"[n.1, n.2, n.3, m1, m2, m3]"
|
||||
"[(m1, ?n α), (m2, ?n α x), (m3, ?n α x)]"
|
||||
"fun (α : Type) (x : ?n α) (y : Nat -> (?n α x)) => f (?n α x) x"
|
||||
|
||||
"[n.1, n.2, n.3, m1, m2, m3]"
|
||||
"[(m1, ?n α), (m2, ?n α x)]"
|
||||
"[n.2]"
|
||||
"fun (α : Type) (x : ?n α) (y : Nat -> (?n α x)) => f (?n α x) y"
|
||||
assigning ?m1 and ?n
|
||||
"fun (α : Type) (x : Nat) (y : Nat -> (?n α x)) => f x y"
|
||||
Loading…
Add table
Reference in a new issue