Skip to content
Snippets Groups Projects
Commit 19706709 authored by Ralf Jung's avatar Ralf Jung
Browse files
parents 62785d61 4e19edb8
No related branches found
No related tags found
No related merge requests found
Pipeline #
......@@ -47,4 +47,5 @@ theories/typing/tests/get_x.v
theories/typing/tests/rebor.v
theories/typing/tests/unbox.v
theories/typing/tests/init_prod.v
theories/typing/tests/option_as_mut.v
theories/typing/unsafe/cell.v
......@@ -41,10 +41,10 @@ Section specs.
Qed.
End specs.
(* FIXME : why are these notations not pretty-printed. *)
Notation "'letalloc:' x := e1 'in' e2" :=
(* FIXME : why are these notations not pretty-printed? *)
Notation "'letalloc:' x <- e1 'in' e2" :=
((Lam (@cons binder x%E%E%E nil) (x <- e1 ;; e2)) [new [ #1]])%E
(at level 102, x at level 1, e1, e2 at level 200) : expr_scope.
Notation "'letalloc:' x :={ n } ! e1 'in' e2" :=
Notation "'letalloc:' x <⋯ !{ n } e1 'in' e2" :=
((Lam (@cons binder x%E%E%E nil) (x <⋯ !{n%Z%V}e1 ;; e2)) [new [ #n]])%E
(at level 102, x at level 1, e1, e2 at level 200) : expr_scope.
......@@ -25,9 +25,9 @@ Notation "# l" := (Lit l%Z%V) (at level 8, format "# l") : expr_scope.
(** Syntax inspired by Coq/Ocaml. Constructions with higher precedence come
first. *)
Notation "'case:' e0 'of' el" := (Case e0%E el%E)
(at level 102, e0, el at level 200) : expr_scope.
(at level 102, e0, el at level 150) : expr_scope.
Notation "'if:' e1 'then' e2 'else' e3" := (If e1%E e2%E e3%E)
(at level 200, e1, e2, e3 at level 200) : expr_scope.
(only parsing, at level 200, e1, e2, e3 at level 150) : expr_scope.
Notation "()" := LitUnit : val_scope.
Notation "! e" := (Read Na1Ord e%E) (at level 9, format "! e") : expr_scope.
Notation "!ˢᶜ e" := (Read ScOrd e%E) (at level 9, format "!ˢᶜ e") : expr_scope.
......@@ -65,25 +65,25 @@ Notation "'funrec:' f xl := e" := (rec: f ("return"::xl) := e)%V
Notation "'let:' x := e1 'in' e2" :=
((Lam (@cons binder x%RustB nil) e2%E) (@cons expr e1%E nil))
(at level 102, x at level 1, e1, e2 at level 200) : expr_scope.
(at level 102, x at level 1, e1, e2 at level 150) : expr_scope.
Notation "e1 ;; e2" := (let: <> := e1 in e2)%E
(at level 100, e2 at level 200, format "e1 ;; e2") : expr_scope.
(at level 100, e2 at level 150, format "e1 ;; e2") : expr_scope.
(* These are not actually values, but we want them to be pretty-printed. *)
Notation "'let:' x := e1 'in' e2" :=
(LamV (@cons binder x%RustB nil) e2%E (@cons expr e1%E nil))
(at level 102, x at level 1, e1, e2 at level 200) : val_scope.
(at level 102, x at level 1, e1, e2 at level 150) : val_scope.
Notation "e1 ;; e2" := (let: <> := e1 in e2)%V
(at level 100, e2 at level 200, format "e1 ;; e2") : val_scope.
(at level 100, e2 at level 150, format "e1 ;; e2") : val_scope.
Notation "'letcont:' k xl := e1 'in' e2" :=
((Lam (@cons binder k%RustB nil) e2%E) [Rec k%RustB xl%RustB e1%E])
(only parsing, at level 102, k, xl at level 1, e1, e2 at level 200) : expr_scope.
Notation "e1 'cont:' k xl := e2" :=
((Lam (@cons binder k%RustB nil) e1%E) [Rec k%RustB xl%RustB e2%E])
(only parsing, at level 151, k, xl at level 1, e2 at level 150) : expr_scope.
Notation "'call:' f args → k" := (f (@cons expr k args))%E
(only parsing, at level 102, f, args, k at level 1) : expr_scope.
Notation "'letcall:' x := f args 'in' e" :=
(letcont: "_k" [ x ] := e in call: f args "_k")%E
(at level 102, x, f, args at level 1, e at level 200) : expr_scope.
(call: f args "_k" cont: "_k" [ x ] := e)%E
(at level 102, x, f, args at level 1, e at level 150) : expr_scope.
Notation "e1 <-{ i } '☇'" := (e1 <- #i)%E
(only parsing, at level 80) : expr_scope.
......
......@@ -19,14 +19,14 @@ Section typing.
rewrite -{3}(vec_to_list_of_list args). iApply ("HC" with "* Htl HL HT").
Qed.
Lemma type_cont argsb L1 T' E L2 C T econt e2 kb :
Lemma type_cont argsb L1 (T' : vec val (length argsb) _) E L2 C T econt e2 kb :
Closed (kb :b: argsb +b+ []) econt Closed (kb :b: []) e2
( k args, typed_body E L1 (k cont(L1, T') :: C) (T' args)
(subst_v (kb::argsb) (k:::args) econt))
( k, typed_body E L2 (k cont(L1, T') :: C) T (subst' kb k e2))
typed_body E L2 C T (letcont: kb argsb := econt in e2).
( k (args : vec val (length argsb)),
typed_body E L1 (k cont(L1, T') :: C) (T' args) (subst_v (kb::argsb) (k:::args) econt))
typed_body E L2 C T (e2 cont: kb argsb := econt).
Proof.
iIntros (Hc1 Hc2 Hecont He2) "!#". iIntros (tid qE) "#HEAP #LFT Htl HE HL HC HT". iApply wp_let'.
iIntros (Hc1 Hc2 He2 Hecont) "!#". iIntros (tid qE) "#HEAP #LFT Htl HE HL HC HT". iApply wp_let'.
{ simpl. rewrite decide_left. done. }
iModIntro. iApply (He2 with "* HEAP LFT Htl HE HL [HC] HT"). clear He2.
iIntros "HE". iLöb as "IH". iIntros (x) "H".
......
......@@ -231,9 +231,6 @@ Section typing.
+ by eapply is_closed_weaken, list_subseteq_nil.
+ eapply Is_true_eq_left, forallb_forall, List.Forall_forall, Forall_impl=>//.
intros. eapply Is_true_eq_true, is_closed_weaken=>//. set_solver+.
- intros k ret. inv_vec ret=>ret. rewrite /subst_v /=.
rewrite ->(is_closed_subst []), incl_cctx_incl; first done; try set_solver+.
apply subst'_is_closed; last done. apply is_closed_of_val.
- intros.
(* TODO : make [simpl_subst] work here. *)
change (subst' "_k" k (p (Var "_k" :: ps))) with
......@@ -242,6 +239,9 @@ Section typing.
assert (map (subst "_k" k) ps = ps) as ->.
{ clear -Hpsc. induction Hpsc=>//=. rewrite is_closed_nil_subst //. congruence. }
eapply type_call; try done. constructor. done.
- move=>/= k ret. inv_vec ret=>ret. rewrite /subst_v /=.
rewrite ->(is_closed_subst []), incl_cctx_incl; first done; try set_solver+.
apply subst'_is_closed; last done. apply is_closed_of_val.
Qed.
Lemma type_rec {A} E L E' fb (argsb : list binder) e
......
......@@ -444,8 +444,8 @@ Arguments elctx_incl {_ _ _} _%EL _%LL _%EL _%EL.
[tctx_extract_hasty] to suceed even if the type is an evar, and
merging makes it diverge in this case. *)
Ltac solve_typing :=
(eauto 100 with lrust_typing typeclass_instances; fail) ||
(eauto 100 with lrust_typing lrust_typing_merge typeclass_instances; fail).
(eauto 100 with lrust_typing typeclass_instances lia; fail) ||
(eauto 100 with lrust_typing lrust_typing_merge typeclass_instances lia; fail).
Create HintDb lrust_typing_merge.
Hint Constructors Forall Forall2 elem_of_list : lrust_typing.
......
......@@ -256,7 +256,7 @@ Section typing.
tctx_extract_hasty E L p ty T T'
ty.(ty_size) = 1%nat
( (v : val), typed_body E L C ((v own 1 ty)::T') (subst x v e))
typed_body E L C T (letalloc: x := p in e).
typed_body E L C T (letalloc: x <- p in e).
Proof.
intros. eapply type_new.
- rewrite /Closed /=. rewrite !andb_True.
......@@ -278,7 +278,7 @@ Section typing.
tctx_extract_hasty E L p ty1 T T'
( (v : val),
typed_body E L C ((v own (ty.(ty_size)) ty)::(p ty2)::T') (subst x v e))
typed_body E L C T (letalloc: x :={ty.(ty_size)} !p in e).
typed_body E L C T (letalloc: x <⋯ !{ty.(ty_size)}p in e).
Proof.
intros. eapply type_new.
- rewrite /Closed /=. rewrite !andb_True.
......
......@@ -235,6 +235,6 @@ End sum.
(* Σ is commonly used for the current functor. So it cannot be defined
as Π for products. We stick to the following form. *)
Notation "Σ[ ty1 ; .. ; tyn ]" :=
(sum (cons ty1 (..(cons tyn nil)..))) : lrust_typing.
(sum (cons ty1%T (..(cons tyn%T nil)..))) : lrust_type_scope.
Hint Resolve sum_mono' sum_proper' : lrust_typing.
......@@ -10,7 +10,7 @@ Section get_x.
Definition get_x : val :=
funrec: <> ["p"] :=
let: "p'" := !"p" in
letalloc: "r" := "p'" + #0 in
letalloc: "r" <- "p'" + #0 in
delete [ #1; "p"] ;; "return" ["r"].
Lemma get_x_type :
......
From lrust.lifetime Require Import definitions.
From lrust.lang Require Import new_delete.
From lrust.typing Require Import programs product product_split own uniq_bor
shr_bor int function lft_contexts uninit cont borrow type_sum.
Set Default Proof Using "Type".
Section option_as_mut.
Context `{typeG Σ}.
Definition option_as_mut :=
(funrec: <> ["o"] :=
let: "o'" := !"o" in case: !"o'" of
[ let: "r" := new [ #2 ] in "r" <-{0} ;;
"k" ["r"];
let: "r" := new [ #2 ] in "r" <-{1} "o'" + #1;;
"k" ["r"] ]
cont: "k" ["r"] :=
delete [ #1; "o"];; "return" ["r"])%E.
Lemma option_as_mut_type τ :
typed_instruction_ty [] [] [] option_as_mut
(fn (λ α, [α])%EL (λ α, [# own 1 (&uniq{α}Σ[unit; τ])])
(λ α, own 2 (Σ[unit; &uniq{α}τ]))).
Proof.
apply type_fn; try apply _. move=> /= α ret p. inv_vec p=>o. simpl_subst.
eapply (type_cont [_] [] (λ r, [o _; r!!!0 _])%TC) ; try solve_typing.
- intros k. simpl_subst.
eapply type_deref; try solve_typing; [apply read_own_move|done|]=>o'. simpl_subst.
eapply type_case_uniq; try solve_typing. constructor; last constructor; last constructor.
+ left. eapply type_new; try solve_typing. intros r. simpl_subst.
eapply (type_sum_assign_unit [unit; &uniq{α}τ]%T); try solve_typing. by apply write_own.
eapply (type_jump [_]); solve_typing.
+ left. eapply type_new; try solve_typing. intros r. simpl_subst.
eapply (type_sum_assign [unit; &uniq{α}τ]%T); try solve_typing. by apply write_own.
eapply (type_jump [_]); solve_typing.
- move=>/= k r. inv_vec r=>r. simpl_subst.
eapply type_delete; try solve_typing.
eapply (type_jump [_]); solve_typing.
Qed.
End option_as_mut.
......@@ -10,11 +10,11 @@ Section rebor.
Definition rebor : val :=
funrec: <> ["t1"; "t2"] :=
Newlft;;
letalloc: "x" := "t1" in
letalloc: "x" <- "t1" in
let: "x'" := !"x" in let: "y" := "x'" + #0 in
"x" <- "t2";;
let: "y'" := !"y" in
letalloc: "r" := "y'" in
letalloc: "r" <- "y'" in
Endlft ;; delete [ #2; "t1"] ;; delete [ #2; "t2"] ;;
delete [ #1; "x"] ;; "return" ["r"].
......
......@@ -10,7 +10,7 @@ Section unbox.
Definition unbox : val :=
funrec: <> ["b"] :=
let: "b'" := !"b" in let: "bx" := !"b'" in
letalloc: "r" := "bx" + #0 in
letalloc: "r" <- "bx" + #0 in
delete [ #1; "b"] ;; "return" ["r"].
Lemma ubox_type :
......
......@@ -151,12 +151,12 @@ Section case.
apply type_case_shr'; first done. eapply Forall2_impl; first done. auto.
Qed.
Lemma type_sum_assign {E L} (i : nat) tyl ty1 ty2 ty p1 p2 :
tyl !! i = Some ty
Lemma type_sum_assign_instr {E L} (i : nat) ty1 tyl ty ty2 p1 p2 :
typed_write E L ty1 (sum tyl) ty2
tyl !! i = Some ty
typed_instruction E L [p1 ty1; p2 ty] (p1 <-{i} p2) (λ _, [p1 ty2]%TC).
Proof.
iIntros (Hty Hw) "!# * #HEAP #LFT $ HE HL Hp".
iIntros (Hw Hty) "!# * #HEAP #LFT $ HE HL Hp".
rewrite tctx_interp_cons tctx_interp_singleton.
iDestruct "Hp" as "[Hp1 Hp2]". iDestruct (closed_hasty with "Hp1") as "%".
iDestruct (closed_hasty with "Hp2") as "%". wp_bind p1.
......@@ -178,7 +178,20 @@ Section case.
iExists i, [_], _. rewrite -Hlen nth_lookup Hty. auto.
Qed.
Lemma type_sum_assign_unit {E L} (i : nat) tyl ty1 ty2 p :
Lemma type_sum_assign {E L} tyl i ty1 ty ty1' C T T' p1 p2 e:
Closed [] e
0 i
tctx_extract_ctx E L [p1 ty1; p2 ty] T T'
typed_write E L ty1 (sum tyl) ty1'
tyl !! (Z.to_nat i) = Some ty
typed_body E L C ((p1 ty1') :: T') e
typed_body E L C T (p1 <-{i} p2 ;; e).
Proof.
intros. rewrite -(Z2Nat.id i) //.
eapply type_seq; [done|by eapply type_sum_assign_instr|done|done].
Qed.
Lemma type_sum_assign_unit_instr {E L} (i : nat) tyl ty1 ty2 p :
tyl !! i = Some unit
typed_write E L ty1 (sum tyl) ty2
typed_instruction E L [p ty1] (p <-{i} ) (λ _, [p ty2]%TC).
......@@ -193,7 +206,20 @@ Section case.
iExists i, [], _. rewrite -Hlen nth_lookup Hty. auto.
Qed.
Lemma type_sum_memcpy {E L} (i : nat) tyl ty1 ty1' ty2 ty2' ty p1 p2 :
Lemma type_sum_assign_unit {E L} tyl i ty1 ty1' C T T' p e:
Closed [] e
0 i
tctx_extract_hasty E L p ty1 T T'
typed_write E L ty1 (sum tyl) ty1'
tyl !! (Z.to_nat i) = Some unit
typed_body E L C ((p ty1') :: T') e
typed_body E L C T (p <-{i} ;; e).
Proof.
intros. rewrite -(Z2Nat.id i) //.
eapply type_seq; [done|by eapply type_sum_assign_unit_instr|solve_typing|done].
Qed.
Lemma type_sum_memcpy_instr {E L} (i : nat) tyl ty1 ty1' ty2 ty2' ty p1 p2 :
tyl !! i = Some ty
typed_write E L ty1 (sum tyl) ty1'
typed_read E L ty2 ty ty2'
......@@ -230,4 +256,19 @@ Section case.
iExists _. iFrame. rewrite /= drop_length. iPureIntro. lia.
- iExists _. iFrame.
Qed.
Lemma type_sum_assign_memcpy {E L} tyl i ty1 ty2 ty n ty1' ty2' C T T' p1 p2 e:
Closed [] e
0 i
tctx_extract_ctx E L [p1 ty1; p2 ty2] T T'
typed_write E L ty1 (sum tyl) ty1'
typed_read E L ty2 ty ty2'
Z.of_nat (ty.(ty_size)) = n
tyl !! (Z.to_nat i) = Some ty
typed_body E L C ((p1 ty1') :: (p2 ty2') :: T') e
typed_body E L C T (p1 <⋯{i} !{n}p2 ;; e).
Proof.
intros ???? Hr ???. subst. rewrite -(Z2Nat.id i) //.
by eapply type_seq; [done|eapply type_sum_memcpy_instr, Hr|done|done].
Qed.
End case.
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment