Commit 7fcdf0d5 authored by Xavier Denis's avatar Xavier Denis

Wip jugement definitions

parent 3b8b268c
......@@ -43,7 +43,7 @@ theories/typing/lft_contexts.v
theories/typing/uniq_cmra.v
theories/typing/type.v
theories/typing/type_context.v
# theories/typing/cont_context.v
theories/typing/cont_context.v
theories/typing/programs.v
# theories/typing/uninit.v
theories/typing/bool.v
......
From lrust.lang Require Import proofmode memcpy.
From lrust.typing Require Export type lft_contexts type_context.
From lrust.typing Require Export type lft_contexts type_context cont_context.
Set Default Proof Using "Type".
Section typing.
......@@ -7,15 +7,17 @@ Section typing.
(** Function Body *)
(* This is an iProp because it is also used by the function type. *)
(* Definition typed_body (E : elctx) (L : llctx) (C : cctx) (T : tctx)
(e : expr) : iProp Σ :=
(* recover the following type coontext from the continuation context! *)
Definition typed_body (E : elctx) (L : llctx) (C : cctx) (T : tctx)
(e : expr) : iProp Σ :=
( tid, lft_ctx - time_ctx - elctx_interp E - na_own tid - llctx_interp L 1 -
cctx_interp tid C - tctx_interp tid T -
(* ⟨ π, ? ⟩ -∗ *)
WP e {{ _, cont_postcondition }})%I.
Global Arguments typed_body _ _ _ _ _%E.
Global Instance typed_body_llctx_permut E :
Proper ((≡ₚ) ==> eq ==> eq ==> eq ==> (⊢)) (typed_body E).
Proper (() ==> eq ==> eq ==> eq ==> ()) (typed_body E).
Proof.
intros L1 L2 HL C ? <- T ? <- e ? <-. rewrite /typed_body.
by setoid_rewrite HL.
......@@ -42,7 +44,7 @@ Section typing.
Global Instance typed_body_mono_flip E L:
Proper (cctx_incl E ==> tctx_incl E L ==> eq ==> flip ())
(typed_body E L).
Proof. intros ?????????. by eapply typed_body_mono. Qed. *)
Proof. intros ?????????. by eapply typed_body_mono. Qed.
Definition extract_elt (π : proph_asn) (t : tctx_elt) : { t : Type & t} :=
match t with
......@@ -69,7 +71,11 @@ Section typing.
| [] => unit
end.
Definition cctx_elt_ty (c : cctx_elt) : Type :=
ctx_ty ( vs, c.(cctxe_T) vs).
(* TODO ideally [ty] => ty instead of ty * () *)
Fixpoint extract_tctx' (π : proph_asn) (t: tctx) : ctx_ty t :=
match t return ctx_ty t with
......@@ -83,7 +89,7 @@ Section typing.
List.map (extract_elt π) t. *)
(** Instruction *)
Notation tctxe := (list { t : Type & t}).
(* Notation tctxe := (list { t : Type & t}). *)
Notation pred_trans A B := ((B Prop) A Prop).
(* TODO correct the type of the post condition context... *)
Definition typed_instruction {A} (E : elctx) (L : llctx)
......@@ -91,7 +97,7 @@ Section typing.
( tid post, lft_ctx - time_ctx - elctx_interp E - na_own tid -
llctx_interp L 1 - tctx_interp tid T1 -
⟨π, pre post (extract_tctx' π T1) -
WP e {{ v, w, na_own tid π, post (w π, extract_tctx' π (T2))
WP e {{ v, w, na_own tid π, post (w π, extract_tctx' π T2)
llctx_interp L 1 tctx_elt_interp tid (r v w) tctx_interp tid (T2) }})%I.
Global Arguments typed_instruction _ _ _ _ _ _%E _ _.
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment