Module Qcert.NRA.Typing.TNRA

Require Import String.
Require Import List.
Require Import Compare_dec.
Require Import Program.
Require Import Utils.
Require Import DataSystem.
Require Import NRA.

Section TNRA.
  Section typ.
    Context {m:basic_model}.
    Context (τconstants:tbindings).

    Inductive nra_type : nra -> rtype -> rtype -> Prop :=
    | type_NRAGetConstant {τin τout} s :
        tdot τconstants s = Some τout ->
        nra_type (NRAGetConstant s) τin τout
    | type_NRAID {τ} :
        nra_type NRAID τ τ
    | type_NRAConst {τin τout} c :
        data_type (normalize_data brand_relation_brands c) τout ->
        nra_type (NRAConst c) τin τout
    | type_NRABinop {τin τ₁ τ₂ τout} b op1 op2 :
        binary_op_type b τ₁ τ₂ τout ->
        nra_type op1 τin τ₁ ->
        nra_type op2 τin τ₂ ->
        nra_type (NRABinop b op1 op2) τin τout
    | type_NRAUnop {τin τ τout} u op :
        unary_op_type u τ τout ->
        nra_type op τin τ ->
        nra_type (NRAUnop u op) τin τout
    | type_NRAMap {τin τ₁ τ₂} op1 op2 :
        nra_type op1 τ₁ τ₂ ->
        nra_type op2 τin (Coll τ₁) ->
        nra_type (NRAMap op1 op2) τin (Coll τ₂)
    | type_NRAMapProduct {τin τ₁ τ₂ τ₃} op1 op2 pf1 pf2 pf3 :
        nra_type op1 (Rec Closed τ₁ pf1) (Coll (Rec Closed τ₂ pf2)) ->
        nra_type op2 τin (Coll (Rec Closed τ₁ pf1)) ->
        rec_concat_sort τ₁ τ₂ = τ₃ ->
        nra_type (NRAMapProduct op1 op2) τin (Coll (Rec Closed τ₃ pf3))
    | type_NRAProduct {τin τ₁ τ₂ τ₃} op1 op2 pf1 pf2 pf3 :
        nra_type op1 τin (Coll (Rec Closed τ₁ pf1)) ->
        nra_type op2 τin (Coll (Rec Closed τ₂ pf2)) ->
        rec_concat_sort τ₁ τ₂ = τ₃ ->
        nra_type (NRAProduct op1 op2) τin (Coll (Rec Closed τ₃ pf3))
    | type_NRASelect {τin τ} op1 op2 :
        nra_type op1 τ Bool ->
        nra_type op2 τin (Coll τ) ->
        nra_type (NRASelect op1 op2) τin (Coll τ)
    | type_NRADefault {τin τ} op1 op2 :
        nra_type op1 τin (Coll τ) ->
        nra_type op2 τin (Coll τ) ->
        nra_type (NRADefault op1 op2) τin (Coll τ)
    | type_NRAEither {τl τr τout} opl opr :
        nra_type opl τl τout ->
        nra_type opr τr τout ->
        nra_type (NRAEither opl opr) (Either τl τr) τout
    | type_NRAEitherConcat {τin rll pfl rlr pfr rlo pfo lo ro} op1 op2 pflo pfro :
        nra_type op1 τin (Either (Rec Closed rll pfl) (Rec Closed rlr pfr)) ->
        nra_type op2 τin (Rec Closed rlo pfo) ->
        rec_concat_sort rll rlo = lo ->
        rec_concat_sort rlr rlo = ro ->
        nra_type (NRAEitherConcat op1 op2) τin (Either (Rec Closed lo pflo) (Rec Closed ro pfro))
    | type_NRAApp {τin τ1 τ2} op1 op2 :
        nra_type op2 τin τ1 ->
        nra_type op1 τ1 τ2 ->
        nra_type (NRAApp op1 op2) τin τ2.

  End typ.
  
  Notation "Op ▷ A >=> B ⊣ C" := (nra_type C Op A B) (at level 70) .

  Context {m:basic_model}.
  
  Lemma lift_map_typed {τc} {τ₁ τ₂ : rtype} c (op1 : nra) (dl : list data) :
    (bindings_type c τc) ->
    (Forall (fun d : data => data_type d τ₁) dl) ->
    (op1 ▷ τ₁ >=> τ₂ ⊣ τc) ->
    (forall d : data,
        data_type d τ₁ -> exists x : data, brand_relation_brands ⊢ op1 @ₐ d ⊣ c = Some x /\ data_type x τ₂) ->
    exists x : list data, (lift_map (nra_eval brand_relation_brands c op1) dl = Some x) /\ data_type (dcoll x) (Coll τ₂).

  Lemma recover_rec k d r τ pf:
    data_type d r ->
    ` r =
    Rec₀ k
      (map
         (fun x : string * {τ₀ : rtype₀ | wf_rtype₀ τ₀ = true} =>
            (fst x, ` (snd x))) τ) ->
    data_type d (Rec k τ pf).

  Lemma recover_rec_forall k l r τ pf:
    Forall (fun d : data => data_type d r) l ->
    ` r =
    Rec₀ k
      (map
         (fun x : string * {τ₀ : rtype₀ | wf_rtype₀ τ₀ = true} =>
            (fst x, ` (snd x))) τ) ->
    Forall (fun d : data => data_type d (Rec k τ pf)) l.

  Lemma omap_concat_typed
        (τ₁ τ₂ τ₃: list (string * rtype)) (dl2: list data)
        (x : list (string * data)) pf1 pf2 pf3:
    (forall x : data, In x dl2 -> data_type x (Rec Closed τ₂ pf2)) ->
    rec_concat_sort τ₁ τ₂ = τ₃ ->
    data_type (drec x) (Rec Closed τ₁ pf1) ->
    (exists y : list data,
       lift_map (fun x1 : data => orecconcat (drec x) x1) dl2
       = Some y /\ data_type (dcoll y) (Coll (Rec Closed τ₃ pf3))).
      
  Lemma oproduct_typed {τ₁ τ₂ τ₃: list (string * rtype)} (dl dl0: list data) pf1 pf2 pf3:
    Forall (fun d : data => data_type d (Rec Closed τ₂ pf2)) dl0 ->
    Forall (fun d : data => data_type d (Rec Closed τ₁ pf1)) dl ->
    rec_concat_sort τ₁ τ₂ = τ₃ ->
    exists x : list data, (oproduct dl dl0 = Some x) /\ data_type (dcoll x) (Coll (Rec Closed τ₃ pf3)).
  
  Lemma data_type_concat l1 l2 τ:
    data_type (dcoll l1) (Coll τ) ->
    data_type (dcoll l2) (Coll τ) ->
    data_type (dcoll (l1 ++ l2)) (Coll τ).

  Lemma omap_product_typed {τc} {τ₁ τ₂ τ₃ : list (string * rtype)} (op1 : nra) c (dl: list data) pf1 pf2 pf3:
    bindings_type c τc ->
    rec_concat_sort τ₁ τ₂ = τ₃ ->
    Forall (fun d : data => data_type d (Rec Closed τ₁ pf1)) dl ->
    (op1 ▷ Rec Closed τ₁ pf1 >=> Coll (Rec Closed τ₂ pf2) ⊣ τc) ->
    (forall d : data,
                data_type d (Rec Closed τ₁ pf1) ->
                exists x : data,
                   brand_relation_brands ⊢ op1 @ₐ d ⊣ c = Some x /\ data_type x (Coll (Rec Closed τ₂ pf2))) ->
    exists x : list data, (omap_product (nra_eval brand_relation_brands c op1) dl = Some x) /\ data_type (dcoll x) (Coll (Rec Closed τ₃ pf3)).

  Lemma omap_product_typed2 {τc} {τ₁ τ₂ τ₃ : list (string * rtype)} τin (op1 : nra) c y (dl: list data) pf1 pf2 pf3:
    bindings_type c τc ->
    rec_concat_sort τ₁ τ₂ = τ₃ ->
    Forall (fun d : data => data_type d (Rec Closed τ₁ pf1)) dl ->
    (op1 ▷ τin >=> Coll (Rec Closed τ₂ pf2) ⊣ τc) ->
    (forall d : data,
                data_type d (Rec Closed τ₁ pf1) ->
                exists x : data,
                   brand_relation_brands ⊢ op1 @ₐ y ⊣ c = Some x /\ data_type x (Coll (Rec Closed τ₂ pf2))) ->
    exists x : list data, (omap_product (fun z => brand_relation_brands ⊢ op1@ₐ y ⊣ c) dl = Some x) /\ data_type (dcoll x) (Coll (Rec Closed τ₃ pf3)).
  

  Theorem typed_nra_yields_typed_data {τc} {τin τout} cenv (d:data) (op:nra):
    bindings_type cenv τc ->
    (data_type d τin) -> (op ▷ τin >=> τout ⊣ τc) ->
    (exists x, brand_relation_brands ⊢ op @ₐ d ⊣ cenv = Some x /\ (data_type x τout)).



  Definition typed_nra_total {τc} {τin τout} (op:nra) (HOpT: op ▷ τin >=> τout ⊣ τc) c (d:data)
    (dt_c: bindings_type c τc) :
    (data_type d τin) -> { x:data | data_type x τout }.

  Lemma typed_nra_total_eq_matches_eval {τc} {τin τout} (op:nra) (HOpT: op ▷ τin >=> τout ⊣ τc) c (d:data)
    (dt_c: bindings_type c τc)
        (pf: data_type d τin) :
    (brand_relation_brands ⊢ op @ₐd ⊣ c) = Some (proj1_sig (typed_nra_total op HOpT c d dt_c pf)).
  
  Definition tnra_eval {τc} {τin τout} (op:nra) (HOpT: op ▷ τin >=> τout ⊣ τc) c (d:data) (dt_c: bindings_type c τc):
    (data_type d τin) -> data.

End TNRA.

Notation "Op ▷ A >=> B ⊣ C" := (nra_type C Op A B) (at level 70): nra_scope.