Qcert.Translation.CAMPtoNRAEnv

Section CAMPtoNRAEnv.

Context {fruntime:foreign_runtime}.

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

Definition envpat_fail := NRAEnvConst (dcoll nil).
Definition envpat_match op := NRAEnvUnop AColl op.

Translation from CAMP to EnvNRA

  Fixpoint nraenv_of_pat (p:pat) : nraenv :=
    match p with
      | pconst d' ⇒ envpat_match (NRAEnvConst d')
      | punop uop p₁ ⇒ NRAEnvMap (NRAEnvUnop uop NRAEnvID) (nraenv_of_pat p₁)
      | pbinop bop p₁ p₂ ⇒
        NRAEnvMap (NRAEnvBinop bop (NRAEnvUnop (ADot "a1") NRAEnvID) (NRAEnvUnop (ADot "a2") NRAEnvID))
              (NRAEnvProduct (NRAEnvMap (NRAEnvUnop (ARec "a1") NRAEnvID) (nraenv_of_pat p₁))
                         (NRAEnvMap (NRAEnvUnop (ARec "a2") NRAEnvID) (nraenv_of_pat p₂)))
      | pmap p₁ ⇒
        envpat_match
          (NRAEnvUnop AFlatten
                  (NRAEnvMap
                     (nraenv_of_pat p₁) NRAEnvID))
      | passert p₁ ⇒
        NRAEnvMap (NRAEnvConst (drec nil)) (NRAEnvSelect NRAEnvID (nraenv_of_pat p₁))
      | porElse p₁ p₂ ⇒ NRAEnvDefault (nraenv_of_pat p₁) (nraenv_of_pat p₂)
      | pit ⇒ envpat_match NRAEnvID
      | pletIt p₁ p₂ ⇒
        NRAEnvUnop AFlatten
               (NRAEnvMap (nraenv_of_pat p₂)
                      (nraenv_of_pat p₁))
      | pgetconstant s ⇒ envpat_match (NRAEnvGetConstant s)
      | penv ⇒ envpat_match NRAEnvEnv
      | pletEnv p₁ p₂ ⇒
        NRAEnvUnop AFlatten
               (NRAEnvAppEnv
                  (NRAEnvMapEnv (nraenv_of_pat p₂))
                  (NRAEnvUnop AFlatten
                          (NRAEnvMap (NRAEnvBinop AMergeConcat NRAEnvEnv NRAEnvID) (nraenv_of_pat p₁))))
      | pleft ⇒
        NRAEnvEither (envpat_match NRAEnvID) (envpat_fail)
      | pright ⇒
        NRAEnvEither (envpat_fail) (envpat_match NRAEnvID)
    end.

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

  Definition nraenv_of_pat_top p :=
    NRAEnvUnop AFlatten
           (NRAEnvMap (nraenv_of_pat p) (NRAEnvUnop AColl NRAEnvID)).

Theorem 4.2: lemma of translation correctness for patterns

  Lemma nraenv_of_pat_cnraenv_of_pat_ident q :
    cnraenv_of_nraenv (nraenv_of_pat q) = cnraenv_of_pat q.

  Lemma nraenv_of_pat_correct h c q env d:
    lift_failure (interp h c q env d) = nraenv_eval h c (nraenv_of_pat q) (drec env) d.

  Lemma nraenv_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) =
    nraenv_eval h c (nraenv_of_pat p) (drec bind) d.

  Lemma nraenv_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 =
    nraenv_eval h c (nraenv_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) = nraenv_eval h c (nraenv_of_pat_top p) (drec nil) d.

  Section Top.
    Definition translate_pat_to_nraenv (p:pat) : nraenv :=

      NRAEnvAppEnv (nraenv_of_pat p) (NRAEnvConst (drec nil)).

  End Top.

  Section size.

Proof showing linear size translation

    Lemma pat_trans_size p :
      nraenv_size (nraenv_of_pat p) ≤ 13 × pat_size p.

  End size.

  Section sugar.
    Definition nraenv_of_pand (p1 p2:pat) : nraenv :=
      nraenv_of_pat (pand p1 p2).

    Definition nraenv_for_pand (q1 q2: nraenv) : nraenv :=
      NRAEnvUnop AFlatten
                 (NRAEnvAppEnv (NRAEnvMapEnv q2)
                               (NRAEnvUnop AFlatten
                                           (NRAEnvMap (NRAEnvBinop AMergeConcat NRAEnvEnv NRAEnvID)
                                                      (NRAEnvMap (NRAEnvConst (drec nil))
                                                                 (NRAEnvSelect NRAEnvID q1))))).

    Lemma nraenv_of_pand_works (p1 p2:pat) :
      nraenv_of_pat (pand p1 p2) = nraenv_for_pand (nraenv_of_pat p1) (nraenv_of_pat p2).

    Definition nraenv_of_WW (p:pat) :=
      nraenv_of_pat (WW p).

  End sugar.

End CAMPtoNRAEnv.