Qcert.Translation.CAMPtocNRAEnv


Section CAMPtocNRAEnv.


  Context {fruntime:foreign_runtime}.

Functions used to map input/ouput values between CAMP and NRA

  Definition envpat_fail := ANConst (dcoll nil).
  Definition envpat_match op := ANUnop AColl op.

Translation from CAMP to EnvNRA

  Fixpoint cnraenv_of_pat (p:pat) : cnraenv :=
    match p with
      | pconst d' ⇒ envpat_match (ANConst d')
      | punop uop p₁ ⇒ ANMap (ANUnop uop ANID) (cnraenv_of_pat p₁)
      | pbinop bop p₁ p₂ ⇒
        ANMap (ANBinop bop (ANUnop (ADot "a1") ANID) (ANUnop (ADot "a2") ANID))
              (ANProduct (ANMap (ANUnop (ARec "a1") ANID) (cnraenv_of_pat p₁))
                         (ANMap (ANUnop (ARec "a2") ANID) (cnraenv_of_pat p₂)))
      | pmap p₁ ⇒
        envpat_match
          (ANUnop AFlatten
                  (ANMap
                     (cnraenv_of_pat p₁) ANID))
      | passert p₁ ⇒
        ANMap (ANConst (drec nil)) (ANSelect ANID (cnraenv_of_pat p₁))
      | porElse p₁ p₂ ⇒ ANDefault (cnraenv_of_pat p₁) (cnraenv_of_pat p₂)
      | pit ⇒ envpat_match ANID
      | pletIt p₁ p₂ ⇒
        ANUnop AFlatten
               (ANMap (cnraenv_of_pat p₂)
                      (cnraenv_of_pat p₁))
      | pgetconstant s ⇒ envpat_match (ANGetConstant s)
      | penv ⇒ envpat_match ANEnv
      | pletEnv p₁ p₂ ⇒
        ANUnop AFlatten
               (ANAppEnv
                  (ANMapEnv (cnraenv_of_pat p₂))
                  (ANUnop AFlatten
                          (ANMap (ANBinop AMergeConcat ANEnv ANID) (cnraenv_of_pat p₁))))
      | pleft ⇒
        ANEither (envpat_match ANID) (envpat_fail)
      | pright ⇒
        ANEither (envpat_fail) (envpat_match ANID)
    end.

top level version sets up the appropriate input (with an empty context)

  Definition cnraenv_of_pat_top p :=
    ANUnop AFlatten
           (ANMap (cnraenv_of_pat p) (ANUnop AColl ANID)).

Theorem 4.2: lemma of translation correctness for patterns


  Lemma cnraenv_of_pat_correct h c q env d:
    lift_failure (interp h c q env d) = cnraenv_eval h c (cnraenv_of_pat q) (drec env) d.

  Lemma cnraenv_of_pat_equiv_to_nra h c p bind d:
    nra_eval h (nra_of_pat p) (pat_context_data (drec (rec_sort c)) (drec bind) d) =
    cnraenv_eval h c (cnraenv_of_pat p) (drec bind) d.

  Lemma cnraenv_of_pat_top_id h c p d :
    Forall (fun x ⇒ data_normalized h (snd x)) c →
    nra_eval h (nra_of_pat_top c p) d =
    cnraenv_eval h c (cnraenv_of_pat_top p) (drec nil) d.

  Lemma epat_trans_top_correct h c p d:
    Forall (fun x ⇒ data_normalized h (snd x)) c →
    
    lift_failure (interp h c p nil d) = cnraenv_eval h c (cnraenv_of_pat_top p) (drec nil) d.

  Section Top.
    Definition translate_pat_to_cnraenv (p:pat) : cnraenv :=
      
      ANAppEnv (cnraenv_of_pat p) (ANConst (drec nil)).

  End Top.

  Section size.

Proof showing linear size translation
    Lemma pat_trans_size p :
      cnraenv_size (cnraenv_of_pat p) ≤ 13 × pat_size p.

  End size.

  Section sugar.
    Definition cnraenv_of_pand (p1 p2:pat) : cnraenv :=
      cnraenv_of_pat (pand p1 p2).

    Definition cnraenv_for_pand (q1 q2: cnraenv) : cnraenv :=
      ANUnop AFlatten
             (ANAppEnv (ANMapEnv q2)
                       (ANUnop AFlatten
                               (ANMap (ANBinop AMergeConcat ANEnv ANID)
                                      (ANMap (ANConst (drec nil))
                                             (ANSelect ANID q1))))).

    Lemma cnraenv_of_pand_works (p1 p2:pat) :
      cnraenv_of_pat (pand p1 p2) = cnraenv_for_pand (cnraenv_of_pat p1) (cnraenv_of_pat p2).


    Definition cnraenv_of_WW (p:pat) :=
      cnraenv_of_pat (WW p).
  End sugar.

End CAMPtocNRAEnv.