Module Qcert.CAMP.Lang.CAMPSugar

Require Import String.
Require Import List.
Require Import EquivDec.
Require Import ZArith.
Require Import Utils.
Require Import DataRuntime.
Require Export CAMP.

Section CAMPSugar.
  Context {fruntime:foreign_runtime}.

    
  Definition paccept := pconst (drec nil).

  Definition pfail : camp := passert (pconst (dconst false)).
  Definition makeSingleton (p:camp) : camp := punop OpBag p.

    
  Definition pand (p1 p2:camp):= pletEnv (passert p1) p2.
    
  Definition toString p := punop OpToString p.

  Definition psome := pleft.
  Definition pnone := pright.
  Definition pnull := (pconst dnone).
  
  Definition punbrand' p := punop OpUnbrand p.
  Definition punbrand := punbrand' pit.

  Definition pcast' b p:= pletIt (punop (OpCast b) p) psome.
  Definition pcast b := pcast' b pit.

  Definition psingleton' p := pletIt (punop OpSingleton p) psome.
  Definition psingleton := psingleton' pit.

    
  Definition pWithBindings : camp -> camp := pletIt penv.
  Definition pvarwith f : camp -> camp := punop (OpRec f).
  Definition pvar f : camp := pvarwith f pit.
  Definition pdot f : camp -> camp := pletIt (punop (OpDot f) pit).
  Definition pbdot s p : camp := (pletIt punbrand (pdot s p)).
  Definition pbsomedot s p : camp := (pletIt (pbdot s p) psome).
  Definition varOf (varName:string) (p:camp) := pletEnv (pvar varName) p.
  Definition lookup c := (pWithBindings (pdot c pit)).

  Definition withVar (name:string) (p:camp) : camp := pletIt (lookup name) p.
  Definition withBrandedVar (name:string) (p:camp) : camp :=
    pletIt (punbrand' (lookup name)) p.

  Definition pIS var p := pletIt p (pvar var).
    
  Example empty_binding := @nil (string*data).

  Definition stringConcat a b := pbinop OpStringConcat (toString a) (toString b).
    

  Fixpoint pFoldRec (camps:list (string*camp)) (init:data) : camp
    := match camps with
       | nil => pconst init
       | (s,p)::ls => pletIt (pletEnv
                                (pdot s (pvar "current"))
                                (pletIt (pFoldRec ls init) (pvar "previous")))
                             p
       end.

  Fixpoint pMapRec (camps:list (string*camp)) : camp
    := match camps with
       | nil => pconst (drec nil)
       | (s,p)::ls => pletEnv (pdot s p) (pMapRec ls)
       end.

  Definition pMapRecFromFold (camps:list (string*camp)) : camp
    := pFoldRec
         (map (fun xy => ((fst xy), pdot "current" (snd xy))) camps)
         (drec nil).


  Fixpoint camp_reduce (f:camp->camp->camp) (l:list camp) : camp
    := match l with
       | nil => passert (pconst (dconst false))
       | p1::l' => match l' with
                   | nil => p1
                   | p2::l'' => f p1 (camp_reduce f l')
                   end
       end.

  Definition camp_binop_reduce (b:binary_op) (l:list camp) : camp :=
    camp_reduce (fun p1 p2 => (pbinop b p1 p2)) l.

  Definition camp_equiv p₁ p₂ := forall h c b d, camp_eval h c p₁ b d = camp_eval h c p₂ b d.

  Theorem withAccept_id p : camp_equiv (pletIt pit p) p.

  Lemma preduce_id b (l:list camp):
    camp_equiv (camp_reduce (pbinop b) l) (camp_binop_reduce b l).
    
  
  Definition typedObject (type:brands) (p:camp) :=
    pletIt (pcast type) p.

  Definition namedObject (varName:string) (type:brands) (p:camp) :=
    pletIt (pcast type)
           (pletEnv (pvar varName)
                    p).

  Definition class (type:brands) (contents:data)
    := dbrand type contents.

  Definition returnVariables (sl:list string) : camp
    := punop (OpRecProject (insertion_sort ODT_lt_dec sl)) penv.

  Definition pnow := pgetConstant ("NOW").

  Definition WW p := pletIt (pgetConstant ("WORLD")) p.

  Notation "p1 ≐ p2" := (passert (pbinop OpEqual p1 p2)) (right associativity, at level 70, only parsing).
  Notation "‵ c" := (pconst (dconst c)) (at level 0).

  Definition mapall p :=
    pletEnv (punop OpCount pit ≐ punop OpCount (pmap p))
            (pmap p).

  Definition mapsnone p := (punop OpCount (pmap p) ≐ ‵(0%Z)).

  Definition mapsone p := (punop OpCount (pmap p) ≐ ‵(1%Z)).

  Definition notholds p := WW (mapsnone p).

End CAMPSugar.
  
Delimit Scope camp_scope with camp.

Notation "p1 |p-eq| p2" := (pbinop OpEqual p1 p2) (right associativity, at level 70): camp_scope.
Notation "p1 |p-union| p2" := (pbinop OpBagUnion p1 p2) (right associativity, at level 70): camp_scope.
Notation "p1 |p-concat| p2" := (pbinop OpRecConcat p1 p2) (right associativity, at level 70): camp_scope.
Notation "p1 |p-mergeconcat| p2" := (pbinop OpRecMerge p1 p2) (right associativity, at level 70): camp_scope.
Notation "p1 |p-and| p2" := (pbinop OpAnd p1 p2) (right associativity, at level 70): camp_scope.
Notation "p1 |p-or| p2" := (pbinop OpOr p1 p2) (right associativity, at level 70): camp_scope.
Notation "p1 |p-lt| p2" := (pbinop OpLt p1 p2) (right associativity, at level 70): camp_scope.
Notation "p1 |p-le| p2" := (pbinop OpLe p1 p2) (right associativity, at level 70): camp_scope.
Notation "p1 |p-bagdiff| p2" := (pbinop OpBagDiff p1 p2) (right associativity, at level 70): camp_scope.
Notation "p1 |p-bagmin| p2" := (pbinop OpBagMin p1 p2) (right associativity, at level 70): camp_scope.
Notation "p1 |p-bagmax| p2" := (pbinop OpBagMax p1 p2) (right associativity, at level 70): camp_scope.
Notation "p1 |p-contains| p2" := (pbinop OpContains p1 p2) (right associativity, at level 70): camp_scope.
Notation "p1 |p-stringconcat| p2" := (pbinop OpStringConcat p1 p2) (right associativity, at level 70): camp_scope.
Notation "a '+s+' b" := (stringConcat a b) (right associativity, at level 60) : camp_scope.

Notation "|p-min-num|( p )" := (punop OpNatMin p) (right associativity, at level 70): camp_scope.
Notation "|p-max-num|( p )" := (punop OpNatMin p) (right associativity, at level 70): camp_scope.

Notation "p1 ≐ p2" := (passert (pbinop OpEqual p1 p2)) (right associativity, at level 70, only parsing): camp_scope.
Notation "p1 ∧ p2" := (pand p1 p2) (right associativity, at level 65): camp_scope.
Notation "…" := pit.
Notation "s ↓ p" := (pdot s p) (right associativity, at level 30): camp_scope.
Notation "'BINDINGS'" := (pWithBindings pit) : camp_scope.
Notation "a 'RETURN' b" := (pletEnv a b) (right associativity, at level 30, only parsing) : camp_scope.

Notation "! x" := (punbrand' x) (at level 0) : camp_scope.
Notation "t 'COLON' p" := (varOf t p) (at level 70) : camp_scope.
Notation "var 'IS' p" := (pIS var p) (at level 71, only parsing) : camp_scope.

Notation "‵ c" := (pconst (dconst c)) (at level 0).
Notation "#` c" := (pconst (dconst c)) (only parsing, at level 0) : camp_scope.
Notation "s #-> p" := (pdot s p) (only parsing, right associativity, at level 30): camp_scope.
Notation "s !#-> p" := (pbdot s p) (only parsing, right associativity, at level 30): camp_scope.
Notation "#_" := pit (only parsing): camp_scope.
Notation "p1 #= p2" := (passert (pbinop OpEqual p1 p2)) (only parsing, right associativity, at level 70): camp_scope.