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

chore: fix tests

Browse source
This commit is contained in:
Leonardo de Moura 2019-11-17 08:53:18 -08:00
parent d88813feff
commit 033f781724
11 changed files with 48 additions and 48 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

18
tests/lean/lvl1.lean
View file

@ -4,16 +4,16 @@ namespace Lean
namespace Level
def mkMax (xs : Array Level) : Level :=
xs.foldlFrom max (xs.get! 0) 1
xs.foldlFrom mkLevelMax (xs.get! 0) 1
#eval toString $ normalize $ succ $ succ $ mkMax #[zero, param `w, succ (succ (succ (param `z))), one, succ (succ (param `x)), zero, param `x, param `y, param `x, param `z, succ one, param `w, succ (param `x)]
#eval toString $ normalize $ max zero (param `x)
#eval toString $ normalize $ max (param `x) zero
#eval toString $ normalize $ max zero one
#eval toString $ normalize $ succ (max (param `x) (param `x))
#eval toString $ normalize $ max (imax (param `x) one) (max (succ (param `x)) (param `x))
#eval toString $ normalize $ imax (imax (param `x) one) (max (succ (param `x)) (param `x))
#eval toString $ #[zero, succ (succ (param `z)), one, succ (succ (param `x)), zero, param `x, param `y, param `x, param `z, succ (param `x)].qsort normLt
#eval toString $ normalize $ mkLevelSucc $ mkLevelSucc $ mkMax #[levelZero, mkLevelParam `w, mkLevelSucc (mkLevelSucc (mkLevelSucc (mkLevelParam `z))), levelOne, mkLevelSucc (mkLevelSucc (mkLevelParam `x)), levelZero, mkLevelParam `x, mkLevelParam `y, mkLevelParam `x, mkLevelParam `z, mkLevelSucc levelOne, mkLevelParam `w, mkLevelSucc (mkLevelParam `x)]
#eval toString $ normalize $ mkLevelMax levelZero (mkLevelParam `x)
#eval toString $ normalize $ mkLevelMax (mkLevelParam `x) levelZero
#eval toString $ normalize $ mkLevelMax levelZero levelOne
#eval toString $ normalize $ mkLevelSucc (mkLevelMax (mkLevelParam `x) (mkLevelParam `x))
#eval toString $ normalize $ mkLevelMax (mkLevelIMax (mkLevelParam `x) levelOne) (mkLevelMax (mkLevelSucc (mkLevelParam `x)) (mkLevelParam `x))
#eval toString $ normalize $ mkLevelIMax (mkLevelIMax (mkLevelParam `x) levelOne) (mkLevelMax (mkLevelSucc (mkLevelParam `x)) (mkLevelParam `x))
#eval toString $ #[levelZero, mkLevelSucc (mkLevelSucc (mkLevelParam `z)), levelOne, mkLevelSucc (mkLevelSucc (mkLevelParam `x)), levelZero, mkLevelParam `x, mkLevelParam `y, mkLevelParam `x, mkLevelParam `z, mkLevelSucc (mkLevelParam `x)].qsort normLt
end Level
end Lean

6
tests/lean/mvar1.lean
View file

@ -14,12 +14,12 @@ def b0 := mkBVar 0
def b1 := mkBVar 1
def b2 := mkBVar 2
def u := Level.param `u
def u := mkLevelParam `u
def typeE := mkSort Level.one
def typeE := mkSort levelOne
def natE := mkConst `Nat []
def boolE := mkConst `Bool []
def vecE := mkConst `Vec [Level.zero]
def vecE := mkConst `Vec [levelZero]
def α := mkFVar `α
def x := mkFVar `x

6
tests/lean/mvar2.lean
View file

@ -14,12 +14,12 @@ def b0 := mkBVar 0
def b1 := mkBVar 1
def b2 := mkBVar 2
def u := Level.param `u
def u := mkLevelParam `u
def typeE := mkSort Level.one
def typeE := mkSort levelOne
def natE := mkConst `Nat []
def boolE := mkConst `Bool []
def vecE := mkConst `Vec [Level.zero]
def vecE := mkConst `Vec [levelZero]
def α := mkFVar `α
def x := mkFVar `x

6
tests/lean/mvar3.lean
View file

@ -20,12 +20,12 @@ def b0 := mkBVar 0
def b1 := mkBVar 1
def b2 := mkBVar 2
def u := Level.param `u
def u := mkLevelParam `u
def typeE := mkSort Level.one
def typeE := mkSort levelOne
def natE := mkConst `Nat
def boolE := mkConst `Bool
def vecE := mkConst `Vec [Level.zero]
def vecE := mkConst `Vec [levelZero]
def α := mkFVar `α
def x := mkFVar `x

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

@ -16,8 +16,8 @@ do let f := mkConst `f [];
#eval tst1
def tst2 : IO Unit :=
do let l1 := Level.max (Level.param `a) (Level.param `b);
let l2 := Level.max (Level.param `b) (Level.param `a);
do let l1 := mkLevelMax (mkLevelParam `a) (mkLevelParam `b);
let l2 := mkLevelMax (mkLevelParam `b) (mkLevelParam `a);
IO.println l1;
IO.println l2;
unless (Level.isEquiv l1 l2) $ throw "not equiv";
@ -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 := mkLambda `x BinderInfo.default (mkSort Level.zero) (mkAppN f #[a, x0]);
let t4 := mkLambda `x BinderInfo.default (mkSort Level.zero) (mkAppN f #[a, x1]);
let t3 := mkLambda `x BinderInfo.default (mkSort levelZero) (mkAppN f #[a, x0]);
let t4 := mkLambda `x BinderInfo.default (mkSort levelZero) (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";

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

@ -1,7 +1,7 @@
import Init.Lean.Expr
open Lean
def exprType : Expr := mkSort Level.one
def exprType : Expr := mkSort levelOne
def biDef := BinderInfo.default
def exprNat := mkConst `Nat []
-- Type -> Type

4
tests/lean/run/instuniv.lean
View file

@ -5,8 +5,8 @@ def tst : IO Unit :=
do env ← importModules [`Init.Data.Array.Default];
match env.find `Array.foldl with
| some info => do
IO.println (info.instantiateTypeLevelParams [Level.zero, Level.zero]);
IO.println (info.instantiateValueLevelParams [Level.zero, Level.zero]);
IO.println (info.instantiateTypeLevelParams [levelZero, levelZero]);
IO.println (info.instantiateValueLevelParams [levelZero, levelZero]);
pure ()
| none => IO.println ("Array.foldl not found");
pure ()

8
tests/lean/run/level.lean
View file

@ -1,7 +1,7 @@
import Init.Lean.Level
open Lean
#eval Level.zero == Level.zero
#eval Level.zero == Level.succ Level.zero
#eval Level.max (Level.succ Level.zero) Level.zero == Level.succ Level.zero
#eval Level.max (Level.succ Level.zero) Level.zero == Level.max (Level.succ Level.zero) Level.zero
#eval levelZero == levelZero
#eval levelZero == mkLevelSucc levelZero
#eval mkLevelMax (mkLevelSucc levelZero) levelZero == mkLevelSucc levelZero
#eval mkLevelMax (mkLevelSucc levelZero) levelZero == mkLevelMax (mkLevelSucc levelZero) levelZero

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

@ -21,7 +21,7 @@ do env ← importModules mods;
| EStateM.Result.error err _ => throw (IO.userError (toString err))
def t1 : Expr :=
let map := mkConst `List.map [Level.one, Level.one];
let map := mkConst `List.map [levelOne, levelOne];
let nat := mkConst `Nat [];
let bool := mkConst `Bool [];
mkAppN map #[nat, bool]
@ -29,7 +29,7 @@ mkAppN map #[nat, bool]
#eval tstInferType [`Init.Data.List] t1
def t2 : Expr :=
let prop := mkSort Level.zero;
let prop := mkSort levelZero;
mkForall `x BinderInfo.default prop prop
#eval tstInferType [`Init.Core] t2
@ -61,12 +61,12 @@ set_option pp.all true
#check @List.cons Nat
def t6 : Expr :=
let map := mkConst `List.map [Level.one, Level.one];
let map := mkConst `List.map [levelOne, levelOne];
let nat := mkConst `Nat [];
let add := mkConst `Nat.add [];
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 cons := mkApp (mkConst `List.cons [levelZero]) nat;
let nil := mkApp (mkConst `List.nil [levelZero]) nat;
let one := mkLit (Literal.natVal 1);
let four := mkLit (Literal.natVal 4);
let xs := mkApp (mkApp cons one) (mkApp (mkApp cons four) nil);
@ -75,9 +75,9 @@ mkAppN map #[nat, nat, f, xs]
#eval tstInferType [`Init.Data.List] t6
#eval tstWHNF [`Init.Data.List] t6
#eval tstInferType [] $ mkSort Level.zero
#eval tstInferType [] $ mkSort levelZero
#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)))
#eval tstInferType [`Init.Data.List] $ mkLambda `a BinderInfo.implicit (mkSort levelOne) (mkLambda `x BinderInfo.default (mkBVar 0) (mkLambda `xs BinderInfo.default (mkApp (mkConst `List [levelZero]) (mkBVar 1)) (mkBVar 0)))
def t7 : Expr :=
let nat := mkConst `Nat [];
@ -98,7 +98,7 @@ mkLet `x nat one (mkAppN add #[one, mkBVar 0])
def t9 : Expr :=
let nat := mkConst `Nat [];
mkLet `a (mkSort Level.one) nat (mkForall `x BinderInfo.default (mkBVar 0) (mkBVar 1))
mkLet `a (mkSort levelOne) nat (mkForall `x BinderInfo.default (mkBVar 0) (mkBVar 1))
#eval tstInferType [`Init.Core] $ t9
#eval tstWHNF [`Init.Core] $ t9
@ -114,7 +114,7 @@ mkLet `a (mkSort Level.one) nat (mkForall `x BinderInfo.default (mkBVar 0) (mkBV
def t10 : Expr :=
let nat := mkConst `Nat [];
let refl := mkApp (mkConst `Eq.refl [Level.one]) nat;
let refl := mkApp (mkConst `Eq.refl [levelOne]) nat;
mkLambda `a BinderInfo.default nat (mkApp refl (mkBVar 0))
#eval tstInferType [`Init.Core] t10
@ -125,17 +125,17 @@ mkLambda `a BinderInfo.default nat (mkApp refl (mkBVar 0))
#eval tstIsProp [`Init.Core] (mkConst `And [])
-- Example where isPropQuick fails
#eval tstIsProp [`Init.Core] (mkAppN (mkConst `id [Level.zero]) #[mkSort Level.zero, mkAppN (mkConst `And []) #[mkConst `True [], mkConst
#eval tstIsProp [`Init.Core] (mkAppN (mkConst `id [levelZero]) #[mkSort levelZero, mkAppN (mkConst `And []) #[mkConst `True [], mkConst
`True []]])
#eval tstIsProp [`Init.Core] (mkAppN (mkConst `Eq [Level.one]) #[mkConst `Nat [], mkLit (Literal.natVal 0), mkLit (Literal.natVal 1)])
#eval tstIsProp [`Init.Core] (mkAppN (mkConst `Eq [levelOne]) #[mkConst `Nat [], mkLit (Literal.natVal 0), mkLit (Literal.natVal 1)])
#eval tstIsProp [`Init.Core] $
mkForall `x BinderInfo.default (mkConst `Nat [])
(mkAppN (mkConst `Eq [Level.one]) #[mkConst `Nat [], mkBVar 0, mkLit (Literal.natVal 1)])
(mkAppN (mkConst `Eq [levelOne]) #[mkConst `Nat [], mkBVar 0, mkLit (Literal.natVal 1)])
#eval tstIsProp [`Init.Core] $
mkApp
(mkLambda `x BinderInfo.default (mkConst `Nat [])
(mkAppN (mkConst `Eq [Level.one]) #[mkConst `Nat [], mkBVar 0, mkLit (Literal.natVal 1)]))
(mkAppN (mkConst `Eq [levelOne]) #[mkConst `Nat [], mkBVar 0, mkLit (Literal.natVal 1)]))
(mkLit (Literal.natVal 0))

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

@ -11,11 +11,11 @@ do let f := mkConst `f [];
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! [levelOne];
let x₂ := x.updateConst! [];
let s := mkSort Level.one;
let s₁ := s.updateSort! Level.one;
let s₂ := s.updateSort! Level.zero;
let s := mkSort levelOne;
let s₁ := s.updateSort! levelOne;
let s₂ := s.updateSort! levelZero;
let a := mkForall `x BinderInfo.default s s;
let a₁ := a.updateForall! BinderInfo.default s s;
let a₂ := a.updateForall! BinderInfo.default s₂ s;

4
tests/lean/typeclass_context.lean
View file

@ -42,13 +42,13 @@ get >>= λ (ctx : Context) => pure $ ctx.eInstantiate t₂
def testEUnify6 : EStateM String Context Expr := do
u ← EStateM.fromStateM Context.uNewMeta;
let t₁ := mkConst "foo" [Level.zero];
let t₁ := mkConst "foo" [levelZero];
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 $ mkSort Level.zero;
e ← EStateM.fromStateM $ Context.eNewMeta $ mkSort levelZero;
let t₁ := mkFVar "foo";
let t₂ := e;
eUnify t₁ t₂;