tests.v 2.37 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

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.
40
41
42
43
    rewrite -(wp_bind _ _ (LetCtx EmptyCtx e2)). rewrite -wp_alloc_pst; last done.
    apply sep_intro_True_r; first done.
    rewrite -later_intro. apply forall_intro=>l.
    apply wand_intro_l. rewrite right_id. apply const_elim_l; move=>_.
Ralf Jung's avatar
Ralf Jung committed
44
    rewrite -wp_lam -later_intro. asimpl.
45
46
    rewrite -(wp_bind _ _ (SeqCtx (StoreRCtx (LocV _)
                                   (PlusLCtx EmptyCtx _)) (Load (Loc _)))).
47
48
49
    rewrite -wp_load_pst; first (apply sep_intro_True_r; first done); last first.
    { apply: lookup_insert. } (* RJ TODO: figure out why apply and eapply fail. *)
    rewrite -later_intro. apply wand_intro_l. rewrite right_id.
50
    rewrite -(wp_bind _ _ (SeqCtx (StoreRCtx (LocV _) EmptyCtx) (Load (Loc _)))).
Ralf Jung's avatar
Ralf Jung committed
51
    rewrite -wp_plus -later_intro.
52
    rewrite -(wp_bind _ _ (SeqCtx EmptyCtx (Load (Loc _)))).
53
54
55
56
    rewrite -wp_store_pst; first (apply sep_intro_True_r; first done); last first.
    { apply: lookup_insert. }
    { reflexivity. }
    rewrite -later_intro. apply wand_intro_l. rewrite right_id.
Ralf Jung's avatar
Ralf Jung committed
57
    rewrite -wp_lam -later_intro. asimpl.
58
59
60
    rewrite -wp_load_pst; first (apply sep_intro_True_r; first done); last first.
    { apply: lookup_insert. }
    rewrite -later_intro. apply wand_intro_l. rewrite right_id.
61
62
63
    by apply const_intro.
  Qed.
End LiftingTests.