Commit e230c27b authored by Simon Friis Vindum's avatar Simon Friis Vindum

Add Java stdlib inspired tail shortcut

parent 8ca249fb
......@@ -75,40 +75,47 @@ Definition MS_dequeue :=
*)
Definition MS_enqueue :=
(Lam (* x. *)
(LetIn
(* n = *) (Alloc (Fold (some (Pair (some (Var 0 (* x *))) (Alloc (Alloc (Fold none)))))))
(Lam (* x *)
(LetIn
(* n = *) (Alloc (Fold (some (Pair (some (Var 0 (* x *))) (Alloc (Alloc (Fold none)))))))
(LetIn
(* tt = *) (Load (Var 3 (* tail *)))
(App
(Rec (* try(c) *)
(LetIn
(* t = *) (Load (Var 1 (* c *)))
(Case
(Unfold (Load (Var 0 (* t *))))
(* c = InjL ... Tail is nil, we can try to insert now *)
(If
(CAS (Var 3 (* c *)) (Var 1 (* t *)) (Var 4 (* n *)))
(* Insertion succeeded, we are done *)
Unit
(* Insertion failed, we try again*)
(App (Var 2 (* try *)) (Var 3 (* c *)))
)
(* c = InjR c' =>. We are not at the end yet, recurse on the tail *)
(App (Var 2 (* try *)) (Snd ((Var 0 (* c' *)))))
)
(Rec (* try(c) *)
(LetIn
(* t = *) (Load (Var 1 (* c *)))
(Case
(Unfold (Load (Var 0 (* t *))))
(* c = InjL ... Tail is nil, we can try to insert now *)
(If
(CAS (Var 3 (* c *)) (Var 1 (* t *)) (Var 5 (* n *)))
(* Insertion succeeded, update tail *)
(Seq
(CAS (Var 8 (* tail *)) (Var 4 (* tt *)) (Var 5 (* n *)))
Unit)
(* Insertion failed, we try again*)
(App (Var 2 (* try *)) (Var 3 (* c *)))
)
(* c = InjR c' =>. We are not at the end yet, recurse on the tail *)
(App (Var 2 (* try *)) (Snd ((Var 0 (* c' *)))))
)
)
(* (Unfold (Load (Load (Var 2 (* head *))))) *)
(Snd (getValue (Unfold (Load (Load (Var 2 (* head *)))))))
)
)
(Snd (getValue (Unfold (Load (Var 0 (* tt *))))))
)
)
)
)
).
Definition MS_queue : expr :=
TLam (* _ *)
(LetIn
(* head = *) (Alloc (Alloc (Fold (some (Pair (none) (Alloc (Alloc (Fold none))))))))
(Pair MS_dequeue MS_enqueue)
).
(LetIn (* node = *) (Alloc (Fold (some (Pair (none) (Alloc (Alloc (Fold none)))))))
(LetIn
(* tail = *) (Alloc (Var 0 (* node *)))
(LetIn
(* head = *) (Alloc (Var 1 (* node *)))
(Pair MS_dequeue MS_enqueue)
))).
Section MS_queue.
Context `{heapIG Σ, cfgSG Σ}.
......@@ -122,7 +129,7 @@ Section MS_queue.
Qed.
Lemma MS_enqueue_type Γ τ :
typed (MS_QueueType τ :: Γ) MS_enqueue (TArrow τ TUnit).
typed (MS_QueueType τ :: MS_QueueType τ :: Γ) MS_enqueue (TArrow τ TUnit).
Proof.
econstructor.
econstructor.
......@@ -130,6 +137,8 @@ Section MS_queue.
apply (TFold _ _ (TNodeBody τ (TVar 0))).
repeat econstructor. asimpl. done.
- econstructor.
{ repeat econstructor. }
econstructor.
2: {
econstructor.
apply getValue_type.
......@@ -142,7 +151,19 @@ Section MS_queue.
+ econstructor.
* apply (TUnfold _ _ (TNodeBody τ (TVar 0))).
repeat constructor.
* repeat econstructor; reflexivity.
* econstructor; simpl.
-- econstructor.
2: { constructor. reflexivity. }
repeat econstructor.
repeat econstructor.
repeat econstructor.
-- econstructor. econstructor.
2: { constructor. reflexivity. }
repeat econstructor.
repeat econstructor. simpl.
repeat econstructor.
repeat econstructor.
-- repeat econstructor.
* repeat econstructor.
Qed.
......@@ -182,12 +203,15 @@ Section MS_queue.
econstructor.
econstructor.
- econstructor.
econstructor.
apply (TFold _ _ (TNodeBody (TVar 0) (TVar 0))).
repeat econstructor.
- econstructor.
+ apply MS_dequeue_type.
+ apply MS_enqueue_type.
+ repeat econstructor.
+ econstructor.
* repeat econstructor.
* econstructor.
-- apply MS_dequeue_type.
-- apply MS_enqueue_type.
Qed.
End MS_queue.
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment