Qcert.NRA.Typing.TNRA

Section TNRA.

  Section typ.
    Context {m:basic_model}.

  Inductive nra_type : nra → rtype → rtype → Prop :=
  | ATID {τ} :
      nra_type AID τ τ
  | ATConst {τin τout} c :
      data_type (normalize_data brand_relation_brands c) τout → nra_type (AConst c) τin τout
  | ATBinop {τin τ₁ τ₂ τout} b op1 op2 :
      
      binOp_type b τ₁ τ₂ τout →
      nra_type op1 τin τ₁ →
      nra_type op2 τin τ₂ →
      nra_type (ABinop b op1 op2) τin τout
  | ATUnop {τin τ τout} u op :
      unaryOp_type u τ τout →
      nra_type op τin τ →
      nra_type (AUnop u op) τin τout
  | ATMap {τin τ₁ τ₂} op1 op2 :
      nra_type op1 τ₁ τ₂ →
      nra_type op2 τin (Coll τ₁) →
      nra_type (AMap op1 op2) τin (Coll τ₂)
  | ATMapConcat {τ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 (AMapConcat op1 op2) τin (Coll (Rec Closed τ₃ pf3))
  | ATProduct {τ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 (AProduct op1 op2) τin (Coll (Rec Closed τ₃ pf3))
  | ATSelect {τin τ} op1 op2 :
      nra_type op1 τ Bool →
      nra_type op2 τin (Coll τ) →
      nra_type (ASelect op1 op2) τin (Coll τ)
  | ATDefault {τin τ} op1 op2 :
      nra_type op1 τin (Coll τ) →
      nra_type op2 τin (Coll τ) →
      nra_type (ADefault op1 op2) τin (Coll τ)
  | ATEither {τl τr τout} opl opr :
      nra_type opl τl τout →
      nra_type opr τr τout →
      nra_type (AEither opl opr) (Either τl τr) τout
  | ATEitherConcat {τ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 (AEitherConcat op1 op2) τin (Either (Rec Closed lo pflo) (Rec Closed ro pfro))
  | ATApp {τin τ1 τ2} op1 op2 :
      nra_type op2 τin τ1 →
      nra_type op1 τ1 τ2 →
      nra_type (AApp op1 op2) τin τ2.
  End typ.

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

  Context {m:basic_model}.

  Lemma rmap_typed {τ₁ τ₂ : rtype} (op1 : nra) (dl : list data) :
    (Forall (fun d : data ⇒ data_type d τ₁) dl) →
    (op1 ▷ τ₁ >=> τ₂) →
    (∀ d : data,
       data_type d τ₁ → ∃ x : data, brand_relation_brands ⊢ op1 @ₐ d = Some x ∧ data_type x τ₂) →
    ∃ x : list data, (rmap (nra_eval brand_relation_brands 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:
    (∀ x : data, In x dl2 → data_type x (Rec Closed τ₂ pf2)) →
    rec_concat_sort τ₁ τ₂ = τ₃ →
    data_type (drec x) (Rec Closed τ₁ pf1) →
    (∃ y : list data,
       rmap (fun x1 : data ⇒ orecconcat (drec x) x1) dl2
       = Some y ∧ data_type (dcoll y) (Coll (Rec Closed τ₃ pf3))).

  Lemma rproduct_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 τ₁ τ₂ = τ₃ →
    ∃ x : list data, (rproduct 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 rmap_concat_typed {τ₁ τ₂ τ₃ : list (string × rtype)} (op1 : nra) (dl: list data) pf1 pf2 pf3:
    rec_concat_sort τ₁ τ₂ = τ₃ →
    Forall (fun d : data ⇒ data_type d (Rec Closed τ₁ pf1)) dl →
    (op1 ▷ Rec Closed τ₁ pf1 >=> Coll (Rec Closed τ₂ pf2)) →
    (∀ d : data,
                data_type d (Rec Closed τ₁ pf1) →
                ∃ x : data,
                   brand_relation_brands ⊢ op1 @ₐ d = Some x ∧ data_type x (Coll (Rec Closed τ₂ pf2))) →
    ∃ x : list data, (rmap_concat (nra_eval brand_relation_brands op1) dl = Some x) ∧ data_type (dcoll x) (Coll (Rec Closed τ₃ pf3)).

  Lemma rmap_concat_typed2 {τ₁ τ₂ τ₃ : list (string × rtype)} τin (op1 : nra) y (dl: list data) pf1 pf2 pf3:
    rec_concat_sort τ₁ τ₂ = τ₃ →
    Forall (fun d : data ⇒ data_type d (Rec Closed τ₁ pf1)) dl →
    (op1 ▷ τin >=> Coll (Rec Closed τ₂ pf2)) →
    (∀ d : data,
                data_type d (Rec Closed τ₁ pf1) →
                ∃ x : data,
                   brand_relation_brands ⊢ op1 @ₐ y = Some x ∧ data_type x (Coll (Rec Closed τ₂ pf2))) →
    ∃ x : list data, (rmap_concat (fun z ⇒ brand_relation_brands ⊢ op1@ₐ y) dl = Some x) ∧ data_type (dcoll x) (Coll (Rec Closed τ₃ pf3)).

  Theorem typed_nra_yields_typed_data {τin τout} (d:data) (op:nra):
    (data_type d τin) → (op ▷ τin >=> τout) →
    (∃ x, brand_relation_brands ⊢ op @ₐ d = Some x ∧ (data_type x τout)).

  Definition typed_nra_total {τin τout} (op:nra) (HOpT: op ▷ τin >=> τout) (d:data):
    (data_type d τin) → { x:data | data_type x τout }.

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

  Definition tnra_eval {τin τout} (op:nra) (HOpT: op ▷ τin >=> τout) (d:data):
    (data_type d τin) → data.

End TNRA.

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