Require Import String.
Require Import List.
Require Import EquivDec.
Require Import Utils.
Require Import DataRuntime.
Require Export CAMPRuntime.

Section CAMPRule.
  Local Open Scope camp_scope.
  Local Open Scope string.

  Context {fruntime:foreign_runtime}.

Abstract Syntax Tree

  Inductive camp_rule :=
  | rule_when : camp -> camp_rule -> camp_rule (* Match against each element of the working memory. *)
  | rule_global : camp -> camp_rule -> camp_rule (* Match against the working memory as a collection *)
  | rule_not : camp -> camp_rule -> camp_rule (* A rule that must not match any working memory element. *)
  | rule_return : camp -> camp_rule (* Rule to return a value for each successful match-set. *)
  | rule_match : camp -> camp_rule. (* This allows a rule to simply match a camp pattern. *)

Translate CAMPRule into the CAMP kernel

  Fixpoint camp_rule_to_camp (rule:camp_rule) : camp
    := match rule with
         | rule_when p ps =>
           punop OpFlatten
                 (WW
                    (pmap
                       (pletEnv
                          p
                          (camp_rule_to_camp ps))))
         | rule_global p ps =>
           punop OpFlatten
                 (makeSingleton
                    (pletEnv
                       (WW p)
                       (camp_rule_to_camp ps)))
         | rule_not p ps =>
           punop OpFlatten
                 (makeSingleton
                    (pletEnv
                       (notholds p RETURN BINDINGS)
                       (camp_rule_to_camp ps)))
         | rule_return p =>
           makeSingleton p
         | rule_match p =>
           p
       end.

Evaluation

  Definition eval_camp_rule_debug (h:list(string*string)) (print_env:bool) (r:camp_rule) (world:list data)
    : presult_debug data
    := camp_eval_debug h (mkWorld world) print_env nil (camp_rule_to_camp r) nil dunit.

  Definition eval_camp_rule_res_to_string
             (h:list(string*string)) (print_env:bool) (r:camp_rule) (world:list data)
    : string
    := let pp := (camp_rule_to_camp r) in
       print_presult_debug pp toString_camp_with_path
                           (camp_eval_debug h
                                         (mkWorld world)
                                         print_env nil pp nil dunit).

  Definition eval_camp_rule_res (h:list(string*string)) (r:camp_rule) (world:list data)
    : presult data
    := camp_eval h (mkWorld world) (camp_rule_to_camp r) nil dunit.

  Definition eval_camp_rule (h:list(string*string)) (r:camp_rule) (world:list data)
    : option (list data)
    := match eval_camp_rule_res h r world with
       | Success l => Some (l::nil)
       | RecoverableError => Some nil
       | TerminalError => None
       end.

  Section Top.
    Context (h:brand_relation_t).

    Definition camp_rule_eval_top (q:camp_rule) (cenv:bindings) :=
      presult_to_result (camp_eval h (rec_sort cenv) (camp_rule_to_camp q) nil dunit).

    Definition camp_rule_eval_top_debug (debug:bool) (q:camp_rule) (cenv:bindings) :=
      let pp := camp_rule_to_camp q in
      print_presult_debug pp toString_camp_with_path
                          (camp_eval_debug h
                                           (rec_sort cenv)
                                           debug nil pp nil dunit).
  End Top.

End CAMPRule.