Qcert.Basic.Typing.TDataInfer

Section TDataInfer.




  Context {fdata:foreign_data}.
  Context {ftype:foreign_type}.
  Context {fdtyping:foreign_data_typing}.

  Context {m:brand_model}.

  Fixpoint infer_data_type (d:data) : option rtype
    := match d with
         | dunit ⇒ Some Unit
         | dnat n ⇒ Some Nat
         | dbool b ⇒ Some Bool
         | dstring s ⇒ Some String
         | dcoll ld ⇒
           lift Coll
                ((fix infer_data_type_dcoll ld : option rtype
                  := match ld with
                       | nil ⇒ Some ⊥
                       | d::ld' ⇒ lift2 join (infer_data_type d) (infer_data_type_dcoll ld')
                     end
                 ) ld)
         | drec lsd ⇒
           match (fix infer_data_type_drec lsd : option (list(string×rtype))
                  := match lsd with
                       | nil ⇒ Some nil
                       | (s,d)::lsd' ⇒
                         match (infer_data_type d), (infer_data_type_drec lsd') with
                           | Some r, Some lsr' ⇒
                             Some ((s,r)::lsr')
                           | _, _ ⇒ None
                         end
                     end
                 ) lsd with
             | Some l ⇒ RecMaybe Closed l
             | None ⇒ None
           end
         | dleft d ⇒
            lift (fun t ⇒ Either t ⊥) (infer_data_type d)
         | dright d ⇒
            lift (fun t ⇒ Either ⊥ t) (infer_data_type d)
         | dbrand b d ⇒
           match is_canon_brands_dec brand_relation_brands b with
              | left pf ⇒ match infer_data_type d with
                           | Some t ⇒
                             if subtype_dec t (brands_type b)
                             then Some (Brand b)
                             else Some ⊤
                  | None ⇒ None
                end
              | right _ ⇒ None
           end
         | dforeign df ⇒ lift Foreign (foreign_data_typing_infer df)
       end.

  Lemma infer_data_type_drec_domain {d:list (string×data)} {r'} :
    (fix infer_data_type_drec lsd : option (list(string×rtype))
                  := match lsd with
                       | nil ⇒ Some nil
                       | (s,d)::lsd' ⇒
                         match (infer_data_type d), (infer_data_type_drec lsd') with
                           | Some r, Some lsr' ⇒
                             Some ((s,r)::lsr')
                           | _, _ ⇒ None
                         end
                     end
                 ) d = Some r' →
     domain d = domain r'.

  Lemma infer_data_type_normalized' {d} :
    data_normalized brand_relation_brands d →
    {τ | infer_data_type d = Some τ}.

  Theorem infer_data_type_normalized {d} :
    data_normalized brand_relation_brands d →
    {τ | infer_data_type d = Some τ}.

  Theorem infer_data_type_correct {d τ} :
    infer_data_type d = Some τ →
    d ▹ τ.

  Theorem infer_data_type_least {d τ₁ τ₂} :
    infer_data_type d = Some τ₁ →
    d ▹τ₂ →
    τ₁ <: τ₂.

  Theorem infer_data_type_complete {d τ} :
    d ▹τ → {τ' | infer_data_type d = Some τ'}.

  Lemma normalized_data_type_infer {d τ} :
    infer_data_type d = Some τ →
    data_normalized brand_relation_brands d.


  Section dt_dec.

    Theorem data_type_dec d τ : {data_type d τ} + {¬ data_type d τ}.
  End dt_dec.

End TDataInfer.