diff --git a/theories/logrel_heaplang/lib/symbol_adt.v b/theories/logrel_heaplang/lib/symbol_adt.v index 65b234f7b59bbb3c619cd57331acf368ddc64640..1acc8070b1f6b66c14df63deb84a4f4f9f4942c0 100644 --- a/theories/logrel_heaplang/lib/symbol_adt.v +++ b/theories/logrel_heaplang/lib/symbol_adt.v @@ -9,7 +9,7 @@ Definition symbol_adt_inc : val := λ: "x" <>, FAA "x" #1. Definition symbol_adt_check : val := λ: "x" "y", assert: "y" < !"x". Definition symbol_adt : val := λ: <>, let: "x" := Alloc #0 in (symbol_adt_inc "x", symbol_adt_check "x"). -Definition symbol_adt_ty `{heapG Σ} : lty := +Definition symbol_adt_ty `{heapG Σ} : lty Σ := (() → ∃ A, (() → A) * (A → ()))%lty. (* The required ghost theory *) @@ -68,7 +68,7 @@ Section ltyped_symbol_adt. Definition symbol_ctx (γ : gname) (l : loc) : iProp Σ := inv symbol_adtN (symbol_inv γ l). - Definition lty_symbol (γ : gname) : lty := Lty (λ w, + Definition lty_symbol (γ : gname) : lty Σ := Lty (λ w, ∃ n : nat, ⌜w = #n⌝ ∧ symbol γ n)%I. Lemma ltyped_symbol_adt Γ : Γ ⊨ symbol_adt : symbol_adt_ty. diff --git a/theories/logrel_heaplang/ltyping.v b/theories/logrel_heaplang/ltyping.v index 0d96b5025ec2ad7fc8800b9d8496040c2f34a832..d79ad16acb62b560580b235dd766678c2042d359 100644 --- a/theories/logrel_heaplang/ltyping.v +++ b/theories/logrel_heaplang/ltyping.v @@ -3,35 +3,35 @@ From iris.base_logic.lib Require Import invariants. From iris.heap_lang Require Import notation proofmode. (* The domain of semantic types: persistent Iris predicates over values *) -Record lty `{heapG Σ} := Lty { +Record lty Σ := Lty { lty_car :> val → iProp Σ; lty_persistent v : Persistent (lty_car v) }. -Arguments Lty {_ _} _%I {_}. -Arguments lty_car {_ _} _ _ : simpl never. +Arguments Lty {_} _%I {_}. +Arguments lty_car {_} _ _ : simpl never. Bind Scope lty_scope with lty. Delimit Scope lty_scope with lty. Existing Instance lty_persistent. (* The COFE structure on semantic types *) Section lty_ofe. - Context `{heapG Σ}. + Context `{Σ : gFunctors}. - Instance lty_equiv : Equiv lty := λ A B, ∀ w, A w ≡ B w. - Instance lty_dist : Dist lty := λ n A B, ∀ w, A w ≡{n}≡ B w. - Lemma lty_ofe_mixin : OfeMixin lty. + Instance lty_equiv : Equiv (lty Σ) := λ A B, ∀ w, A w ≡ B w. + Instance lty_dist : Dist (lty Σ) := λ n A B, ∀ w, A w ≡{n}≡ B w. + Lemma lty_ofe_mixin : OfeMixin (lty Σ). Proof. by apply (iso_ofe_mixin (lty_car : _ → val -c> _)). Qed. - Canonical Structure ltyC := OfeT lty lty_ofe_mixin. + Canonical Structure ltyC := OfeT (lty Σ) lty_ofe_mixin. Global Instance lty_cofe : Cofe ltyC. Proof. apply (iso_cofe_subtype' (λ A : val -c> iProp Σ, ∀ w, Persistent (A w)) - (@Lty _ _) lty_car)=> //. + (@Lty _) lty_car)=> //. - apply _. - apply limit_preserving_forall=> w. by apply bi.limit_preserving_Persistent=> n ??. Qed. - Global Instance lty_inhabited : Inhabited lty := populate (Lty inhabitant). + Global Instance lty_inhabited : Inhabited (lty Σ) := populate (Lty inhabitant). Global Instance lty_car_ne n : Proper (dist n ==> (=) ==> dist n) lty_car. Proof. by intros A A' ? w ? <-. Qed. @@ -39,46 +39,48 @@ Section lty_ofe. Proof. by intros A A' ? w ? <-. Qed. End lty_ofe. +Arguments ltyC : clear implicits. + (* Typing for operators *) -Class LTyUnboxed `{heapG Σ} (A : lty) := +Class LTyUnboxed `{heapG Σ} (A : lty Σ) := lty_unboxed v : A v -∗ ⌜ val_is_unboxed v ⌝. -Class LTyUnOp `{heapG Σ} (op : un_op) (A B : lty) := +Class LTyUnOp `{heapG Σ} (op : un_op) (A B : lty Σ) := lty_un_op v : A v -∗ ∃ w, ⌜ un_op_eval op v = Some w ⌝ ∧ B w. -Class LTyBinOp `{heapG Σ} (op : bin_op) (A1 A2 B : lty) := +Class LTyBinOp `{heapG Σ} (op : bin_op) (A1 A2 B : lty Σ) := lty_bin_op v1 v2 : A1 v1 -∗ A2 v2 -∗ ∃ w, ⌜ bin_op_eval op v1 v2 = Some w ⌝ ∧ B w. (* The type formers *) Section types. Context `{heapG Σ}. - Definition lty_unit : lty := Lty (λ w, ⌜ w = #() ⌝%I). - Definition lty_bool : lty := Lty (λ w, ∃ b : bool, ⌜ w = #b ⌝)%I. - Definition lty_int : lty := Lty (λ w, ∃ n : Z, ⌜ w = #n ⌝)%I. + Definition lty_unit : lty Σ := Lty (λ w, ⌜ w = #() ⌝%I). + Definition lty_bool : lty Σ := Lty (λ w, ∃ b : bool, ⌜ w = #b ⌝)%I. + Definition lty_int : lty Σ := Lty (λ w, ∃ n : Z, ⌜ w = #n ⌝)%I. - Definition lty_arr (A1 A2 : lty) : lty := Lty (λ w, + Definition lty_arr (A1 A2 : lty Σ) : lty Σ := Lty (λ w, □ ∀ v, A1 v -∗ WP App w v {{ A2 }})%I. - Definition lty_prod (A1 A2 : lty) : lty := Lty (λ w, + Definition lty_prod (A1 A2 : lty Σ) : lty Σ := Lty (λ w, ∃ w1 w2, ⌜w = PairV w1 w2⌝ ∧ A1 w1 ∧ A2 w2)%I. - Definition lty_sum (A1 A2 : lty) : lty := Lty (λ w, + Definition lty_sum (A1 A2 : lty Σ) : lty Σ := Lty (λ w, (∃ w1, ⌜w = InjLV w1⌝ ∧ A1 w1) ∨ (∃ w2, ⌜w = InjRV w2⌝ ∧ A2 w2))%I. - Definition lty_forall (C : lty → lty) : lty := Lty (λ w, - □ ∀ A : lty, WP w #() {{ w, C A w }})%I. - Definition lty_exist (C : lty → lty) : lty := Lty (λ w, - ∃ A : lty, C A w)%I. + Definition lty_forall (C : lty Σ → lty Σ) : lty Σ := Lty (λ w, + □ ∀ A : lty Σ, WP w #() {{ w, C A w }})%I. + Definition lty_exist (C : lty Σ → lty Σ) : lty Σ := Lty (λ w, + ∃ A : lty Σ, C A w)%I. - Definition lty_rec1 (C : ltyC -n> ltyC) (rec : lty) : lty := Lty (λ w, + Definition lty_rec1 (C : ltyC Σ -n> ltyC Σ) (rec : lty Σ) : lty Σ := Lty (λ w, ▷ C rec w)%I. Instance lty_rec1_contractive C : Contractive (lty_rec1 C). Proof. solve_contractive. Qed. - Definition lty_rec (C : ltyC -n> ltyC) : lty := fixpoint (lty_rec1 C). + Definition lty_rec (C : ltyC Σ -n> ltyC Σ) : lty Σ := fixpoint (lty_rec1 C). Definition tyN := nroot .@ "ty". - Definition lty_ref (A : lty) : lty := Lty (λ w, + Definition lty_ref (A : lty Σ) : lty Σ := Lty (λ w, ∃ l : loc, ⌜w = #l⌝ ∧ inv (tyN .@ l) (∃ v, l ↦ v ∗ A v))%I. End types. @@ -94,12 +96,12 @@ Notation "∃ A1 .. An , C" := Notation "'ref' A" := (lty_ref A) : lty_scope. (* The semantic typing judgment *) -Definition env_ltyped `{heapG Σ} (Γ : gmap string lty) +Definition env_ltyped `{heapG Σ} (Γ : gmap string (lty Σ)) (vs : gmap string val) : iProp Σ := (⌜ ∀ x, is_Some (Γ !! x) ↔ is_Some (vs !! x) ⌝ ∧ [∗ map] i ↦ Av ∈ map_zip Γ vs, lty_car Av.1 Av.2)%I. Definition ltyped `{heapG Σ} - (Γ : gmap string lty) (e : expr) (A : lty) : iProp Σ := + (Γ : gmap string (lty Σ)) (e : expr) (A : lty Σ) : iProp Σ := (□ ∀ vs, env_ltyped Γ vs -∗ WP subst_map vs e {{ A }})%I. Notation "Γ ⊨ e : A" := (ltyped Γ e A) (at level 100, e at next level, A at level 200). @@ -110,26 +112,26 @@ Definition rec_unfold : val := λ: "x", "x". Section types_properties. Context `{heapG Σ}. - Implicit Types A B : lty. - Implicit Types C : lty → lty. + Implicit Types A B : lty Σ. + Implicit Types C : lty Σ → lty Σ. (* Boring stuff: all type formers are non-expansive *) - Global Instance lty_prod_ne : NonExpansive2 lty_prod. + Global Instance lty_prod_ne : NonExpansive2 (@lty_prod Σ). Proof. solve_proper. Qed. - Global Instance lty_sum_ne : NonExpansive2 lty_sum. + Global Instance lty_sum_ne : NonExpansive2 (@lty_sum Σ). Proof. solve_proper. Qed. - Global Instance lty_arr_ne : NonExpansive2 lty_arr. + Global Instance lty_arr_ne : NonExpansive2 (@lty_arr Σ _). Proof. solve_proper. Qed. - Global Instance lty_forall_ne n : Proper (pointwise_relation _ (dist n) ==> dist n) lty_forall. + Global Instance lty_forall_ne n : Proper (pointwise_relation _ (dist n) ==> dist n) (@lty_forall Σ _). Proof. solve_proper. Qed. - Global Instance lty_exist_ne n : Proper (pointwise_relation _ (dist n) ==> dist n) lty_exist. + Global Instance lty_exist_ne n : Proper (pointwise_relation _ (dist n) ==> dist n) (@lty_exist Σ). Proof. solve_proper. Qed. - Global Instance lty_rec_ne n : Proper (dist n ==> dist n) lty_rec. + Global Instance lty_rec_ne n : Proper (dist n ==> dist n) (@lty_rec Σ). Proof. intros C C' HC. apply fixpoint_ne. solve_proper. Qed. - Global Instance lty_ref_ne : NonExpansive2 lty_ref. + Global Instance lty_ref_ne : NonExpansive2 (@lty_ref Σ _). Proof. solve_proper. Qed. - Lemma lty_rec_unfold (C : ltyC -n> ltyC) : lty_rec C ≡ lty_rec1 C (lty_rec C). + Lemma lty_rec_unfold (C : ltyC Σ -n> ltyC Σ) : lty_rec C ≡ lty_rec1 C (lty_rec C). Proof. apply fixpoint_unfold. Qed. (* Environments *) @@ -229,14 +231,14 @@ Section types_properties. wp_apply (wp_wand with "(H1 [//])"); iIntros (v) "#HA". by iApply "HA". Qed. - Lemma ltyped_fold Γ e (B : ltyC -n> ltyC) : + Lemma ltyped_fold Γ e (B : ltyC Σ -n> ltyC Σ) : (Γ ⊨ e : B (lty_rec B)) -∗ Γ ⊨ e : lty_rec B. Proof. iIntros "#H" (vs) "!# #HΓ /=". wp_apply (wp_wand with "(H [//])"); iIntros (w) "#HB". by iEval (rewrite lty_rec_unfold /lty_car /=). Qed. - Lemma ltyped_unfold Γ e (B : ltyC -n> ltyC) : + Lemma ltyped_unfold Γ e (B : ltyC Σ -n> ltyC Σ) : (Γ ⊨ e : lty_rec B) -∗ Γ ⊨ rec_unfold e : B (lty_rec B). Proof. iIntros "#H" (vs) "!# #HΓ /=".