Commit 1e25cde7 authored by Ralf Jung's avatar Ralf Jung
Browse files

substitution stuff

parent 4be2ffb7
......@@ -48,40 +48,28 @@ Definition subst' (mx : binder) (es : expr) : expr → expr :=
Fixpoint subst_l (xl : list binder) (esl : list expr) (e : expr) : option expr :=
match xl, esl with
| [], [] => Some e
| x::xl, es::esl => subst' x es <$> subst_l xl esl e
| x::xl, es::esl => subst_l xl esl (subst' x es e)
| _, _ => None
end.
Arguments subst_l _%binder _ _%E.
Definition subst_v (xl : list binder) (vsl : vec result (length xl))
(e : expr) : expr :=
Vector.fold_right2 (λ b, subst' b of_result) e _ (list_to_vec xl) vsl.
Arguments subst_v _%binder _ _%E.
Lemma subst_v_eq (xl : list binder) (vsl : vec result (length xl)) e :
Some $ subst_v xl vsl e = subst_l xl (of_result <$> vec_to_list vsl) e.
Proof.
revert vsl. induction xl=>/= vsl; inv_vec vsl=>//=v vsl. by rewrite -IHxl.
Qed.
Lemma subst_l_is_Some xl el e :
length xl = length el is_Some (subst_l xl el e).
Proof.
revert el. induction xl as [|x xl IH] => el.
revert el e. induction xl as [|x xl IH] => el e.
{ destruct el; [by eexists|done]. }
destruct el as [|e1 el]; [done|].
rewrite /= /subst'. intros ?.
destruct (IH el) as [? Eq2]; [lia|]. rewrite Eq2 /=. by eexists.
eapply IH. congruence.
Qed.
Lemma subst_l_is_Some_length xl el e e' :
subst_l xl el e = Some e' length xl = length el.
Proof.
revert e' el. induction xl as [|x xl IH] => e' el; [by destruct el|].
revert e e' el. induction xl as [|x xl IH] => e e' el; [by destruct el|].
destruct el as [|e1 el]; [done|].
rewrite /= /subst'. intros Eq. f_equal.
destruct (subst_l xl el e) as [e2|] eqn:Eqs; [|done]. simplify_option_eq.
by apply (IH _ _ Eqs).
eapply IH. done.
Qed.
Lemma subst_l_nil_is_Some el e e' :
......
......@@ -200,3 +200,38 @@ Proof.
exists j. rewrite Eql. split; [|done]. rewrite lookup_app_l //.
rewrite reverse_length. lia.
Qed.
Lemma list_find_fmap {A B : Type} (P : A Prop) `{! x, Decision (P x)}
(f : B A) (l : list B) :
list_find P (f <$> l) = prod_map id f <$> list_find (P f) l.
Proof.
induction l as [|x y IH]; [done|]. simpl.
case_decide; [done|].
change (list_fmap B A f y) with (f <$> y). (* FIXME it simplified too much *)
rewrite IH. by destruct (list_find (P f) y).
Qed.
Lemma list_find_proper {A : Type} (P Q : A Prop)
`{ x, Decision (P x)} `{ x, Decision (Q x)} l :
( x, P x Q x)
list_find P l = list_find Q l.
Proof.
intros HPQ. induction l as [|x y IH]; [done|]. simpl.
erewrite decide_iff by done. by rewrite IH.
Qed.
Lemma list_fmap_omap {A B C : Type} (f : A option B) (g : B C) (l : list A) :
g <$> omap f l = omap (λ x, g <$> (f x)) l.
Proof.
induction l as [|x y IH]; [done|]. simpl.
destruct (f x); [|done]. simpl. by f_equal.
Qed.
Lemma omap_ext' {A B C : Type} (f : A option C) (g : B option C) l1 l2 :
Forall2 (λ a b, f a = g b) l1 l2
omap f l1 = omap g l2.
Proof.
induction 1 as [|x y l l' Hfg ? IH]; first done.
simpl. rewrite Hfg. destruct (g y); last done.
by f_equal.
Qed.
From stbor.lang Require Import expr_semantics.
(** Substitution with a *map*, for the reflexivity proof. *)
Fixpoint subst_map (xs : gmap string result) (e : expr) : expr :=
Definition is_var {T: Type} (y: string) (x: string * T) :=
x.1 = y.
Global Instance is_var_dec {T: Type} y x : Decision (@is_var T y x).
Proof. rewrite /is_var /=. apply _. Qed.
(** Substitution with a list of pairs instead of a pair of lists.
This lets us do a total operation. *)
Fixpoint subst_map (xs : list (string * result)) (e : expr) : expr :=
match e with
| Var y => if xs !! y is Some v then of_result v else Var y
| Var y => if list_find (is_var y) xs is Some (_, (_, v)) then of_result v else Var y
| Val v => Val v
(* | Rec f xl e =>
Rec f xl $ if bool_decide (BNamed x f BNamed x xl) then subst_map xs e else e *)
| Call e el => Call (subst_map xs e) (map (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
(* | App e1 el => App (subst_map xs e1) (map (subst_map xs) el) *)
| BinOp op e1 e2 => BinOp op (subst_map xs e1) (subst_map xs e2)
| Proj e1 e2 => Proj (subst_map xs e1) (subst_map xs e2)
| Conc e1 e2 => Conc (subst_map xs e1) (subst_map xs e2)
......@@ -25,6 +28,55 @@ Fixpoint subst_map (xs : gmap string result) (e : expr) : expr :=
| Let x1 e1 e2 =>
Let x1
(subst_map xs e1)
(subst_map (if x1 is BNamed s then delete s xs else xs) e2)
(subst_map (if x1 is BNamed s then list_filter (λ x, ¬is_var s x) _ xs else xs) e2)
| Case e el => Case (subst_map xs e) (map (subst_map xs) el)
end.
Lemma subst_map_empty e :
subst_map [] e = e.
Proof.
induction e; simpl; f_equal; eauto.
- admit.
- destruct x; done.
- admit.
Admitted.
Lemma subst_map_cons x rx xs e :
subst_map ((x,rx)::xs) e = subst_map xs (subst x rx e).
Proof.
revert x rx xs; induction e; intros xx rx xs; try (simpl; f_equal; eauto).
- destruct (decide (x=xx)) as [<-|ne].
+ rewrite decide_True //. rewrite bool_decide_true //.
destruct rx; done.
+ rewrite decide_False. { intros ?. apply ne. done. }
rewrite bool_decide_false //.
simpl. destruct (list_find (is_var x) xs); last done.
simpl. destruct p as [? [? ?]]. done.
- admit.
- destruct x; simpl. done.
destruct (decide (s=xx)) as [<-|ne].
+ rewrite decide_False //. { intros HH. apply HH. done. }
rewrite bool_decide_false //. intros ?. done.
+ rewrite decide_True //. { intros ?. apply ne. done. }
rewrite bool_decide_true //. intros [= HH]. done.
- admit.
Admitted.
Definition fn_lists_to_subst {T: Type} (xbs : list binder) (xes : list T) :=
omap (λ '(x, e), if x is BNamed s then Some (s, e) else None) (zip xbs xes).
Lemma subst_l_map (xbs : list binder) (xes : list value) (e es : expr) :
subst_l xbs (Val <$> xes) e = Some es
es = subst_map (fn_lists_to_subst xbs (ValR <$> xes)) e.
Proof.
revert xes es e; induction xbs; intros xes es e; destruct xes; try done.
- intros [= ->]. simpl.
by rewrite subst_map_empty.
- simpl.
set eo := subst_l _ _ _. destruct eo eqn:EQ; last done.
subst eo. intros [=<-].
specialize (IHxbs _ _ _ EQ).
destruct a.
+ done.
+ rewrite subst_map_cons. done.
Qed.
......@@ -59,12 +59,12 @@ Definition sem_post (r: resUR) (n: nat) rs css' rt cst': Prop :=
(** We define a "semantic well-formedness", in some context. *)
Definition sem_wf (r: resUR) es et :=
xs : gmap string (result * result),
map_Forall (λ _ '(rs, rt), rrel r rs rt) xs
xs : list (string * (result * result)),
Forall (λ '(_, (rs, rt)), rrel r rs rt) xs
r ⊨ˢ{sem_steps,fs,ft}
(subst_map (fst <$> xs) es, css)
(subst_map (prod_map id fst <$> xs) es, css)
(subst_map (snd <$> xs) et, cst)
(subst_map (prod_map id snd <$> xs) et, cst)
: sem_post.
Lemma value_wf_soundness r v :
......@@ -77,6 +77,13 @@ Proof.
+ apply IHv. done.
Qed.
Lemma list_find_var {A B : Type} x (f : A B) (xs : list (string * A)):
list_find (is_var x) (prod_map id f <$> xs) =
prod_map id (prod_map id f) <$> list_find (is_var x) xs.
Proof.
rewrite list_find_fmap. f_equal. apply list_find_proper. auto.
Qed.
Lemma expr_wf_soundness r e :
expr_wf e sem_wf r e e.
Proof.
......@@ -89,13 +96,13 @@ Proof.
apply value_wf_soundness. done.
- (* Variable *)
move=>{Hwf} xs Hxswf /=.
rewrite !lookup_fmap. specialize (Hxswf x).
destruct (xs !! x).
+ simpl. intros σs σt ??.
eapply sim_body_result=>_.
rewrite !list_find_var. destruct (list_find (is_var x) xs) eqn:Hfind; simpl.
+ destruct p as [i [x' [rs rt]]]. simpl.
destruct (list_find_Some _ _ _ _ Hfind).
intros σs σt ??. eapply sim_body_result=>_.
split; first admit.
split; first done. split; first done.
specialize (Hxswf p). destruct p. auto.
eapply (Forall_lookup_1 _ _ _ _ Hxswf H).
+ simpl.
(* FIXME: need lemma for when both sides are stuck on an unbound var. *)
admit.
......@@ -124,7 +131,29 @@ Proof.
- eexists. split. subst cst css. rewrite <-Hstacks. congruence.
admit. (* end_call_sat *)
- admit. (* need to show they are values?!? *)
}
}
rewrite (subst_l_map _ _ _ _ Hsubst1).
rewrite (subst_l_map _ _ _ _ Hsubst2).
set subst := fn_lists_to_subst (fun_args f) (zip (ValR <$> vs) (ValR <$> vt)).
replace (fn_lists_to_subst (fun_args f) (ValR <$> vs)) with (prod_map id fst <$> subst); last first.
{ rewrite /subst /fn_lists_to_subst. rewrite list_fmap_omap.
apply omap_ext'. revert Hrel. clear. revert vs vt.
induction (fun_args f); intros vs vt Hrel; simpl; first constructor.
inversion Hrel; simplify_eq/=; first constructor.
constructor. by destruct a. exact: IHl. }
replace (fn_lists_to_subst (fun_args f) (ValR <$> vt)) with (prod_map id snd <$> subst); last first.
{ rewrite /subst /fn_lists_to_subst. rewrite list_fmap_omap.
apply omap_ext'. revert Hrel. clear. revert vs vt.
induction (fun_args f); intros vs vt Hrel; simpl; first constructor.
inversion Hrel; simplify_eq/=; first constructor.
constructor. by destruct a. exact: IHl. }
eapply sim_simplify, expr_wf_soundness; [done..|].
subst subst. revert Hrel. clear. revert vs vt.
induction (fun_args f); intros vs vt Hrel; simpl; first constructor.
inversion Hrel; simplify_eq/=; first constructor.
destruct a; first exact: IHl. constructor.
{ admit. (* resource stuff. *) }
exact: IHl.
Admitted.
Lemma sim_mod_funs_refl prog :
......
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