Qcert.NRA.Lang.NRASugar

Section NRASugar.



  Context {fruntime:foreign_runtime}.


  Definition pat_bind := AUnop (ADot "PBIND") AID.
  Definition pat_const_env := AUnop (ADot "PCONST") AID.
  Definition pat_data := AUnop (ADot "PDATA") AID.
  Definition pat_data_op op := AUnop (ADot "PDATA") op.

  Definition pat_fail := AConst (dcoll nil).
  Definition pat_match op := AUnop AColl op.
  Definition pat_triple s1 s2 s3 (aconst:nra) (abind:nra) (adata:nra) :=
    ABinop AConcat
           (AUnop (ARec s1) aconst)
           (ABinop AConcat
                   (AUnop (ARec s2) abind)
                   (AUnop (ARec s3) adata)).

  Definition pat_context (aconst:nra) (abind:nra) (adata:nra) :=
    pat_triple "PCONST" "PBIND" "PDATA" aconst abind adata.

  Definition pat_withbinding :=
    pat_context pat_const_env pat_bind pat_bind.

  Definition pat_context_data dconst dbind dpid : data :=
    drec (("PBIND",dbind)
            ::("PCONST",dconst)
            ::("PDATA",dpid)
            :: nil).

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

  Definition pat_wrap op :=
    pat_triple "PCONST" "PBIND" "PDATA" pat_const_env pat_bind op.

  Definition pat_wrap_a1 op :=
    pat_triple "PCONST" "PBIND" "a1" pat_const_env pat_bind op.

  Definition pat_wrap_bind_a1 op :=
    pat_triple "PCONST" "a1" "PDATA" pat_const_env pat_bind op.

  Definition pat_wrap_with_bind op1 :=
    pat_context pat_const_env op1 AID.

  Definition pat_project_wrap :=
    pat_wrap_with_bind pat_fail.

  Lemma data_normalized_pat_context_data h constants env d:
    data_normalized h constants →
    data_normalized h env →
    data_normalized h d →
    data_normalized h (pat_context_data constants env d).

  Lemma data_normalized_pat_context_data_inv h constants env d:
    data_normalized h (pat_context_data constants env d) →
     data_normalized h constants ∧
    data_normalized h env ∧
    data_normalized h d.

End NRASugar.