Module Qcert.DNNRC.Lang.DNNRC

Require Import Utils.
Require Import DataRuntime.
Require Import DNNRCBase.
Require Import Dataframe.

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

  Definition dnnrc := @dnnrc_base _ unit dataframe.

  Global Program Instance SparkIRPlug : (@AlgPlug _ dataframe) :=
    mkAlgPlug wrap_dataframe_eval dataframe_eval_normalized.

  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.