tests.v 735 Bytes
Newer Older
Ralf Jung's avatar
Ralf Jung committed
1
2
(** This file is essentially a bunch of testcases. *)
Require Import modures.base.
3
Require Import barrier.parameter.
Ralf Jung's avatar
Ralf Jung committed
4
5
6
7
8
9
10
11
12

Module LangTests.
  Definition add := Op2 plus (Lit 21) (Lit 21).

  Goal  σ, prim_step add σ (Lit 42) σ None.
  Proof.
    apply Op2S.
  Qed.

13
  Definition rec := Rec (App (Var 0) (Var 1)). (* fix f x => f x *)
Ralf Jung's avatar
Ralf Jung committed
14
15
16
  Definition rec_app := App rec (Lit 0).
  Goal  σ, prim_step rec_app σ rec_app σ None.
  Proof.
17
    move=>?. eapply BetaS.
Ralf Jung's avatar
Ralf Jung committed
18
19
20
21
22
23
24
25
26
27
28
29
30
    reflexivity.
  Qed.

  Definition lam := Lam (Op2 plus (Var 0) (Lit 21)).
  Goal  σ, prim_step (App lam (Lit 21)) σ add σ None.
  Proof.
    move=>?. eapply BetaS. reflexivity.
  Qed.
End LangTests.

Module ParamTests.
  Print Assumptions Σ.
End ParamTests.