Module Qcert.Compiler.Lib.QCAMPRule

Require Import CompilerRuntime.
Require String.
Require QOperators QData QCAMP.
Require CAMPRuleRuntime.

Module QCAMPRule(runtime:CompilerRuntime).

  Module Data := QData.QData runtime.
  Module Ops := QOperators.QOperators runtime.
  Module CAMP := QCAMP.QCAMP runtime.

  Definition camp_rule : Set
    := CAMPRule.camp_rule.
  Definition t : Set
    := camp_rule.
  
  Definition rule_when : CAMP.camp -> camp_rule -> camp_rule
    := CAMPRule.rule_when.
  Definition rule_global : CAMP.camp -> camp_rule -> camp_rule
    := CAMPRule.rule_global.
  Definition rule_not : CAMP.camp -> camp_rule -> camp_rule
    := CAMPRule.rule_not.
  Definition rule_return : CAMP.camp -> camp_rule
    := CAMPRule.rule_return.
  Definition rule_match : CAMP.camp -> camp_rule
    := CAMPRule.rule_match.

  Definition aggregate : (camp_rule -> camp_rule) -> Ops.Unary.op -> CAMP.camp -> nat -> CAMP.camp
    := CAMPRuleSugar.aggregate.

  Definition instanceOf : String.string -> BrandRelation.brands -> CAMP.camp -> CAMP.camp
    := CAMPRuleSugar.instanceOf.

  Definition matches : BrandRelation.brands -> CAMP.camp -> CAMP.camp
    := CAMPRuleSugar.matches.

  Definition fetchRef : BrandRelation.brands -> String.string -> String.string -> CAMP.camp -> CAMP.camp -> CAMP.camp
    := CAMPRuleSugar.fetchRef.

End QCAMPRule.