Module NNRCtoDNNRC
Section NNRCtoDNNRC.
Require Import String.
Require Import List.
Require Import Arith.
Require Import EquivDec.
Require Import Morphisms.
Require Import Utils.
Require Import BasicRuntime.
Require Import NNRCSystem.
Require Import DNNRCSystem.
Context {
fruntime:
foreign_runtime}.
Fixpoint nnrc_to_dnnrc {
A:
Set} {
plug_type:
Set} (
annot:
A) (
tenv:
list (
var*
dlocalization)) (
n:
nnrc) : @
dnnrc _ A plug_type :=
match n with
|
NNRCVar v =>
match lookup equiv_dec tenv v with
|
None =>
DNNRCVar annot v
|
Some Vlocal =>
DNNRCVar annot v
|
Some Vdistr =>
DNNRCCollect annot (
DNNRCVar annot v)
end
|
NNRCConst d =>
DNNRCConst annot d
|
NNRCBinop b n1 n2 =>
DNNRCBinop annot b (
nnrc_to_dnnrc annot tenv n1) (
nnrc_to_dnnrc annot tenv n2)
|
NNRCUnop u n1 =>
DNNRCUnop annot u (
nnrc_to_dnnrc annot tenv n1)
|
NNRCLet v n1 n2 =>
DNNRCLet annot v (
nnrc_to_dnnrc annot tenv n1) (
nnrc_to_dnnrc annot ((
v,
Vlocal)::
tenv)
n2)
|
NNRCFor v n1 n2 =>
DNNRCFor annot v (
nnrc_to_dnnrc annot tenv n1) (
nnrc_to_dnnrc annot ((
v,
Vlocal)::
tenv)
n2)
|
NNRCIf n1 n2 n3 =>
DNNRCIf annot (
nnrc_to_dnnrc annot tenv n1) (
nnrc_to_dnnrc annot tenv n2) (
nnrc_to_dnnrc annot tenv n3)
|
NNRCEither n0 v1 n1 v2 n2 =>
DNNRCEither annot (
nnrc_to_dnnrc annot tenv n0)
v1 (
nnrc_to_dnnrc annot ((
v1,
Vlocal)::
tenv)
n1)
v2 (
nnrc_to_dnnrc annot ((
v2,
Vlocal)::
tenv)
n2)
|
NNRCGroupBy g sl n1 =>
DNNRCGroupBy annot g sl (
nnrc_to_dnnrc annot tenv n1)
end.
Definition wf_localization (
tl:
option dlocalization) (
dl:
option ddata) :=
match tl,
dl with
|
Some Vlocal,
Some (
Dlocal _) =>
True
|
Some Vlocal,
Some (
Ddistr _) =>
False
|
Some Vdistr,
Some (
Ddistr _) =>
True
|
Some Vdistr,
Some (
Dlocal _) =>
False
|
_,
_ =>
False
end.
Definition wf_denv (
tenv:
list (
var*
dlocalization)) (
denv:
list (
var*
ddata)) :=
(
domain tenv =
domain denv) /\
forall v,
wf_localization (
lookup equiv_dec tenv v) (
lookup equiv_dec denv v).
Lemma wf_denv_cons v d tenv denv :
wf_denv tenv denv ->
wf_denv ((
v,
Vlocal) ::
tenv) ((
v,
Dlocal d) ::
denv).
Proof.
intros.
unfold wf_denv in *;
simpl.
elim H;
intros;
clear H.
split; [
rewrite H0;
reflexivity| ];
intros.
destruct (
equiv_dec v0 v).
-
reflexivity.
-
apply H1;
assumption.
Qed.
Lemma lookup_denv_local v d denv :
lookup equiv_dec denv v =
Some (
Dlocal d) ->
lift Dlocal (
lookup equiv_dec (
localize_denv denv)
v) =
lookup equiv_dec denv v.
Proof.
intros;
induction denv;
simpl in *; [
reflexivity| ].
destruct a;
simpl in *.
destruct (
equiv_dec v s);
try congruence.
-
rewrite e in *;
clear e.
inversion H;
subst;
clear H.
reflexivity.
-
apply (
IHdenv H).
Qed.
Lemma lookup_denv_distr v l denv :
lookup equiv_dec denv v =
Some (
Ddistr l) ->
lift Dlocal (
lookup equiv_dec (
localize_denv denv)
v) =
lift Dlocal (
olift checkDistrAndCollect (
lookup equiv_dec denv v)).
Proof.
intros.
induction denv; [
reflexivity| ];
simpl in *.
destruct a;
simpl in *.
destruct (
equiv_dec v s);
simpl in *.
-
inversion H;
subst;
reflexivity.
-
apply IHdenv.
apply H.
Qed.
Lemma rmap_nnrc_to_dnnrc_correct {
A:
Set} {
plug_type:
Set} {
plug:
AlgPlug plug_type} (
h:
brand_relation_t) (
annot:
A)
tenv denv v l n2 :
wf_denv tenv denv ->
(
forall (
tenv :
list (
var *
dlocalization))
(
denv :
list (
var *
ddata)),
wf_denv tenv denv ->
lift Dlocal (
nnrc_core_eval h (
localize_denv denv)
n2) =
dnnrc_eval h denv (
nnrc_to_dnnrc annot tenv n2)) ->
rmap
(
fun d1 :
data =>
olift checkLocal
(
dnnrc_eval h ((
v,
Dlocal d1) ::
denv)
(
nnrc_to_dnnrc annot ((
v,
Vlocal) ::
tenv)
n2)))
l =
rmap (
fun d1 :
data =>
nnrc_core_eval h ((
v,
d1) ::
localize_denv denv)
n2)
l.
Proof.
Global Arguments dnnrc :
clear implicits.
Lemma nnrc_to_dnnrc_correct {
A plug_type:
Set} (
annot:
A) {
plug:
AlgPlug plug_type}
h (
tenv:
list (
var*
dlocalization)) (
n:
nnrc) :
forall denv:
list (
var*
ddata),
wf_denv tenv denv ->
lift Dlocal (
nnrc_core_eval h (
localize_denv denv)
n) =
dnnrc_eval h denv (
nnrc_to_dnnrc annot tenv n).
Proof.
Section Top.
Require Import NRAEnvRuntime.
Require Import Dataframe.
Context {
ftype:
ForeignType.foreign_type}.
Definition nnrc_to_dnnrc_dataframe {
A:
Set} (
annot:
A) (
tenv:
vdbindings) (
n:
nnrc) :=
@
nnrc_to_dnnrc A dataframe annot (
mkConstants tenv)
n.
Definition nnrc_to_dnnrc_top (
tenv:
vdbindings) (
n:
nnrc) :
dnnrc_dataframe :=
nnrc_to_dnnrc_dataframe tt tenv n.
Theorem nnrc_to_dnnrc_top_correct h (
tenv:
vdbindings) (
n:
nnrc) :
forall denv:
dbindings,
wf_denv (
mkConstants tenv)
denv ->
lift Dlocal (
nnrc_core_eval h (
localize_denv denv)
n) =
dnnrc_eval h denv (
nnrc_to_dnnrc_top tenv n).
Proof.
End Top.
End NNRCtoDNNRC.