diff --git a/examples/proofs/btree/btree_learn.v b/examples/proofs/btree/btree_learn.v
index 851f53cbe450d3b64d6801dc7c483a007bbf3256..a11935f9a108ebc0430d66e9ad827df250fbedd1 100644
--- a/examples/proofs/btree/btree_learn.v
+++ b/examples/proofs/btree/btree_learn.v
@@ -11,7 +11,7 @@ Section learnable.
}.
Next Obligation.
iIntros (r l β) "Hl". rewrite btree_t_unfold /ty_own /=.
- iDestruct "Hl" as ([[[n ks] vs] cs]) "Hl". rewrite tyexists_eq /=.
+ iDestruct "Hl" as ([[[n ks] vs] cs]) "Hl". rewrite tyexists_eq /persistent_own_constraint /=.
rewrite /ty_own /=. iDestruct "Hl" as "[_ %]". iPureIntro. naive_solver.
Qed.
End learnable.
diff --git a/theories/lithium/classes.v b/theories/lithium/classes.v
index 9f5f95a8ae99f2701bd60db6cce29f0b63277d3c..dfd8fc95a2bf0de9e2f32c1d0b5499556b373445 100644
--- a/theories/lithium/classes.v
+++ b/theories/lithium/classes.v
@@ -100,6 +100,28 @@ Global Instance simplify_goal_id_inst {Σ} (P : iProp Σ):
SimplifyGoal P None | 100 :=
λ T, i2p (simplify_goal_id P T).
+(* TODO: Is the following useful? *)
+(* Lemma simplify_persistent_pure_goal {Σ} (Φ : Prop) T: *)
+(* T ⌜Φ⌠-∗ simplify_goal (Σ := Σ) (â–¡ ⌜ΦâŒ) T. *)
+(* Proof. iIntros "HT". iExists _. iFrame. by iIntros (?). Qed. *)
+(* Global Instance simplify_persistent_pure_goal_id {Σ} (Φ : Prop): *)
+(* SimplifyGoal (Σ:=Σ) (â–¡ ⌜ΦâŒ) (Some 0%N) := *)
+(* λ T, i2p (simplify_persistent_pure_goal Φ T). *)
+
+(* Lemma simplify_persistent_pure_hyp {Σ} (Φ : Prop) T: *)
+(* (⌜Φ⌠-∗ T) -∗ simplify_hyp (Σ := Σ) (â–¡ ⌜ΦâŒ) T. *)
+(* Proof. iIntros "HT" (?). by iApply "HT". Qed. *)
+(* Global Instance simplify_persistent_pure_hyp_inst {Σ} (Φ : Prop): *)
+(* SimplifyHyp (Σ:=Σ) (â–¡ ⌜ΦâŒ) (Some 0%N) := *)
+(* λ T, i2p (simplify_persistent_pure_hyp Φ T). *)
+
+(* Lemma simplify_persistent_sep_hyp {Σ} (P Q : iProp Σ) T: *)
+(* (□ P -∗ □ Q -∗ T) -∗ simplify_hyp (Σ := Σ) (□ (P ∗ Q)) T. *)
+(* Proof. iIntros "HT [HP HQ]". iApply ("HT" with "HP HQ"). Qed. *)
+(* Global Instance simplify_persistent_sep_hyp_inst {Σ} (P Q : iProp Σ): *)
+(* SimplifyHyp (Σ:=Σ) (□ (P ∗ Q)) (Some 0%N) := *)
+(* λ T, i2p (simplify_persistent_sep_hyp P Q T). *)
+
(** * Subsumption *)
(** ** Definition *)
Definition subsume {Σ} (P1 P2 T : iProp Σ) : iProp Σ :=
diff --git a/theories/typing/constrained.v b/theories/typing/constrained.v
index 5bc1b9bf675d04a6842ea350e495439530abb788..d0c34ac1f3f572b06cce7de9dc243fe19a3a1b8e 100644
--- a/theories/typing/constrained.v
+++ b/theories/typing/constrained.v
@@ -2,78 +2,6 @@ From refinedc.typing Require Export type.
From refinedc.typing Require Import programs optional.
Set Default Proof Using "Type".
-Section constrained.
- Context `{!typeG Σ}.
-
- Program Definition constrained (ty : type) (P : iProp Σ) : type := {|
- ty_own β l := (l â—â‚—{β} ty ∗ â–¡ P)%I
- |}.
- Next Obligation. move => ty P ? l ?. iIntros "[H $]". by iApply ty_share. Qed.
-
- Global Instance constrained_rty_ne n : Proper ((dist n) ==> (dist n) ==> (dist n)) constrained.
- Proof. solve_type_proper. Qed.
- Global Instance constrained_rty_proper : Proper ((≡) ==> (≡) ==> (≡)) constrained.
- Proof. solve_type_proper. Qed.
-
- Global Program Instance constrained_movable ty P `{!Movable ty} : Movable (constrained ty P) := {|
- ty_layout := ty.(ty_layout);
- ty_own_val v := (v â—áµ¥ ty ∗ â–¡ P)%I;
- |}.
- Next Obligation. iIntros (????) "[? _]". by iApply ty_aligned. Qed.
- Next Obligation. iIntros (????) "[? _]". by iApply ty_size_eq. Qed.
- Next Obligation. iIntros (????) "[? $]". by iApply ty_deref. Qed.
- Next Obligation. iIntros (??????) "Hl [? $]". by iApply (ty_ref with "[//] [Hl]"). Qed.
-
- Global Instance constrained_loc_in_bounds ty β P `{!LocInBounds ty β} :
- LocInBounds (constrained ty P) β.
- Proof.
- constructor. iIntros (l) "[Hl _]". by iApply loc_in_bounds_in_bounds.
- Qed.
-
- Lemma simplify_hyp_place_constrained P l β ty T `{!Persistent P}:
- (P -∗ l â—â‚—{β} ty -∗ T) -∗ simplify_hyp (lâ—â‚—{β} constrained ty P) T.
- Proof. iIntros "HT [Hl #?]". by iApply "HT". Qed.
- Global Instance simplify_hyp_place_constrained_inst P l β ty `{!Persistent P}:
- SimplifyHypPlace l β (constrained ty P)%I (Some 0%N) :=
- λ T, i2p (simplify_hyp_place_constrained P l β ty T).
-
- Lemma simplify_goal_place_constrained P l β ty T `{!Persistent P}:
- T (l â—â‚—{β} ty ∗ P) -∗ simplify_goal (lâ—â‚—{β} constrained ty P) T.
- Proof. iIntros "HT". iExists _. iFrame. iIntros "[$ #?]". by iModIntro. Qed.
- Global Instance simplify_goal_place_constrained_inst P l β ty `{!Persistent P}:
- SimplifyGoalPlace l β (constrained ty P)%I (Some 0%N) :=
- λ T, i2p (simplify_goal_place_constrained P l β ty T).
-
- Lemma simplify_hyp_val_constrained P v ty T `{!Movable ty}:
- (P -∗ v â—áµ¥ ty -∗ T) -∗ simplify_hyp (vâ—áµ¥ constrained ty P) T.
- Proof. iIntros "HT [Hl #?]". by iApply "HT". Qed.
- Global Instance simplify_hyp_val_constrained_inst P v ty `{!Movable ty}:
- SimplifyHypVal v (constrained ty P)%I (Some 0%N) :=
- λ T, i2p (simplify_hyp_val_constrained P v ty T).
-
- Lemma simplify_goal_val_constrained P v ty T `{!Movable ty} `{!Persistent P}:
- T (v â—áµ¥ ty ∗ P) -∗ simplify_goal (vâ—áµ¥ constrained ty P) T.
- Proof. iIntros "HT". iExists _. iFrame. iIntros "[$ #?]". by iModIntro. Qed.
- Global Instance simplify_goal_val_constrained_inst P v ty `{!Movable ty} `{!Persistent P}:
- SimplifyGoalVal v (constrained ty P)%I (Some 0%N) :=
- λ T, i2p (simplify_goal_val_constrained P v ty T).
-
- Global Program Instance constrained_optional ty P optty ot1 ot2 `{!Movable ty} `{!Movable optty} `{!Optionable ty optty ot1 ot2} : Optionable (constrained ty P) optty ot1 ot2 := {|
- opt_pre v1 v2 := opt_pre ty v1 v2
- |}.
- Next Obligation. move => ???????? /=. apply opt_alt_sz. Qed.
- Next Obligation.
- iIntros (????????[]?????) "Hpre H1 H2". 1: iDestruct "H1" as "[H1 _]".
- by iApply (opt_bin_op true with "Hpre H1 H2").
- by iApply (opt_bin_op false with "Hpre H1 H2").
- Qed.
-
- Global Instance optionable_agree_constrained P (ty2 : type) `{!OptionableAgree ty1 ty2} : OptionableAgree (constrained ty1 P) ty2.
- Proof. done. Qed.
-End constrained.
-Typeclasses Opaque constrained.
-
-
Class OwnConstraint `{!typeG Σ} (P : own_state → iProp Σ) : Prop := {
own_constraint_persistent : Persistent (P Shr);
own_constraint_share E : ↑shrN ⊆ E → P Own ={E}=∗ P Shr;
@@ -83,7 +11,7 @@ Global Existing Instance own_constraint_persistent.
Section own_constrained.
Context `{!typeG Σ}.
- Program Definition own_constrained (ty : type) (P : own_state → iProp Σ) `{!OwnConstraint P} : type := {|
+ Program Definition own_constrained (P : own_state → iProp Σ) `{!OwnConstraint P} (ty : type) : type := {|
ty_own β l := (l â—â‚—{β} ty ∗ P β)%I
|}.
Next Obligation.
@@ -92,7 +20,12 @@ Section own_constrained.
by iApply own_constraint_share.
Qed.
- Global Program Instance own_constrained_movable ty P `{!Movable ty} `{!OwnConstraint P} : Movable (own_constrained ty P) := {|
+ Global Instance own_constrained_rty_ne n P `{!OwnConstraint P} : Proper ((dist n) ==> (dist n)) (own_constrained P).
+ Proof. solve_type_proper. Qed.
+ Global Instance own_constrained_rty_proper P `{!OwnConstraint P} : Proper ((≡) ==> (≡)) (own_constrained P).
+ Proof. solve_type_proper. Qed.
+
+ Global Program Instance own_constrained_movable ty P `{!Movable ty} `{!OwnConstraint P} : Movable (own_constrained P ty) := {|
ty_layout := ty.(ty_layout);
ty_own_val v := (v â—áµ¥ ty ∗ P Own)%I;
|}.
@@ -101,34 +34,53 @@ Section own_constrained.
Next Obligation. iIntros (?????) "[? $]". by iApply ty_deref. Qed.
Next Obligation. iIntros (???????) "Hl [? $]". by iApply (ty_ref with "[//] [Hl]"). Qed.
+ Global Instance own_constrained_loc_in_bounds ty β P `{!OwnConstraint P} `{!LocInBounds ty β} :
+ LocInBounds (own_constrained P ty) β.
+ Proof.
+ constructor. iIntros (l) "[Hl _]". by iApply loc_in_bounds_in_bounds.
+ Qed.
+
Lemma simplify_hyp_place_own_constrained P l β ty T `{!OwnConstraint P}:
- (P β -∗ l â—â‚—{β} ty -∗ T) -∗ simplify_hyp (lâ—â‚—{β} own_constrained ty P) T.
+ (P β -∗ l â—â‚—{β} ty -∗ T) -∗ simplify_hyp (lâ—â‚—{β} own_constrained P ty) T.
Proof. iIntros "HT [Hl HP]". by iApply ("HT" with "HP"). Qed.
Global Instance simplify_hyp_place_own_constrained_inst P l β ty `{!OwnConstraint P}:
- SimplifyHypPlace l β (own_constrained ty P)%I (Some 0%N) :=
+ SimplifyHypPlace l β (own_constrained P ty)%I (Some 0%N) :=
λ T, i2p (simplify_hyp_place_own_constrained P l β ty T).
Lemma simplify_goal_place_own_constrained P l β ty T `{!OwnConstraint P}:
- T (l â—â‚—{β} ty ∗ P β) -∗ simplify_goal (lâ—â‚—{β} own_constrained ty P) T.
+ T (l â—â‚—{β} ty ∗ P β) -∗ simplify_goal (lâ—â‚—{β} own_constrained P ty) T.
Proof. iIntros "HT". iExists _. iFrame. iIntros "[$ $]". Qed.
Global Instance simplify_goal_place_own_constrained_inst P l β ty `{!OwnConstraint P}:
- SimplifyGoalPlace l β (own_constrained ty P)%I (Some 0%N) :=
+ SimplifyGoalPlace l β (own_constrained P ty)%I (Some 0%N) :=
λ T, i2p (simplify_goal_place_own_constrained P l β ty T).
Lemma simplify_hyp_val_own_constrained P v ty T `{!Movable ty} `{!OwnConstraint P}:
- (P Own -∗ v â—áµ¥ ty -∗ T) -∗ simplify_hyp (v â—áµ¥ own_constrained ty P) T.
+ (P Own -∗ v â—áµ¥ ty -∗ T) -∗ simplify_hyp (v â—áµ¥ own_constrained P ty) T.
Proof. iIntros "HT [Hl HP]". by iApply ("HT" with "HP"). Qed.
Global Instance simplify_hyp_val_own_constrained_inst P v ty `{!Movable ty} `{!OwnConstraint P}:
- SimplifyHypVal v (own_constrained ty P)%I (Some 0%N) :=
+ SimplifyHypVal v (own_constrained P ty)%I (Some 0%N) :=
λ T, i2p (simplify_hyp_val_own_constrained P v ty T).
Lemma simplify_goal_val_own_constrained P v ty T `{!Movable ty} `{!OwnConstraint P}:
- T (v â—áµ¥ ty ∗ P Own) -∗ simplify_goal (v â—áµ¥ own_constrained ty P) T.
+ T (v â—áµ¥ ty ∗ P Own) -∗ simplify_goal (v â—áµ¥ own_constrained P ty) T.
Proof. iIntros "HT". iExists _. iFrame. iIntros "[$ $]". Qed.
Global Instance simplify_goal_val_own_constrained_inst P v ty `{!Movable ty} `{!OwnConstraint P}:
- SimplifyGoalVal v (own_constrained ty P)%I (Some 0%N) :=
+ SimplifyGoalVal v (own_constrained P ty)%I (Some 0%N) :=
λ T, i2p (simplify_goal_val_own_constrained P v ty T).
+ Global Program Instance own_constrained_optional ty P optty ot1 ot2 `{!Movable ty} `{!Movable optty} `{!OwnConstraint P} `{!Optionable ty optty ot1 ot2} : Optionable (own_constrained P ty) optty ot1 ot2 := {|
+ opt_pre v1 v2 := opt_pre ty v1 v2
+ |}.
+ Next Obligation. move => ????????? /=. apply opt_alt_sz. Qed.
+ Next Obligation.
+ iIntros (?????????[]?????) "Hpre H1 H2". 1: iDestruct "H1" as "[H1 _]".
+ by iApply (opt_bin_op true with "Hpre H1 H2").
+ by iApply (opt_bin_op false with "Hpre H1 H2").
+ Qed.
+
+ Global Instance optionable_agree_own_constrained P (ty2 : type) `{!OwnConstraint P} `{!OptionableAgree ty1 ty2} : OptionableAgree (own_constrained P ty1) ty2.
+ Proof. done. Qed.
+
Definition tyown_constraint (l : loc) (ty : type) (β : own_state) : iProp Σ := l â—â‚—{β} ty.
@@ -149,5 +101,62 @@ Section own_constrained.
SimplifyGoal (tyown_constraint l ty β) (Some 0%N) :=
λ T, i2p (simplify_goal_place_tyown_constrained l β ty T).
End own_constrained.
+
Typeclasses Opaque own_constrained tyown_constraint.
Arguments tyown_constraint : simpl never.
+
+Section constrained.
+ Context `{!typeG Σ}.
+
+ Definition persistent_own_constraint (P : iProp Σ) (β : own_state) : iProp Σ := □ P.
+
+ Global Instance persistent_own_constraint_inst P: OwnConstraint (persistent_own_constraint P).
+ Proof. constructor; [by apply _ | by iIntros (??) "H !>"]. Qed.
+
+ Lemma simplify_hyp_place_persistent_constrained P β T:
+ (P -∗ T) -∗ simplify_hyp (persistent_own_constraint P β) T.
+ Proof. iIntros "HT #Hl". by iApply "HT". Qed.
+ Global Instance simplify_hyp_place_persistent_constrained_inst P β:
+ SimplifyHyp (persistent_own_constraint P β) (Some 0%N) :=
+ λ T, i2p (simplify_hyp_place_persistent_constrained P β T).
+
+ Lemma simplify_goal_place_persistent_constrained P `{!Persistent P} β T:
+ T P -∗ simplify_goal (persistent_own_constraint P β) T.
+ Proof. iIntros "HT". iExists _. iFrame. iIntros "#$". Qed.
+ Global Instance simplify_goal_place_persistent_constrained_inst P `{!Persistent P} β:
+ SimplifyGoal (persistent_own_constraint P β) (Some 0%N) :=
+ λ T, i2p (simplify_goal_place_persistent_constrained P β T).
+End constrained.
+
+Typeclasses Opaque persistent_own_constraint.
+Arguments persistent_own_constraint : simpl never.
+
+Notation constrained ty P := (own_constrained (persistent_own_constraint P) ty).
+
+Section nonshr_constrained.
+ Context `{!typeG Σ}.
+
+ Definition nonshr_constraint (P : iProp Σ) (β : own_state) : iProp Σ :=
+ match β with | Own => P | Shr => True end.
+
+ Global Program Instance nonshr_constraint_own_constraint P: OwnConstraint (nonshr_constraint P).
+ Next Obligation. iIntros (???) "?". done. Qed.
+
+ Lemma simplify_hyp_place_nonshr_constrained P T:
+ (P -∗ T) -∗ simplify_hyp (nonshr_constraint P Own) T.
+ Proof. iIntros "HT Hl". by iApply "HT". Qed.
+ Global Instance simplify_hyp_place_nonshr_constrained_inst P:
+ SimplifyHyp (nonshr_constraint P Own) (Some 0%N) :=
+ λ T, i2p (simplify_hyp_place_nonshr_constrained P T).
+
+ Lemma simplify_goal_place_nonshr_constrained P T:
+ T P -∗ simplify_goal (nonshr_constraint P Own) T.
+ Proof. iIntros "HT". iExists _. iFrame. iIntros "$". Qed.
+ Global Instance simplify_goal_place_nonshr_constrained_inst P:
+ SimplifyGoal (nonshr_constraint P Own) (Some 0%N) :=
+ λ T, i2p (simplify_goal_place_nonshr_constrained P T).
+
+End nonshr_constrained.
+
+Typeclasses Opaque nonshr_constraint.
+Arguments nonshr_constraint : simpl never.
diff --git a/theories/typing/singleton.v b/theories/typing/singleton.v
index ec66a7b7f9569d0b632edbc9925c2cae74219d88..8b389650a00f435517c815fa81ffcc43207c1f5c 100644
--- a/theories/typing/singleton.v
+++ b/theories/typing/singleton.v
@@ -38,6 +38,21 @@ Section singleton_val.
SubsumeVal v ty (singleton_val ly v') :=
λ T, i2p (singleton_val_subsume_goal v v' ly ty T).
+ Lemma singleton_val_subsume_goal_loc l v' ly ty `{!Movable ty} T:
+ (∀ v, v â—áµ¥ ty -∗ ⌜ty.(ty_layout) = ly⌠∗ ⌜v = v'⌠∗ T) -∗
+ subsume (l â—â‚— ty) (l â—â‚— singleton_val ly v') T.
+ Proof.
+ iIntros "HT Hty".
+ iDestruct (ty_aligned with "Hty") as %Hal.
+ iDestruct (ty_deref with "Hty") as (v) "[Hmt Hty]".
+ iDestruct (ty_size_eq with "Hty") as %Hly.
+ iDestruct ("HT" with "Hty") as (<- ->) "$".
+ by iFrame.
+ Qed.
+ Global Instance singleton_val_subsume_goal_loc_inst l v' ly ty `{!Movable ty}:
+ SubsumePlace l Own ty (singleton_val ly v') :=
+ λ T, i2p (singleton_val_subsume_goal_loc l v' ly ty T).
+
Lemma singleton_val_merge v l ly T:
(find_in_context (FindVal v) (λ ty:mtype, ⌜ty.(ty_layout) = ly⌠∗ (l â—â‚— ty -∗ T))) -∗
simplify_hyp (l â—â‚— singleton_val ly v) T.
diff --git a/theories/typing/tyfold.v b/theories/typing/tyfold.v
index 9d0674f7b5ff8922bb2bc1ae1a255cbbf7480bfe..c867b8bd1029c6f9a50e954561ca771c96372599 100644
--- a/theories/typing/tyfold.v
+++ b/theories/typing/tyfold.v
@@ -24,12 +24,11 @@ Section tyfold.
rty := tyfold_type tys base
|}.
- Typeclasses Transparent own_constrained constrained.
+ Typeclasses Transparent own_constrained persistent_own_constraint.
Lemma simplify_hyp_place_tyfold_optional l β ls tys b T:
(l â—â‚—{β} (maybe2 cons tys) @ optionalO (λ '(ty, tys), tyexists (λ l2, tyexists (λ ls2,
constrained (
- own_constrained (ty (singleton_place l2))
- (tyown_constraint l2 (ls2 @ tyfold tys b))) (⌜ls = l2::ls2âŒ)))) b -∗ T) -∗
+ own_constrained (tyown_constraint l2 (ls2 @ tyfold tys b)) (ty (singleton_place l2))) (⌜ls = l2::ls2âŒ)))) b -∗ T) -∗
simplify_hyp (lâ—â‚—{β} ls @ tyfold tys b) T.
Proof.
iIntros "HT Hl". iApply "HT". iDestruct "Hl" as (Hlen) "[Htys Hb]".
diff --git a/theories/typing/type.v b/theories/typing/type.v
index 525c129f033a5609844d7990f779c6f261acff16..d26d0a1980b414033913dff640729b038e1b833d 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -544,6 +544,10 @@ Ltac f_equiv' :=
destruct H
| |- _ = _ => reflexivity
+ | |- ?R (?f _) _ => simple apply (_ : Proper (R ==> R) f)
+ | |- ?R (?f _ _) _ => simple apply (_ : Proper (R ==> R ==> R) f)
+ | |- ?R (?f _ _ _) _ => simple apply (_ : Proper (R ==> R ==> R ==> R) f)
+ | |- ?R (?f _ _ _ _) _ => simple apply (_ : Proper (R ==> R ==> R ==> R ==> R) f)
| |- ?R (?f _ _ _ _) _ => simple apply (_ : Proper (_ ==> _ ==> _ ==> _ ==> R) f)
| |- ?R (?f _ _ _) _ => simple apply (_ : Proper (_ ==> _ ==> _ ==> R) f)
| |- ?R (?f _ _) _ => simple apply (_ : Proper (_ ==> _ ==> R) f)
diff --git a/theories/typing/wand.v b/theories/typing/wand.v
index 5ae8c8062afce0af81628fae732e4bbed961d85c..4286b0ab28d7682fa27a947ac1e17c2d8676c519 100644
--- a/theories/typing/wand.v
+++ b/theories/typing/wand.v
@@ -5,15 +5,16 @@ Set Default Proof Using "Type".
Section wand.
Context `{!typeG Σ}.
- Program Definition wand_ex {A} (P : A → iProp Σ) (ty : A → type) : type := {|
+ Context {A : Type}.
+ Implicit Types (P : A → iProp Σ).
+
+ Program Definition wand_ex P (ty : A → type) : type := {|
ty_own β l := match β return _ with
| Own => ∀ x, P x -∗ l â—â‚— (ty x)
| Shr => True
end
|}%I.
- Next Obligation. by iIntros (??????) "?". Qed.
-
- Context {A : Type}. Implicit Types (P : A → iProp Σ).
+ Next Obligation. by iIntros (?????) "?". Qed.
Lemma subsume_wand l P1 P2 ty1 ty2 T:
(* The trick is that we prove the wand at the very end so it can
@@ -59,3 +60,89 @@ Section wand.
End wand.
Notation wand P ty := (wand_ex (A:=unit) (λ _, P) (λ _, ty)).
+
+Section wand_val.
+ Context `{!typeG Σ}.
+
+ Context {A : Type}.
+ Implicit Types (P : A → iProp Σ).
+
+ Program Definition wand_val_ex ly P (ty : A → type) `{!∀ x, Movable (ty x)} : type := {|
+ ty_own β l :=
+ ∃ v, ⌜l `has_layout_loc` ly⌠∗ ⌜v `has_layout_val` ly⌠∗ l ↦[β] v ∗
+ match β return _ with
+ | Own => ∀ x, P x -∗ v â—áµ¥ (ty x)
+ | Shr => True
+ end
+ |}%I.
+ Next Obligation.
+ iIntros (???????) "H". iDestruct "H" as (v) "(Hly1&Hly2&Hl&_)".
+ iMod (heap_mapsto_own_state_share with "Hl") as "Hl". eauto with iFrame.
+ Qed.
+
+ Global Program Instance wand_val_movable P ly ty
+ `{!∀ x, Movable (ty x)} : Movable (wand_val_ex ly P ty) := {|
+ ty_layout := ly;
+ ty_own_val v := (⌜v `has_layout_val` ly⌠∗ ∀ x, P x -∗ v â—áµ¥ (ty x))%I;
+ |}.
+ Next Obligation. iIntros (?????) "Hl". iDestruct "Hl" as (?) "[$ _]". Qed.
+ Next Obligation. iIntros (?????) "[$ _]". Qed.
+ Next Obligation. iIntros (?????) "Hl". iDestruct "Hl" as (v) "(?&?&?&?)". eauto with iFrame. Qed.
+ Next Obligation. iIntros (????? v) "??[??]". iExists v. iFrame. Qed.
+
+ Global Instance wand_val_loc_in_bounds P ly (ty : A → type)
+ `{!∀ x, Movable (ty x)} `{!∀ x, LocInBounds (ty x) β}:
+ LocInBounds (wand_val_ex ly P ty) β.
+ Proof.
+ constructor. iIntros (l) "Hl". iDestruct "Hl" as (?) "(_&_&Hl&_)".
+ iDestruct (heap_mapsto_own_state_loc_in_bounds with "Hl") as "H".
+ iApply (loc_in_bounds_shorten with "H"). lia.
+ Qed.
+
+ Lemma subsume_wand_val v ly1 ly2 P1 P2 ty1 ty2 T `{!∀ x, Movable (ty1 x)} `{!∀ x, Movable (ty2 x)}:
+ (* The trick is that we prove the wand at the very end so it can
+ use all leftover resources. This only works if there is at most
+ one wand per block (but this is enough for iterating over linked
+ lists). *)
+ ⌜ly1 = ly2⌠∗ T ∗ (∀ x, P2 x -∗ ∃ y, P1 y ∗ (v â—áµ¥ ty1 y -∗ v â—áµ¥ ty2 x ∗ True)) -∗
+ subsume (v â—áµ¥ wand_val_ex ly1 P1 ty1) (v â—áµ¥ wand_val_ex ly2 P2 ty2) T.
+ Proof.
+ iIntros "(->&$&Hwand) ($&Hty1)" (x) "HP2".
+ iDestruct ("Hwand" with "HP2") as (y) "[HP1 Hwand]".
+ iDestruct ("Hty1" with "HP1") as "Hty1". iDestruct ("Hwand" with "Hty1") as "[$_]".
+ Qed.
+ Global Instance subsume_wand_val_inst v ly1 ly2 P1 P2 ty1 ty2 `{!∀ x, Movable (ty1 x)} `{!∀ x, Movable (ty2 x)}:
+ SubsumeVal v (wand_val_ex ly1 P1 ty1)%I (wand_val_ex ly2 P2 ty2)%I :=
+ λ T, i2p (subsume_wand_val v ly1 ly2 P1 P2 ty1 ty2 T).
+
+ Lemma simplify_hyp_resolve_wand_val v ly P ty T `{!∀ x, Movable (ty x)}:
+ (∃ x, P x ∗ (v â—áµ¥ ty x -∗ T)) -∗
+ simplify_hyp (v â—áµ¥ wand_val_ex ly P ty) T.
+ Proof.
+ iDestruct 1 as (x) "[HP HT]". iIntros "[_ Hwand]".
+ iApply "HT". by iApply "Hwand".
+ Qed.
+ (* must be before [simplify_goal_place_refine_r] *)
+ Global Instance simplify_hyp_resolve_wand_val_inst v ly P ty `{!∀ x, Movable (ty x)}:
+ SimplifyHypVal v (wand_val_ex ly P ty) (Some 9%N) :=
+ λ T, i2p (simplify_hyp_resolve_wand_val v ly P ty T).
+
+ Lemma simplify_goal_wand_val_eq v ly (ty : A → type) T `{!∀ x, Movable (ty x)}:
+ ⌜v `has_layout_val` ly⌠∗ T True -∗
+ simplify_goal (v â—áµ¥ wand_val_ex ly (λ x, v â—áµ¥ (ty x)) ty) T.
+ Proof. iIntros "[??]". iExists _. iFrame. by eauto. Qed.
+ Global Instance simplify_goal_wand_val_eq_inst v ly ty `{!∀ x, Movable (ty x)}:
+ SimplifyGoalVal v (wand_val_ex ly (λ x, v â—áµ¥ (ty x)) ty)%I (Some 0%N) :=
+ λ T, i2p (simplify_goal_wand_val_eq v ly ty T).
+
+ (* TODO: make this more general, maybe with a SimpleSubsume
+ judgement, which does not have a continutation?*)
+ Lemma simplify_goal_wand_val_eq_ref v ly ty (x1 x2 : A → _) T `{!RMovable ty}:
+ ⌜v `has_layout_val` ly⌠∗ T ⌜∀ x, x1 x = x2 x⌠-∗
+ simplify_goal (v â—áµ¥ wand_val_ex ly (λ x, v â—áµ¥ (x1 x) @ ty) (λ x, (x2 x) @ ty)) T.
+ Proof. iIntros "[??]". iExists _. iFrame. iIntros (Heq x) "?". by rewrite Heq. Qed.
+ Global Instance simplify_goal_wand_val_eq_ref_inst v ly ty x1 x2 `{!RMovable ty}:
+ SimplifyGoalVal v (wand_val_ex ly (λ x, v â—áµ¥ (x1 x) @ ty) (λ x, (x2 x) @ ty))%I (Some 0%N) :=
+ λ T, i2p (simplify_goal_wand_val_eq_ref v ly ty x1 x2 T).
+End wand_val.
+Notation wand_val ly P ty := (wand_val_ex (A:=unit) ly (λ _, P) (λ _, ty)).
diff --git a/tutorial/proofs/t03_list/generated_code.v b/tutorial/proofs/t03_list/generated_code.v
index f642ed05474c99f12f045131a43d1cfb22e647ad..029212d6a51b14bd0e5cc0d0951291302a33eacf 100644
--- a/tutorial/proofs/t03_list/generated_code.v
+++ b/tutorial/proofs/t03_list/generated_code.v
@@ -6,163 +6,163 @@ Set Default Proof Using "Type".
(* Generated from [tutorial/t03_list.c]. *)
Section code.
Definition file_0 : string := "tutorial/t03_list.c".
- Definition loc_2 : location_info := LocationInfo file_0 154 4 154 25.
- Definition loc_3 : location_info := LocationInfo file_0 155 4 155 42.
- Definition loc_4 : location_info := LocationInfo file_0 156 4 156 42.
- Definition loc_5 : location_info := LocationInfo file_0 157 4 157 42.
- Definition loc_6 : location_info := LocationInfo file_0 159 4 159 28.
- Definition loc_7 : location_info := LocationInfo file_0 161 4 161 15.
- Definition loc_8 : location_info := LocationInfo file_0 162 4 162 15.
- Definition loc_9 : location_info := LocationInfo file_0 163 4 163 15.
- Definition loc_10 : location_info := LocationInfo file_0 165 4 165 29.
- Definition loc_11 : location_info := LocationInfo file_0 166 4 166 29.
- Definition loc_12 : location_info := LocationInfo file_0 167 4 167 29.
- Definition loc_13 : location_info := LocationInfo file_0 169 4 169 29.
- Definition loc_14 : location_info := LocationInfo file_0 171 4 171 25.
- Definition loc_15 : location_info := LocationInfo file_0 173 4 173 29.
- Definition loc_16 : location_info := LocationInfo file_0 175 4 175 23.
- Definition loc_17 : location_info := LocationInfo file_0 176 4 176 23.
- Definition loc_18 : location_info := LocationInfo file_0 177 4 177 23.
- Definition loc_19 : location_info := LocationInfo file_0 179 4 179 28.
- Definition loc_20 : location_info := LocationInfo file_0 181 4 181 32.
- Definition loc_21 : location_info := LocationInfo file_0 182 4 182 32.
- Definition loc_22 : location_info := LocationInfo file_0 183 4 183 32.
- Definition loc_23 : location_info := LocationInfo file_0 185 4 185 32.
- Definition loc_24 : location_info := LocationInfo file_0 186 4 186 32.
- Definition loc_25 : location_info := LocationInfo file_0 187 4 187 32.
- Definition loc_26 : location_info := LocationInfo file_0 187 4 187 8.
- Definition loc_27 : location_info := LocationInfo file_0 187 4 187 8.
- Definition loc_28 : location_info := LocationInfo file_0 187 9 187 23.
- Definition loc_29 : location_info := LocationInfo file_0 187 25 187 30.
- Definition loc_30 : location_info := LocationInfo file_0 187 25 187 30.
- Definition loc_31 : location_info := LocationInfo file_0 186 4 186 8.
- Definition loc_32 : location_info := LocationInfo file_0 186 4 186 8.
- Definition loc_33 : location_info := LocationInfo file_0 186 9 186 23.
- Definition loc_34 : location_info := LocationInfo file_0 186 25 186 30.
- Definition loc_35 : location_info := LocationInfo file_0 186 25 186 30.
- Definition loc_36 : location_info := LocationInfo file_0 185 4 185 8.
- Definition loc_37 : location_info := LocationInfo file_0 185 4 185 8.
- Definition loc_38 : location_info := LocationInfo file_0 185 9 185 23.
- Definition loc_39 : location_info := LocationInfo file_0 185 25 185 30.
- Definition loc_40 : location_info := LocationInfo file_0 185 25 185 30.
- Definition loc_41 : location_info := LocationInfo file_0 183 11 183 30.
- Definition loc_42 : location_info := LocationInfo file_0 183 11 183 17.
- Definition loc_43 : location_info := LocationInfo file_0 183 11 183 17.
- Definition loc_44 : location_info := LocationInfo file_0 183 12 183 17.
- Definition loc_45 : location_info := LocationInfo file_0 183 12 183 17.
- Definition loc_46 : location_info := LocationInfo file_0 183 21 183 30.
- Definition loc_47 : location_info := LocationInfo file_0 183 29 183 30.
- Definition loc_48 : location_info := LocationInfo file_0 182 11 182 30.
- Definition loc_49 : location_info := LocationInfo file_0 182 11 182 17.
- Definition loc_50 : location_info := LocationInfo file_0 182 11 182 17.
- Definition loc_51 : location_info := LocationInfo file_0 182 12 182 17.
- Definition loc_52 : location_info := LocationInfo file_0 182 12 182 17.
- Definition loc_53 : location_info := LocationInfo file_0 182 21 182 30.
- Definition loc_54 : location_info := LocationInfo file_0 182 29 182 30.
- Definition loc_55 : location_info := LocationInfo file_0 181 11 181 30.
- Definition loc_56 : location_info := LocationInfo file_0 181 11 181 17.
- Definition loc_57 : location_info := LocationInfo file_0 181 11 181 17.
- Definition loc_58 : location_info := LocationInfo file_0 181 12 181 17.
- Definition loc_59 : location_info := LocationInfo file_0 181 12 181 17.
- Definition loc_60 : location_info := LocationInfo file_0 181 21 181 30.
- Definition loc_61 : location_info := LocationInfo file_0 181 29 181 30.
- Definition loc_62 : location_info := LocationInfo file_0 179 11 179 26.
- Definition loc_63 : location_info := LocationInfo file_0 179 11 179 19.
- Definition loc_64 : location_info := LocationInfo file_0 179 11 179 19.
- Definition loc_65 : location_info := LocationInfo file_0 179 20 179 25.
- Definition loc_66 : location_info := LocationInfo file_0 179 21 179 25.
- Definition loc_67 : location_info := LocationInfo file_0 177 4 177 9.
- Definition loc_68 : location_info := LocationInfo file_0 177 12 177 22.
- Definition loc_69 : location_info := LocationInfo file_0 177 12 177 15.
- Definition loc_70 : location_info := LocationInfo file_0 177 12 177 15.
- Definition loc_71 : location_info := LocationInfo file_0 177 16 177 21.
- Definition loc_72 : location_info := LocationInfo file_0 177 17 177 21.
- Definition loc_73 : location_info := LocationInfo file_0 176 4 176 9.
- Definition loc_74 : location_info := LocationInfo file_0 176 12 176 22.
- Definition loc_75 : location_info := LocationInfo file_0 176 12 176 15.
- Definition loc_76 : location_info := LocationInfo file_0 176 12 176 15.
- Definition loc_77 : location_info := LocationInfo file_0 176 16 176 21.
- Definition loc_78 : location_info := LocationInfo file_0 176 17 176 21.
- Definition loc_79 : location_info := LocationInfo file_0 175 4 175 9.
- Definition loc_80 : location_info := LocationInfo file_0 175 12 175 22.
- Definition loc_81 : location_info := LocationInfo file_0 175 12 175 15.
- Definition loc_82 : location_info := LocationInfo file_0 175 12 175 15.
- Definition loc_83 : location_info := LocationInfo file_0 175 16 175 21.
- Definition loc_84 : location_info := LocationInfo file_0 175 17 175 21.
- Definition loc_85 : location_info := LocationInfo file_0 173 11 173 27.
- Definition loc_86 : location_info := LocationInfo file_0 173 11 173 17.
- Definition loc_87 : location_info := LocationInfo file_0 173 11 173 17.
- Definition loc_88 : location_info := LocationInfo file_0 173 18 173 23.
- Definition loc_89 : location_info := LocationInfo file_0 173 19 173 23.
- Definition loc_90 : location_info := LocationInfo file_0 173 25 173 26.
- Definition loc_91 : location_info := LocationInfo file_0 171 4 171 8.
- Definition loc_92 : location_info := LocationInfo file_0 171 11 171 24.
- Definition loc_93 : location_info := LocationInfo file_0 171 11 171 18.
- Definition loc_94 : location_info := LocationInfo file_0 171 11 171 18.
- Definition loc_95 : location_info := LocationInfo file_0 171 19 171 23.
- Definition loc_96 : location_info := LocationInfo file_0 171 19 171 23.
- Definition loc_97 : location_info := LocationInfo file_0 169 11 169 27.
- Definition loc_98 : location_info := LocationInfo file_0 169 11 169 17.
- Definition loc_99 : location_info := LocationInfo file_0 169 11 169 17.
- Definition loc_100 : location_info := LocationInfo file_0 169 18 169 23.
- Definition loc_101 : location_info := LocationInfo file_0 169 19 169 23.
- Definition loc_102 : location_info := LocationInfo file_0 169 25 169 26.
- Definition loc_103 : location_info := LocationInfo file_0 167 4 167 8.
- Definition loc_104 : location_info := LocationInfo file_0 167 11 167 28.
- Definition loc_105 : location_info := LocationInfo file_0 167 11 167 15.
- Definition loc_106 : location_info := LocationInfo file_0 167 11 167 15.
- Definition loc_107 : location_info := LocationInfo file_0 167 16 167 20.
- Definition loc_108 : location_info := LocationInfo file_0 167 16 167 20.
- Definition loc_109 : location_info := LocationInfo file_0 167 22 167 27.
- Definition loc_110 : location_info := LocationInfo file_0 167 22 167 27.
- Definition loc_111 : location_info := LocationInfo file_0 166 4 166 8.
- Definition loc_112 : location_info := LocationInfo file_0 166 11 166 28.
- Definition loc_113 : location_info := LocationInfo file_0 166 11 166 15.
- Definition loc_114 : location_info := LocationInfo file_0 166 11 166 15.
- Definition loc_115 : location_info := LocationInfo file_0 166 16 166 20.
- Definition loc_116 : location_info := LocationInfo file_0 166 16 166 20.
- Definition loc_117 : location_info := LocationInfo file_0 166 22 166 27.
- Definition loc_118 : location_info := LocationInfo file_0 166 22 166 27.
- Definition loc_119 : location_info := LocationInfo file_0 165 4 165 8.
- Definition loc_120 : location_info := LocationInfo file_0 165 11 165 28.
- Definition loc_121 : location_info := LocationInfo file_0 165 11 165 15.
- Definition loc_122 : location_info := LocationInfo file_0 165 11 165 15.
- Definition loc_123 : location_info := LocationInfo file_0 165 16 165 20.
- Definition loc_124 : location_info := LocationInfo file_0 165 16 165 20.
- Definition loc_125 : location_info := LocationInfo file_0 165 22 165 27.
- Definition loc_126 : location_info := LocationInfo file_0 165 22 165 27.
- Definition loc_127 : location_info := LocationInfo file_0 163 4 163 10.
- Definition loc_128 : location_info := LocationInfo file_0 163 5 163 10.
- Definition loc_129 : location_info := LocationInfo file_0 163 5 163 10.
- Definition loc_130 : location_info := LocationInfo file_0 163 13 163 14.
- Definition loc_131 : location_info := LocationInfo file_0 162 4 162 10.
- Definition loc_132 : location_info := LocationInfo file_0 162 5 162 10.
- Definition loc_133 : location_info := LocationInfo file_0 162 5 162 10.
- Definition loc_134 : location_info := LocationInfo file_0 162 13 162 14.
- Definition loc_135 : location_info := LocationInfo file_0 161 4 161 10.
- Definition loc_136 : location_info := LocationInfo file_0 161 5 161 10.
- Definition loc_137 : location_info := LocationInfo file_0 161 5 161 10.
- Definition loc_138 : location_info := LocationInfo file_0 161 13 161 14.
- Definition loc_139 : location_info := LocationInfo file_0 159 11 159 26.
- Definition loc_140 : location_info := LocationInfo file_0 159 11 159 19.
- Definition loc_141 : location_info := LocationInfo file_0 159 11 159 19.
- Definition loc_142 : location_info := LocationInfo file_0 159 20 159 25.
- Definition loc_143 : location_info := LocationInfo file_0 159 21 159 25.
- Definition loc_144 : location_info := LocationInfo file_0 157 20 157 41.
- Definition loc_145 : location_info := LocationInfo file_0 157 20 157 25.
- Definition loc_146 : location_info := LocationInfo file_0 157 20 157 25.
- Definition loc_147 : location_info := LocationInfo file_0 157 26 157 40.
- Definition loc_150 : location_info := LocationInfo file_0 156 20 156 41.
- Definition loc_151 : location_info := LocationInfo file_0 156 20 156 25.
- Definition loc_152 : location_info := LocationInfo file_0 156 20 156 25.
- Definition loc_153 : location_info := LocationInfo file_0 156 26 156 40.
- Definition loc_156 : location_info := LocationInfo file_0 155 20 155 41.
- Definition loc_157 : location_info := LocationInfo file_0 155 20 155 25.
- Definition loc_158 : location_info := LocationInfo file_0 155 20 155 25.
- Definition loc_159 : location_info := LocationInfo file_0 155 26 155 40.
- Definition loc_162 : location_info := LocationInfo file_0 154 18 154 24.
- Definition loc_163 : location_info := LocationInfo file_0 154 18 154 22.
- Definition loc_164 : location_info := LocationInfo file_0 154 18 154 22.
+ Definition loc_2 : location_info := LocationInfo file_0 173 4 173 25.
+ Definition loc_3 : location_info := LocationInfo file_0 174 4 174 42.
+ Definition loc_4 : location_info := LocationInfo file_0 175 4 175 42.
+ Definition loc_5 : location_info := LocationInfo file_0 176 4 176 42.
+ Definition loc_6 : location_info := LocationInfo file_0 178 4 178 28.
+ Definition loc_7 : location_info := LocationInfo file_0 180 4 180 15.
+ Definition loc_8 : location_info := LocationInfo file_0 181 4 181 15.
+ Definition loc_9 : location_info := LocationInfo file_0 182 4 182 15.
+ Definition loc_10 : location_info := LocationInfo file_0 184 4 184 29.
+ Definition loc_11 : location_info := LocationInfo file_0 185 4 185 29.
+ Definition loc_12 : location_info := LocationInfo file_0 186 4 186 29.
+ Definition loc_13 : location_info := LocationInfo file_0 188 4 188 29.
+ Definition loc_14 : location_info := LocationInfo file_0 190 4 190 25.
+ Definition loc_15 : location_info := LocationInfo file_0 192 4 192 29.
+ Definition loc_16 : location_info := LocationInfo file_0 194 4 194 23.
+ Definition loc_17 : location_info := LocationInfo file_0 195 4 195 23.
+ Definition loc_18 : location_info := LocationInfo file_0 196 4 196 23.
+ Definition loc_19 : location_info := LocationInfo file_0 198 4 198 28.
+ Definition loc_20 : location_info := LocationInfo file_0 200 4 200 32.
+ Definition loc_21 : location_info := LocationInfo file_0 201 4 201 32.
+ Definition loc_22 : location_info := LocationInfo file_0 202 4 202 32.
+ Definition loc_23 : location_info := LocationInfo file_0 204 4 204 32.
+ Definition loc_24 : location_info := LocationInfo file_0 205 4 205 32.
+ Definition loc_25 : location_info := LocationInfo file_0 206 4 206 32.
+ Definition loc_26 : location_info := LocationInfo file_0 206 4 206 8.
+ Definition loc_27 : location_info := LocationInfo file_0 206 4 206 8.
+ Definition loc_28 : location_info := LocationInfo file_0 206 9 206 23.
+ Definition loc_29 : location_info := LocationInfo file_0 206 25 206 30.
+ Definition loc_30 : location_info := LocationInfo file_0 206 25 206 30.
+ Definition loc_31 : location_info := LocationInfo file_0 205 4 205 8.
+ Definition loc_32 : location_info := LocationInfo file_0 205 4 205 8.
+ Definition loc_33 : location_info := LocationInfo file_0 205 9 205 23.
+ Definition loc_34 : location_info := LocationInfo file_0 205 25 205 30.
+ Definition loc_35 : location_info := LocationInfo file_0 205 25 205 30.
+ Definition loc_36 : location_info := LocationInfo file_0 204 4 204 8.
+ Definition loc_37 : location_info := LocationInfo file_0 204 4 204 8.
+ Definition loc_38 : location_info := LocationInfo file_0 204 9 204 23.
+ Definition loc_39 : location_info := LocationInfo file_0 204 25 204 30.
+ Definition loc_40 : location_info := LocationInfo file_0 204 25 204 30.
+ Definition loc_41 : location_info := LocationInfo file_0 202 11 202 30.
+ Definition loc_42 : location_info := LocationInfo file_0 202 11 202 17.
+ Definition loc_43 : location_info := LocationInfo file_0 202 11 202 17.
+ Definition loc_44 : location_info := LocationInfo file_0 202 12 202 17.
+ Definition loc_45 : location_info := LocationInfo file_0 202 12 202 17.
+ Definition loc_46 : location_info := LocationInfo file_0 202 21 202 30.
+ Definition loc_47 : location_info := LocationInfo file_0 202 29 202 30.
+ Definition loc_48 : location_info := LocationInfo file_0 201 11 201 30.
+ Definition loc_49 : location_info := LocationInfo file_0 201 11 201 17.
+ Definition loc_50 : location_info := LocationInfo file_0 201 11 201 17.
+ Definition loc_51 : location_info := LocationInfo file_0 201 12 201 17.
+ Definition loc_52 : location_info := LocationInfo file_0 201 12 201 17.
+ Definition loc_53 : location_info := LocationInfo file_0 201 21 201 30.
+ Definition loc_54 : location_info := LocationInfo file_0 201 29 201 30.
+ Definition loc_55 : location_info := LocationInfo file_0 200 11 200 30.
+ Definition loc_56 : location_info := LocationInfo file_0 200 11 200 17.
+ Definition loc_57 : location_info := LocationInfo file_0 200 11 200 17.
+ Definition loc_58 : location_info := LocationInfo file_0 200 12 200 17.
+ Definition loc_59 : location_info := LocationInfo file_0 200 12 200 17.
+ Definition loc_60 : location_info := LocationInfo file_0 200 21 200 30.
+ Definition loc_61 : location_info := LocationInfo file_0 200 29 200 30.
+ Definition loc_62 : location_info := LocationInfo file_0 198 11 198 26.
+ Definition loc_63 : location_info := LocationInfo file_0 198 11 198 19.
+ Definition loc_64 : location_info := LocationInfo file_0 198 11 198 19.
+ Definition loc_65 : location_info := LocationInfo file_0 198 20 198 25.
+ Definition loc_66 : location_info := LocationInfo file_0 198 21 198 25.
+ Definition loc_67 : location_info := LocationInfo file_0 196 4 196 9.
+ Definition loc_68 : location_info := LocationInfo file_0 196 12 196 22.
+ Definition loc_69 : location_info := LocationInfo file_0 196 12 196 15.
+ Definition loc_70 : location_info := LocationInfo file_0 196 12 196 15.
+ Definition loc_71 : location_info := LocationInfo file_0 196 16 196 21.
+ Definition loc_72 : location_info := LocationInfo file_0 196 17 196 21.
+ Definition loc_73 : location_info := LocationInfo file_0 195 4 195 9.
+ Definition loc_74 : location_info := LocationInfo file_0 195 12 195 22.
+ Definition loc_75 : location_info := LocationInfo file_0 195 12 195 15.
+ Definition loc_76 : location_info := LocationInfo file_0 195 12 195 15.
+ Definition loc_77 : location_info := LocationInfo file_0 195 16 195 21.
+ Definition loc_78 : location_info := LocationInfo file_0 195 17 195 21.
+ Definition loc_79 : location_info := LocationInfo file_0 194 4 194 9.
+ Definition loc_80 : location_info := LocationInfo file_0 194 12 194 22.
+ Definition loc_81 : location_info := LocationInfo file_0 194 12 194 15.
+ Definition loc_82 : location_info := LocationInfo file_0 194 12 194 15.
+ Definition loc_83 : location_info := LocationInfo file_0 194 16 194 21.
+ Definition loc_84 : location_info := LocationInfo file_0 194 17 194 21.
+ Definition loc_85 : location_info := LocationInfo file_0 192 11 192 27.
+ Definition loc_86 : location_info := LocationInfo file_0 192 11 192 17.
+ Definition loc_87 : location_info := LocationInfo file_0 192 11 192 17.
+ Definition loc_88 : location_info := LocationInfo file_0 192 18 192 23.
+ Definition loc_89 : location_info := LocationInfo file_0 192 19 192 23.
+ Definition loc_90 : location_info := LocationInfo file_0 192 25 192 26.
+ Definition loc_91 : location_info := LocationInfo file_0 190 4 190 8.
+ Definition loc_92 : location_info := LocationInfo file_0 190 11 190 24.
+ Definition loc_93 : location_info := LocationInfo file_0 190 11 190 18.
+ Definition loc_94 : location_info := LocationInfo file_0 190 11 190 18.
+ Definition loc_95 : location_info := LocationInfo file_0 190 19 190 23.
+ Definition loc_96 : location_info := LocationInfo file_0 190 19 190 23.
+ Definition loc_97 : location_info := LocationInfo file_0 188 11 188 27.
+ Definition loc_98 : location_info := LocationInfo file_0 188 11 188 17.
+ Definition loc_99 : location_info := LocationInfo file_0 188 11 188 17.
+ Definition loc_100 : location_info := LocationInfo file_0 188 18 188 23.
+ Definition loc_101 : location_info := LocationInfo file_0 188 19 188 23.
+ Definition loc_102 : location_info := LocationInfo file_0 188 25 188 26.
+ Definition loc_103 : location_info := LocationInfo file_0 186 4 186 8.
+ Definition loc_104 : location_info := LocationInfo file_0 186 11 186 28.
+ Definition loc_105 : location_info := LocationInfo file_0 186 11 186 15.
+ Definition loc_106 : location_info := LocationInfo file_0 186 11 186 15.
+ Definition loc_107 : location_info := LocationInfo file_0 186 16 186 20.
+ Definition loc_108 : location_info := LocationInfo file_0 186 16 186 20.
+ Definition loc_109 : location_info := LocationInfo file_0 186 22 186 27.
+ Definition loc_110 : location_info := LocationInfo file_0 186 22 186 27.
+ Definition loc_111 : location_info := LocationInfo file_0 185 4 185 8.
+ Definition loc_112 : location_info := LocationInfo file_0 185 11 185 28.
+ Definition loc_113 : location_info := LocationInfo file_0 185 11 185 15.
+ Definition loc_114 : location_info := LocationInfo file_0 185 11 185 15.
+ Definition loc_115 : location_info := LocationInfo file_0 185 16 185 20.
+ Definition loc_116 : location_info := LocationInfo file_0 185 16 185 20.
+ Definition loc_117 : location_info := LocationInfo file_0 185 22 185 27.
+ Definition loc_118 : location_info := LocationInfo file_0 185 22 185 27.
+ Definition loc_119 : location_info := LocationInfo file_0 184 4 184 8.
+ Definition loc_120 : location_info := LocationInfo file_0 184 11 184 28.
+ Definition loc_121 : location_info := LocationInfo file_0 184 11 184 15.
+ Definition loc_122 : location_info := LocationInfo file_0 184 11 184 15.
+ Definition loc_123 : location_info := LocationInfo file_0 184 16 184 20.
+ Definition loc_124 : location_info := LocationInfo file_0 184 16 184 20.
+ Definition loc_125 : location_info := LocationInfo file_0 184 22 184 27.
+ Definition loc_126 : location_info := LocationInfo file_0 184 22 184 27.
+ Definition loc_127 : location_info := LocationInfo file_0 182 4 182 10.
+ Definition loc_128 : location_info := LocationInfo file_0 182 5 182 10.
+ Definition loc_129 : location_info := LocationInfo file_0 182 5 182 10.
+ Definition loc_130 : location_info := LocationInfo file_0 182 13 182 14.
+ Definition loc_131 : location_info := LocationInfo file_0 181 4 181 10.
+ Definition loc_132 : location_info := LocationInfo file_0 181 5 181 10.
+ Definition loc_133 : location_info := LocationInfo file_0 181 5 181 10.
+ Definition loc_134 : location_info := LocationInfo file_0 181 13 181 14.
+ Definition loc_135 : location_info := LocationInfo file_0 180 4 180 10.
+ Definition loc_136 : location_info := LocationInfo file_0 180 5 180 10.
+ Definition loc_137 : location_info := LocationInfo file_0 180 5 180 10.
+ Definition loc_138 : location_info := LocationInfo file_0 180 13 180 14.
+ Definition loc_139 : location_info := LocationInfo file_0 178 11 178 26.
+ Definition loc_140 : location_info := LocationInfo file_0 178 11 178 19.
+ Definition loc_141 : location_info := LocationInfo file_0 178 11 178 19.
+ Definition loc_142 : location_info := LocationInfo file_0 178 20 178 25.
+ Definition loc_143 : location_info := LocationInfo file_0 178 21 178 25.
+ Definition loc_144 : location_info := LocationInfo file_0 176 20 176 41.
+ Definition loc_145 : location_info := LocationInfo file_0 176 20 176 25.
+ Definition loc_146 : location_info := LocationInfo file_0 176 20 176 25.
+ Definition loc_147 : location_info := LocationInfo file_0 176 26 176 40.
+ Definition loc_150 : location_info := LocationInfo file_0 175 20 175 41.
+ Definition loc_151 : location_info := LocationInfo file_0 175 20 175 25.
+ Definition loc_152 : location_info := LocationInfo file_0 175 20 175 25.
+ Definition loc_153 : location_info := LocationInfo file_0 175 26 175 40.
+ Definition loc_156 : location_info := LocationInfo file_0 174 20 174 41.
+ Definition loc_157 : location_info := LocationInfo file_0 174 20 174 25.
+ Definition loc_158 : location_info := LocationInfo file_0 174 20 174 25.
+ Definition loc_159 : location_info := LocationInfo file_0 174 26 174 40.
+ Definition loc_162 : location_info := LocationInfo file_0 173 18 173 24.
+ Definition loc_163 : location_info := LocationInfo file_0 173 18 173 22.
+ Definition loc_164 : location_info := LocationInfo file_0 173 18 173 22.
Definition loc_169 : location_info := LocationInfo file_0 27 4 27 26.
Definition loc_170 : location_info := LocationInfo file_0 27 11 27 25.
Definition loc_173 : location_info := LocationInfo file_0 35 4 35 32.
@@ -312,113 +312,139 @@ Section code.
Definition loc_337 : location_info := LocationInfo file_0 107 5 107 6.
Definition loc_338 : location_info := LocationInfo file_0 107 5 107 6.
Definition loc_339 : location_info := LocationInfo file_0 107 10 107 24.
- Definition loc_342 : location_info := LocationInfo file_0 117 2 117 19.
- Definition loc_343 : location_info := LocationInfo file_0 121 2 123 3.
- Definition loc_344 : location_info := LocationInfo file_0 124 2 124 12.
- Definition loc_345 : location_info := LocationInfo file_0 124 2 124 6.
- Definition loc_346 : location_info := LocationInfo file_0 124 3 124 6.
- Definition loc_347 : location_info := LocationInfo file_0 124 3 124 6.
- Definition loc_348 : location_info := LocationInfo file_0 124 9 124 11.
- Definition loc_349 : location_info := LocationInfo file_0 124 9 124 11.
- Definition loc_350 : location_info := LocationInfo file_0 121 2 123 3.
- Definition loc_351 : location_info := LocationInfo file_0 121 31 123 3.
- Definition loc_352 : location_info := LocationInfo file_0 122 4 122 26.
- Definition loc_353 : location_info := LocationInfo file_0 121 2 123 3.
- Definition loc_354 : location_info := LocationInfo file_0 121 2 123 3.
- Definition loc_355 : location_info := LocationInfo file_0 122 4 122 7.
- Definition loc_356 : location_info := LocationInfo file_0 122 10 122 25.
- Definition loc_357 : location_info := LocationInfo file_0 122 11 122 25.
- Definition loc_358 : location_info := LocationInfo file_0 122 12 122 18.
- Definition loc_359 : location_info := LocationInfo file_0 122 12 122 18.
- Definition loc_360 : location_info := LocationInfo file_0 122 14 122 17.
- Definition loc_361 : location_info := LocationInfo file_0 122 14 122 17.
- Definition loc_362 : location_info := LocationInfo file_0 121 8 121 30.
- Definition loc_363 : location_info := LocationInfo file_0 121 8 121 12.
- Definition loc_364 : location_info := LocationInfo file_0 121 8 121 12.
- Definition loc_365 : location_info := LocationInfo file_0 121 9 121 12.
- Definition loc_366 : location_info := LocationInfo file_0 121 9 121 12.
- Definition loc_367 : location_info := LocationInfo file_0 121 16 121 30.
- Definition loc_368 : location_info := LocationInfo file_0 117 16 117 18.
- Definition loc_369 : location_info := LocationInfo file_0 117 16 117 18.
- Definition loc_374 : location_info := LocationInfo file_0 134 4 134 21.
- Definition loc_375 : location_info := LocationInfo file_0 139 4 148 5.
- Definition loc_376 : location_info := LocationInfo file_0 149 4 149 13.
- Definition loc_377 : location_info := LocationInfo file_0 149 11 149 12.
- Definition loc_378 : location_info := LocationInfo file_0 139 4 148 5.
- Definition loc_379 : location_info := LocationInfo file_0 139 35 148 5.
- Definition loc_380 : location_info := LocationInfo file_0 140 8 140 27.
- Definition loc_381 : location_info := LocationInfo file_0 142 8 142 33.
- Definition loc_382 : location_info := LocationInfo file_0 143 8 145 9.
- Definition loc_383 : location_info := LocationInfo file_0 147 8 147 26.
- Definition loc_384 : location_info := LocationInfo file_0 139 4 148 5.
- Definition loc_385 : location_info := LocationInfo file_0 139 4 148 5.
- Definition loc_386 : location_info := LocationInfo file_0 147 8 147 12.
- Definition loc_387 : location_info := LocationInfo file_0 147 15 147 25.
- Definition loc_388 : location_info := LocationInfo file_0 147 16 147 25.
- Definition loc_389 : location_info := LocationInfo file_0 147 16 147 19.
- Definition loc_390 : location_info := LocationInfo file_0 147 16 147 19.
- Definition loc_391 : location_info := LocationInfo file_0 143 23 145 9.
- Definition loc_392 : location_info := LocationInfo file_0 144 12 144 21.
- Definition loc_393 : location_info := LocationInfo file_0 144 19 144 20.
- Definition loc_395 : location_info := LocationInfo file_0 143 11 143 21.
- Definition loc_396 : location_info := LocationInfo file_0 143 11 143 16.
- Definition loc_397 : location_info := LocationInfo file_0 143 11 143 16.
- Definition loc_398 : location_info := LocationInfo file_0 143 12 143 16.
- Definition loc_399 : location_info := LocationInfo file_0 143 12 143 16.
- Definition loc_400 : location_info := LocationInfo file_0 143 20 143 21.
- Definition loc_401 : location_info := LocationInfo file_0 143 20 143 21.
- Definition loc_402 : location_info := LocationInfo file_0 142 23 142 32.
- Definition loc_403 : location_info := LocationInfo file_0 142 23 142 32.
- Definition loc_404 : location_info := LocationInfo file_0 142 23 142 26.
- Definition loc_405 : location_info := LocationInfo file_0 142 23 142 26.
- Definition loc_408 : location_info := LocationInfo file_0 140 21 140 26.
- Definition loc_409 : location_info := LocationInfo file_0 140 21 140 26.
- Definition loc_410 : location_info := LocationInfo file_0 140 22 140 26.
- Definition loc_411 : location_info := LocationInfo file_0 140 22 140 26.
- Definition loc_414 : location_info := LocationInfo file_0 139 10 139 33.
- Definition loc_415 : location_info := LocationInfo file_0 139 10 139 15.
- Definition loc_416 : location_info := LocationInfo file_0 139 10 139 15.
- Definition loc_417 : location_info := LocationInfo file_0 139 11 139 15.
- Definition loc_418 : location_info := LocationInfo file_0 139 11 139 15.
- Definition loc_419 : location_info := LocationInfo file_0 139 19 139 33.
- Definition loc_420 : location_info := LocationInfo file_0 134 19 134 20.
- Definition loc_421 : location_info := LocationInfo file_0 134 19 134 20.
- Definition loc_426 : location_info := LocationInfo file_0 194 2 194 18.
- Definition loc_427 : location_info := LocationInfo file_0 204 2 209 3.
- Definition loc_428 : location_info := LocationInfo file_0 204 2 209 3.
- Definition loc_429 : location_info := LocationInfo file_0 204 31 209 3.
- Definition loc_430 : location_info := LocationInfo file_0 205 4 205 25.
- Definition loc_431 : location_info := LocationInfo file_0 206 4 206 20.
- Definition loc_432 : location_info := LocationInfo file_0 207 4 207 14.
- Definition loc_433 : location_info := LocationInfo file_0 208 4 208 19.
- Definition loc_434 : location_info := LocationInfo file_0 204 2 209 3.
- Definition loc_435 : location_info := LocationInfo file_0 204 2 209 3.
- Definition loc_436 : location_info := LocationInfo file_0 208 4 208 7.
- Definition loc_437 : location_info := LocationInfo file_0 208 10 208 18.
- Definition loc_438 : location_info := LocationInfo file_0 208 10 208 18.
- Definition loc_439 : location_info := LocationInfo file_0 207 4 207 7.
- Definition loc_440 : location_info := LocationInfo file_0 207 5 207 7.
- Definition loc_441 : location_info := LocationInfo file_0 207 5 207 7.
- Definition loc_442 : location_info := LocationInfo file_0 207 10 207 13.
- Definition loc_443 : location_info := LocationInfo file_0 207 10 207 13.
- Definition loc_444 : location_info := LocationInfo file_0 206 4 206 13.
- Definition loc_445 : location_info := LocationInfo file_0 206 4 206 7.
- Definition loc_446 : location_info := LocationInfo file_0 206 4 206 7.
- Definition loc_447 : location_info := LocationInfo file_0 206 16 206 19.
- Definition loc_448 : location_info := LocationInfo file_0 206 16 206 19.
- Definition loc_449 : location_info := LocationInfo file_0 206 17 206 19.
- Definition loc_450 : location_info := LocationInfo file_0 206 17 206 19.
- Definition loc_451 : location_info := LocationInfo file_0 205 4 205 12.
- Definition loc_452 : location_info := LocationInfo file_0 205 15 205 24.
- Definition loc_453 : location_info := LocationInfo file_0 205 15 205 24.
- Definition loc_454 : location_info := LocationInfo file_0 205 15 205 18.
- Definition loc_455 : location_info := LocationInfo file_0 205 15 205 18.
- Definition loc_456 : location_info := LocationInfo file_0 204 8 204 29.
- Definition loc_457 : location_info := LocationInfo file_0 204 8 204 11.
- Definition loc_458 : location_info := LocationInfo file_0 204 8 204 11.
- Definition loc_459 : location_info := LocationInfo file_0 204 15 204 29.
- Definition loc_460 : location_info := LocationInfo file_0 194 15 194 17.
- Definition loc_461 : location_info := LocationInfo file_0 194 15 194 17.
+ Definition loc_342 : location_info := LocationInfo file_0 120 2 120 17.
+ Definition loc_343 : location_info := LocationInfo file_0 125 2 128 3.
+ Definition loc_344 : location_info := LocationInfo file_0 129 2 129 13.
+ Definition loc_345 : location_info := LocationInfo file_0 129 9 129 12.
+ Definition loc_346 : location_info := LocationInfo file_0 129 9 129 12.
+ Definition loc_347 : location_info := LocationInfo file_0 125 2 128 3.
+ Definition loc_348 : location_info := LocationInfo file_0 125 30 128 3.
+ Definition loc_349 : location_info := LocationInfo file_0 126 4 126 16.
+ Definition loc_350 : location_info := LocationInfo file_0 127 4 127 13.
+ Definition loc_351 : location_info := LocationInfo file_0 125 2 128 3.
+ Definition loc_352 : location_info := LocationInfo file_0 125 2 128 3.
+ Definition loc_353 : location_info := LocationInfo file_0 127 4 127 7.
+ Definition loc_354 : location_info := LocationInfo file_0 127 4 127 12.
+ Definition loc_355 : location_info := LocationInfo file_0 127 4 127 7.
+ Definition loc_356 : location_info := LocationInfo file_0 127 4 127 7.
+ Definition loc_357 : location_info := LocationInfo file_0 127 11 127 12.
+ Definition loc_358 : location_info := LocationInfo file_0 126 4 126 5.
+ Definition loc_359 : location_info := LocationInfo file_0 126 8 126 15.
+ Definition loc_360 : location_info := LocationInfo file_0 126 8 126 15.
+ Definition loc_361 : location_info := LocationInfo file_0 126 8 126 9.
+ Definition loc_362 : location_info := LocationInfo file_0 126 8 126 9.
+ Definition loc_363 : location_info := LocationInfo file_0 125 9 125 28.
+ Definition loc_364 : location_info := LocationInfo file_0 125 9 125 10.
+ Definition loc_365 : location_info := LocationInfo file_0 125 9 125 10.
+ Definition loc_366 : location_info := LocationInfo file_0 125 14 125 28.
+ Definition loc_367 : location_info := LocationInfo file_0 120 15 120 16.
+ Definition loc_372 : location_info := LocationInfo file_0 136 2 136 19.
+ Definition loc_373 : location_info := LocationInfo file_0 140 2 142 3.
+ Definition loc_374 : location_info := LocationInfo file_0 143 2 143 12.
+ Definition loc_375 : location_info := LocationInfo file_0 143 2 143 6.
+ Definition loc_376 : location_info := LocationInfo file_0 143 3 143 6.
+ Definition loc_377 : location_info := LocationInfo file_0 143 3 143 6.
+ Definition loc_378 : location_info := LocationInfo file_0 143 9 143 11.
+ Definition loc_379 : location_info := LocationInfo file_0 143 9 143 11.
+ Definition loc_380 : location_info := LocationInfo file_0 140 2 142 3.
+ Definition loc_381 : location_info := LocationInfo file_0 140 31 142 3.
+ Definition loc_382 : location_info := LocationInfo file_0 141 4 141 26.
+ Definition loc_383 : location_info := LocationInfo file_0 140 2 142 3.
+ Definition loc_384 : location_info := LocationInfo file_0 140 2 142 3.
+ Definition loc_385 : location_info := LocationInfo file_0 141 4 141 7.
+ Definition loc_386 : location_info := LocationInfo file_0 141 10 141 25.
+ Definition loc_387 : location_info := LocationInfo file_0 141 11 141 25.
+ Definition loc_388 : location_info := LocationInfo file_0 141 12 141 18.
+ Definition loc_389 : location_info := LocationInfo file_0 141 12 141 18.
+ Definition loc_390 : location_info := LocationInfo file_0 141 14 141 17.
+ Definition loc_391 : location_info := LocationInfo file_0 141 14 141 17.
+ Definition loc_392 : location_info := LocationInfo file_0 140 8 140 30.
+ Definition loc_393 : location_info := LocationInfo file_0 140 8 140 12.
+ Definition loc_394 : location_info := LocationInfo file_0 140 8 140 12.
+ Definition loc_395 : location_info := LocationInfo file_0 140 9 140 12.
+ Definition loc_396 : location_info := LocationInfo file_0 140 9 140 12.
+ Definition loc_397 : location_info := LocationInfo file_0 140 16 140 30.
+ Definition loc_398 : location_info := LocationInfo file_0 136 16 136 18.
+ Definition loc_399 : location_info := LocationInfo file_0 136 16 136 18.
+ Definition loc_404 : location_info := LocationInfo file_0 153 4 153 21.
+ Definition loc_405 : location_info := LocationInfo file_0 158 4 167 5.
+ Definition loc_406 : location_info := LocationInfo file_0 168 4 168 13.
+ Definition loc_407 : location_info := LocationInfo file_0 168 11 168 12.
+ Definition loc_408 : location_info := LocationInfo file_0 158 4 167 5.
+ Definition loc_409 : location_info := LocationInfo file_0 158 35 167 5.
+ Definition loc_410 : location_info := LocationInfo file_0 159 8 159 27.
+ Definition loc_411 : location_info := LocationInfo file_0 161 8 161 33.
+ Definition loc_412 : location_info := LocationInfo file_0 162 8 164 9.
+ Definition loc_413 : location_info := LocationInfo file_0 166 8 166 26.
+ Definition loc_414 : location_info := LocationInfo file_0 158 4 167 5.
+ Definition loc_415 : location_info := LocationInfo file_0 158 4 167 5.
+ Definition loc_416 : location_info := LocationInfo file_0 166 8 166 12.
+ Definition loc_417 : location_info := LocationInfo file_0 166 15 166 25.
+ Definition loc_418 : location_info := LocationInfo file_0 166 16 166 25.
+ Definition loc_419 : location_info := LocationInfo file_0 166 16 166 19.
+ Definition loc_420 : location_info := LocationInfo file_0 166 16 166 19.
+ Definition loc_421 : location_info := LocationInfo file_0 162 23 164 9.
+ Definition loc_422 : location_info := LocationInfo file_0 163 12 163 21.
+ Definition loc_423 : location_info := LocationInfo file_0 163 19 163 20.
+ Definition loc_425 : location_info := LocationInfo file_0 162 11 162 21.
+ Definition loc_426 : location_info := LocationInfo file_0 162 11 162 16.
+ Definition loc_427 : location_info := LocationInfo file_0 162 11 162 16.
+ Definition loc_428 : location_info := LocationInfo file_0 162 12 162 16.
+ Definition loc_429 : location_info := LocationInfo file_0 162 12 162 16.
+ Definition loc_430 : location_info := LocationInfo file_0 162 20 162 21.
+ Definition loc_431 : location_info := LocationInfo file_0 162 20 162 21.
+ Definition loc_432 : location_info := LocationInfo file_0 161 23 161 32.
+ Definition loc_433 : location_info := LocationInfo file_0 161 23 161 32.
+ Definition loc_434 : location_info := LocationInfo file_0 161 23 161 26.
+ Definition loc_435 : location_info := LocationInfo file_0 161 23 161 26.
+ Definition loc_438 : location_info := LocationInfo file_0 159 21 159 26.
+ Definition loc_439 : location_info := LocationInfo file_0 159 21 159 26.
+ Definition loc_440 : location_info := LocationInfo file_0 159 22 159 26.
+ Definition loc_441 : location_info := LocationInfo file_0 159 22 159 26.
+ Definition loc_444 : location_info := LocationInfo file_0 158 10 158 33.
+ Definition loc_445 : location_info := LocationInfo file_0 158 10 158 15.
+ Definition loc_446 : location_info := LocationInfo file_0 158 10 158 15.
+ Definition loc_447 : location_info := LocationInfo file_0 158 11 158 15.
+ Definition loc_448 : location_info := LocationInfo file_0 158 11 158 15.
+ Definition loc_449 : location_info := LocationInfo file_0 158 19 158 33.
+ Definition loc_450 : location_info := LocationInfo file_0 153 19 153 20.
+ Definition loc_451 : location_info := LocationInfo file_0 153 19 153 20.
+ Definition loc_456 : location_info := LocationInfo file_0 213 2 213 18.
+ Definition loc_457 : location_info := LocationInfo file_0 223 2 228 3.
+ Definition loc_458 : location_info := LocationInfo file_0 223 2 228 3.
+ Definition loc_459 : location_info := LocationInfo file_0 223 31 228 3.
+ Definition loc_460 : location_info := LocationInfo file_0 224 4 224 25.
+ Definition loc_461 : location_info := LocationInfo file_0 225 4 225 20.
+ Definition loc_462 : location_info := LocationInfo file_0 226 4 226 14.
+ Definition loc_463 : location_info := LocationInfo file_0 227 4 227 19.
+ Definition loc_464 : location_info := LocationInfo file_0 223 2 228 3.
+ Definition loc_465 : location_info := LocationInfo file_0 223 2 228 3.
+ Definition loc_466 : location_info := LocationInfo file_0 227 4 227 7.
+ Definition loc_467 : location_info := LocationInfo file_0 227 10 227 18.
+ Definition loc_468 : location_info := LocationInfo file_0 227 10 227 18.
+ Definition loc_469 : location_info := LocationInfo file_0 226 4 226 7.
+ Definition loc_470 : location_info := LocationInfo file_0 226 5 226 7.
+ Definition loc_471 : location_info := LocationInfo file_0 226 5 226 7.
+ Definition loc_472 : location_info := LocationInfo file_0 226 10 226 13.
+ Definition loc_473 : location_info := LocationInfo file_0 226 10 226 13.
+ Definition loc_474 : location_info := LocationInfo file_0 225 4 225 13.
+ Definition loc_475 : location_info := LocationInfo file_0 225 4 225 7.
+ Definition loc_476 : location_info := LocationInfo file_0 225 4 225 7.
+ Definition loc_477 : location_info := LocationInfo file_0 225 16 225 19.
+ Definition loc_478 : location_info := LocationInfo file_0 225 16 225 19.
+ Definition loc_479 : location_info := LocationInfo file_0 225 17 225 19.
+ Definition loc_480 : location_info := LocationInfo file_0 225 17 225 19.
+ Definition loc_481 : location_info := LocationInfo file_0 224 4 224 12.
+ Definition loc_482 : location_info := LocationInfo file_0 224 15 224 24.
+ Definition loc_483 : location_info := LocationInfo file_0 224 15 224 24.
+ Definition loc_484 : location_info := LocationInfo file_0 224 15 224 18.
+ Definition loc_485 : location_info := LocationInfo file_0 224 15 224 18.
+ Definition loc_486 : location_info := LocationInfo file_0 223 8 223 29.
+ Definition loc_487 : location_info := LocationInfo file_0 223 8 223 11.
+ Definition loc_488 : location_info := LocationInfo file_0 223 8 223 11.
+ Definition loc_489 : location_info := LocationInfo file_0 223 15 223 29.
+ Definition loc_490 : location_info := LocationInfo file_0 213 15 213 17.
+ Definition loc_491 : location_info := LocationInfo file_0 213 15 213 17.
(* Definition of struct [list]. *)
Program Definition struct_list := {|
@@ -795,6 +821,53 @@ Section code.
)%E
|}.
+ (* Definition of function [length_val]. *)
+ Definition impl_length_val : function := {|
+ f_args := [
+ ("p", LPtr)
+ ];
+ f_local_vars := [
+ ("len", it_layout size_t)
+ ];
+ f_init := "#0";
+ f_code := (
+ <[ "#0" :=
+ "len" <-{ it_layout size_t }
+ LocInfoE loc_367 (UnOp (CastOp $ IntOp size_t) (IntOp i32) (LocInfoE loc_367 (i2v 0 i32))) ;
+ locinfo: loc_343 ;
+ Goto "#1"
+ ]> $
+ <[ "#1" :=
+ locinfo: loc_363 ;
+ if: LocInfoE loc_363 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_363 ((LocInfoE loc_364 (use{LPtr} (LocInfoE loc_365 ("p")))) !={PtrOp, PtrOp} (LocInfoE loc_366 (NULL)))))
+ then
+ locinfo: loc_349 ;
+ Goto "#2"
+ else
+ locinfo: loc_344 ;
+ Goto "#3"
+ ]> $
+ <[ "#2" :=
+ locinfo: loc_349 ;
+ LocInfoE loc_358 ("p") <-{ LPtr }
+ LocInfoE loc_359 (use{LPtr} (LocInfoE loc_360 ((LocInfoE loc_361 (!{LPtr} (LocInfoE loc_362 ("p")))) at{struct_list} "tail"))) ;
+ locinfo: loc_350 ;
+ LocInfoE loc_353 ("len") <-{ it_layout size_t }
+ LocInfoE loc_354 ((LocInfoE loc_355 (use{it_layout size_t} (LocInfoE loc_356 ("len")))) +{IntOp size_t, IntOp size_t} (LocInfoE loc_357 (UnOp (CastOp $ IntOp size_t) (IntOp i32) (LocInfoE loc_357 (i2v 1 i32))))) ;
+ locinfo: loc_351 ;
+ Goto "continue22"
+ ]> $
+ <[ "#3" :=
+ locinfo: loc_344 ;
+ Return (LocInfoE loc_345 (use{it_layout size_t} (LocInfoE loc_346 ("len"))))
+ ]> $
+ <[ "continue22" :=
+ locinfo: loc_343 ;
+ Goto "#1"
+ ]> $∅
+ )%E
+ |}.
+
(* Definition of function [append]. *)
Definition impl_append : function := {|
f_args := [
@@ -808,35 +881,35 @@ Section code.
f_code := (
<[ "#0" :=
"end" <-{ LPtr }
- LocInfoE loc_368 (use{LPtr} (LocInfoE loc_369 ("l1"))) ;
- locinfo: loc_343 ;
+ LocInfoE loc_398 (use{LPtr} (LocInfoE loc_399 ("l1"))) ;
+ locinfo: loc_373 ;
Goto "#1"
]> $
<[ "#1" :=
- locinfo: loc_362 ;
- if: LocInfoE loc_362 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_362 ((LocInfoE loc_363 (use{LPtr} (LocInfoE loc_365 (!{LPtr} (LocInfoE loc_366 ("end")))))) !={PtrOp, PtrOp} (LocInfoE loc_367 (NULL)))))
+ locinfo: loc_392 ;
+ if: LocInfoE loc_392 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_392 ((LocInfoE loc_393 (use{LPtr} (LocInfoE loc_395 (!{LPtr} (LocInfoE loc_396 ("end")))))) !={PtrOp, PtrOp} (LocInfoE loc_397 (NULL)))))
then
- locinfo: loc_352 ;
+ locinfo: loc_382 ;
Goto "#2"
else
- locinfo: loc_344 ;
+ locinfo: loc_374 ;
Goto "#3"
]> $
<[ "#2" :=
- locinfo: loc_352 ;
- LocInfoE loc_355 ("end") <-{ LPtr }
- LocInfoE loc_356 (&(LocInfoE loc_357 ((LocInfoE loc_358 (!{LPtr} (LocInfoE loc_360 (!{LPtr} (LocInfoE loc_361 ("end")))))) at{struct_list} "tail"))) ;
- locinfo: loc_353 ;
- Goto "continue22"
+ locinfo: loc_382 ;
+ LocInfoE loc_385 ("end") <-{ LPtr }
+ LocInfoE loc_386 (&(LocInfoE loc_387 ((LocInfoE loc_388 (!{LPtr} (LocInfoE loc_390 (!{LPtr} (LocInfoE loc_391 ("end")))))) at{struct_list} "tail"))) ;
+ locinfo: loc_383 ;
+ Goto "continue26"
]> $
<[ "#3" :=
- locinfo: loc_344 ;
- LocInfoE loc_346 (!{LPtr} (LocInfoE loc_347 ("end"))) <-{ LPtr }
- LocInfoE loc_348 (use{LPtr} (LocInfoE loc_349 ("l2"))) ;
+ locinfo: loc_374 ;
+ LocInfoE loc_376 (!{LPtr} (LocInfoE loc_377 ("end"))) <-{ LPtr }
+ LocInfoE loc_378 (use{LPtr} (LocInfoE loc_379 ("l2"))) ;
Return (VOID)
]> $
- <[ "continue22" :=
- locinfo: loc_343 ;
+ <[ "continue26" :=
+ locinfo: loc_373 ;
Goto "#1"
]> $∅
)%E
@@ -857,54 +930,54 @@ Section code.
f_code := (
<[ "#0" :=
"prev" <-{ LPtr }
- LocInfoE loc_420 (use{LPtr} (LocInfoE loc_421 ("p"))) ;
- locinfo: loc_375 ;
+ LocInfoE loc_450 (use{LPtr} (LocInfoE loc_451 ("p"))) ;
+ locinfo: loc_405 ;
Goto "#1"
]> $
<[ "#1" :=
- locinfo: loc_414 ;
- if: LocInfoE loc_414 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_414 ((LocInfoE loc_415 (use{LPtr} (LocInfoE loc_417 (!{LPtr} (LocInfoE loc_418 ("prev")))))) !={PtrOp, PtrOp} (LocInfoE loc_419 (NULL)))))
+ locinfo: loc_444 ;
+ if: LocInfoE loc_444 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_444 ((LocInfoE loc_445 (use{LPtr} (LocInfoE loc_447 (!{LPtr} (LocInfoE loc_448 ("prev")))))) !={PtrOp, PtrOp} (LocInfoE loc_449 (NULL)))))
then
Goto "#2"
else
- locinfo: loc_376 ;
+ locinfo: loc_406 ;
Goto "#3"
]> $
<[ "#2" :=
"cur" <-{ LPtr }
- LocInfoE loc_408 (use{LPtr} (LocInfoE loc_410 (!{LPtr} (LocInfoE loc_411 ("prev"))))) ;
+ LocInfoE loc_438 (use{LPtr} (LocInfoE loc_440 (!{LPtr} (LocInfoE loc_441 ("prev"))))) ;
"head" <-{ LPtr }
- LocInfoE loc_402 (UnOp (CastOp $ PtrOp) (PtrOp) (LocInfoE loc_402 (use{LPtr} (LocInfoE loc_403 ((LocInfoE loc_404 (!{LPtr} (LocInfoE loc_405 ("cur")))) at{struct_list} "head"))))) ;
- locinfo: loc_395 ;
- if: LocInfoE loc_395 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_395 ((LocInfoE loc_396 (use{it_layout size_t} (LocInfoE loc_398 (!{LPtr} (LocInfoE loc_399 ("head")))))) ={IntOp size_t, IntOp size_t} (LocInfoE loc_400 (use{it_layout size_t} (LocInfoE loc_401 ("k")))))))
+ LocInfoE loc_432 (UnOp (CastOp $ PtrOp) (PtrOp) (LocInfoE loc_432 (use{LPtr} (LocInfoE loc_433 ((LocInfoE loc_434 (!{LPtr} (LocInfoE loc_435 ("cur")))) at{struct_list} "head"))))) ;
+ locinfo: loc_425 ;
+ if: LocInfoE loc_425 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_425 ((LocInfoE loc_426 (use{it_layout size_t} (LocInfoE loc_428 (!{LPtr} (LocInfoE loc_429 ("head")))))) ={IntOp size_t, IntOp size_t} (LocInfoE loc_430 (use{it_layout size_t} (LocInfoE loc_431 ("k")))))))
then
- locinfo: loc_392 ;
+ locinfo: loc_422 ;
Goto "#5"
else
- locinfo: loc_383 ;
+ locinfo: loc_413 ;
Goto "#6"
]> $
<[ "#3" :=
- locinfo: loc_376 ;
- Return (LocInfoE loc_377 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_377 (i2v 0 i32))))
+ locinfo: loc_406 ;
+ Return (LocInfoE loc_407 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_407 (i2v 0 i32))))
]> $
<[ "#4" :=
- locinfo: loc_383 ;
- LocInfoE loc_386 ("prev") <-{ LPtr }
- LocInfoE loc_387 (&(LocInfoE loc_388 ((LocInfoE loc_389 (!{LPtr} (LocInfoE loc_390 ("cur")))) at{struct_list} "tail"))) ;
- locinfo: loc_384 ;
- Goto "continue26"
+ locinfo: loc_413 ;
+ LocInfoE loc_416 ("prev") <-{ LPtr }
+ LocInfoE loc_417 (&(LocInfoE loc_418 ((LocInfoE loc_419 (!{LPtr} (LocInfoE loc_420 ("cur")))) at{struct_list} "tail"))) ;
+ locinfo: loc_414 ;
+ Goto "continue30"
]> $
<[ "#5" :=
- locinfo: loc_392 ;
- Return (LocInfoE loc_393 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_393 (i2v 1 i32))))
+ locinfo: loc_422 ;
+ Return (LocInfoE loc_423 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_423 (i2v 1 i32))))
]> $
<[ "#6" :=
- locinfo: loc_383 ;
+ locinfo: loc_413 ;
Goto "#4"
]> $
- <[ "continue26" :=
- locinfo: loc_375 ;
+ <[ "continue30" :=
+ locinfo: loc_405 ;
Goto "#1"
]> $∅
)%E
@@ -924,40 +997,40 @@ Section code.
f_code := (
<[ "#0" :=
"cur" <-{ LPtr }
- LocInfoE loc_460 (use{LPtr} (LocInfoE loc_461 ("l1"))) ;
- locinfo: loc_427 ;
+ LocInfoE loc_490 (use{LPtr} (LocInfoE loc_491 ("l1"))) ;
+ locinfo: loc_457 ;
Goto "#1"
]> $
<[ "#1" :=
- locinfo: loc_456 ;
- if: LocInfoE loc_456 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_456 ((LocInfoE loc_457 (use{LPtr} (LocInfoE loc_458 ("cur")))) !={PtrOp, PtrOp} (LocInfoE loc_459 (NULL)))))
+ locinfo: loc_486 ;
+ if: LocInfoE loc_486 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_486 ((LocInfoE loc_487 (use{LPtr} (LocInfoE loc_488 ("cur")))) !={PtrOp, PtrOp} (LocInfoE loc_489 (NULL)))))
then
- locinfo: loc_430 ;
+ locinfo: loc_460 ;
Goto "#2"
else
Goto "#3"
]> $
<[ "#2" :=
- locinfo: loc_430 ;
- LocInfoE loc_451 ("cur_tail") <-{ LPtr }
- LocInfoE loc_452 (use{LPtr} (LocInfoE loc_453 ((LocInfoE loc_454 (!{LPtr} (LocInfoE loc_455 ("cur")))) at{struct_list} "tail"))) ;
- locinfo: loc_431 ;
- LocInfoE loc_444 ((LocInfoE loc_445 (!{LPtr} (LocInfoE loc_446 ("cur")))) at{struct_list} "tail") <-{ LPtr }
- LocInfoE loc_447 (use{LPtr} (LocInfoE loc_449 (!{LPtr} (LocInfoE loc_450 ("l2"))))) ;
- locinfo: loc_432 ;
- LocInfoE loc_440 (!{LPtr} (LocInfoE loc_441 ("l2"))) <-{ LPtr }
- LocInfoE loc_442 (use{LPtr} (LocInfoE loc_443 ("cur"))) ;
- locinfo: loc_433 ;
- LocInfoE loc_436 ("cur") <-{ LPtr }
- LocInfoE loc_437 (use{LPtr} (LocInfoE loc_438 ("cur_tail"))) ;
- locinfo: loc_434 ;
- Goto "continue33"
+ locinfo: loc_460 ;
+ LocInfoE loc_481 ("cur_tail") <-{ LPtr }
+ LocInfoE loc_482 (use{LPtr} (LocInfoE loc_483 ((LocInfoE loc_484 (!{LPtr} (LocInfoE loc_485 ("cur")))) at{struct_list} "tail"))) ;
+ locinfo: loc_461 ;
+ LocInfoE loc_474 ((LocInfoE loc_475 (!{LPtr} (LocInfoE loc_476 ("cur")))) at{struct_list} "tail") <-{ LPtr }
+ LocInfoE loc_477 (use{LPtr} (LocInfoE loc_479 (!{LPtr} (LocInfoE loc_480 ("l2"))))) ;
+ locinfo: loc_462 ;
+ LocInfoE loc_470 (!{LPtr} (LocInfoE loc_471 ("l2"))) <-{ LPtr }
+ LocInfoE loc_472 (use{LPtr} (LocInfoE loc_473 ("cur"))) ;
+ locinfo: loc_463 ;
+ LocInfoE loc_466 ("cur") <-{ LPtr }
+ LocInfoE loc_467 (use{LPtr} (LocInfoE loc_468 ("cur_tail"))) ;
+ locinfo: loc_464 ;
+ Goto "continue37"
]> $
<[ "#3" :=
Return (VOID)
]> $
- <[ "continue33" :=
- locinfo: loc_427 ;
+ <[ "continue37" :=
+ locinfo: loc_457 ;
Goto "#1"
]> $∅
)%E
diff --git a/tutorial/proofs/t03_list/generated_proof_length_val.v b/tutorial/proofs/t03_list/generated_proof_length_val.v
new file mode 100644
index 0000000000000000000000000000000000000000..39dbb4779bd773ffda0ae6675b9ba5a5caaca35f
--- /dev/null
+++ b/tutorial/proofs/t03_list/generated_proof_length_val.v
@@ -0,0 +1,34 @@
+From refinedc.typing Require Import typing.
+From refinedc.tutorial.t03_list Require Import generated_code.
+From refinedc.tutorial.t03_list Require Import generated_spec.
+Set Default Proof Using "Type".
+
+(* Generated from [tutorial/t03_list.c]. *)
+Section proof_length_val.
+ Context `{!typeG Σ} `{!globalG Σ}.
+
+ (* Typing proof for [length_val]. *)
+ Lemma type_length_val :
+ ⊢ typed_function impl_length_val type_of_length_val.
+ Proof.
+ start_function "length_val" ([v l]) => arg_p local_len.
+ split_blocks ((
+ <[ "#1" :=
+ ∃ v2 : val,
+ ∃ l1 : list type,
+ arg_p â—â‚— (own_constrained (nonshr_constraint (v2 â—áµ¥ l1 @ list_t)) (singleton_val (LPtr) (v2))) ∗
+ local_len â—â‚— ((length l - length l1) @ (int (size_t))) ∗
+ (v â—áµ¥ wand_val LPtr (v2 â—áµ¥ l1 @ list_t) (l @ list_t))
+ ]> $
+ ∅
+ )%I : gmap label (iProp Σ)) ((
+ ∅
+ )%I : gmap label (iProp Σ)).
+ - repeat liRStep; liShow.
+ all: print_typesystem_goal "length_val" "#0".
+ - repeat liRStep; liShow.
+ all: print_typesystem_goal "length_val" "#1".
+ Unshelve. all: sidecond_hook; prepare_sideconditions; normalize_and_simpl_goal; try solve_goal; unsolved_sidecond_hook.
+ all: print_sidecondition_goal "length_val".
+ Qed.
+End proof_length_val.
diff --git a/tutorial/proofs/t03_list/generated_spec.v b/tutorial/proofs/t03_list/generated_spec.v
index 15833f2767632d5f77a1a7bcea9e02700dc9901a..0b37edb7b389bbd5c1021e8dd8c1e5fa8ba6200d 100644
--- a/tutorial/proofs/t03_list/generated_spec.v
+++ b/tutorial/proofs/t03_list/generated_spec.v
@@ -132,6 +132,11 @@ Section spec.
fn(∀ (v, l) : val * (list type); (singleton_val (LPtr) (v)); (v â—áµ¥ l @ list_t) ∗ ⌜length l <= max_int size_tâŒ)
→ ∃ () : (), ((length l) @ (int (size_t))); (v â—áµ¥ l @ list_t).
+ (* Specifications for function [length_val]. *)
+ Definition type_of_length_val :=
+ fn(∀ (v, l) : val * (list type); (singleton_val (LPtr) (v)); (v â—áµ¥ l @ list_t) ∗ ⌜length l <= max_int size_tâŒ)
+ → ∃ () : (), ((length l) @ (int (size_t))); (v â—áµ¥ l @ list_t).
+
(* Specifications for function [append]. *)
Definition type_of_append :=
fn(∀ (p, l1, l2) : loc * (list type) * (list type); (p @ (&own (l1 @ (list_t)))), (l2 @ (list_t)); True)
diff --git a/tutorial/proofs/t03_list/proof_files b/tutorial/proofs/t03_list/proof_files
index 5ab37abd5cd8d4e8ad3045e4bbb8133af66c8180..6df08389f3f169174fc040bab5701c35771acb56 100644
--- a/tutorial/proofs/t03_list/proof_files
+++ b/tutorial/proofs/t03_list/proof_files
@@ -6,6 +6,7 @@ generated_proof_free_array.v
generated_proof_init.v
generated_proof_is_empty.v
generated_proof_length.v
+generated_proof_length_val.v
generated_proof_length_val_rec.v
generated_proof_member.v
generated_proof_pop.v
diff --git a/tutorial/t03_list.c b/tutorial/t03_list.c
index 410a504181277b7667d01edf213ad1b3ddf03b51..a086602d16eae08c950ad8c9b363e4e7c19ad366 100644
--- a/tutorial/t03_list.c
+++ b/tutorial/t03_list.c
@@ -110,6 +110,25 @@ size_t length_val_rec (list_t p) {
return length_val_rec(p->tail) + 1;
}
+[[rc::parameters("v : val", "l : {list type}")]]
+[[rc::args("singleton_val<LPtr, v>")]]
+[[rc::requires("[v â—áµ¥ l @ list_t]")]]
+[[rc::requires("{length l <= max_int size_t}")]]
+[[rc::returns("{length l} @ int<size_t>")]]
+[[rc::ensures("[v â—áµ¥ l @ list_t]")]] // TODO: there should be nicer syntax for this
+size_t length_val (list_t p) {
+ size_t len = 0;
+ [[rc::exists("v2 : val", "l1 : {list type}")]]
+ [[rc::inv_vars("p : own_constrained<nonshr_constraint<{v2 â—áµ¥ l1 @ list_t}>, singleton_val<LPtr, v2>>",
+ "len : {length l - length l1} @ int<size_t>")]]
+ [[rc::constraints("[v â—áµ¥ wand_val LPtr (v2 â—áµ¥ l1 @ list_t) (l @ list_t)]")]]
+ while (p != NULL) {
+ p = p->tail;
+ len += 1;
+ }
+ return len;
+}
+
[[rc::parameters("p : loc", "l1 : {list type}", "l2 : {list type}")]]
[[rc::args("p @ &own<l1 @ list_t>", "l2 @ list_t")]]
[[rc::ensures("p @ &own<{l1 ++ l2} @ list_t>")]]