Qcert.Translation.NRAtocNNRC

Section NRAtocNNRC.


  Context {fruntime:foreign_runtime}.

  Fixpoint nra_to_nnrc (op:nra) (var:var) : nnrc :=
    match op with
      
      | AID ⇒ NNRCVar var
      
      | AConst rd ⇒ NNRCConst rd
      
      | ABinop bop op1 op2 ⇒
        NNRCBinop bop (nra_to_nnrc op1 var) (nra_to_nnrc op2 var)
      
      | AUnop uop op1 ⇒
        NNRCUnop uop (nra_to_nnrc op1 var)
      
      | AMap op1 op2 ⇒
        let nnrc2 := (nra_to_nnrc op2 var) in
        let t := fresh_var "tmap$" (var::nil) in
        NNRCFor t nnrc2 (nra_to_nnrc op1 t)
      
      | AMapConcat op1 op2 ⇒
        let nnrc2 := (nra_to_nnrc op2 var) in
        let (t1,t2) := fresh_var2 "tmc$" "tmc$" (var::nil) in
        NNRCUnop AFlatten
                (NNRCFor t1 nnrc2
                        (NNRCFor t2 (nra_to_nnrc op1 t1)
                                ((NNRCBinop AConcat) (NNRCVar t1) (NNRCVar t2))))
        
      | AProduct op1 op2 ⇒
        let nnrc1 := (nra_to_nnrc op1 var) in
        let nnrc2 := (nra_to_nnrc op2 var) in
        let (t1,t2) := fresh_var2 "tprod$" "tprod$" (var::nil) in
        NNRCUnop AFlatten
                (NNRCFor t1 nnrc1
                        (NNRCFor t2 nnrc2
                                ((NNRCBinop AConcat) (NNRCVar t1) (NNRCVar t2))))
      
      | ASelect op1 op2 ⇒
        let nnrc2 := (nra_to_nnrc op2 var) in
        let t := fresh_var "tsel$" (var::nil) in
        let nnrc1 := (nra_to_nnrc op1 t) in
        NNRCUnop AFlatten
                (NNRCFor t nnrc2
                        (NNRCIf nnrc1 (NNRCUnop AColl (NNRCVar t)) (NNRCConst (dcoll nil))))
      
      | ADefault op1 op2 ⇒
        let nnrc1 := (nra_to_nnrc op1 var) in
        let nnrc2 := (nra_to_nnrc op2 var) in
        let t := fresh_var "tdef$" (var::nil) in
        (NNRCLet t nnrc1
                (NNRCIf (NNRCBinop AEq
                                 (NNRCVar t)
                                 (NNRCUnop AFlatten (NNRCConst (dcoll nil))))
                       nnrc2 (NNRCVar t)))
      
      | AEither opl opr ⇒
        let nnrcl := (nra_to_nnrc opl var) in
        let nnrcr := (nra_to_nnrc opr var) in
        NNRCEither (NNRCVar var) var nnrcl var nnrcr
      | AEitherConcat op1 op2 ⇒
        let nnrc1 := (nra_to_nnrc op1 var) in
        let nnrc2 := (nra_to_nnrc op2 var) in
        let t := fresh_var "ec$" (var::nil) in
        NNRCLet t nnrc2
        (NNRCEither nnrc1 var (NNRCUnop ALeft (NNRCBinop AConcat (NNRCVar var) (NNRCVar t)))
                  var (NNRCUnop ARight (NNRCBinop AConcat (NNRCVar var) (NNRCVar t))))
      | AApp op1 op2 ⇒
        let nnrc2 := (nra_to_nnrc op2 var) in
        let t := fresh_var "tapp$" (var::nil) in
        let nnrc1 := (nra_to_nnrc op1 t) in
        (NNRCLet t nnrc2 nnrc1)
    end.

  Lemma map_sem_correct (h:list (string×string)) (op:nra) (l:list data) (env:bindings) (v:var):
    (∀ (d : data) (env : bindings) (v : var),
          lookup equiv_dec env v = Some d →
          nnrc_core_eval h env (nra_to_nnrc op v) = h ⊢ op @ₐ d) →
    rmap
      (fun x : data ⇒
         nnrc_core_eval h ((v, x) :: env) (nra_to_nnrc op v)) l
    =
    rmap (nra_eval h op) l.

  Theorem nra_sem_correct (h:list (string×string)) (op:nra) (env:bindings) (v:var) (d:data) :
    lookup equiv_dec env v = Some d →
    nnrc_core_eval h env (nra_to_nnrc op v) = h ⊢ op @ₐ d.

  Section size.


  Theorem nraToNNRC_size op v :
    nnrc_size (nra_to_nnrc op v) ≤ 10 × nra_size op.

  End size.

  Section core.
    Definition nra_to_nnrc_core q init_vid :=
      nnrc_to_nnrc_core (nra_to_nnrc q init_vid).
  End core.

End NRAtocNNRC.