Module Qcert.LambdaNRA.Lang.LambdaNRASugar

Require Import String.
Require Import List.
Require Import Arith.
Require Import EquivDec.
Require Import Utils.
Require Import DataRuntime.
Require Import LambdaNRA.

Section LambdaNRASugar.
  Context {fruntime:foreign_runtime}.

  Definition LNRAStruct (el:list (string * lambda_nra)) :=
    match el with
    | nil => LNRAConst (drec nil)
    | (s0,x) :: rest =>
      let init_rec := LNRAUnop (OpRec s0) x in
      let proc_one (e:string * lambda_nra) acc :=
          LNRABinop OpRecConcat (LNRAUnop (OpRec (fst e)) (snd e)) acc
      in
      fold_right proc_one init_rec rest
    end.

  Definition LNRADot (s:string) (e:lambda_nra) := LNRAUnop (OpDot s) e.
  Definition LNRAArrow (s:string) (e:lambda_nra) := LNRAUnop (OpDot s) (LNRAUnop OpUnbrand e).
  Definition LNRAFlatMap (l:lnra_lambda) (e:lambda_nra) :=
    LNRAUnop OpFlatten (LNRAMap l e).
  
  Definition la_tableify_one_var (e:lambda_nra) (v:string) : lambda_nra :=
    lambda_nra_subst e v (LNRATable v).

  Definition la_tableify (e:lambda_nra) : lambda_nra :=
    let free_vars := lambda_nra_free_vars e in
    fold_left la_tableify_one_var free_vars e.
  
End LambdaNRASugar.