From iris_logrel Require Export logrel. (* stack τ = μ x. ref (Unit + τ * x) *) Definition FG_StackType τ := TRec (Tref (TSum TUnit (TProd τ.[ren (+1)] (TVar 0)))). Notation Conse h t := (Fold (Alloc (InjR (Pair h t)))). Notation Nile := (Fold (Alloc (InjL #()))). Definition FG_push : val := rec: "push" "st" := λ: "x", let: "stv" := !"st" in if: (CAS "st" "stv" (Conse "x" "stv")) then #() else "push" "st" "x". (* 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)*) Definition FG_pop : val := rec: "pop" "st" := λ: <>, let: "stv" := !"st" in let: "x" := !(Unfold "stv") in 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" #() end. (* iter f = λ st. case (load st) of | nil => #() | cons y ys => f y ;; iter f ys *) Definition FG_iter : val := rec: "iter" "f" := λ: "st", match: !(Unfold "st") with InjL <> => #() | InjR "x" => 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"). (* stack = Λα. (λ (s : stack α). stack_body s) (ref (ref nil)) *) Definition FG_stack : val := Λ: let: "st" := ref Nile in FG_stack_body "st". 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. 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! *) (* EqType (stack τ) would mean that we can compare two stacks for equality, we need this for compare-and-swap *) Context (HEQTP : ∀ τ, EqType (FG_StackType τ)). Lemma FG_push_type Γ τ : typed Γ FG_push (TArrow (Tref (FG_StackType τ)) (TArrow τ TUnit)). Proof. unfold FG_push. unlock. repeat (econstructor; eauto with typeable). asimpl. eauto with typeable. Qed. End FG_push_type. Hint Resolve FG_push_type : typeable. Global Opaque FG_push. (* Fine-grained pop *) 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 τ)). Lemma FG_pop_type Γ τ : typed Γ FG_pop (TArrow (Tref (FG_StackType τ)) (TArrow TUnit (TSum TUnit τ))). Proof. unfold FG_pop. unlock. repeat (econstructor; eauto 10 with typeable). cbn. asimpl. eauto 20 with typeable. Qed. End FG_pop_type. Hint Resolve FG_pop_type : typeable. Global Opaque FG_pop. (* Fine-grained iter *) Lemma FG_iter_type Γ τ : typed Γ FG_iter (TArrow (TArrow τ TUnit) (TArrow (FG_StackType τ) TUnit)). Proof. unfold FG_iter. unlock. repeat (econstructor; eauto 10 with typeable). asimpl. eauto with typeable. Qed. Hint Resolve FG_iter_type : typeable. Global Opaque FG_iter. Lemma FG_read_iter_type Γ τ : typed Γ FG_read_iter (TArrow (Tref (FG_StackType τ)) (TArrow (TArrow τ TUnit) TUnit)). Proof. unfold FG_read_iter. unlock. eauto 20 with typeable. Qed. Hint Resolve FG_read_iter_type : typeable. 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 τ)). Lemma FG_stack_body_type Γ τ : typed Γ FG_stack_body (TArrow (Tref (FG_StackType τ)) (TProd (TProd (TArrow τ TUnit) (TArrow TUnit (TSum TUnit τ))) (TArrow (TArrow τ TUnit) TUnit))). Proof. unfold FG_stack_body. unlock. eauto 20 with typeable. Qed. End FG_stack_body_type. Hint Resolve FG_stack_body_type : typeable. 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 Γ : typed Γ FG_stack (TForall (TProd (TProd (TArrow (TVar 0) TUnit) (TArrow TUnit (TSum TUnit (TVar 0))) ) (TArrow (TArrow (TVar 0) TUnit) TUnit) )). Proof. unfold FG_stack. unlock. eauto 20 with typeable. Qed. End FG_stack_type. Hint Resolve FG_stack_type : typeable. End FG_stack.