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

test: add etaExpanded? tests

Browse source
This commit is contained in:
Leonardo de Moura 2019-11-12 12:24:31 -08:00
parent 4cc413e4f6
commit 28d7fe3f49
1 changed files with 34 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -53,8 +53,40 @@ do let f := Expr.const `f [];
unless (t2.hasLooseBVar 0) $ throw "failed-2";
unless (!t3.hasLooseBVar 0) $ throw "failed-3";
unless (t4.hasLooseBVar 0) $ throw "failed-4";
unless (!t4.hasLooseBVar 1) $ throw "failed-4";
unless (!t2.hasLooseBVar 1) $ throw "failed-5";
unless (!t4.hasLooseBVar 1) $ throw "failed-5";
unless (!t2.hasLooseBVar 1) $ throw "failed-6";
pure ()
#eval tst4
def tst5 : IO Unit :=
do let f := Expr.const `f [];
let a := Expr.const `a [];
let nat := Expr.const `Nat [];
let x0 := Expr.bvar 0;
let x1 := Expr.bvar 1;
let x2 := Expr.bvar 2;
let t := Expr.lam `x BinderInfo.default nat (Expr.app 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);
unless (t.etaExpanded? == none) $ throw "failed-2";
let t := Expr.lam `x BinderInfo.default nat (mkApp f #[a, x0]);
unless (t.etaExpanded? == some (Expr.app f a)) $ throw "failed-3";
let t := Expr.lam `x BinderInfo.default nat (mkApp 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));
unless (t.etaExpanded? == none) $ throw "failed-5";
let t := Expr.lam `x BinderInfo.default nat (Expr.lam `y BinderInfo.default nat (mkApp 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 (mkApp 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 (mkApp f #[a, x2, x1, x0])));
IO.println t;
unless (t.etaExpanded? == some (Expr.app f a)) $ throw "failed-8";
IO.println t.etaExpanded?;
pure ()
#eval tst5