Qcert.LambdaNRA.Lang.LambdaNRASugar

Section LambdaNRASugar.


  Context {fruntime:foreign_runtime}.

  Definition LNRAStruct (el:list (string × lnra)) :=
    match el with
    | nil ⇒ LNRAConst (drec nil)
    | (s0,x) :: rest ⇒
      let init_rec := LNRAUnop (ARec s0) x in
      let proc_one (e:string × lnra) acc :=
          LNRABinop AConcat (LNRAUnop (ARec (fst e)) (snd e)) acc
      in
      fold_right proc_one init_rec rest
    end.

  Definition LNRADot (s:string) (e:lnra) := LNRAUnop (ADot s) e.
  Definition LNRAArrow (s:string) (e:lnra) := LNRAUnop (ADot s) (LNRAUnop AUnbrand e).

  Definition la_tableify_one_var (e:lnra) (v:string) : lnra :=
    lnra_subst e v (LNRATable v).

  Definition la_tableify (e:lnra) : lnra :=
    let free_vars := lnra_free_vars e in
    fold_left la_tableify_one_var free_vars e.

End LambdaNRASugar.