Commit a35bc4c0 authored by charguer's avatar charguer

cf_lifted_def

parent cf84cfd6
......@@ -44,13 +44,112 @@ Instance Enc_loc : Enc loc.
Proof using. constructor. applys val_loc. Defined.
Instance Enc_unit : Enc unit.
Proof using. constructor. applys (fun x:unit => val_unit). Defined.
Proof using. constructor. applys (fun (x:unit) => val_unit). Defined.
Instance Enc_int : Enc int.
Proof using. constructor. applys val_int. Defined.
Instance Enc_func : Enc func.
Proof using. constructor. applys (fun x:func => x). Defined.
Proof using. constructor. applys (fun (x:func) => x). Defined.
Instance Enc_val : Enc val.
Proof using. constructor. applys (fun (x:val) => x). Defined.
Instance Enc_prim : Enc prim.
Proof using. constructor. applys (fun (p:prim) => val_prim p). Defined.
Instance Enc_pair : forall A B, Enc A -> Enc B -> Enc (A*B).
Proof using.
constructor.
applys (fun (p:A*B) => val_pair (enc (fst p)) (enc (snd p))).
Defined.
(*------------------------------------------------------------------*)
(* ** Representation of values packed with their type and encoder *)
(** Representation of dependent pairs *)
Record dyn := Dyn {
dyn_type : Type;
dyn_enc : Enc dyn_type;
dyn_value : dyn_type }.
Implicit Arguments Dyn [dyn_type [dyn_enc]].
Lemma dyn_inj : forall A `{EA:Enc A} (x y : A),
Dyn x = Dyn y -> x = y.
Proof using. introv H. inverts~ H. Qed.
Lemma dyn_inj_type : forall A1 `{EA1:Enc A1} A2 `{EA2:Enc A2} (x1:A1) (x2:A2),
Dyn x1 = Dyn x2 -> A1 = A2.
Proof using. introv H. inverts~ H. Qed.
Lemma dyn_def : forall (d:dyn),
d = @Dyn _ (dyn_enc d) (dyn_value d).
Proof using. intros. destruct~ d. Qed.
(** Conversion of dyns to values *)
Definition dyn_val (d:dyn) :=
@enc _ (dyn_enc d) (dyn_value d).
Instance Enc_dyn : Enc dyn.
Proof using. constructor. applys dyn_val. Defined.
(* paragraphase of definition
Lemma enc_dyn_def : forall (d:dyn),
enc d = dyn_val d.
Proof using. auto. Qed.
*)
Lemma enc_dyn_def : forall (d:dyn),
enc d = @enc _ (dyn_enc d) (dyn_value d).
Proof using. auto. Qed.
(** List of dyns and encoder for lists *)
Definition dyns := list dyn.
Definition encs (ds:dyns) : list val :=
List.map dyn_val ds.
(*------------------------------------------------------------------*)
(* ** Decoder *)
Fixpoint decode (v:val) : dyn :=
match v with
| val_unit => Dyn tt
| val_int n => Dyn n
| val_pair v1 v2 =>
let d1 := decode v1 in
let d2 := decode v2 in
@Dyn _ (Enc_pair (dyn_enc d1) (dyn_enc d2))
(dyn_value d1, dyn_value d2)
| val_loc l => Dyn l
| val_prim p => Dyn p
| val_fix f xs t => Dyn (v:func)
| val_var x => Dyn v (* not meant to be used *)
end.
Lemma decode_encode : forall (v:val),
enc (decode v) = v.
Proof using.
intros. induction v; auto.
{ unfolds dyn_val. simpl. fequals. }
Qed.
Definition decodes (vs:vals) : dyns :=
List.map decode vs.
Definition decodes_encodes : forall (vs:vals),
encs (decodes vs) = vs.
Proof using.
intros. induction vs.
{ auto. }
{ simpl. fequals. applys decode_encode. }
Qed.
(*------------------------------------------------------------------*)
......@@ -104,40 +203,6 @@ Qed.
Hint Resolve PostEnc_himpl.
(*------------------------------------------------------------------*)
(* ** Representation of values packed with their type and encoder *)
(** Representation of dependent pairs *)
Record dyn := Dyn {
dyn_type : Type;
dyn_enc : Enc dyn_type;
dyn_value : dyn_type }.
Implicit Arguments Dyn [dyn_type [dyn_enc]].
Lemma dyn_inj : forall A `{EA:Enc A} (x y : A),
Dyn x = Dyn y -> x = y.
Proof using. introv H. inverts~ H. Qed.
Lemma dyn_inj_type : forall A1 `{EA1:Enc A1} A2 `{EA2:Enc A2} (x1:A1) (x2:A2),
Dyn x1 = Dyn x2 -> A1 = A2.
Proof using. introv H. inverts~ H. Qed.
Lemma dyn_def : forall (d:dyn),
d = @Dyn _ (dyn_enc d) (dyn_value d).
Proof using. intros. destruct~ d. Qed.
(** Conversion of dyns to values *)
Definition dyn_val (d:dyn) : val :=
@enc _ (dyn_enc d) (dyn_value d).
Definition dyns := list dyn.
Definition encs (ds:dyns) : list val :=
List.map dyn_val ds.
(*------------------------------------------------------------------*)
(* ** Lifting of substitution *)
......@@ -150,7 +215,7 @@ Notation "'fun' ''' ( x1 , x2 ) '=>' E" :=
(at level 200, format "'fun' ''' ( x1 , x2 ) '=>' E").
Definition Ctx_ctx (E:Ctx) :=
List.map (fun '(x,d) => (x,dyn_val d)) E.
List.map (fun '(x,d) => (x,enc d)) E.
Definition Subst_trm (E:list(var*dyn)) (t:trm) : trm :=
subst_trm (Ctx_ctx E) t.
......@@ -393,13 +458,37 @@ Ltac xlocal_core tt ::=
(*------------------------------------------------------------------*)
(* ** Definition of CF blocks *)
Inductive forced_decode : forall A `{EA:Enc A}, val -> (A -> Prop) -> Prop :=
| forced_decode_intro : forall v,
let d := decode v in
forall (K : dyn_type d -> Prop),
K (dyn_value d) ->
@forced_decode _ (dyn_enc d) v K.
Implicit Arguments forced_decode [A [EA]].
(** These auxiliary definitions give the characteristic formula
associated with each term construct. *)
Definition cf_val v : formula := fun `{Enc A} H (Q:A->hprop) =>
forced_decode v (fun (V:A) => H ==> Q V).
Definition cf_val' v : formula := fun `{Enc A} H (Q:A->hprop) =>
exists V, v = enc V /\ H ==> Q V.
Definition cf_if_val v (F1 F2 : formula) : formula := fun `{Enc A} H (Q:A->hprop) =>
(* DEPRECATED
Inductive cf_val'' v : formula :=
| cf_val_intro :
let d := decode v in
forall H (Q:(dyn_type d)->hprop),
@cf_val' v _ (dyn_enc d) H (fun x => \[x = dyn_value d] \* H).
*)
Definition cf_if_val v (F1 F2 : formula) : formula := fun `{EA:Enc A} H (Q:A->hprop) =>
forced_decode v (fun (V:int) =>
(V <> 0 -> 'F1 H Q) /\ (V = 0 -> 'F2 H Q)).
Definition cf_if_val' v (F1 F2 : formula) : formula := fun `{Enc A} H (Q:A->hprop) =>
exists (V:int), v = enc V /\
(V <> 0 -> 'F1 H Q) /\ (V = 0 -> 'F2 H Q).
......@@ -412,9 +501,12 @@ Definition cf_let (F1 : formula) (F2of : forall `{EA1:Enc A1}, A1 -> formula) :
Definition cf_if (F0 F1 F2 : formula) : formula :=
cf_let F0 (fun A1 EA1 X => cf_if_val (enc X) F1 F2).
Definition cf_app f vs : formula := fun `{Enc A} H (Q:A->hprop) =>
Definition cf_app' f vs : formula := fun `{Enc A} H (Q:A->hprop) =>
exists Vs, vs = encs Vs /\ app f Vs H Q.
Definition cf_app f vs : formula := fun `{Enc A} H (Q:A->hprop) =>
app f (decodes vs) H Q.
Definition cf_fix (F1of : func -> dyns -> formula) (F2of : func -> formula) : formula :=
fun `{Enc A} H (Q:A->hprop) =>
forall (F:val),
......
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