Module Qcert.tDNNRC.Lang.tDNNRC

Require Import Utils.
Require Import DataSystem.
Require Import DNNRCSystem.
  
Section tDNNRC.
  Context {fruntime:foreign_runtime}.
  Context {ftype: ForeignType.foreign_type}.
  Context {br:brand_relation}.

  Record type_annotation {A:Set} : Set :=
    mkType_annotation {
        ta_base:A
        ; ta_inferred:drtype
        ; ta_required:drtype
                        
      }.

  Global Arguments type_annotation : clear implicits.
  Global Arguments mkType_annotation {A} ta_base ta_inferred ta_required.
  
  Definition dnnrc_typed := @dnnrc_base _ (type_annotation unit) dataframe.

  Section Top.
    Context (h:brand_relation_t).

    Definition dnnrc_typed_eval_top
               (q:dnnrc_typed) (cenv:dbindings) : option data :=
      lift unlocalize_data (@dnnrc_base_eval _ _ _ h (rec_sort cenv) SparkIRPlug nil q).
  End Top.
  
End tDNNRC.