Syntactic sugar

Require Import String.
Require Import List.
Require Import Qcert.NNRC.NNRCRuntime.
Require Import ErgoSpec.Common.Names.
Require Import ErgoSpec.ErgoNNRC.Lang.ErgoNNRC.
Require Import ErgoSpec.Backend.QLib.

Section ErgoNNRCSugar.
  Open Scope string.

  Definition fresh_in_match {A} (eccases:list (A * nnrc_expr)) (ecdefault:nnrc_expr) :=
    fresh_var
      "$match"
      (List.app
         (List.concat
            (List.map (fun eccase => nnrc_free_vars (snd eccase)) eccases))
         (nnrc_free_vars ecdefault)).

  Definition fresh_in_case (pattern_expr:nnrc_expr) (else_expr:nnrc_expr) : string :=
    fresh_var "$case"
              (List.app (nnrc_free_vars pattern_expr) (nnrc_free_vars else_expr)).

  Definition fresh_in_lift_error (e:nnrc_expr) :=
    fresh_var2 "$lifte" "$lifte"
               (nnrc_free_vars e).
  Definition fresh_in_lift_optional (e:nnrc_expr) :=
    fresh_var2 "$lifto" "$lifto"
               (nnrc_free_vars e).

  Definition new_array (el:list nnrc_expr) : nnrc_expr :=
    match el with
    | nil => NNRCConst (dcoll nil)
    | e1::erest =>
      fold_left (fun acc e => NNRCBinop OpBagUnion acc (NNRCUnop OpBag e)) erest (NNRCUnop OpBag e1)
    end.

  Definition new_expr (brand:string) (struct_expr:nnrc_expr) : nnrc_expr :=
    NNRCUnop (OpBrand (brand :: nil)) struct_expr.

  Section Examples.
    Definition el1 := (NNRCConst (dnat 1))::(NNRCConst (dnat 2))::(NNRCConst (dnat 3))::nil.

  End Examples.
End ErgoNNRCSugar.