Qcert.Translation.NNRCtoDNNRC

Section NNRCtoDNNRC.



  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) ∧
    ∀ 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).

  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.

  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)).

  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 →
    (∀ (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.

  Lemma nnrc_to_dnnrc_correct {A plug_type:Set} (annot:A) {plug:AlgPlug plug_type} h (tenv:list (var×dlocalization)) (n:nnrc) :
    ∀ 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).

  Context {ftype: ForeignType.foreign_type}.
  Definition nnrc_to_dnnrc_dataset {A:Set} (annot:A) (tenv:list (var×dlocalization)) (n:nnrc) := @nnrc_to_dnnrc A dataset annot (mkConstants tenv) n.

End NNRCtoDNNRC.