Module NRASugar

Section NRASugar.
  Require Import String List Compare_dec.
  Require Import EquivDec.
  
  Require Import Utils BasicRuntime.
  Require Import NRA.


  Context {fruntime:foreign_runtime}.

  Open Scope string_scope.

  Definition nra_bind := AUnop (ADot "PBIND") AID.
  Definition nra_data := AUnop (ADot "PDATA") AID.
  Definition nra_data_op op := AUnop (ADot "PDATA") op.

  Definition nra_fail := AConst (dcoll nil).
  Definition nra_match op := AUnop AColl op.
  Definition nra_double s1 s2 (abind:nra) (adata:nra) :=
    ABinop AConcat
           (AUnop (ARec s1) abind)
           (AUnop (ARec s2) adata).
  
  Definition nra_context (abind:nra) (adata:nra) :=
    nra_double "PBIND" "PDATA" abind adata.
  
  Definition nra_withbinding :=
    nra_context nra_bind nra_bind.
  
  Definition nra_context_data dbind dpid : data :=
    drec (("PBIND",dbind)
            ::("PDATA",dpid)
            :: nil).

  Definition make_fixed_nra_context_data (env:data) : nra
    := ABinop AConcat
              (AUnop (ARec "PBIND"%string) (AConst env))
              (AUnop (ARec "PDATA"%string) AID).

  Definition nra_wrap op :=
    nra_double "PBIND" "PDATA" nra_bind op.
  
  Definition nra_wrap_a1 op :=
    nra_double "PBIND" "a1" nra_bind op.

  Definition nra_wrap_bind_a1 op :=
    nra_double "a1" "PDATA" nra_bind op.

  Definition nra_wrap_with_bind op1 :=
    nra_context op1 AID.
  
  Definition nra_project_wrap :=
    nra_wrap_with_bind nra_fail.

  Lemma data_normalized_nra_context_data h env d:
    data_normalized h env ->
    data_normalized h d ->
    data_normalized h (nra_context_data env d).

  Lemma data_normalized_nra_context_data_inv h env d:
    data_normalized h (nra_context_data env d) ->
    data_normalized h env /\
    data_normalized h d.

End NRASugar.

Hint Resolve data_normalized_nra_context_data.