tests.v 2.13 KB
Newer Older
Ralf Jung's avatar
Ralf Jung committed
1
(** This file is essentially a bunch of testcases. *)
2
3
4
Require Import modures.logic.
Require Import barrier.lifting.
Import uPred.
Ralf Jung's avatar
Ralf Jung committed
5
6

Module LangTests.
7
8
  Definition add :=  Plus (LitNat 21) (LitNat 21).
  Goal  σ, prim_step add σ (LitNat 42) σ None.
Ralf Jung's avatar
Ralf Jung committed
9
  Proof.
10
    constructor.
Ralf Jung's avatar
Ralf Jung committed
11
12
  Qed.

13
  Definition rec := Rec (App (Var 0) (Var 1)). (* fix f x => f x *)
14
  Definition rec_app := App rec (LitNat 0).
Ralf Jung's avatar
Ralf Jung committed
15
16
  Goal  σ, prim_step rec_app σ rec_app σ None.
  Proof.
17
    move=>?. eapply BetaS.
Ralf Jung's avatar
Ralf Jung committed
18
19
20
    reflexivity.
  Qed.

21
22
  Definition lam := Lam (Plus (Var 0) (LitNat 21)).
  Goal  σ, prim_step (App lam (LitNat 21)) σ add σ None.
Ralf Jung's avatar
Ralf Jung committed
23
24
25
26
27
28
29
30
  Proof.
    move=>?. eapply BetaS. reflexivity.
  Qed.
End LangTests.

Module ParamTests.
  Print Assumptions Σ.
End ParamTests.
31
32
33
34
35
36
37
38
39
40

Module LiftingTests.
  (* TODO RJ: Some syntactic sugar for language expressions would be nice. *)
  Definition e3 := Load (Var 0).
  Definition e2 := Seq (Store (Var 0) (Plus (Load (Var 0)) (LitNat 1))) e3.
  Definition e := Let (Alloc (LitNat 1)) e2.
  Goal  σ E, (ownP (Σ:=Σ) σ)  (wp (Σ:=Σ) E e (λ v, (v = LitNatV 2))).
  Proof.
    move=> σ E. rewrite /e.
    rewrite -(wp_bind _ _ (LetCtx EmptyCtx e2)). rewrite -wp_mono.
41
    { eapply wp_alloc_pst; done. }
42
    move=>v; apply exist_elim=>l. apply const_elim_l; move=>[-> _] {v}.
Ralf Jung's avatar
Ralf Jung committed
43
    rewrite -wp_lam -later_intro. asimpl.
44
45
46
    rewrite -(wp_bind _ _ (SeqCtx (StoreRCtx (LocV _)
                                   (PlusLCtx EmptyCtx _)) (Load (Loc _)))).
    rewrite -wp_mono.
47
    { eapply wp_load_pst. apply: lookup_insert. } (* RJ TODO: figure out why apply and eapply fail. *)
48
49
    move=>v; apply const_elim_l; move=>-> {v}.
    rewrite -(wp_bind _ _ (SeqCtx (StoreRCtx (LocV _) EmptyCtx) (Load (Loc _)))).
Ralf Jung's avatar
Ralf Jung committed
50
    rewrite -wp_plus -later_intro.
51
52
    rewrite -(wp_bind _ _ (SeqCtx EmptyCtx (Load (Loc _)))).
    rewrite -wp_mono.
53
    { eapply wp_store_pst; first reflexivity. apply: lookup_insert. }
54
    move=>v; apply const_elim_l; move=>-> {v}.
Ralf Jung's avatar
Ralf Jung committed
55
    rewrite -wp_lam -later_intro. asimpl.
56
    rewrite -wp_mono.
57
    { eapply wp_load_pst. apply: lookup_insert. }
58
59
60
61
    move=>v; apply const_elim_l; move=>-> {v}.
    by apply const_intro.
  Qed.
End LiftingTests.