Qcert.Translation.cNRAEnvtocNNRC


Section cNRAEnvtocNNRC.


  Context {fruntime:foreign_runtime}.

Translation from NRA+Env to Named Nested Relational Calculus
  Fixpoint cnraenv_to_nnrc (op:cnraenv) (varid varenv:var) : nnrc :=
    match op with
      
      | ANID ⇒ NNRCVar varid
      
      | ANConst rd ⇒ NNRCConst rd
      
      | ANBinop bop op1 op2 ⇒
        NNRCBinop bop (cnraenv_to_nnrc op1 varid varenv) (cnraenv_to_nnrc op2 varid varenv)
      
      | ANUnop uop op1 ⇒
        NNRCUnop uop (cnraenv_to_nnrc op1 varid varenv)
      
      | ANMap op1 op2 ⇒
        let nnrc2 := (cnraenv_to_nnrc op2 varid varenv) in
        let t := fresh_var "tmap$" (varid::varenv::nil) in
        NNRCFor t nnrc2 (cnraenv_to_nnrc op1 t varenv)
      
      | ANMapConcat op1 op2 ⇒
        let nnrc2 := (cnraenv_to_nnrc op2 varid varenv) in
        let (t1,t2) := fresh_var2 "tmc$" "tmc$" (varid::varenv::nil) in
        NNRCUnop AFlatten
                (NNRCFor t1 nnrc2
                        (NNRCFor t2 (cnraenv_to_nnrc op1 t1 varenv)
                                ((NNRCBinop AConcat) (NNRCVar t1) (NNRCVar t2))))
      
      | ANProduct op1 op2 ⇒
        let nnrc1 := (cnraenv_to_nnrc op1 varid varenv) in
        let nnrc2 := (cnraenv_to_nnrc op2 varid varenv) in
        let (t1,t2) := fresh_var2 "tprod$" "tprod$" (varid::varenv::nil) in
        NNRCUnop AFlatten
                (NNRCFor t1 nnrc1
                        (NNRCFor t2 nnrc2
                                ((NNRCBinop AConcat) (NNRCVar t1) (NNRCVar t2))))
      
      | ANSelect op1 op2 ⇒
        let nnrc2 := (cnraenv_to_nnrc op2 varid varenv) in
        let t := fresh_var "tsel$" (varid::varenv::nil) in
        let nnrc1 := (cnraenv_to_nnrc op1 t varenv) in
        NNRCUnop AFlatten
                (NNRCFor t nnrc2
                        (NNRCIf nnrc1 (NNRCUnop AColl (NNRCVar t)) (NNRCConst (dcoll nil))))
      
      | ANDefault op1 op2 ⇒
        let nnrc1 := (cnraenv_to_nnrc op1 varid varenv) in
        let nnrc2 := (cnraenv_to_nnrc op2 varid varenv) in
        let t := fresh_var "tdef$" (varid::varenv::nil) in
        (NNRCLet t nnrc1
                (NNRCIf (NNRCBinop AEq
                                 (NNRCVar t)
                                 (NNRCUnop AFlatten (NNRCConst (dcoll nil))))
                       nnrc2 (NNRCVar t)))
      
      | ANEither opl opr ⇒
        let (t1,t2) := fresh_var2 "teitherL$" "teitherR$" (varid::varenv::nil) in
        let nnrcl := (cnraenv_to_nnrc opl t1 varenv) in
        let nnrcr := (cnraenv_to_nnrc opr t2 varenv) in
        NNRCEither (NNRCVar varid) t1 nnrcl t2 nnrcr
      | ANEitherConcat op1 op2 ⇒
        let nnrc1 := (cnraenv_to_nnrc op1 varid varenv) in
        let nnrc2 := (cnraenv_to_nnrc op2 varid varenv) in
        let t := fresh_var "tec$" (varid::varenv::nil) in
        NNRCLet t nnrc2
        (NNRCEither nnrc1 varid (NNRCUnop ALeft (NNRCBinop AConcat (NNRCVar varid) (NNRCVar t)))
                  varid (NNRCUnop ARight (NNRCBinop AConcat (NNRCVar varid) (NNRCVar t))))
      | ANApp op1 op2 ⇒
        let nnrc2 := (cnraenv_to_nnrc op2 varid varenv) in
        let t := fresh_var "tapp$" (varid::varenv::nil) in
        let nnrc1 := (cnraenv_to_nnrc op1 t varenv) in
        (NNRCLet t nnrc2 nnrc1)
      
      | ANGetConstant s ⇒ NNRCVar (append CONST_PREFIX s)
      
      | ANEnv ⇒ NNRCVar varenv
      
      | ANAppEnv op1 op2 ⇒
        let nnrc2 := (cnraenv_to_nnrc op2 varid varenv) in
        let t := fresh_var "tappe$" (varid::varenv::nil) in
        let nnrc1 := (cnraenv_to_nnrc op1 varid t) in
        (NNRCLet t nnrc2 nnrc1)
      
      | ANMapEnv op1 ⇒
        let t1 := fresh_var "tmape$" (varid::varenv::nil) in
        let nnrc1 := (cnraenv_to_nnrc op1 varid t1) in
        (NNRCFor t1 (NNRCVar varenv) nnrc1)
    end.

Auxiliary lemmas used in the proof of correctness for the translation

  Lemma map_sem_correct (h:list (string×string)) (op:cnraenv) dcenv (denv:data) (l:list data) (env:bindings) (vid venv:var):
    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 venv = Some denv →
    (∀ cenv (did denv : data) (env : bindings) (vid venv : var),
    prefix CONST_PREFIX vid = false →
    prefix CONST_PREFIX venv = false →
    vid ≠ venv →
    (∀ x,
        assoc_lookupr equiv_dec (mkConstants cenv) x
        = lookup equiv_dec (filterConstants env) x) →
      lookup equiv_dec env vid = Some did →
       lookup equiv_dec env venv = Some denv →
       nnrc_core_eval h env (cnraenv_to_nnrc op vid venv) = (cnraenv_eval h cenv op denv did)) →
    rmap
      (fun x : data ⇒
         nnrc_core_eval h ((vid, x) :: env) (cnraenv_to_nnrc op vid venv)) l
    =
    rmap (cnraenv_eval h dcenv op denv) l.

Theorem 5.2: proof of correctness for the translation


  Theorem nraenv_sem_correct (h:list (string×string)) (op:cnraenv) (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_core_eval h env (cnraenv_to_nnrc op vid venv) = h ⊢ₑ op @ₑ did ⊣ dcenv;denv.


  Lemma cnraenv_to_nnrc_no_free_vars (op: cnraenv):
    ∀ (vid venv: var),
    ∀ v,
      In v (nnrc_free_vars (cnraenv_to_nnrc op vid venv)) →
      (prefix CONST_PREFIX v = true
      
      
      
      )
      ∨ v = vid ∨ v = venv.

  Section Top.
    Definition cnraenv_to_nnrc_top (q:cnraenv) (init_vid init_venv:var) : nnrc :=
      NNRCLet init_venv (NNRCConst (drec nil))
             (NNRCLet init_vid (NNRCConst dunit)
                     (cnraenv_to_nnrc q init_vid init_venv)).
  End Top.

Lemma and proof of linear size translation

  Section size.


  Theorem cnraenvToNNRC_size op vid venv :
    nnrc_size (cnraenv_to_nnrc op vid venv) ≤ 10 × cnraenv_size op.

  End size.

End cNRAEnvtocNNRC.