Qcert.NNRC.Typing.TcNNRC

Section TcNNRC.

  Section typ.

    Context {m:basic_model}.

    Inductive nnrc_type : tbindings → nnrc → rtype → Prop :=
    | TNNRCVar {τ} tenv v : lookup equiv_dec tenv v = Some τ → nnrc_type tenv (NNRCVar v) τ
    | TNNRCConst {τ} tenv c : data_type (normalize_data brand_relation_brands c) τ → nnrc_type tenv (NNRCConst c) τ
    | TNNRCBinop {τ₁ τ₂ τ} tenv b e1 e2 :
        binOp_type b τ₁ τ₂ τ →
        nnrc_type tenv e1 τ₁ →
        nnrc_type tenv e2 τ₂ →
        nnrc_type tenv (NNRCBinop b e1 e2) τ
    | TNNRCUnop {τ₁ τ} tenv u e1 :
        unaryOp_type u τ₁ τ →
        nnrc_type tenv e1 τ₁ →
        nnrc_type tenv (NNRCUnop u e1) τ
    | TNNRCLet {τ₁ τ₂} v tenv e1 e2 :
        nnrc_type tenv e1 τ₁ →
        nnrc_type ((v,τ₁)::tenv) e2 τ₂ →
        nnrc_type tenv (NNRCLet v e1 e2) τ₂
    | TNNRCFor {τ₁ τ₂} v tenv e1 e2 :
        nnrc_type tenv e1 (Coll τ₁) →
        nnrc_type ((v,τ₁)::tenv) e2 τ₂ →
        nnrc_type tenv (NNRCFor v e1 e2) (Coll τ₂)
    | TNNRCIf {τ} tenv e1 e2 e3 :
        nnrc_type tenv e1 Bool →
        nnrc_type tenv e2 τ →
        nnrc_type tenv e3 τ →
        nnrc_type tenv (NNRCIf e1 e2 e3) τ
    | TNNRCEither {τ τl τr} tenv ed xl el xr er :
        nnrc_type tenv ed (Either τl τr) →
        nnrc_type ((xl,τl)::tenv) el τ →
        nnrc_type ((xr,τr)::tenv) er τ →
        nnrc_type tenv (NNRCEither ed xl el xr er) τ.

  End typ.

  Theorem typed_nnrc_yields_typed_data {m:basic_model} {τ} (env:bindings) (tenv:tbindings) (e:nnrc) :
    bindings_type env tenv →
    nnrc_type tenv e τ →
    (∃ x, (nnrc_core_eval brand_relation_brands env e) = Some x ∧ (data_type x τ)).

  Global Instance nnrc_type_lookup_equiv_prop {m:basic_model} :
    Proper (lookup_equiv ==> eq ==> eq ==> iff) nnrc_type.

End TcNNRC.