tests.v 2.16 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
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61

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.
    { eapply wp_alloc; done. }
    move=>v; apply exist_elim=>l. apply const_elim_l; move=>[-> _] {v}.
    rewrite (later_intro (ownP _)); apply wp_lam. asimpl.
    rewrite -(wp_bind _ _ (SeqCtx (StoreRCtx (LocV _)
                                   (PlusLCtx EmptyCtx _)) (Load (Loc _)))).
    rewrite -wp_mono.
    { eapply wp_load. apply: lookup_insert. } (* RJ TODO: figure out why apply and eapply fail. *)
    move=>v; apply const_elim_l; move=>-> {v}.
    rewrite -(wp_bind _ _ (SeqCtx (StoreRCtx (LocV _) EmptyCtx) (Load (Loc _)))).
    rewrite (later_intro (ownP _)); apply wp_plus.
    rewrite -(wp_bind _ _ (SeqCtx EmptyCtx (Load (Loc _)))).
    rewrite -wp_mono.
    { eapply wp_store; first reflexivity. apply: lookup_insert. }
    move=>v; apply const_elim_l; move=>-> {v}.
    rewrite (later_intro (ownP _)); apply wp_lam. asimpl.
    rewrite -wp_mono.
    { eapply wp_load. apply: lookup_insert. }
    move=>v; apply const_elim_l; move=>-> {v}.
    by apply const_intro.
  Qed.
End LiftingTests.