Commit f24dab9d authored by Ralf Jung's avatar Ralf Jung

Proj and Case

parent fed183ec
......@@ -14,11 +14,11 @@ Fixpoint subst (x : string) (es : expr) (e : expr) : expr :=
| Val v => Val v
(* | Rec f xl e =>
Rec f xl $ if bool_decide (BNamed x f BNamed x xl) then subst x es e else e *)
| Call e el => Call (subst x es e) (map (subst x es) el)
| Call e el => Call (subst x es e) (fmap (subst x es) el)
| InitCall e => InitCall (subst x es e)
| EndCall e => EndCall (subst x es e)
| Place l tag T => Place l tag T
(* | App e1 el => App (subst x es e1) (map (subst x es) el) *)
(* | App e1 el => App (subst x es e1) (fmap (subst x es) el) *)
| BinOp op e1 e2 => BinOp op (subst x es e1) (subst x es e2)
| Proj e1 e2 => Proj (subst x es e1) (subst x es e2)
| Conc e1 e2 => Conc (subst x es e1) (subst x es e2)
......@@ -36,7 +36,7 @@ Fixpoint subst (x : string) (es : expr) (e : expr) : expr :=
| Let x1 e1 e2 =>
Let x1 (subst x es e1)
(if bool_decide (BNamed x x1) then subst x es e2 else e2)
| Case e el => Case (subst x es e) (map (subst x es) el)
| Case e el => Case (subst x es e) (fmap (subst x es) el)
(* | Fork e => Fork (subst x es e) *)
(* | SysCall id => SysCall id *)
end.
......
......@@ -314,7 +314,7 @@ Proof. intros EqN. destruct Ki; simplify_option_eq; eauto. Qed.
Lemma list_expr_result_eq_inv rl1 rl2 e1 e2 el1 el2 :
to_result e1 = None to_result e2 = None
map of_result rl1 ++ e1 :: el1 = map of_result rl2 ++ e2 :: el2
fmap of_result rl1 ++ e1 :: el1 = fmap of_result rl2 ++ e2 :: el2
rl1 = rl2 el1 = el2.
Proof.
revert rl2; induction rl1; destruct rl2; intros H1 H2; inversion 1.
......
......@@ -47,7 +47,7 @@ Fixpoint subst_map (xs : gmap string result) (e : expr) : expr :=
match e with
| Var y => if xs !! y is Some v then of_result v else Var y
| Val v => Val v
| Call e el => Call (subst_map xs e) (map (subst_map xs) el)
| Call e el => Call (subst_map xs e) (fmap (subst_map xs) el)
| InitCall e => InitCall (subst_map xs e)
| EndCall e => EndCall (subst_map xs e)
| Place l tag T => Place l tag T
......@@ -65,7 +65,7 @@ Fixpoint subst_map (xs : gmap string result) (e : expr) : expr :=
Let x1
(subst_map xs e1)
(subst_map (binder_delete x1 xs) e2)
| Case e el => Case (subst_map xs e) (map (subst_map xs) el)
| Case e el => Case (subst_map xs e) (fmap (subst_map xs) el)
end.
Lemma subst_map_empty e :
......
......@@ -5,7 +5,7 @@ Set Default Proof Using "Type".
(** Enable use of [Forall] in recursion. *)
Lemma Forall_id {A: Type} (P: A Prop) (l: list A) :
Forall P l Forall id (map P l).
Forall id (fmap P l) Forall P l.
Proof.
induction l; simpl; first by eauto using Forall_nil.
split; intros [??]%Forall_cons_1; apply Forall_cons; simpl; tauto.
......@@ -25,8 +25,8 @@ Fixpoint expr_wf (e: expr) : Prop :=
(* Structural cases. *)
| Var _ | Alloc _ => True
| Val v => value_wf v
| Call f args => expr_wf f Forall id (map expr_wf args)
| Case e branches => expr_wf e Forall id (map expr_wf branches)
| Call f args => expr_wf f Forall id (fmap expr_wf args)
| Case e branches => expr_wf e Forall id (fmap expr_wf branches)
| Deref e _ | Ref e | Copy e | Retag e _ =>
expr_wf e
| Proj e1 e2 | Conc e1 e2 | BinOp _ e1 e2 | Let _ e1 e2 | Write e1 e2 =>
......@@ -80,16 +80,29 @@ Proof.
eapply (Hrel _ _ Hlk).
Qed.
Lemma srel_frame_core r rf xs :
(core r rf) srel r xs srel (core r rf) xs.
Lemma srel_core_mono r rf xs:
srel r xs rf core r rf srel rf xs.
Proof.
move=>Hval /srel_persistent. apply: srel_mono; first done.
eexists. eauto.
intros Hrel%srel_persistent ??. eapply srel_mono; done.
Qed.
Lemma rrel_core_mono r rf r1 r2 :
rrel r r1 r2 rf core r rf rrel rf r1 r2.
Proof.
intros Hrel%rrel_persistent ??. eapply rrel_mono; done.
Qed.
Lemma arel_core_mono r rf a1 a2 :
arel r a1 a2 rf core r rf arel rf a1 a2.
Proof.
intros Hrel%arel_persistent ??. eapply arel_mono; done.
Qed.
(** Hints. *)
Local Hint Extern 0 (_ _) => exact: cmra_included_r : core. (* needs to be written like this to trump the reflexivity Hint. *)
Local Hint Resolve srel_frame_core.
Local Hint Extern 10 (srel _ _) => apply: srel_core_mono; first fast_done : core.
Local Hint Extern 10 (rrel _ _ _) => apply: rrel_core_mono; first fast_done : core.
Local Hint Extern 10 (arel _ _ _) => apply: arel_core_mono; first fast_done : core.
Local Hint Extern 50 (_ _) => solve_res : core.
(** We define a "semantic well-formedness", in some context. *)
Definition sem_steps := 10%nat.
......@@ -141,7 +154,22 @@ Proof.
admit.
- (* InitCall *) done.
- (* EndCall *) done.
- (* Proj *) admit.
- (* Proj *)
move=>[Hwf1 Hwf2] xs Hxs /=. sim_bind (subst_map _ e1) (subst_map _ e1).
eapply sim_simple_frame_core.
eapply sim_simple_post_mono, IHe1; [|by auto..].
intros r' n' rs css' rt cst' (-> & -> & -> & [Hrel ?]%rrel_with_eq) Hval.
simplify_eq/=. sim_bind (subst_map _ e2) (subst_map _ e2).
eapply sim_simple_frame_more_core.
eapply sim_simple_post_mono, IHe2; [|by auto..].
intros r'' n' rs' css' rt' cst' (-> & -> & -> & [Hrel' ?]%rrel_with_eq) Hval'.
simplify_eq/=. eapply sim_simple_proj; [done..|].
intros vi vv idx ?? Hidx ?. simplify_eq.
do 3 (split; first done).
move:Hrel=>/= /Forall2_lookup=>Hrel.
specialize (Hrel (Z.to_nat idx)).
rewrite Hidx in Hrel. inversion Hrel. simplify_eq/=.
constructor; last done. auto.
- (* Conc *) admit.
- (* BinOp *) admit.
- (* Place *) done.
......@@ -172,11 +200,23 @@ Proof.
change rs with (fst (rs, rt)). change rt with (snd (rs, rt)) at 2.
rewrite !binder_insert_map.
eapply IHe2; [by auto..|].
destruct b; first exact: srel_frame_core. simpl.
destruct b; first by auto. simpl.
apply map_Forall_insert_2.
+ eapply rrel_mono; eauto.
+ eapply srel_frame_core; eauto.
- (* Case *) admit.
+ eapply rrel_mono; last done; auto.
+ eapply srel_core_mono; eauto.
- (* Case *)
move=>[Hwf1 /Forall_id Hwf2] xs Hxs /=. sim_bind (subst_map _ e) (subst_map _ e).
eapply sim_simple_frame_core.
eapply sim_simple_post_mono, IHe; [|by auto..].
intros r' n' rs css' rt cst' (-> & -> & -> & [Hrel ?]%rrel_with_eq) Hval.
simplify_eq/=. eapply sim_simple_case.
{ rewrite !fmap_length //. }
intros es et ??. rewrite !list_lookup_fmap.
destruct (el !! Z.to_nat i) eqn:Hlk; last done.
intros. simplify_eq/=.
eapply (Forall_lookup_1 _ _ _ _ H Hlk).
+ eapply (Forall_lookup_1 _ _ _ _ Hwf2 Hlk).
+ eauto.
Admitted.
End sem.
......
......@@ -29,6 +29,18 @@ Notation "r ⊨ˢ{ n , fs , ft } ( es , css ) ≥ ( et , cst ) : Φ" :=
Section simple.
Implicit Types Φ: resUR nat result call_id_stack result call_id_stack Prop.
(* TODO: also allow rewriting the postcondition. *)
Global Instance sim_simple_proper fs ft :
Proper (() ==> (=) ==> (=) ==> (=) ==> (=) ==> (=) ==> (=) ==> ())
(sim_simple fs ft).
Proof.
intros r1 r2 EQr n ? <- es ? <- css ? <- et ? <- cst ? <- Φ ? <-.
split; intros HH σs σt ??.
- rewrite -EQr. exact: HH.
- rewrite EQr. exact: HH.
Qed.
Global Instance: Params sim_simple 2.
(* FIXME: does this [apply]? *)
Lemma sim_simplify
(Φnew: resUR nat result call_id_stack result call_id_stack Prop)
......@@ -54,6 +66,24 @@ Proof.
intros HΦ <-<-. eapply sim_simplify. done.
Qed.
Lemma sim_simple_frame_l Φ r rf n fs ft es css et cst :
r ⊨ˢ{ n , fs , ft }
(es, css) (et, cst)
: (λ r' n' es' css' et' cst', (rf r') Φ (rf r') n' es' css' et' cst')
rf r ⊨ˢ{ n , fs , ft } (es, css) (et, cst) : Φ.
Proof.
intros Hold σs σt <-<-. eapply sim_body_frame_l. auto.
Qed.
Lemma sim_simple_frame_r Φ r rf n fs ft es css et cst :
r ⊨ˢ{ n , fs , ft }
(es, css) (et, cst)
: (λ r' n' es' css' et' cst', (r' rf) Φ (r' rf) n' es' css' et' cst')
r rf ⊨ˢ{ n , fs , ft } (es, css) (et, cst) : Φ.
Proof.
intros Hold σs σt <-<-. eapply sim_body_frame_r. auto.
Qed.
Lemma sim_simple_frame_core Φ r n fs ft es css et cst :
r ⊨ˢ{ n , fs , ft }
(es, css) (et, cst)
......@@ -63,6 +93,19 @@ Proof.
intros Hold σs σt <-<-. eapply sim_body_frame_core. auto.
Qed.
Lemma sim_simple_frame_more_core Φ r r' n fs ft es css et cst :
core r r' ⊨ˢ{ n , fs , ft }
(es, css) (et, cst)
: (λ r'' n' es' css' et' cst', ((core r core r') r'') Φ ((core r core r') r'') n' es' css' et' cst')
core r r' ⊨ˢ{ n , fs , ft } (es, css) (et, cst) : Φ.
Proof.
intros HH. assert (core r r' (core r core r') (core r r')) as ->.
{ rewrite {1}cmra_core_dup. rewrite - !assoc. f_equiv.
rewrite [core r' _]comm - !assoc. f_equiv.
rewrite cmra_core_r //. }
eapply sim_simple_frame_l, HH.
Qed.
Lemma sim_simple_post_mono Φ1 Φ2 r n fs ft es css et cst :
Φ1 <6= Φ2
r ⊨ˢ{ n , fs , ft } (es, css) (et, cst) : Φ1
......@@ -254,12 +297,15 @@ Lemma sim_simple_var fs ft r n css cst var Φ :
r ⊨ˢ{n,fs,ft} (Var var, css) (Var var, cst) : Φ.
Proof. intros σs σt <-<-. apply sim_body_var; eauto. Qed.
Lemma sim_simple_proj fs ft r n (v i: result) css cst Φ :
( vi vv iv, v = ValR vv i = ValR [ScInt iv]
Lemma sim_simple_proj fs ft r n (v i: expr) (vr ir: result) css cst Φ :
v = of_result vr i = of_result ir
( vi vv iv, vr = ValR vv ir = ValR [ScInt iv]
vv !! (Z.to_nat iv) = Some vi 0 iv
Φ r n (ValR [vi]) css (ValR [vi]) cst)
r ⊨ˢ{n,fs,ft} (Proj v i, css) (Proj v i, cst) : Φ.
Proof. intros HH σs σt <-<-. apply sim_body_proj; eauto. Qed.
Proof.
intros ->-> HH σs σt <-<-. apply sim_body_proj; eauto.
Qed.
Lemma sim_simple_conc fs ft r n (r1 r2: result) css cst Φ :
( v1 v2, r1 = ValR v1 r2 = ValR v2
......@@ -267,4 +313,17 @@ Lemma sim_simple_conc fs ft r n (r1 r2: result) css cst Φ :
r ⊨ˢ{n,fs,ft} (Conc r1 r2, css) (Conc r1 r2, cst) : Φ.
Proof. intros HH σs σt <-<-. apply sim_body_conc; eauto. Qed.
Lemma sim_simple_case fs ft r n (rc: result) els elt css cst Φ :
length els = length elt
( (es et: expr) (i: Z), 0 i
els !! (Z.to_nat i) = Some es
elt !! (Z.to_nat i) = Some et
rc = ValR [ScInt i]
r ⊨ˢ{n,fs,ft} (es, css) (et, cst) : Φ)
r ⊨ˢ{n,fs,ft} (Case rc els, css) (Case rc elt, cst) : Φ.
Proof.
intros ? HH σs σt <-<-. apply sim_body_case; first done.
intros. eapply HH; eauto.
Qed.
End simple.
......@@ -4,37 +4,41 @@ From stbor.sim Require Import body.
Ltac reshape_expr e tac :=
(* [vs] is the accumulator *)
let rec go_list K Ki v vs es :=
let rec go_call K v vs es :=
match es with
| (Val ?v) :: ?es => go_list K v (v :: vs) es
| ?e :: ?es => go (Ki v (reverse vs) es :: K) e
| (Val ?v) :: ?es => go_call K v (v :: vs) es
| ?e :: ?es => go (CallRCtx v (reverse vs) es :: K) e
end
(* [K] accumulates the context *)
with go K e :=
match e with
| _ => tac K e
| Call (Val ?v) ?el => go_list K CallRCtx v (@nil val) el
| Call (Val ?v) ?el => go_call K (ValR v) (@nil val) el
| Call (of_result ?r) ?el => go_call K r (@nil val) el
| Call ?e ?el => go (CallLCtx el :: K) e
| EndCall ?e => go (EndCallCtx :: K) e
| BinOp ?op (Val ?v1) ?e2 => go (BinOpRCtx op v1 :: K) e2
| BinOp ?op (Val ?v1) ?e2 => go (BinOpRCtx op (ValR v1) :: K) e2
| BinOp ?op (of_result ?r) ?e2 => go (BinOpRCtx op r :: K) e2
| BinOp ?op ?e1 ?e2 => go (BinOpLCtx op e2 :: K) e1
| Proj (Val ?v1) ?e2 => go (ProjRCtx v1 :: K) e2
| Proj ?e1 ?e2 => go (ProjLCtx op e2 :: K) e1
| Conc (Val ?v1) ?e2 => go (ConcRCtx v1 :: K) e2
| Proj (Val ?v1) ?e2 => go (ProjRCtx (ValR v1) :: K) e2
| Proj (of_result ?r1) ?e2 => go (ProjRCtx r1 :: K) e2
| Proj ?e1 ?e2 => go (ProjLCtx e2 :: K) e1
| Conc (Val ?v1) ?e2 => go (ConcRCtx (ValR v1) :: K) e2
| Conc (of_result ?r1) ?e2 => go (ConcRCtx r1 :: K) e2
| Conc ?e1 ?e2 => go (ConcLCtx op e2 :: K) e1
| Copy ?e => go (CopyCtx :: K) e
| Write (Val ?v1) ?e2 => go (WriteRCtx v1 :: K) e2
| Write (Place ?l1 ?tg ?ty) ?e2 => go (WriteRCtx (PlaceR l1 tg ty) :: K) e2
| Write (of_result ?r1) ?e2 => go (WriteRCtx r1 :: K) e2
| Write ?e1 ?e2 => go (WriteLCtx op e2 :: K) e1
| Free ?e => go (FreeCtx :: K) e
| Deref ?e ?T => go (DerefCtx T :: K) e
| Ref ?e => go (RefCtx :: K) e
| Retag ?e ?k => go (RetagCtx k :: K) e
| Let ?x ?e1 ?e2 => go (LetCtx x e2 :: K) e1
| CaseCtx (Val ?v) ?el => go_list K CaseCtx v (@nil val) el
| Case ?e ?el => go (CaseCtx el :: K) e
end
in go (@nil ectx_item) e.
(** bind if K is not empty. Otherwise do nothing.
Binds cost us steps, so don't waste them! *)
Ltac sim_body_bind_core Ks Kt es et :=
......@@ -111,6 +115,12 @@ Proof. rewrite right_id //. Qed.
Lemma res_search_singleton (R W : resUR) :
W ε W.
Proof. rewrite left_id //. Qed.
Lemma res_search_from_incl (r1 r2 r3 : resUR) :
r2 r3 r1
r1 r2.
Proof.
intros EQ. eexists. rewrite EQ [r3 _]comm. done.
Qed.
Ltac solve_res :=
match goal with
| |- _ _ _ =>
......@@ -127,4 +137,7 @@ Ltac solve_res :=
an operator on the LHS. *)
simple apply res_search_descend;
solve_res
| |- _ _ =>
simple eapply res_search_from_incl;
solve_res
end.
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