Module OQLSugar

Require Import String.
Require Import List.
Require Import Arith.
Require Import EquivDec.

Section OQLSugar.

  Require Import Utils BasicSystem.
  Require Import OQL.

  Context {fruntime:foreign_runtime}.

  Definition OStruct (el:list (string * oql_expr)) :=
    match el with
    | nil => OConst (drec nil)
    | (s0,x) :: rest =>
      let init_rec := OUnop (ARec s0) x in
      let proc_one (e:string * oql_expr) acc :=
          OBinop AConcat (OUnop (ARec (fst e)) (snd e)) acc
      in
      fold_right proc_one init_rec rest
    end.

  Definition ODot (s:string) (e:oql_expr) := OUnop (ADot s) e.
  Definition OArrow (s:string) (e:oql_expr) := OUnop (ADot s) (OUnop AUnbrand e).
  
  Definition tableify_one_var (e:oql_expr) (v:string) : oql_expr :=
    oql_subst e v (OTable v).

  Definition tableify (e:oql_expr) : oql_expr :=
    let free_vars := oql_free_vars e in
    fold_left tableify_one_var free_vars e.
  
End OQLSugar.