Module Qcert.CAMPRule.Lang.CAMPRuleSugar

Require Import String.
Require Import List.
Require Import Utils.
Require Import DataRuntime.
Require Export CAMPSugar.
Require Export CAMPRule.

Section CAMPRuleSugar.
  Local Open Scope camp_scope.
  Local Open Scope string.

  Context {fruntime:foreign_runtime}.

  Fixpoint flattenn (n:nat) (p:camp)
    := match n with
       | 0 => p
       | S m =>flattenn m (punop OpFlatten p)
       end.
  
  Definition aggregate (rules:camp_rule->camp_rule) (op:unary_op) (secondMap:camp) (nflat:nat): camp
    := pletIt
          (camp_rule_to_camp (rules (rule_return penv)))
          (punop op (flattenn nflat (pmap (pletEnv pit secondMap)))).

  Definition aggregate_group_by (rules:camp_rule->camp_rule) (opg:camp) (op:unary_op) (secondMap:camp) : camp
    := pletIt
          (camp_rule_to_camp (rules (rule_return penv)))
          (punop op (pmap (pletEnv pit secondMap))).

  Definition fetchRef (entity:brands) (keyatt:string) (tempvar:string) (keyval:camp) : camp -> camp
    := pletIt
         (pletEnv (pvarwith tempvar keyval)
                  (WW
                     (pletIt
                        (pmap
                           (pletIt (pcast entity) (pand ((pletIt punbrand (keyatt ↓ …) |p-eq| (lookup tempvar))) pit)))
                        psingleton))).

  Definition instanceOf n t p := namedObject n t (p RETURN BINDINGS).
  Definition matches t p := typedObject t (p RETURN BINDINGS).
End CAMPRuleSugar.

Delimit Scope camp_scope with camp_rule.

Notation "n 'INSTANCEOF' t 'WHERE' p" := ((instanceOf n t p)%camp_rule) (at level 70) : camp_scope.
Notation "p 'TEMPVAR' t 'FETCH' e 'KEY' a 'DO' pcont" := ((fetchRef e a t p pcont)%camp_rule) (at level 70) : camp_scope.
Notation "'MATCHES' t 'WHERE' p" := ((matches t p)%camp_rule) (at level 70) : camp_scope.
Notation "'VARIABLES' sl" := (returnVariables sl) (at level 70) : camp_scope.

Notation " 'AGGREGATE' m1 'DO' op 'OVER' m2 'FLATTEN' f" := (aggregate m1 op m2 f) (at level 70) : camp_scope.
Notation " 'AGGREGATEG' m1 'GROUPBY' opg 'DO' op 'OVER' m2" := (aggregate_group_by m1 opg op m2) (at level 70) : camp_scope.
Notation "p1 'ANDMAPSNONES' p2" := ((p1 ∧ notholds p2 RETURN BINDINGS)%camp_rule) (left associativity, at level 83) : camp_scope.

Notation "a ;; b" := (a b) (at level 99, right associativity, only parsing) : camp_scope.

Notation "a ;;; b" := (fun x => a (b x)) (at level 99, right associativity, only parsing) : camp_scope.