Module Qcert.Translation.Lang.cNRAEnvtoNRA

Require Import String.
Require Import List.
Require Import Utils.
Require Import DataRuntime.
Require Import cNRAEnvRuntime.
Require Import NRARuntime.

Section cNRAEnvtoNRA.
  Context {fr:foreign_runtime}.

  Section Top.
    Context (h:brand_relation_t).

    Definition nraenv_core_to_nra_top (q:nraenv_core) : nra :=
      NRAApp (nra_of_nraenv_core q) (nra_context (NRAConst (drec nil)) (NRAConst dunit)).

    Theorem nraenv_core_to_nra_top_correct :
      forall q:nraenv_core, forall global_env:bindings,
          nraenv_core_eval_top h q global_env =
          nra_eval_top h (nraenv_core_to_nra_top q) global_env.
  End Top.
    
End cNRAEnvtoNRA.