Qcert.DNNRC.Typing.TDNNRC

  Section TDNNRC.

    Context {m:basic_model}.
    Section tplug.

      Class TAlgPlug {plug_type:Set} {plug:AlgPlug plug_type} :=
        mkTAlgPlug {
            plug_typing : plug_type → tbindings → rtype → Prop;
          }.

    End tplug.

    Section typ.

      Fixpoint tcombine (l:list string) (l':list drtype) {struct l} : option tbindings :=
      match l with
      | [] ⇒ Some []
      | x :: tl ⇒
        match l' with
        | [] ⇒ Some []
        | (Tlocal _) :: _ ⇒ None
        | (Tdistr y) :: tl' ⇒
          match tcombine tl tl' with
          | Some tl'' ⇒ Some ((x,y) :: tl'')
          | None ⇒ None
          end
        end
      end.

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


  End typ.

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

End TDNNRC.