Qcert.Translation.NRAEnvtoNNRC

Section NRAEnvtoNNRC.


  Context {fruntime:foreign_runtime}.

  Fixpoint nraenv_to_nnrc_ext (op:nraenv) (varid varenv:var) : nnrc :=
    match op with
    
    | NRAEnvID ⇒ NNRCVar varid
    
    | NRAEnvConst rd ⇒ NNRCConst rd
    
    | NRAEnvBinop bop op1 op2 ⇒
      NNRCBinop bop (nraenv_to_nnrc_ext op1 varid varenv) (nraenv_to_nnrc_ext op2 varid varenv)
    
    | NRAEnvUnop uop op1 ⇒
      NNRCUnop uop (nraenv_to_nnrc_ext op1 varid varenv)
    
    | NRAEnvMap op1 op2 ⇒
      let nrc2 := (nraenv_to_nnrc_ext op2 varid varenv) in
      let t := fresh_var "tmap$" (varid::varenv::nil) in
      NNRCFor t nrc2 (nraenv_to_nnrc_ext op1 t varenv)
    
    | NRAEnvMapConcat op1 op2 ⇒
      let nrc2 := (nraenv_to_nnrc_ext op2 varid varenv) in
      let (t1,t2) := fresh_var2 "tmc$" "tmc$" (varid::varenv::nil) in
      NNRCUnop AFlatten
              (NNRCFor t1 nrc2
                      (NNRCFor t2 (nraenv_to_nnrc_ext op1 t1 varenv)
                              ((NNRCBinop AConcat) (NNRCVar t1) (NNRCVar t2))))
    
    | NRAEnvProduct op1 op2 ⇒
      let nrc1 := (nraenv_to_nnrc_ext op1 varid varenv) in
      let nrc2 := (nraenv_to_nnrc_ext op2 varid varenv) in
      let (t1,t2) := fresh_var2 "tprod$" "tprod$" (varid::varenv::nil) in
      NNRCUnop AFlatten
              (NNRCFor t1 nrc1
                      (NNRCFor t2 nrc2
                              ((NNRCBinop AConcat) (NNRCVar t1) (NNRCVar t2))))
    
    | NRAEnvSelect op1 op2 ⇒
      let nrc2 := (nraenv_to_nnrc_ext op2 varid varenv) in
      let t := fresh_var "tsel$" (varid::varenv::nil) in
      let nrc1 := (nraenv_to_nnrc_ext op1 t varenv) in
      NNRCUnop AFlatten
              (NNRCFor t nrc2
                      (NNRCIf nrc1 (NNRCUnop AColl (NNRCVar t)) (NNRCConst (dcoll nil))))
    
    | NRAEnvDefault op1 op2 ⇒
      let nrc1 := (nraenv_to_nnrc_ext op1 varid varenv) in
      let nrc2 := (nraenv_to_nnrc_ext op2 varid varenv) in
      let t := fresh_var "tdef$" (varid::varenv::nil) in
      (NNRCLet t nrc1
              (NNRCIf (NNRCBinop AEq
                               (NNRCVar t)
                               (NNRCUnop AFlatten (NNRCConst (dcoll nil))))
                     nrc2 (NNRCVar t)))
    
    | NRAEnvEither opl opr ⇒
      let (t1,t2) := fresh_var2 "teitherL$" "teitherR$" (varid::varenv::nil) in
      let nrcl := (nraenv_to_nnrc_ext opl t1 varenv) in
      let nrcr := (nraenv_to_nnrc_ext opr t2 varenv) in
      NNRCEither (NNRCVar varid) t1 nrcl t2 nrcr
    | NRAEnvEitherConcat op1 op2 ⇒
      let nrc1 := (nraenv_to_nnrc_ext op1 varid varenv) in
      let nrc2 := (nraenv_to_nnrc_ext op2 varid varenv) in
      let t := fresh_var "tec$" (varid::varenv::nil) in
      NNRCLet t nrc2
             (NNRCEither nrc1 varid (NNRCUnop ALeft (NNRCBinop AConcat (NNRCVar varid) (NNRCVar t)))
                        varid (NNRCUnop ARight (NNRCBinop AConcat (NNRCVar varid) (NNRCVar t))))
    | NRAEnvApp op1 op2 ⇒
      let nrc2 := (nraenv_to_nnrc_ext op2 varid varenv) in
      let t := fresh_var "tapp$" (varid::varenv::nil) in
      let nrc1 := (nraenv_to_nnrc_ext op1 t varenv) in
      (NNRCLet t nrc2 nrc1)
    
    | NRAEnvGetConstant s ⇒ NNRCVar (append CONST_PREFIX s)
    
    | NRAEnvEnv ⇒ NNRCVar varenv
    
    | NRAEnvAppEnv op1 op2 ⇒
      let nrc2 := (nraenv_to_nnrc_ext op2 varid varenv) in
      let t := fresh_var "tappe$" (varid::varenv::nil) in
      let nrc1 := (nraenv_to_nnrc_ext op1 varid t) in
      (NNRCLet t nrc2 nrc1)
    
    | NRAEnvMapEnv op1 ⇒
      let t1 := fresh_var "tmape$" (varid::varenv::nil) in
      let nrc1 := (nraenv_to_nnrc_ext op1 varid t1) in
      (NNRCFor t1 (NNRCVar varenv) nrc1)
    
    | NRAEnvFlatMap op1 op2 ⇒
      let nrc2 := (nraenv_to_nnrc_ext op2 varid varenv) in
      let t := fresh_var "tmap$" (varid::varenv::nil) in
      NNRCUnop AFlatten (NNRCFor t nrc2 (nraenv_to_nnrc_ext op1 t varenv))
    | NRAEnvJoin op1 op2 op3 ⇒
      let nrc2 :=
          let nrc2 := (nraenv_to_nnrc_ext op2 varid varenv) in
          let nrc3 := (nraenv_to_nnrc_ext op3 varid varenv) in
          let (t2,t3) := fresh_var2 "tprod$" "tprod$" (varid::varenv::nil) in
          NNRCUnop AFlatten
                       (NNRCFor t2 nrc2
                                    (NNRCFor t3 nrc3
                                                 ((NNRCBinop AConcat) (NNRCVar t2) (NNRCVar t3))))
      in
      let t := fresh_var "tsel$" (varid::varenv::nil) in
      let nrc1 := (nraenv_to_nnrc_ext op1 t varenv) in
      NNRCUnop AFlatten
              (NNRCFor t nrc2
                      (NNRCIf nrc1 (NNRCUnop AColl (NNRCVar t)) (NNRCConst (dcoll nil))))
    | NRAEnvProject sl op1 ⇒
      let t := fresh_var "tmap$" (varid::varenv::nil) in
      NNRCFor t (nraenv_to_nnrc_ext op1 varid varenv) (NNRCUnop (ARecProject sl) (NNRCVar t))
    | NRAEnvGroupBy g sl op1 ⇒
      NNRCGroupBy g sl (nraenv_to_nnrc_ext op1 varid varenv)
    | NRAEnvUnnest a b op1 ⇒
      let nrc1 := (nraenv_to_nnrc_ext op1 varid varenv) in
      let (t1,t2) := fresh_var2 "tmc$" "tmc$" (varid::varenv::nil) in
      let nrc2 :=
          let t := fresh_var "tmap$" (varid::varenv::nil) in
          NNRCFor t (NNRCUnop (ADot a) (NNRCVar t1)) (NNRCUnop (ARec b) (NNRCVar t))
      in
      let nrc3 :=
          NNRCUnop AFlatten
                   (NNRCFor t1 nrc1
                            (NNRCFor t2 nrc2
                                     ((NNRCBinop AConcat) (NNRCVar t1) (NNRCVar t2))))
      in
      let nrc4 :=
          let t := fresh_var "tmap$" (varid::varenv::nil) in
          NNRCFor t nrc3 (NNRCUnop (ARecRemove a) (NNRCVar t))
      in
      nrc4
    end.


  Section negResult.
    Example nraenv_to_nnrc_codepaths_different vid venv:
      ∃ op,
        ¬ (nnrc_ext_to_nnrc (nraenv_to_nnrc_ext op vid venv)
           = cnraenv_to_nnrc (cnraenv_of_nraenv op) vid venv).
  End negResult.

  Lemma nnrc_core_eval_binop_eq h env b op1 op2 op1' op2' :
    nnrc_core_eval h env op1 = nnrc_core_eval h env op1' →
    nnrc_core_eval h env op2 = nnrc_core_eval h env op2' →
    nnrc_core_eval h env (NNRCBinop b op1 op2) =
    nnrc_core_eval h env (NNRCBinop b op1' op2').

  Lemma nnrc_core_eval_unop_eq h env u op1 op1' :
    nnrc_core_eval h env op1 = nnrc_core_eval h env op1' →
    nnrc_core_eval h env (NNRCUnop u op1) =
    nnrc_core_eval h env (NNRCUnop u op1').

  Lemma nnrc_core_eval_for_eq h env x op1 op2 op1' op2' :
      nnrc_core_eval h env op1 = nnrc_core_eval h env op1' →
      (∀ l,
          nnrc_core_eval h env op1 = Some (dcoll l) →
          ∀ d,
            In d l →
            nnrc_core_eval h ((x,d)::env) op2 = nnrc_core_eval h ((x,d)::env) op2') →
      nnrc_core_eval h env (NNRCFor x op1 op2) =
      nnrc_core_eval h env (NNRCFor x op1' op2').

  Lemma nnrc_core_eval_if_eq h env bop bop' op1 op2 op1' op2' :
    nnrc_core_eval h env bop = nnrc_core_eval h env bop' →
    nnrc_core_eval h env op1 = nnrc_core_eval h env op1' →
    nnrc_core_eval h env op2 = nnrc_core_eval h env op2' →
    nnrc_core_eval h env (NNRCIf bop op1 op2) =
    nnrc_core_eval h env (NNRCIf bop' op1' op2').

  Lemma nnrc_core_eval_let_eq h env x op1 op2 op1' op2' :
      nnrc_core_eval h env op1 = nnrc_core_eval h env op1' →
      (∀ d,
          nnrc_core_eval h env op1 = Some d →
            nnrc_core_eval h ((x,d)::env) op2 = nnrc_core_eval h ((x,d)::env) op2') →
      nnrc_core_eval h env (NNRCLet x op1 op2) =
      nnrc_core_eval h env (NNRCLet x op1' op2').

  Lemma nnrc_core_eval_either_eq h env x y eop eop' op1 op2 op1' op2' :
      nnrc_core_eval h env eop = nnrc_core_eval h env eop' →
      (∀ d,
          nnrc_core_eval h env eop = Some (dleft d) →
            nnrc_core_eval h ((x,d)::env) op1 = nnrc_core_eval h ((x,d)::env) op1') →
      (∀ d,
          nnrc_core_eval h env eop = Some (dright d) →
            nnrc_core_eval h ((y,d)::env) op2 = nnrc_core_eval h ((y,d)::env) op2') →
      nnrc_core_eval h env (NNRCEither eop x op1 y op2) =
      nnrc_core_eval h env (NNRCEither eop' x op1' y op2').

  Theorem nraenv_to_nnrc_codepaths_equivalent h env op vid venv:
    nnrc_core_eval h env (nnrc_ext_to_nnrc (nraenv_to_nnrc_ext op vid venv))
    = nnrc_core_eval h env (cnraenv_to_nnrc (cnraenv_of_nraenv op) vid venv).

  Theorem nraenv_sem_correct (h:list (string×string)) (op:nraenv) (env:bindings) (vid venv:var) dcenv (did denv:data) :
    prefix CONST_PREFIX vid = false →
    prefix CONST_PREFIX venv = false →
    vid ≠ venv →
    (∀ x,
        assoc_lookupr equiv_dec (mkConstants dcenv) x
        = lookup equiv_dec (filterConstants env) x) →
    lookup equiv_dec env vid = Some did →
    lookup equiv_dec env venv = Some denv →
    @nnrc_ext_eval _ h env (nraenv_to_nnrc_ext op vid venv) = nraenv_eval h dcenv op denv did.

  Lemma nraenv_to_nnrc_ext_no_free_vars (op: nraenv):
    ∀ (vid venv: var),
    ∀ v,
      In v (nnrc_free_vars (nraenv_to_nnrc_ext op vid venv)) →
      (prefix CONST_PREFIX v = true
      
      
      
      )
      ∨ v = vid ∨ v = venv.

  Section Top.
    Definition nraenv_to_nnrc_ext_top (q:nraenv) (init_vid init_venv:var) : nnrc :=
      NNRCLet init_venv (NNRCConst (drec nil))
             (NNRCLet init_vid (NNRCConst dunit)
                     (nraenv_to_nnrc_ext q init_vid init_venv)).
  End Top.

  Section size.


    Theorem nraenvToNNNRC_size op vid venv :
      nnrc_size (nraenv_to_nnrc_ext op vid venv) ≤ 14 × nraenv_size op.

  End size.

End NRAEnvtoNNRC.