Module CAMPRuletoCAMP

Section CAMPRuletoCAMP.

  Require Import String.
  Require Import List.

  Require Import Utils BasicRuntime.
  Require Import CAMPRuleRuntime.
  Require Import CAMPRuntime.
  
  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.