Qcert.DNNRC.Typing.TDNNRCSub

  Section TDNNRCSub.

    Context {m:basic_model}.

    Section typ.

      Inductive dnnrc_type_sub {A plug_type:Set}
                {plug:AlgPlug plug_type} {tplug: TAlgPlug plug_type} :
        tdbindings → dnnrc A plug_type → drtype → Prop :=
      | TDNNRCVar {τ} tenv v : ∀ (a:A), lookup equiv_dec tenv v = Some τ → dnnrc_type_sub tenv (DNNRCVar a v) τ
      | TDNNRCConst {τ} tenv c : ∀ (a:A), data_type (normalize_data brand_relation_brands c) τ → dnnrc_type_sub tenv (DNNRCConst a c) (Tlocal τ)
      | TDNNRCBinop {τ₁ τ₂ τ} tenv b e1 e2 :
          ∀ (a:A),
            binOp_type b τ₁ τ₂ τ →
            dnnrc_type_sub tenv e1 (Tlocal τ₁) →
            dnnrc_type_sub tenv e2 (Tlocal τ₂) →
            dnnrc_type_sub tenv (DNNRCBinop a b e1 e2) (Tlocal τ)
      | TDNNRCUnop {τ₁ τ} tenv u e1 :
          ∀ (a:A),
            unaryOp_type u τ₁ τ →
            dnnrc_type_sub tenv e1 (Tlocal τ₁) →
            dnnrc_type_sub tenv (DNNRCUnop a u e1) (Tlocal τ)
      | TDNNRCLet {τ₁ τ₂} v tenv e1 e2 :
          ∀ (a:A),
            dnnrc_type_sub tenv e1 τ₁ →
            dnnrc_type_sub ((v,τ₁)::tenv) e2 τ₂ →
            dnnrc_type_sub tenv (DNNRCLet a v e1 e2) τ₂
      | TDNRCForLocal {τ₁ τ₂} v tenv e1 e2 :
          ∀ (a:A),
            dnnrc_type_sub tenv e1 (Tlocal (Coll τ₁)) →
            dnnrc_type_sub ((v,(Tlocal τ₁))::tenv) e2 (Tlocal τ₂) →
            dnnrc_type_sub tenv (DNNRCFor a v e1 e2) (Tlocal (Coll τ₂))
      | TDNRCForDist {τ₁ τ₂} v tenv e1 e2 :
          ∀ (a:A),
            dnnrc_type_sub tenv e1 (Tdistr τ₁) →
            dnnrc_type_sub ((v,(Tlocal τ₁))::tenv) e2 (Tlocal τ₂) →
            dnnrc_type_sub tenv (DNNRCFor a v e1 e2) (Tdistr τ₂)
      | TDNRCIf {τ} tenv e1 e2 e3 :
          ∀ (a:A),
            dnnrc_type_sub tenv e1 (Tlocal Bool) →
            dnnrc_type_sub tenv e2 τ →
            dnnrc_type_sub tenv e3 τ →
            dnnrc_type_sub tenv (DNNRCIf a e1 e2 e3) τ
      | TDNNRCEither {τ τl τr} tenv ed xl el xr er :
          ∀ (a:A),
            dnnrc_type_sub tenv ed (Tlocal (Either τl τr)) →
            dnnrc_type_sub ((xl,(Tlocal τl))::tenv) el τ →
            dnnrc_type_sub ((xr,(Tlocal τr))::tenv) er τ →
            dnnrc_type_sub tenv (DNNRCEither a ed xl el xr er) τ
      | TDNNRCCollect {τ} tenv e :
          ∀ (a:A),
            dnnrc_type_sub tenv e (Tdistr τ) →
            dnnrc_type_sub tenv (DNNRCCollect a e) (Tlocal (Coll τ))
      | TDNNRCDispatch {τ} tenv e :
          ∀ (a:A),
            dnnrc_type_sub tenv e (Tlocal (Coll τ)) →
            dnnrc_type_sub tenv (DNNRCDispatch a e) (Tdistr τ)
      
      | TDNNRCAlg {τout} tenv tbindings op nl :
        ∀ (a:A),
          Forall2 (fun n τ ⇒ fst n = fst τ
                              ∧ dnnrc_type_sub tenv (snd n) (Tdistr (snd τ)))
                  nl tbindings →
           plug_typing op tbindings (Coll τout) →
           dnnrc_type_sub tenv (DNNRCAlg a op nl) (Tdistr τout)
      | TDNNRCSubsumption {τenv τout} τenv' τout' e:
         tdbindings_sub τenv' τenv →
         drtype_sub τout τout' →
         dnnrc_type_sub τenv e τout →
         dnnrc_type_sub τenv' e τout'
      .

      Global Instance dnnrc_type_sub_proper {A plug_type:Set} {plug:AlgPlug plug_type} {tplug: TAlgPlug plug_type} :
        Proper (tdbindings_sub --> eq ==> drtype_sub ==> impl) (dnnrc_type_sub (A:=A)).

     Global Instance dbindings_type_proper :
       Proper (eq ==> tdbindings_sub ==> impl) dbindings_type.

  End typ.

    Section lift.

      Lemma dnnrc_type_to_dnnrc_type_sub {A} (plug_type:Set) (plug:AlgPlug plug_type) {tplug:TAlgPlug plug_type} {τ} (env:dbindings) (tenv:tdbindings) (e:dnnrc A plug_type) :
        dnnrc_type tenv e τ →
        dnnrc_type_sub tenv e τ.

    End lift.

    Theorem typed_dnnrc_yields_typed_data {A} {plug_type:Set} (plug:AlgPlug plug_type) {tplug:TAlgPlug plug_type} {τ} (env:dbindings) (tenv:tdbindings) (e:dnnrc A plug_type) :
    dbindings_type env tenv →
    dnnrc_type_sub tenv e τ →
    (∃ x, (dnnrc_eval brand_relation_brands env e) = Some x ∧ (ddata_type x τ)).

  End TDNNRCSub.