Qcert.CAMP.Typing.TCAMP

Section TCAMP.

Auxiliary lemmas

Lemma rec_sort_is_sorted {A} (l:list (string ×A)) :
is_list_sorted ODT_lt_dec (domain (rec_sort l)) = true.

Auxiliary definitions and lemmas for type environments

Typing for CAMP

Context {m:basic_model}.

Reserved Notation "Γ |= p ; a ~> b" (at level 90).

Typing rules for CAMP Patterns

  Section t.
    Context (constants:tbindings).
  Inductive pat_type :
    tbindings → pat → rtype → rtype → Prop :=
    | PTconst Γ τ₁ {τ₂} d :
        data_type (normalize_data brand_relation_brands d) τ ₂ →
        Γ |= pconst d ; τ ₁ ~> τ ₂
    | PTunop {Γ τ₁ τ₂ τ₃ u p} :
        Γ |= p ; τ ₁ ~> τ ₂ →
        unaryOp_type u τ ₂ τ ₃ →
        Γ |= punop u p ; τ ₁ ~> τ ₃
    | PTbinop {Γ τ₁ τ₂₁ τ₂₂ τ₃ b p₁ p₂} :
        Γ |= p₁ ; τ ₁ ~> τ ₂₁ →
        Γ |= p₂ ; τ ₁ ~> τ ₂₂ →
        binOp_type b τ ₂₁ τ ₂₂ τ ₃ →
        Γ |= pbinop b p₁ p₂ ; τ ₁ ~> τ ₃
    | PTmap {Γ τ₁ τ₂ p} :
        Γ |= p ; τ ₁ ~> τ ₂ →
                 Γ |= pmap p ; Coll τ ₁ ~> Coll τ ₂

    | PTassert {Γ τ₁ p} pf :
        Γ |= p ; τ ₁ ~> Bool →
        Γ |= passert p ; τ ₁ ~> Rec Closed nil pf
    | PTorElse {Γ τ₁ τ₂ p₁ p₂} :
        Γ |= p₁ ; τ ₁ ~> τ ₂ →
        Γ |= p₂ ; τ ₁ ~> τ ₂ →
        Γ |= porElse p₁ p₂ ; τ ₁ ~> τ ₂
    | PTit Γ τ : Γ |= pit ; τ ~> τ
    | PTletIt {Γ τ₁ τ₂ τ₃ p₁ p₂} :
        Γ |= p₁ ; τ ₁ ~> τ ₂ →
        Γ |= p₂ ; τ ₂ ~> τ ₃ →
        Γ |= pletIt p₁ p₂ ; τ ₁ ~> τ ₃
    | PTgetconstant {Γ} τ₁ s τout:
        tdot constants s = Some τ out →
        Γ |= pgetconstant s ; τ ₁ ~> τ out
    | PTenv {Γ} τ₁ pf :
        Γ |= penv ; τ ₁ ~> Rec Closed Γ pf
    | PTletEnv {Γ τ₁ τ₂ p₁ p₂} Γ' pf Γ'' :
        Γ |= p₁ ; τ ₁ ~> Rec Closed Γ' pf →
        Some Γ'' = merge_bindings Γ Γ' →
        Γ'' |= p₂ ; τ ₁ ~> τ ₂ →
        Γ |= pletEnv p₁ p₂ ; τ ₁ ~> τ ₂
    | PTLeft Γ τl τr :
        Γ |= pleft ; (Either τ l τ r ) ~> τ l
    | PTRight Γ τl τr :
        Γ |= pright ; (Either τ l τ r ) ~> τ r
       where "g |= p ; a ~> b" := (pat_type g p a b).

  End t.

Auxiliary lemmas for the type soudness results

  Lemma data_type_drec_nil pf :
    data_type (drec nil) (Rec Closed nil pf).

  Lemma concat_bindings_type {env₁ env₂ Γ₁ Γ₂} :
    bindings_type env₁ Γ₁ →
    bindings_type env₂ Γ₂ →
    bindings_type (env₁ ++ env₂)
                         (Γ₁ ++ Γ₂).

  Lemma insertion_sort_insert_bindings_type {env Γ d r} s :
     bindings_type env Γ →
     data_type d r →
     bindings_type
     (RSort.insertion_sort_insert rec_field_lt_dec
        (s , d ) env)
     (RSort.insertion_sort_insert rec_field_lt_dec
        (s , r ) Γ).

  Lemma rec_sort_bindings_type {env Γ} :
    bindings_type env Γ →
    bindings_type (rec_sort env)
                         (rec_sort Γ).

  Lemma rec_concat_sort_bindings_type {env₁ env₂ Γ₁ Γ₂} :
    bindings_type env₁ Γ₁ →
    bindings_type env₂ Γ₂ →
    bindings_type (rec_concat_sort env₁ env₂)
                         (rec_concat_sort Γ₁ Γ₂).

  Lemma merge_bindings_type {env₁ env₂ env₃ Γ₁ Γ₂ Γ₃} :
        bindings_type env₁ Γ₁ →
        bindings_type env₂ Γ₂ →
        Some env₃ = merge_bindings env₁ env₂ →
        Some Γ₃ = merge_bindings Γ₁ Γ₂ →
        bindings_type env₃ Γ₃.

Main type soudness lemma

  Notation "[ c & g ] |= p ; a ~> b" := (pat_type c g p a b) (at level 90).

  Theorem typed_pat_success_or_recoverable {c} {τc}
          {Γ τin τout} {p:pat} {env} {d} :
    bindings_type c τ c →
     bindings_type env Γ →
     ([τ c & Γ ] |= p ; τin ~> τ out ) →
     (data_type d τin) →
        (∃ x, interp brand_relation_brands c p env d = Success x ∧ (data_type x τ out ))
        ∨ (interp brand_relation_brands c p env d = RecoverableError ).

Additional lemma used in the correctness for typed translation from NNRC to CAMP

  Lemma pat_type_tenv_rec {τc Γ p τ₁ τ₂} :
    NoDup (domain Γ) →
    [τ c & Γ ] |= p ; τ ₁ ~> τ ₂ →
    [τ c & rec_sort Γ ] |= p ; τ ₁ ~> τ ₂.

  Lemma pat_type_const_sort_f {τc Γ p τ₁ τ₂} :
    [rec_sort τ c & Γ ] |= p ; τ ₁ ~> τ ₂ →
    [τ c & Γ ] |= p ; τ ₁ ~> τ ₂.

  Lemma pat_type_const_sort_b {τc Γ p τ₁ τ₂} :
    [τ c & Γ ] |= p ; τ ₁ ~> τ ₂ →
    [rec_sort τ c & Γ ] |= p ; τ ₁ ~> τ ₂.

  Lemma pat_type_const_sort {τc Γ p τ₁ τ₂} :
    [rec_sort τ c & Γ ] |= p ; τ ₁ ~> τ ₂ ↔
    [τ c & Γ ] |= p ; τ ₁ ~> τ ₂.

End TCAMP.

Notation "[ c & g ] |= p ; a ~> b" := (pat_type c g p a b) (at level 90) : rule_scope.