Module Qcert.Translation.Lang.CAMPRuletoCAMP

Require Import String.
Require Import List.
Require Import Utils.
Require Import DataRuntime.
Require Import CAMPRuleRuntime.
Require Import CAMPRuntime.
  
Section CAMPRuletoCAMP.
  Section Top.
    Context {fr:foreign_runtime}.
    Definition camp_rule_to_camp_top (q:camp_rule) : camp := camp_rule_to_camp q.

    Context (h:brand_relation_t).

    Theorem camp_rule_to_camp_top_correct :
      forall q:camp_rule, forall global_env:bindings,
          camp_rule_eval_top h q global_env =
          camp_eval_top h (camp_rule_to_camp_top q) global_env.
  End Top.
    
End CAMPRuletoCAMP.