Qcert.OQL.Lang.OQLSugar

Section OQLSugar.


  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.