Section Dataset.




  Context {fruntime:foreign_runtime}.
  Context {ftype: ForeignType.foreign_type}.
  Context {m : TBrandModel.brand_model}.

  Definition var := string.

  Inductive column :=
  | CCol : string → column
  | CDot : string → column → column
  | CLit : data × rtype₀ → column
  | CPlus : column → column → column
  | CEq : column → column → column
  | CLessThan : column → column → column
  | CNeg : column → column
  
  | CToString : column → column
  | CSConcat : column → column → column
  
  | CUDFCast : list string → column → column
  | CUDFUnbrand : rtype₀ → column → column.

  Inductive dataset :=
  | DSVar : string → dataset
  | DSSelect : list (string × column) → dataset → dataset
  | DSFilter : column → dataset → dataset
  | DSCartesian : dataset → dataset → dataset
  | DSExplode : string → dataset → dataset.

  Section eval.
    Context (h:brand_relation_t).

    Fixpoint fun_of_column (c: column) (row: list (string × data)) : option data :=
      let fc := flip fun_of_column row in
      match c with
      | CCol n ⇒
        lookup string_eqdec row n
      | CNeg c1 ⇒
        olift (unudbool negb) (fc c1)
      | CDot n c1 ⇒
        match fc c1 with
        | Some (drec fs) ⇒ edot fs n
        | _ ⇒ None
        end
      | CLit (d, _) ⇒ Some (normalize_data h d)
      | CPlus c1 c2 ⇒
        match fc c1, fc c2 with
        | Some (dnat l), Some (dnat r) ⇒ Some (dnat (Z.add l r))
        | _, _ ⇒ None
        end
      | CEq c1 c2 ⇒
        
        lift2 (fun x y ⇒ dbool (if data_eq_dec x y then true else false)) (fc c1) (fc c2)
      | CLessThan c1 c2 ⇒
        None
      | CToString c1 ⇒
        lift (compose dstring dataToString) (fc c1)
      | CSConcat c1 c2 ⇒
        match fc c1, fc c2 with
        | Some (dstring l), Some (dstring r) ⇒ Some (dstring (l ++ r))
        | _, _ ⇒ None
        end
      | CUDFCast target_brands column_of_runtime_brands ⇒
        match fc column_of_runtime_brands with
        | Some (dcoll runtime_brand_strings) ⇒
          lift (fun runtime_brands ⇒
                  dbool (if sub_brands_dec h runtime_brands target_brands then true else false))
               (listo_to_olist (map (fun s ⇒ match s with dstring s ⇒ Some s | _ ⇒ None end) runtime_brand_strings))
        | _ ⇒ None
        end
      | CUDFUnbrand _ _ ⇒ None
      end.

    Fixpoint dataset_eval (dsenv : coll_bindings) (e: dataset) : option (list data) :=
      match e with
      | DSVar s ⇒ lookup equiv_dec dsenv s
      | DSSelect cs d ⇒
        match dataset_eval dsenv d with
        | Some rows ⇒
          
          let cfuns: list (string × (list (string × data) → option data)) :=
              map (fun p ⇒ (fst p, fun_of_column (snd p))) (rec_sort cs) in
          
          let rfun: data → option (list (string × data)) :=
              fun row ⇒
                match row with
                | drec fs ⇒
                  listo_to_olist (map (fun p ⇒ lift (fun r ⇒ (fst p, r)) ((snd p) fs)) cfuns)
                | _ ⇒ None
                end
          in
          let results := map (compose (lift drec) rfun) rows in
          listo_to_olist results
        | _ ⇒ None
        end
      | DSFilter c d ⇒
        let cfun := fun_of_column c in
        lift
                  (filter (fun row ⇒
                             match row with
                             | drec fs ⇒
                               match cfun fs with
                               | Some (dbool true) ⇒ true
                               | _ ⇒ false
                               end
                             | _ ⇒ false
                             end))
                  (dataset_eval dsenv d)
      | DSCartesian d1 d2 ⇒
        match dataset_eval dsenv d1, dataset_eval dsenv d2 with
        | Some rs1, Some rs2 ⇒
          let data :=
              flat_map (fun r1 ⇒ map (fun r2 ⇒
                                         match r1, r2 with
                                         | drec a, drec b ⇒ Some (drec (rec_concat_sort a b))
                                         | _, _ ⇒ None
                                         end)
                                      rs2)
                       rs1 in
          listo_to_olist data
        | _, _ ⇒ None
        end
      | DSExplode s d1 ⇒
        match dataset_eval dsenv d1 with
        | Some l ⇒
          let data :=
              flat_map (fun row ⇒
                          match row with
                          | drec fields ⇒
                            match edot fields s with
                            | Some (dcoll inners) ⇒
                              map (fun inner ⇒
                                     orecconcat (drec fields) (drec ((s, inner)::nil)))
                                  inners
                            | _ ⇒ None::nil
                            end
                          | _ ⇒ None::nil
                          end)
                       l in
          listo_to_olist data
        | _ ⇒ None
        end
      end.
  End eval.

  Section DatasetPlug.

    Definition wrap_dataset_eval h dsenv q :=
      lift dcoll (@dataset_eval h dsenv q).

    Lemma fun_of_column_normalized {h c r o}:
      Forall (fun d : string × data ⇒ data_normalized h (snd d)) r →
      fun_of_column h c r = Some o →
      data_normalized h o.

    Lemma dataset_eval_normalized h :
      ∀ q:dataset, ∀ (constant_env:coll_bindings) (o:data),
      Forall (fun x ⇒ data_normalized h (snd x)) (bindings_of_coll_bindings constant_env) →
      wrap_dataset_eval h constant_env q = Some o →
      data_normalized h o.


  End DatasetPlug.

End Dataset.