Module Qcert.DNNRC.Lang.DNNRC


Section DNNRC.

  Require Import Utils BasicSystem.

  Require Import DNNRCBase.
  Require Import Dataframe.

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

  Definition dnnrc_dataframe := @dnnrc _ unit dataframe.

  Section Top.
    Context (h:brand_relation_t).

    Definition dnnrc_dataframe_eval_top (q:dnnrc_dataframe) (cenv:dbindings) : option data :=
      lift unlocalize_data (dnnrc_eval h (rec_sort cenv) nil q).

  End Top.

End DNNRC.