From 0a18f1b8c020dcbb33e69444cb3522d610e7ec25 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Fri, 11 May 2018 20:07:31 +0200
Subject: [PATCH] Examples.
---
_CoqProject | 6 ++
theories/typing/examples/get_x.v | 23 +++++
theories/typing/examples/init_prod.v | 28 ++++++
theories/typing/examples/lazy_lft.v | 44 +++++++++
theories/typing/examples/nonlexical.v | 128 ++++++++++++++++++++++++++
theories/typing/examples/rebor.v | 36 ++++++++
theories/typing/examples/unbox.v | 24 +++++
7 files changed, 289 insertions(+)
create mode 100644 theories/typing/examples/get_x.v
create mode 100644 theories/typing/examples/init_prod.v
create mode 100644 theories/typing/examples/lazy_lft.v
create mode 100644 theories/typing/examples/nonlexical.v
create mode 100644 theories/typing/examples/rebor.v
create mode 100644 theories/typing/examples/unbox.v
diff --git a/_CoqProject b/_CoqProject
index 9d4134e7..a8156fdf 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -57,3 +57,9 @@ theories/typing/lib/refcell/ref_code.v
theories/typing/lib/refcell/refmut_code.v
theories/typing/lib/refcell/refmut.v
theories/typing/lib/refcell/ref.v
+theories/typing/examples/get_x.v
+theories/typing/examples/rebor.v
+theories/typing/examples/unbox.v
+theories/typing/examples/init_prod.v
+theories/typing/examples/lazy_lft.v
+theories/typing/examples/nonlexical.v
diff --git a/theories/typing/examples/get_x.v b/theories/typing/examples/get_x.v
new file mode 100644
index 00000000..53c49df0
--- /dev/null
+++ b/theories/typing/examples/get_x.v
@@ -0,0 +1,23 @@
+From lrust.typing Require Import typing.
+Set Default Proof Using "Type".
+
+Section get_x.
+ Context `{typeG Σ}.
+
+ Definition get_x : val :=
+ funrec: <> ["p"] :=
+ let: "p'" := !"p" in
+ letalloc: "r" <- "p'" +ₗ #0 in
+ delete [ #1; "p"] ;; return: ["r"].
+
+ Lemma get_x_type :
+ typed_val get_x (fn(∀ α, ∅; &uniq{α}(Π[int; int])) → &shr{α}int).
+ Proof.
+ intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros (α ϝ ret p).
+ inv_vec p=>p. simpl_subst.
+ iApply type_deref; [solve_typing..|]. iIntros (p'); simpl_subst.
+ iApply (type_letalloc_1 (&shr{α}int)); [solve_typing..|]. iIntros (r). simpl_subst.
+ iApply type_delete; [solve_typing..|].
+ iApply type_jump; solve_typing.
+ Qed.
+End get_x.
diff --git a/theories/typing/examples/init_prod.v b/theories/typing/examples/init_prod.v
new file mode 100644
index 00000000..ceb1feb0
--- /dev/null
+++ b/theories/typing/examples/init_prod.v
@@ -0,0 +1,28 @@
+From lrust.typing Require Import typing.
+Set Default Proof Using "Type".
+
+Section init_prod.
+ Context `{typeG Σ}.
+
+ Definition init_prod : val :=
+ funrec: <> ["x"; "y"] :=
+ let: "x'" := !"x" in let: "y'" := !"y" in
+ let: "r" := new [ #2] in
+ "r" +ₗ #0 <- "x'";; "r" +ₗ #1 <- "y'";;
+ delete [ #1; "x"] ;; delete [ #1; "y"] ;; return: ["r"].
+
+ Lemma init_prod_type : typed_val init_prod (fn(∅; int, int) → Π[int;int]).
+ Proof.
+ intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+ iIntros ([] ϝ ret p). inv_vec p=>x y. simpl_subst.
+ iApply type_deref; [solve_typing..|]. iIntros (x'). simpl_subst.
+ iApply type_deref; [solve_typing..|]. iIntros (y'). simpl_subst.
+ iApply (type_new_subtype (Π[uninit 1; uninit 1])); [solve_typing..|].
+ iIntros (r). simpl_subst. unfold Z.to_nat, Pos.to_nat; simpl.
+ iApply (type_assign (own_ptr 2 (uninit 1))); [solve_typing..|].
+ iApply type_assign; [solve_typing..|].
+ iApply type_delete; [solve_typing..|].
+ iApply type_delete; [solve_typing..|].
+ iApply type_jump; solve_typing.
+ Qed.
+End init_prod.
diff --git a/theories/typing/examples/lazy_lft.v b/theories/typing/examples/lazy_lft.v
new file mode 100644
index 00000000..54cd056f
--- /dev/null
+++ b/theories/typing/examples/lazy_lft.v
@@ -0,0 +1,44 @@
+From lrust.typing Require Import typing.
+Set Default Proof Using "Type".
+
+Section lazy_lft.
+ Context `{typeG Σ}.
+
+ Definition lazy_lft : val :=
+ funrec: <> [] :=
+ Newlft;;
+ let: "t" := new [ #2] in let: "f" := new [ #1] in let: "g" := new [ #1] in
+ let: "42" := #42 in "f" <- "42";;
+ "t" +ₗ #0 <- "f";; "t" +ₗ #1 <- "f";;
+ let: "t0'" := !("t" +ₗ #0) in "t0'";;
+ let: "23" := #23 in "g" <- "23";;
+ "t" +ₗ #1 <- "g";;
+ let: "r" := new [ #0] in
+ Endlft;; delete [ #2; "t"];; delete [ #1; "f"];; delete [ #1; "g"];; return: ["r"].
+
+ Lemma lazy_lft_type : typed_val lazy_lft (fn(∅) → unit).
+ Proof.
+ intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+ iIntros ([] ϝ ret p). inv_vec p. simpl_subst.
+ iApply (type_newlft []). iIntros (α).
+ iApply (type_new_subtype (Π[uninit 1;uninit 1])); [solve_typing..|].
+ iIntros (t). simpl_subst.
+ iApply type_new; [solve_typing..|]. iIntros (f). simpl_subst.
+ iApply type_new; [solve_typing..|]. iIntros (g). simpl_subst.
+ iApply type_int. iIntros (v42). simpl_subst.
+ iApply type_assign; [solve_typing..|].
+ iApply (type_assign _ (&shr{α}_)); [solve_typing..|].
+ iApply type_assign; [solve_typing..|].
+ iApply type_deref; [solve_typing..|]. iIntros (t0'). simpl_subst.
+ iApply type_letpath; [solve_typing|]. iIntros (dummy). simpl_subst.
+ iApply type_int. iIntros (v23). simpl_subst.
+ iApply type_assign; [solve_typing..|].
+ iApply (type_assign _ (&shr{α}int)); [solve_typing..|].
+ iApply type_new; [solve_typing..|]. iIntros (r). simpl_subst.
+ iApply type_endlft; [solve_typing..|].
+ iApply (type_delete (Π[&shr{α}_;&shr{α}_])%T); [solve_typing..|].
+ iApply type_delete; [solve_typing..|].
+ iApply type_delete; [solve_typing..|].
+ iApply type_jump; solve_typing.
+ Qed.
+End lazy_lft.
diff --git a/theories/typing/examples/nonlexical.v b/theories/typing/examples/nonlexical.v
new file mode 100644
index 00000000..91141690
--- /dev/null
+++ b/theories/typing/examples/nonlexical.v
@@ -0,0 +1,128 @@
+From lrust.typing Require Import typing lib.option.
+
+(* Typing "problem case #3" from:
+ http://smallcultfollowing.com/babysteps/blog/2016/04/27/non-lexical-lifetimes-introduction/
+
+ Differences with the original implementation:
+
+ We ignore dropping.
+ We have to add a Copy bound on the key type.
+ We do not support panic, hence we do not support option::unwrap. We use
+ unwrap_or as a replacement.
+*)
+
+Section non_lexical.
+ Context `{typeG Σ} (HashMap K V : type)
+ `{!TyWf hashmap, !TyWf K, !TyWf V, !Copy K}
+ (defaultv get_mut insert: val).
+
+ Hypothesis defaultv_type :
+ typed_val defaultv (fn(∅) → V).
+
+ Hypothesis get_mut_type :
+ typed_val get_mut (fn(∀ '(α, β), ∅; &uniq{α} hashmap, &shr{β} K) →
+ option (&uniq{α} V)).
+
+ Hypothesis insert_type :
+ typed_val insert (fn(∀ α, ∅; &uniq{α} hashmap, K, V) → option V).
+
+ Definition get_default : val :=
+ funrec: <> ["map"; "key"] :=
+ let: "get_mut" := get_mut in
+ let: "map'" := !"map" in
+
+ Newlft;;
+
+ Newlft;;
+ letalloc: "map0" <- "map'" in
+ letalloc: "key0" <- "key" in
+ letcall: "o" := "get_mut" ["map0"; "key0"]%E in
+ Endlft;;
+ withcont: "k":
+ case: !"o" of
+ [ (* None *)
+ Endlft;;
+
+ let: "insert" := insert in
+ Newlft;;
+ letalloc: "map0" <- "map'" in
+ letalloc: "key0" <-{K.(ty_size)} !"key" in
+ let: "defaultv" := defaultv in
+ letcall: "default0" := "defaultv" [] in
+ letcall: "old" := "insert" ["map0"; "key0"; "default0"]%E in
+ Endlft;;
+ delete [ #(option V).(ty_size); "old"];; (* We should drop here. *)
+
+ Newlft;;
+ letalloc: "map0" <- "map'" in
+ letalloc: "key0" <- "key" in
+ letcall: "r'" := "get_mut" ["map0"; "key0"]%E in
+ Endlft;;
+ let: "unwrap" := option_unwrap (&uniq{static}V) in
+ letcall: "r" := "unwrap" ["r'"]%E in
+ "k" ["r"];
+
+ (* Some *)
+ letalloc: "r" <-{1} !("o" +ₗ #1) in
+ "k" ["r"]
+ ]
+ cont: "k" ["r"] :=
+ delete [ #(option (&uniq{static}V)).(ty_size); "o"];;
+ delete [ #1; "map"];; delete [ #K.(ty_size); "key"];; (* We should drop key here *)
+ return: ["r"].
+
+ Lemma get_default_type :
+ typed_val get_default (fn(∀ m, ∅; &uniq{m} hashmap, K) → &uniq{m} V).
+ Proof.
+ intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+ iIntros (m ϝ ret p). inv_vec p=>map key. simpl_subst.
+ iApply type_let; [iApply get_mut_type|solve_typing|].
+ iIntros (get_mut'). simpl_subst.
+ iApply type_deref; [solve_typing..|]. iIntros (map'). simpl_subst.
+ iApply (type_newlft [m]). iIntros (κ).
+ iApply (type_newlft [ϝ]). iIntros (α).
+ iApply (type_letalloc_1 (&uniq{κ}_)); [solve_typing..|]. iIntros (map0). simpl_subst.
+ iApply (type_letalloc_1 (&shr{α}K)); [solve_typing..|]. iIntros (key0). simpl_subst.
+ iApply (type_letcall (κ, α)); [solve_typing..|]. iIntros (o). simpl_subst.
+ iApply type_endlft.
+ iApply (type_cont [_] [ϝ ⊑ₗ []]
+ (λ r, [o ◁ box (Π[uninit 1;uninit 1]); map ◁ box (uninit 1);
+ key ◁ box K; r!!!0 ◁ box (&uniq{m} V)])).
+ { iIntros (k). simpl_subst.
+ iApply type_case_own;
+ [solve_typing| constructor; [|constructor; [|constructor]]; left].
+ - iApply type_endlft.
+ iApply type_let; [iApply insert_type|solve_typing|].
+ iIntros (insert'). simpl_subst.
+ iApply (type_newlft [ϝ]). iIntros (β). clear map0 key0.
+ iApply (type_letalloc_1 (&uniq{β}_)); [solve_typing..|].
+ iIntros (map0). simpl_subst.
+ iApply (type_letalloc_n _(box K)); [solve_typing..|]. iIntros (key0). simpl_subst.
+ iApply type_let; [iApply defaultv_type|solve_typing|].
+ iIntros (defaultv'). simpl_subst.
+ iApply (type_letcall ()); [solve_typing..|]. iIntros (default0). simpl_subst.
+ iApply (type_letcall β); [solve_typing..|]. iIntros (old). simpl_subst.
+ iApply type_endlft.
+ iApply type_delete; [solve_typing..|].
+ iApply (type_newlft [ϝ]). iIntros (γ). clear map0 key0.
+ iApply (type_letalloc_1 (&uniq{m}_)); [solve_typing..|].
+ iIntros (map0). simpl_subst.
+ iApply (type_letalloc_1 (&shr{γ}K)); [solve_typing..|].
+ iIntros (key0). simpl_subst.
+ iApply (type_letcall (m, γ)); [solve_typing..|]. iIntros (r'). simpl_subst.
+ iApply type_endlft.
+ iApply type_let; [iApply (option_unwrap_type (&uniq{m}V))|solve_typing|].
+ iIntros (unwrap'). simpl_subst.
+ iApply (type_letcall ()); [solve_typing..|]. iIntros (r). simpl_subst.
+ iApply type_jump; solve_typing.
+ - iApply type_equivalize_lft.
+ iApply (type_letalloc_n (&uniq{m}V) (own_ptr _ (&uniq{m}V))); [solve_typing..|].
+ iIntros (r). simpl_subst.
+ iApply type_jump; solve_typing. }
+ iIntros "!# *". inv_vec args=>r. simpl_subst.
+ iApply type_delete; [solve_typing..|].
+ iApply type_delete; [solve_typing..|].
+ iApply type_delete; [solve_typing..|].
+ iApply type_jump; solve_typing.
+ Qed.
+End non_lexical.
diff --git a/theories/typing/examples/rebor.v b/theories/typing/examples/rebor.v
new file mode 100644
index 00000000..aeb0740c
--- /dev/null
+++ b/theories/typing/examples/rebor.v
@@ -0,0 +1,36 @@
+From lrust.typing Require Import typing.
+Set Default Proof Using "Type".
+
+Section rebor.
+ Context `{typeG Σ}.
+
+ Definition rebor : val :=
+ funrec: <> ["t1"; "t2"] :=
+ Newlft;;
+ letalloc: "x" <- "t1" in
+ let: "x'" := !"x" in let: "y" := "x'" +ₗ #0 in
+ "x" <- "t2";;
+ let: "y'" := !"y" in
+ letalloc: "r" <- "y'" in
+ Endlft ;; delete [ #2; "t1"] ;; delete [ #2; "t2"] ;;
+ delete [ #1; "x"] ;; return: ["r"].
+
+ Lemma rebor_type :
+ typed_val rebor (fn(∅; Π[int; int], Π[int; int]) → int).
+ Proof.
+ intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+ iIntros ([] ϝ ret p). inv_vec p=>t1 t2. simpl_subst.
+ iApply (type_newlft []). iIntros (α).
+ iApply (type_letalloc_1 (&uniq{α}(Π[int; int]))); [solve_typing..|]. iIntros (x). simpl_subst.
+ iApply type_deref; [solve_typing..|]. iIntros (x'). simpl_subst.
+ iApply (type_letpath (&uniq{α}int)); [solve_typing|]. iIntros (y). simpl_subst.
+ iApply (type_assign _ (&uniq{α}(Π[int; int]))); [solve_typing..|].
+ iApply type_deref; [solve_typing..|]. iIntros (y'). simpl_subst.
+ iApply type_letalloc_1; [solve_typing..|]. iIntros (r). simpl_subst.
+ iApply type_endlft.
+ iApply type_delete; [solve_typing..|].
+ iApply type_delete; [solve_typing..|].
+ iApply type_delete; [solve_typing..|].
+ iApply type_jump; solve_typing.
+ Qed.
+End rebor.
diff --git a/theories/typing/examples/unbox.v b/theories/typing/examples/unbox.v
new file mode 100644
index 00000000..302b7883
--- /dev/null
+++ b/theories/typing/examples/unbox.v
@@ -0,0 +1,24 @@
+From lrust.typing Require Import typing.
+Set Default Proof Using "Type".
+
+Section unbox.
+ Context `{typeG Σ}.
+
+ Definition unbox : val :=
+ funrec: <> ["b"] :=
+ let: "b'" := !"b" in let: "bx" := !"b'" in
+ letalloc: "r" <- "bx" +ₗ #0 in
+ delete [ #1; "b"] ;; return: ["r"].
+
+ Lemma ubox_type :
+ typed_val unbox (fn(∀ α, ∅; &uniq{α}(box(Π[int; int]))) → &uniq{α}int).
+ Proof.
+ intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+ iIntros (α ϝ ret b). inv_vec b=>b. simpl_subst.
+ iApply type_deref; [solve_typing..|]. iIntros (b'); simpl_subst.
+ iApply type_deref_uniq_own; [solve_typing..|]. iIntros (bx); simpl_subst.
+ iApply type_letalloc_1; [solve_typing..|]. iIntros (r). simpl_subst.
+ iApply type_delete; [solve_typing..|].
+ iApply type_jump; solve_typing.
+ Qed.
+End unbox.
--
GitLab