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

chore: avoid Expr constructors in tests

Browse source
This commit is contained in:
Leonardo de Moura 2019-11-14 16:54:36 -08:00
parent c341486e28
commit 524872d68a
13 changed files with 121 additions and 122 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
tests/compiler/expr.lean
View file

@ -3,7 +3,7 @@ open Lean
def main : IO UInt32 :=
do
let e := Expr.app (Expr.app (Expr.const `f []) (Expr.const `a [])) (Expr.const `b []);
let e := mkAppN (mkConst `f) #[mkConst `a, mkConst `b];
IO.println e;
IO.println ("hash: " ++ toString e.hash);
IO.println e.getAppArgs;

26
tests/lean/abst.lean
View file

@ -4,21 +4,21 @@ open Lean
def tst : IO Unit :=
do
let f := mkConst `f;
let x := Expr.fvar `x;
let y := Expr.fvar `y;
let t := Expr.app (Expr.app (Expr.app f x) y) (Expr.app f x);
IO.println t.dbgToString;
let x := mkFVar `x;
let y := mkFVar `y;
let t := mkApp (mkApp (mkApp f x) y) (mkApp f x);
IO.println t;
let p := t.abstract [x, y].toArray;
IO.println p.dbgToString;
IO.println (p.instantiateRev [x, y].toArray).dbgToString;
IO.println p;
IO.println $ p.instantiateRev #[x, y];
let a := mkConst `a;
let b := Expr.app f (mkConst `b);
IO.println (p.instantiateRev [a, b].toArray).dbgToString;
IO.println (p.instantiate [a].toArray).dbgToString;
let p := t.abstractRange 1 [x, y].toArray;
IO.println p.dbgToString;
let p := t.abstractRange 3 [x, y].toArray;
IO.println p.dbgToString;
let b := mkApp f (mkConst `b);
IO.println $ p.instantiateRev #[a, b];
IO.println $ p.instantiate #[a];
let p := t.abstractRange 1 #[x, y];
IO.println p;
let p := t.abstractRange 3 #[x, y];
IO.println p;
pure ()
#eval tst

8
tests/lean/inst.lean
View file

@ -4,11 +4,11 @@ open Lean
def tst : IO Unit :=
do
let f := mkConst `f;
let x := Expr.bvar 0;
let y := Expr.bvar 1;
let t := Expr.app (Expr.app (Expr.app f x) y) x;
let x := mkBVar 0;
let y := mkBVar 1;
let t := mkApp (mkApp (mkApp f x) y) x;
let a := mkConst `a;
let b := Expr.app f (mkConst `b);
let b := mkApp f (mkConst `b);
let c := mkConst `c;
IO.println t;
IO.println (t.instantiate #[a, b]);

5
tests/lean/mvar1.lean
View file

@ -35,8 +35,7 @@ def m5 := mkMVar `m5
def m6 := mkMVar `m6
def bi := BinderInfo.default
def arrow (d b : Expr) := Expr.forallE `_ bi d b
def arrow (d b : Expr) := mkForall `_ bi d b
def lctx1 : LocalContext := {}
def lctx2 := lctx1.mkLocalDecl `α `α typeE
def lctx3 := lctx2.mkLocalDecl `x `x natE
@ -44,7 +43,7 @@ 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] (Expr.app f z)]
def t1 := lctx5.mkLambda #[α, x, y] $ mkAppN f #[α, mkAppN g #[x, y], lctx5.mkLambda #[z] (mkApp f z)]
#eval check (!t1.hasFVar)
#eval t1

4
tests/lean/mvar2.lean
View file

@ -16,7 +16,7 @@ def b2 := mkBVar 2
def u := Level.param `u
def typeE := Expr.sort Level.one
def typeE := mkSort Level.one
def natE := mkConst `Nat []
def boolE := mkConst `Bool []
def vecE := mkConst `Vec [Level.zero]
@ -32,7 +32,7 @@ def m2 := mkMVar `m2
def m3 := mkMVar `m3
def bi := BinderInfo.default
def arrow (d b : Expr) := Expr.forallE `_ bi d b
def arrow (d b : Expr) := mkForall `_ bi d b
def lctx1 : LocalContext := {}
def lctx2 := lctx1.mkLocalDecl `α `α typeE

18
tests/lean/mvar3.lean
View file

@ -1,7 +1,7 @@
import Init.Lean.MetavarContext
open Lean
def mkLambda (mctx : MetavarContext) (ngen : NameGenerator) (lctx : LocalContext) (xs : Array Expr) (e : Expr)
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 lctx { mctx := mctx, ngen := ngen } with
| EStateM.Result.ok e s => Except.ok (s.mctx, s.ngen, e)
@ -22,7 +22,7 @@ def b2 := mkBVar 2
def u := Level.param `u
def typeE := Expr.sort Level.one
def typeE := mkSort Level.one
def natE := mkConst `Nat
def boolE := mkConst `Bool
def vecE := mkConst `Vec [Level.zero]
@ -33,12 +33,12 @@ def y := mkFVar `y
def z := mkFVar `z
def w := mkFVar `w
def m1 := Expr.mvar `m1
def m2 := Expr.mvar `m2
def m3 := Expr.mvar `m3
def m1 := mkMVar `m1
def m2 := mkMVar `m2
def m3 := mkMVar `m3
def bi := BinderInfo.default
def arrow (d b : Expr) := Expr.forallE `_ bi d b
def arrow (d b : Expr) := mkForall `_ bi d b
def lctx1 : LocalContext := {}
def lctx2 := lctx1.mkLocalDecl `α `α typeE
@ -52,7 +52,7 @@ def mctx4 := mctx3.addExprMVarDecl `m3 `m3 lctx3 natE
def mctx4' := mctx3.addExprMVarDecl `m3 `m3 lctx3 natE true
def R1 :=
match mkLambda mctx4 {namePrefix := `n} lctx4 #[α, x, y] $ mkAppN f #[m3, x] with
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
@ -64,7 +64,7 @@ def mctx5 := R1.1
#eval check (!e1.hasFVar)
def R2 :=
match mkLambda mctx4' {namePrefix := `n} lctx4 #[α, x, y] $ mkAppN f #[m3, y] with
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
@ -79,7 +79,7 @@ def mctx6 := R2.1
#print "assigning ?m1 and ?n.1"
def R3 :=
let mctx := mctx6.assignExpr `m3 x;
let mctx := mctx.assignExpr (Name.mkNumeral `n 1) (Expr.lam `_ bi typeE natE);
let mctx := mctx.assignExpr (Name.mkNumeral `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

12
tests/lean/mvar_fvar.lean
View file

@ -1,10 +1,10 @@
import Init.Lean
open Lean
#eval (Expr.fvar `a).hasFVar
#eval (Expr.app (Expr.const `foo []) (Expr.fvar `a)).hasFVar
#eval (Expr.app (Expr.const `foo []) (Expr.const `a [])).hasFVar
#eval (mkFVar `a).hasFVar
#eval (mkApp (mkConst `foo) (mkFVar `a)).hasFVar
#eval (mkApp (mkConst `foo) (mkConst `a)).hasFVar
#eval (Expr.mvar `a).hasMVar
#eval (Expr.app (Expr.const `foo []) (Expr.mvar `a)).hasMVar
#eval (Expr.app (Expr.const `foo []) (Expr.const `a [])).hasMVar
#eval (mkMVar `a).hasMVar
#eval (mkApp (mkConst `foo) (mkMVar `a)).hasMVar
#eval (mkApp (mkConst `foo) (mkConst `a)).hasMVar

28
tests/lean/run/expr1.lean
View file

@ -47,8 +47,8 @@ do let f := mkConst `f [];
let x1 := mkBVar 1;
let t1 := mkAppN f #[a, b];
let t2 := mkAppN f #[a, x0];
let t3 := Expr.lam `x BinderInfo.default (Expr.sort Level.zero) (mkAppN f #[a, x0]);
let t4 := Expr.lam `x BinderInfo.default (Expr.sort Level.zero) (mkAppN f #[a, x1]);
let t3 := mkLambda `x BinderInfo.default (mkSort Level.zero) (mkAppN f #[a, x0]);
let t4 := mkLambda `x BinderInfo.default (mkSort Level.zero) (mkAppN f #[a, x1]);
unless (!t1.hasLooseBVar 0) $ throw "failed-1";
unless (t2.hasLooseBVar 0) $ throw "failed-2";
unless (!t3.hasLooseBVar 0) $ throw "failed-3";
@ -66,29 +66,29 @@ do let f := mkConst `f [];
let x0 := mkBVar 0;
let x1 := mkBVar 1;
let x2 := mkBVar 2;
let t := Expr.lam `x BinderInfo.default nat (Expr.app f x0);
let t := mkLambda `x BinderInfo.default nat (mkApp f x0);
IO.println t.etaExpanded?;
unless (t.etaExpanded? == some f) $ throw "failed-1";
let t := Expr.lam `x BinderInfo.default nat (Expr.app f x1);
let t := mkLambda `x BinderInfo.default nat (mkApp f x1);
unless (t.etaExpanded? == none) $ throw "failed-2";
let t := Expr.lam `x BinderInfo.default nat (mkAppN f #[a, x0]);
unless (t.etaExpanded? == some (Expr.app f a)) $ throw "failed-3";
let t := Expr.lam `x BinderInfo.default nat (mkAppN f #[x0, x0]);
let t := mkLambda `x BinderInfo.default nat (mkAppN f #[a, x0]);
unless (t.etaExpanded? == some (mkApp f a)) $ throw "failed-3";
let t := mkLambda `x BinderInfo.default nat (mkAppN f #[x0, x0]);
unless (t.etaExpanded? == none) $ throw "failed-4";
let t := Expr.lam `x BinderInfo.default nat (Expr.lam `y BinderInfo.default nat (Expr.app f x0));
let t := mkLambda `x BinderInfo.default nat (mkLambda `y BinderInfo.default nat (mkApp f x0));
unless (t.etaExpanded? == none) $ throw "failed-5";
let t := Expr.lam `x BinderInfo.default nat (Expr.lam `y BinderInfo.default nat (mkAppN f #[x1, x0]));
let t := mkLambda `x BinderInfo.default nat (mkLambda `y BinderInfo.default nat (mkAppN f #[x1, x0]));
IO.println t;
unless (t.etaExpanded? == some f) $ throw "failed-6";
let t := Expr.lam `x BinderInfo.default nat (Expr.lam `y BinderInfo.default nat (Expr.lam `z BinderInfo.default nat (mkAppN f #[x2, x1, x0])));
let t := mkLambda `x BinderInfo.default nat (mkLambda `y BinderInfo.default nat (mkLambda `z BinderInfo.default nat (mkAppN f #[x2, x1, x0])));
IO.println t;
unless (t.etaExpanded? == some f) $ throw "failed-7";
let t := Expr.lam `x BinderInfo.default nat (Expr.lam `y BinderInfo.default nat (Expr.lam `z BinderInfo.default nat (mkAppN f #[a, x2, x1, x0])));
let t := mkLambda `x BinderInfo.default nat (mkLambda `y BinderInfo.default nat (mkLambda `z BinderInfo.default nat (mkAppN f #[a, x2, x1, x0])));
IO.println t;
unless (t.etaExpanded? == some (Expr.app f a)) $ throw "failed-8";
unless (t.etaExpanded? == some (mkApp f a)) $ throw "failed-8";
IO.println t.etaExpanded?;
let t := Expr.app f a;
unless (t.etaExpanded? == some (Expr.app f a)) $ throw "failed-9";
let t := mkApp f a;
unless (t.etaExpanded? == some (mkApp f a)) $ throw "failed-9";
pure ()
#eval tst5

24
tests/lean/run/expr_maps.lean
View file

@ -1,21 +1,21 @@
import Init.Lean.Expr
open Lean
def exprType : Expr := Expr.sort Level.one
def exprType : Expr := mkSort Level.one
def biDef := BinderInfo.default
def exprNat := Expr.const `Nat []
def exprNat := mkConst `Nat []
-- Type -> Type
def TypeArrowType := Expr.forallE `α biDef exprType exprType
def TypeArrowType := mkForall `α biDef exprType exprType
-- Type -> Type
def TypeArrowType2 := Expr.forallE `β biDef exprType exprType
-- fun (x : Nat), x
def exprT1 := Expr.lam `x biDef exprNat (Expr.bvar 0)
-- fun (y : Nat), x
def exprT2 := Expr.lam `y biDef exprNat (Expr.bvar 0)
-- fun (x : Nat), (f x)
def exprT3 := Expr.lam `x biDef exprNat (Expr.app (Expr.const `f []) (Expr.bvar 0))
-- fun (x : Nat), (f x)
def exprT4 := Expr.lam `x BinderInfo.implicit exprNat (Expr.app (Expr.const `f []) (Expr.bvar 0))
def TypeArrowType2 := mkForall `β biDef exprType exprType
-- fun (x : Nat) => x
def exprT1 := mkLambda `x biDef exprNat (mkBVar 0)
-- fun (y : Nat) => x
def exprT2 := mkLambda `y biDef exprNat (mkBVar 0)
-- fun (x : Nat) => (f x)
def exprT3 := mkLambda `x biDef exprNat (mkApp (mkConst `f []) (mkBVar 0))
-- fun (x : Nat) => (f x)
def exprT4 := mkLambda `x BinderInfo.implicit exprNat (mkApp (mkConst `f []) (mkBVar 0))
def check (b : Bool) : IO Unit :=
unless b (throw "failed")

76
tests/lean/run/meta1.lean
View file

@ -29,30 +29,30 @@ mkAppN map #[nat, bool]
#eval tstInferType [`Init.Data.List] t1
def t2 : Expr :=
let prop := Expr.sort Level.zero;
Expr.forallE `x BinderInfo.default prop prop
let prop := mkSort Level.zero;
mkForall `x BinderInfo.default prop prop
#eval tstInferType [`Init.Core] t2
def t3 : Expr :=
let nat := mkConst `Nat [];
let natLe := mkConst `Nat.le [];
let zero := Expr.lit (Literal.natVal 0);
let p := mkAppN natLe #[Expr.bvar 0, zero];
Expr.forallE `x BinderInfo.default nat p
let zero := mkLit (Literal.natVal 0);
let p := mkAppN natLe #[mkBVar 0, zero];
mkForall `x BinderInfo.default nat p
#eval tstInferType [`Init.Data.Nat] t3
def t4 : Expr :=
let nat := mkConst `Nat [];
let p := mkAppN (mkConst `Nat.succ []) #[Expr.bvar 0];
Expr.lam `x BinderInfo.default nat p
let p := mkAppN (mkConst `Nat.succ []) #[mkBVar 0];
mkLambda `x BinderInfo.default nat p
#eval tstInferType [`Init.Core] t4
def t5 : Expr :=
let add := mkConst `Nat.add [];
mkAppN add #[Expr.lit (Literal.natVal 3), Expr.lit (Literal.natVal 5)]
mkAppN add #[mkLit (Literal.natVal 3), mkLit (Literal.natVal 5)]
#eval tstWHNF [`Init.Data.Nat] t5
#eval tstWHNF [`Init.Data.Nat] t5 TransparencyMode.reducible
@ -64,58 +64,58 @@ def t6 : Expr :=
let map := mkConst `List.map [Level.one, Level.one];
let nat := mkConst `Nat [];
let add := mkConst `Nat.add [];
let f := Expr.lam `x BinderInfo.default nat (mkAppN add #[Expr.bvar 0, Expr.lit (Literal.natVal 1)]);
let cons := Expr.app (mkConst `List.cons [Level.zero]) nat;
let nil := Expr.app (mkConst `List.nil [Level.zero]) nat;
let one := Expr.lit (Literal.natVal 1);
let four := Expr.lit (Literal.natVal 4);
let xs := Expr.app (Expr.app cons one) (Expr.app (Expr.app cons four) nil);
let f := mkLambda `x BinderInfo.default nat (mkAppN add #[mkBVar 0, mkLit (Literal.natVal 1)]);
let cons := mkApp (mkConst `List.cons [Level.zero]) nat;
let nil := mkApp (mkConst `List.nil [Level.zero]) nat;
let one := mkLit (Literal.natVal 1);
let four := mkLit (Literal.natVal 4);
let xs := mkApp (mkApp cons one) (mkApp (mkApp cons four) nil);
mkAppN map #[nat, nat, f, xs]
#eval tstInferType [`Init.Data.List] t6
#eval tstWHNF [`Init.Data.List] t6
#eval tstInferType [] $ Expr.sort Level.zero
#eval tstInferType [] $ mkSort Level.zero
#eval tstInferType [`Init.Data.List] $ Expr.lam `a BinderInfo.implicit (Expr.sort Level.one) (Expr.lam `x BinderInfo.default (Expr.bvar 0) (Expr.lam `xs BinderInfo.default (Expr.app (mkConst `List [Level.zero]) (Expr.bvar 1)) (Expr.bvar 0)))
#eval tstInferType [`Init.Data.List] $ mkLambda `a BinderInfo.implicit (mkSort Level.one) (mkLambda `x BinderInfo.default (mkBVar 0) (mkLambda `xs BinderInfo.default (mkApp (mkConst `List [Level.zero]) (mkBVar 1)) (mkBVar 0)))
def t7 : Expr :=
let nat := mkConst `Nat [];
let one := Expr.lit (Literal.natVal 1);
Expr.letE `x nat one one
let one := mkLit (Literal.natVal 1);
mkLet `x nat one one
#eval tstInferType [`Init.Core] $ t7
#eval tstWHNF [`Init.Core] $ t7
def t8 : Expr :=
let nat := mkConst `Nat [];
let one := Expr.lit (Literal.natVal 1);
let one := mkLit (Literal.natVal 1);
let add := mkConst `Nat.add [];
Expr.letE `x nat one (mkAppN add #[one, Expr.bvar 0])
mkLet `x nat one (mkAppN add #[one, mkBVar 0])
#eval tstInferType [`Init.Core] $ t8
#eval tstWHNF [`Init.Core] $ t8
def t9 : Expr :=
let nat := mkConst `Nat [];
Expr.letE `a (Expr.sort Level.one) nat (Expr.forallE `x BinderInfo.default (Expr.bvar 0) (Expr.bvar 1))
mkLet `a (mkSort Level.one) nat (mkForall `x BinderInfo.default (mkBVar 0) (mkBVar 1))
#eval tstInferType [`Init.Core] $ t9
#eval tstWHNF [`Init.Core] $ t9
#eval tstInferType [`Init.Core] $ Expr.lit (Literal.natVal 10)
#eval tstInferType [`Init.Core] $ Expr.lit (Literal.strVal "hello")
#eval tstInferType [`Init.Core] $ Expr.mdata {} $ Expr.lit (Literal.natVal 10)
#eval tstInferType [`Init.Core] $ mkLit (Literal.natVal 10)
#eval tstInferType [`Init.Core] $ mkLit (Literal.strVal "hello")
#eval tstInferType [`Init.Core] $ mkMData {} $ mkLit (Literal.natVal 10)
#eval tstInferType [`Init.Lean.Trace] (Expr.proj `Inhabited 0 (mkConst `Lean.TraceState.Inhabited []))
#eval tstInferType [`Init.Lean.Trace] (Expr.proj `Lean.TraceState 0 (Expr.proj `Inhabited 0 (mkConst `Lean.TraceState.Inhabited [])))
#eval tstWHNF [`Init.Lean.Trace] (Expr.proj `Inhabited 0 (mkConst `Lean.TraceState.Inhabited []))
#eval tstWHNF [`Init.Lean.Trace] (Expr.proj `Lean.TraceState 0 (Expr.proj `Inhabited 0 (mkConst `Lean.TraceState.Inhabited [])))
#eval tstInferType [`Init.Lean.Trace] (mkProj `Inhabited 0 (mkConst `Lean.TraceState.Inhabited []))
#eval tstInferType [`Init.Lean.Trace] (mkProj `Lean.TraceState 0 (mkProj `Inhabited 0 (mkConst `Lean.TraceState.Inhabited [])))
#eval tstWHNF [`Init.Lean.Trace] (mkProj `Inhabited 0 (mkConst `Lean.TraceState.Inhabited []))
#eval tstWHNF [`Init.Lean.Trace] (mkProj `Lean.TraceState 0 (mkProj `Inhabited 0 (mkConst `Lean.TraceState.Inhabited [])))
def t10 : Expr :=
let nat := mkConst `Nat [];
let refl := Expr.app (mkConst `Eq.refl [Level.one]) nat;
Expr.lam `a BinderInfo.default nat (Expr.app refl (Expr.bvar 0))
let refl := mkApp (mkConst `Eq.refl [Level.one]) nat;
mkLambda `a BinderInfo.default nat (mkApp refl (mkBVar 0))
#eval tstInferType [`Init.Core] t10
#eval tstIsProp [`Init.Core] t10
@ -125,17 +125,17 @@ Expr.lam `a BinderInfo.default nat (Expr.app refl (Expr.bvar 0))
#eval tstIsProp [`Init.Core] (mkConst `And [])
-- Example where isPropQuick fails
#eval tstIsProp [`Init.Core] (mkAppN (mkConst `id [Level.zero]) #[Expr.sort Level.zero, mkAppN (mkConst `And []) #[mkConst `True [], mkConst
#eval tstIsProp [`Init.Core] (mkAppN (mkConst `id [Level.zero]) #[mkSort Level.zero, mkAppN (mkConst `And []) #[mkConst `True [], mkConst
`True []]])
#eval tstIsProp [`Init.Core] (mkAppN (mkConst `Eq [Level.one]) #[mkConst `Nat [], Expr.lit (Literal.natVal 0), Expr.lit (Literal.natVal 1)])
#eval tstIsProp [`Init.Core] (mkAppN (mkConst `Eq [Level.one]) #[mkConst `Nat [], mkLit (Literal.natVal 0), mkLit (Literal.natVal 1)])
#eval tstIsProp [`Init.Core] $
Expr.forallE `x BinderInfo.default (mkConst `Nat [])
(mkAppN (mkConst `Eq [Level.one]) #[mkConst `Nat [], Expr.bvar 0, Expr.lit (Literal.natVal 1)])
mkForall `x BinderInfo.default (mkConst `Nat [])
(mkAppN (mkConst `Eq [Level.one]) #[mkConst `Nat [], mkBVar 0, mkLit (Literal.natVal 1)])
#eval tstIsProp [`Init.Core] $
Expr.app
(Expr.lam `x BinderInfo.default (mkConst `Nat [])
(mkAppN (mkConst `Eq [Level.one]) #[mkConst `Nat [], Expr.bvar 0, Expr.lit (Literal.natVal 1)]))
(Expr.lit (Literal.natVal 0))
mkApp
(mkLambda `x BinderInfo.default (mkConst `Nat [])
(mkAppN (mkConst `Eq [Level.one]) #[mkConst `Nat [], mkBVar 0, mkLit (Literal.natVal 1)]))
(mkLit (Literal.natVal 0))

24
tests/lean/run/update.lean
View file

@ -2,28 +2,28 @@ import Init.Lean.Expr
open Lean
def main : IO Unit :=
do let f := Expr.const `f [];
let x := Expr.const `x [];
let y := Expr.const `y [];
let t1 := Expr.app f x;
do let f := mkConst `f [];
let x := mkConst `x [];
let y := mkConst `y [];
let t1 := mkApp f x;
let t2 := t1.updateApp! f y;
let t3 := t1.updateApp! f x;
let t4 := Expr.proj `Prod 1 x;
let t4 := mkProj `Prod 1 x;
let t5 := t4.updateProj! y;
let t6 := t4.updateProj! x;
let x₁ := x.updateConst! [Level.one];
let x₂ := x.updateConst! [];
let s := Expr.sort Level.one;
let s := mkSort Level.one;
let s₁ := s.updateSort! Level.one;
let s₂ := s.updateSort! Level.zero;
let a := Expr.forallE `x BinderInfo.default s s;
let a := mkForall `x BinderInfo.default s s;
let a₁ := a.updateForall! BinderInfo.default s s;
let a₂ := a.updateForall! BinderInfo.default s₂ s;
let nat := Expr.const `Nat [];
let id := Expr.lam `x BinderInfo.default nat (Expr.bvar 0);
let id₁ := id.updateLambda! BinderInfo.default s (Expr.bvar 0);
let id₂ := id.updateLambda! BinderInfo.default nat (Expr.bvar 0);
let l := Expr.letE `z nat x t1;
let nat := mkConst `Nat [];
let id := mkLambda `x BinderInfo.default nat (mkBVar 0);
let id₁ := id.updateLambda! BinderInfo.default s (mkBVar 0);
let id₂ := id.updateLambda! BinderInfo.default nat (mkBVar 0);
let l := mkLet `z nat x t1;
let l₁ := l.updateLet! nat x t2;
let l₂ := l.updateLet! nat x t1;
IO.println [t1, t2, t3, t5, t6, x₁, x₂, s₁, s₂, a₁, a₂, id₁, id₂, l₁, l₂];

14
tests/lean/typeclass_context.lean
View file

@ -31,25 +31,25 @@ get >>= λ (ctx : Context) => pure $ ctx.eInstantiate t
def testEUnify4 : EStateM String Context Expr := do
t₁ ← EStateM.fromStateM $ eNewMeta (mkConst "Term");
t₂ ← EStateM.fromStateM $ eNewMeta (mkConst "Term");
eUnify (Expr.forallE "foo" BinderInfo.default t₂ t₁) (Expr.forallE "foo" BinderInfo.default t₁ t₂);
eUnify (mkForall "foo" BinderInfo.default t₂ t₁) (mkForall "foo" BinderInfo.default t₁ t₂);
get >>= λ (ctx : Context) => pure $ ctx.eInstantiate t₂
def testEUnify5 : EStateM String Context Expr := do
t₁ ← EStateM.fromStateM $ eNewMeta (mkConst "Term");
t₂ ← EStateM.fromStateM $ eNewMeta (mkConst "Term");
eUnify (Expr.forallE "foo" BinderInfo.default t₁ t₂) (Expr.forallE "foo" BinderInfo.default t₂ t₁);
eUnify (mkForall "foo" BinderInfo.default t₁ t₂) (mkForall "foo" BinderInfo.default t₂ t₁);
get >>= λ (ctx : Context) => pure $ ctx.eInstantiate t₂
def testEUnify6 : EStateM String Context Expr := do
u ← EStateM.fromStateM Context.uNewMeta;
let t₁ := Expr.const "foo" [Level.zero];
let t₂ := Expr.const "foo" [u];
let t₁ := mkConst "foo" [Level.zero];
let t₂ := mkConst "foo" [u];
eUnify t₁ t₂;
get >>= λ (ctx : Context) => pure $ ctx.eInstantiate t₂
def testEUnify7 : EStateM String Context Expr := do
e ← EStateM.fromStateM $ Context.eNewMeta $ Expr.sort Level.zero;
let t₁ := Expr.fvar "foo";
e ← EStateM.fromStateM $ Context.eNewMeta $ mkSort Level.zero;
let t₁ := mkFVar "foo";
let t₂ := e;
eUnify t₁ t₂;
get >>= λ (ctx : Context) => pure $ ctx.eInstantiate t₂
@ -98,7 +98,7 @@ pure $ αNorm (mkConst "f")
def testAlphaNorm4 : EStateM String Context Expr := do
t₁ ← EStateM.fromStateM $ eNewMeta (mkConst "Term");
t₂ ← EStateM.fromStateM $ eNewMeta (mkConst "Term");
pure $ αNorm $ Expr.forallE "foo" BinderInfo.default (mkAppN (mkConst "f") #[t₂]) (mkAppN (mkConst "g") #[t₁])
pure $ αNorm $ mkForall "foo" BinderInfo.default (mkAppN (mkConst "f") #[t₂]) (mkAppN (mkConst "g") #[t₁])
#eval testEUnify1.run {}
#eval testEUnify2.run {}

2
tests/playground/ir.lean
View file

@ -4,7 +4,7 @@ open Lean.IR
def tst1 : IO Unit :=
let fbody : FnBody :=
FnBody.vdecl `x IRType.uint32 (Expr.lit (LitVal.num 0)) $
FnBody.ret `x in
FnBody.ret `x;
IO.println $ format fbody
def main : IO Unit :=