Module Qcert.Translation.TCAMPtoNRAEnv


Section TCAMPtoNRAEnv.
  Require Import String.
  Require Import List.
  Require Import CommonSystem.
  Require Import NRASystem.
  Require Import NRAEnvSystem.
  Require Import CAMPSystem.
  Require Import CAMPtoNRAEnv.
  Require Import TCAMPtoNRA.
  Require Import TCAMPtocNRAEnv.

  Local Open Scope string_scope.
  Local Open Scope list_scope.
  Local Open Scope camp_scope.

  Hint Constructors unary_op_type binary_op_type.

  Context {m:basic_model}.

  Lemma nraenv_of_camp_type_preserve τc Γ pf p τin τout :
    [τc&Γ] |= p ; τin ~> τout ->
    nraenv_of_camp p ▷ₓ τin >=> Coll τout ⊣ τc;(Rec Closed Γ pf).
Proof.
    Hint Resolve data_type_drec_nil.
    unfold nraenv_type.
    rewrite nraenv_of_camp_nraenv_core_of_camp_ident.
    apply nraenv_core_of_camp_type_preserve.
  Qed.

Some corollaries of the main Lemma

  Lemma nraenv_of_camp_nraenv_of_camp_top p τc τin τout :
    nraenv_of_camp p ▷ₓ τin >=> Coll τout ⊣ τc;(Rec Closed nil eq_refl) ->
    nraenv_of_camp_top p ▷ₓ τin >=> Coll τout ⊣ τc;(Rec Closed nil eq_refl).
Proof.
    intros.
    repeat (econstructor; eauto).
  Qed.
    
  Theorem alg_of_camp_top_type_preserve p τc τin τout :
    [τc&nil] |= p ; τin ~> τout ->
    nraenv_of_camp_top p ▷ₓ τin >=> Coll τout ⊣ τc;(Rec Closed nil eq_refl).
Proof.
    intros.
    apply nraenv_of_camp_nraenv_of_camp_top.
    apply nraenv_of_camp_type_preserve; eauto.
  Qed.

End TCAMPtoNRAEnv.