FG_stack.v 7.23 KB
Newer Older
1
From iris_logrel Require Export logrel.
Amin Timany's avatar
Amin Timany committed
2

3
(* stack τ = μ x. ref (Unit + τ * x) *)
4 5 6
Definition FG_StackType τ :=
  TRec (Tref (TSum TUnit (TProd τ.[ren (+1)] (TVar 0)))).

7
Notation Conse h t := (Fold (Alloc (InjR (Pair h t)))).
8
Notation Nile := (Fold (Alloc (InjL #()))).
9 10 11 12

Definition FG_push : val := rec: "push" "st" := λ: "x",
  let: "stv" := !"st" in
  if: (CAS "st" "stv" (Conse "x" "stv"))
13
  then #()
14 15
  else "push" "st" "x".

16

17 18 19 20 21 22 23 24 25 26
(* pop st = λ (),
     (λ str. 
       (λ x. match x with 
             | nil => InjL #()
             | cons y ys => 
               if CAS(st, str, ys)
                  (InjR y)
                  (pop st ())) 
       (load str)) 
     (load st)*)
27 28 29
Definition FG_pop : val := rec: "pop" "st" := λ: <>,
  let: "stv" := !"st" in
  let: "x" := !(Unfold "stv") in
30 31 32 33 34 35
  match: "x" with
    InjL <> => InjL #()
  | InjR "x" => let: "y" := Fst "x" in let: "ys" := Snd "x" in
                if: (CAS "st" "stv" "ys")
                then (InjR "y")
                else "pop" "st" #()
36
  end.
37

38 39 40 41
(* iter f = λ st.
   case (load st) of
   | nil => #()
   | cons y ys => f y ;; iter f ys *)
42
Definition FG_iter : val := rec: "iter" "f" := λ: "st",
43 44 45
  match: !(Unfold "st") with
    InjL <> => #()
  | InjR "x" =>
46 47 48 49 50 51 52 53 54 55
    let: "y" := Fst "x" in
    let: "ys" := Snd "x" in
    "f" "y";; "iter" "f" "ys"
  end.

Definition FG_read_iter : val := λ: "st" "f",
  FG_iter "f" (!"st").

Definition FG_stack_body : val := λ: "st",
  (FG_push "st", FG_pop "st", FG_read_iter "st").
56

57
(* stack = Λα. (λ (s : stack α). stack_body s) (ref (ref nil)) *)
58 59 60
Definition FG_stack : val :=
  Λ: let: "st" := ref Nile in
     FG_stack_body "st".
61

62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125
Definition sτ (α : type) : type := Tref (FG_StackType α).
Definition newStack : val := Λ: λ: <>, ref Nile.
Definition popStack : val := Λ: λ: "st", FG_pop "st" #().
Definition pushStack : val := Λ: FG_push.
Definition stackmod : val := Λ:
  Pack (TApp newStack, TApp popStack, TApp pushStack).

Section typing.
  Context (HEQTP :  τ, EqType (FG_StackType τ)).

  Hint Unfold sτ : typeable.
  Lemma newStack_typed Γ :
    Γ ⊢ₜ newStack : TForall (TArrow TUnit (sτ (TVar 0))).
  Proof.
    unlock sτ newStack. (* TODO need to explicitly unlock newStack here *)
    solve_typed.
  Qed.
  Hint Resolve newStack_typed : typeable.

  Lemma popStack_typed Γ :
    Γ ⊢ₜ popStack : TForall $ TArrow (sτ (TVar 0)) (TSum TUnit (TVar 0)).
  Proof.
    unlock sτ popStack. (* TODO need to explicitly unlock newStack here *)
    unlock FG_pop.
    repeat (econstructor; eauto 10 with typeable).
  Qed.
  Hint Resolve popStack_typed : typeable.

  Lemma pushStack_typed Γ :
    Γ ⊢ₜ pushStack : TForall $ TArrow (sτ (TVar 0)) (TArrow (TVar 0) TUnit).
  Proof.
    unlock sτ pushStack. (* TODO need to explicitly unlock newStack here *)
    unlock FG_push.
    solve_typed.
  Qed.
  Hint Resolve pushStack_typed : typeable.

  Lemma stackmod_typed Γ :
    Γ ⊢ₜ stackmod : TForall $ TExists $ TProd (TProd
                                                 (TArrow TUnit (TVar 0))
                                                 (TArrow (TVar 0) (TSum TUnit (TVar 1))))
                                                 (TArrow (TVar 0) (TArrow (TVar 1) TUnit)).
  Proof.
    unlock stackmod.
    econstructor.
    eapply TPack with (sτ (TVar 0)).
    econstructor; [econstructor | ].
    - simpl.
      replace (TArrow TUnit (sτ (TVar 0))) with ((TArrow TUnit (sτ (TVar 0))).[TVar 0/]); last first.
      { autosubst. }
      solve_typed.
    - simpl.
      replace (TArrow (sτ (TVar 0)) (TSum TUnit (ids 0)))
        with (TArrow (sτ (TVar 0)) (TSum TUnit (TVar 0))).[TVar 0/]; last first.
      { autosubst. }
      solve_typed.
    - simpl.
      replace (TArrow (sτ (TVar 0)) (TArrow (ids 0) TUnit))
        with (TArrow (sτ (TVar 0)) (TArrow (ids 0) TUnit)).[TVar 0/] by autosubst.
      solve_typed.
  Qed.
  Hint Resolve stackmod_typed.
End typing.

Amin Timany's avatar
Amin Timany committed
126 127 128 129 130 131 132
Section FG_stack.
  (* Fine-grained push *)

  Section FG_push_type.
    (* The following assumption is simply ** WRONG ** *)
    (* We assume it though to just be able to prove that the
       stack we are implementing is /type-sane/ so to speak! *)
133 134
    (* EqType (stack τ) would mean that we can compare two stacks for
       equality, we need this for compare-and-swap *)
Amin Timany's avatar
Amin Timany committed
135 136
    Context (HEQTP :  τ, EqType (FG_StackType τ)).

137 138
    Lemma FG_push_type Γ τ :      
      typed Γ FG_push (TArrow (Tref (FG_StackType τ)) (TArrow τ TUnit)).
Amin Timany's avatar
Amin Timany committed
139
    Proof.
140 141 142
      unfold FG_push. unlock.
      repeat (econstructor; eauto with typeable).
      asimpl. eauto with typeable.
Amin Timany's avatar
Amin Timany committed
143 144
    Qed.

145
  End FG_push_type.
Amin Timany's avatar
Amin Timany committed
146

147
  Hint Resolve FG_push_type : typeable.
Amin Timany's avatar
Amin Timany committed
148 149 150

  Global Opaque FG_push.

151
  (* Fine-grained pop *)
Amin Timany's avatar
Amin Timany committed
152 153 154 155 156 157
  Section FG_pop_type.
    (* The following assumption is simply ** WRONG ** *)
    (* We assume it though to just be able to prove that the
       stack we are implementing is /type-sane/ so to speak! *)
    Context (HEQTP :  τ, EqType (FG_StackType τ)).

158 159
    Lemma FG_pop_type Γ τ :
      typed Γ FG_pop (TArrow (Tref (FG_StackType τ)) (TArrow TUnit (TSum TUnit τ))).
Amin Timany's avatar
Amin Timany committed
160
    Proof.
161 162 163
      unfold FG_pop. unlock.
      repeat (econstructor; eauto 10 with typeable).
      cbn. asimpl. eauto 20 with typeable.
Amin Timany's avatar
Amin Timany committed
164 165
    Qed.

166 167 168
  End FG_pop_type.
  
  Hint Resolve FG_pop_type : typeable.
Amin Timany's avatar
Amin Timany committed
169 170 171 172

  Global Opaque FG_pop.

  (* Fine-grained iter *)
173 174 175

  Lemma FG_iter_type Γ τ :
    typed Γ FG_iter (TArrow (TArrow τ TUnit) (TArrow (FG_StackType τ) TUnit)).
Amin Timany's avatar
Amin Timany committed
176
  Proof.
177 178 179
    unfold FG_iter. unlock.
    repeat (econstructor; eauto 10 with typeable).
    asimpl. eauto with typeable.
Amin Timany's avatar
Amin Timany committed
180 181
  Qed.

182
  Hint Resolve FG_iter_type : typeable.
Amin Timany's avatar
Amin Timany committed
183 184 185

  Global Opaque FG_iter.

186 187 188
  Lemma FG_read_iter_type Γ τ :
    typed Γ FG_read_iter
          (TArrow (Tref (FG_StackType τ)) (TArrow (TArrow τ TUnit) TUnit)).
Amin Timany's avatar
Amin Timany committed
189
  Proof.
190 191
    unfold FG_read_iter. unlock.
    eauto 20 with typeable.
Amin Timany's avatar
Amin Timany committed
192 193
  Qed.

194
  Hint Resolve FG_read_iter_type : typeable.
Amin Timany's avatar
Amin Timany committed
195 196 197 198 199 200 201 202 203

  Global Opaque FG_iter.

  Section FG_stack_body_type.
    (* The following assumption is simply ** WRONG ** *)
    (* We assume it though to just be able to prove that the
       stack we are implementing is /type-sane/ so to speak! *)
    Context (HEQTP :  τ, EqType (FG_StackType τ)).

204 205
    Lemma FG_stack_body_type Γ τ :
      typed Γ FG_stack_body (TArrow (Tref (FG_StackType τ))
Amin Timany's avatar
Amin Timany committed
206 207
            (TProd
               (TProd (TArrow τ TUnit) (TArrow TUnit (TSum TUnit τ)))
208
               (TArrow (TArrow τ TUnit) TUnit))).
Amin Timany's avatar
Amin Timany committed
209
    Proof.
210 211
      unfold FG_stack_body. unlock.
      eauto 20 with typeable.
Amin Timany's avatar
Amin Timany committed
212 213 214
    Qed.
  End FG_stack_body_type.

215
  Hint Resolve FG_stack_body_type : typeable.
Amin Timany's avatar
Amin Timany committed
216 217 218 219 220 221 222 223 224
  Opaque FG_read_iter.

  Section FG_stack_type.
    (* The following assumption is simply ** WRONG ** *)
    (* We assume it though to just be able to prove that the
       stack we are implementing is /type-sane/ so to speak! *)
    Context (HEQTP :  τ, EqType (FG_StackType τ)).

    Lemma FG_stack_type Γ :
225
      typed Γ FG_stack
Amin Timany's avatar
Amin Timany committed
226 227 228 229 230 231 232 233 234
            (TForall
               (TProd
                  (TProd
                     (TArrow (TVar 0) TUnit)
                     (TArrow TUnit (TSum TUnit (TVar 0)))
                  )
                  (TArrow (TArrow (TVar 0) TUnit) TUnit)
            )).
    Proof.
235 236
      unfold FG_stack. unlock.
      eauto 20 with typeable.
Amin Timany's avatar
Amin Timany committed
237 238 239
    Qed.
  End FG_stack_type.

240 241
  Hint Resolve FG_stack_type : typeable.

Robbert Krebbers's avatar
Robbert Krebbers committed
242
End FG_stack.