Module Qcert.DNNRC.Lang.DNNRC


Section DNNRC.
  Require Import Utils.
  Require Import CommonSystem.
  Require Import DNNRCBase.
  Require Import Dataframe.

  Context {fruntime:foreign_runtime}.
  Context {ftype: ForeignType.foreign_type}.

  Definition dnnrc := @dnnrc_base _ unit dataframe.

  Section Top.
    Context (h:brand_relation_t).

    Definition dnnrc_eval_top (q:dnnrc) (cenv:dbindings) : option data :=
      lift unlocalize_data (dnnrc_base_eval h (rec_sort cenv) nil q).

  End Top.

End DNNRC.