Qcert.OQL.Typing.TOQL

Section TOQL.

Typing for CAMP

  Section typ.

    Context {m:basic_model}.
    Section constt.
      Context (τconstants:tbindings).

      Inductive oql_expr_type : tbindings → oql_expr → rtype → Prop :=
      | OTConst {τ} tenv c :
          data_type (normalize_data brand_relation_brands c) τ →
          oql_expr_type tenv (OConst c) τ
      | OTVar {τ} tenv v :
          edot tenv v = Some τ → oql_expr_type tenv (OVar v) τ
      | OTTable {τ} tenv s :
          tdot τ constants s = Some τ →
          oql_expr_type tenv (OTable s) τ
      | OTBinop {τ₁ τ₂ τout} tenv b e₁ e₂ :
          oql_expr_type tenv e₁ τ ₁ →
          oql_expr_type tenv e₂ τ ₂ →
          binOp_type b τ ₁ τ ₂ τ out →
          oql_expr_type tenv (OBinop b e₁ e₂) τ out
      | OTUnop {τ₁ τout} tenv u e₁ :
          oql_expr_type tenv e₁ τ ₁ →
          unaryOp_type u τ ₁ τ out →
          oql_expr_type tenv (OUnop u e₁) τ out.

    End constt.

    Context (τconstants:tbindings).

    Inductive oql_query_program_type : tbindings → tbindings → oql_query_program → rtype → Prop :=
    | OTDefineQuery {tenv s e rest τ} {tdefls τ₁} :
        oql_expr_type (rec_concat_sort τ constants tdefls) tenv e τ ₁ →
        oql_query_program_type (rec_concat_sort tdefls ((s ,τ ₁ )::nil)) tenv rest τ →
        oql_query_program_type tdefls tenv (ODefineQuery s e rest) τ
    | OTUndefineQuery {tenv s rest tdefls τ} :
        oql_query_program_type (rremove tdefls s) tenv rest τ →
        oql_query_program_type tdefls tenv (OUndefineQuery s rest) τ
    |OTQuery {tdefls tenv e τ}:
     oql_expr_type (rec_concat_sort τ constants tdefls) tenv e τ →
     oql_query_program_type tdefls tenv (OQuery e) τ.

    Definition oql_type (o:oql_query_program) (τ:rtype) : Prop
      := oql_query_program_type nil nil o τ.

    End typ.

  Theorem typed_oql_expr_yields_typed_data {m:basic_model} {τc} {τenv τout} c (env:list (string ×data)) (q:oql_expr):
    bindings_type c τ c →
    bindings_type env τ env →
    (oql_expr_type τ c τ env q τ out ) →
    (∃ x, (oql_expr_interp brand_relation_brands c q env = Some x ∧ (x ▹ τ out ))).

  Lemma bindings_type_app {m:basic_model} l1 l2 r1 r2 :
    bindings_type l1 r1 → bindings_type l2 r2 →
    bindings_type (l1 ++ l2) (r1 ++ r2) .

  Lemma bindings_type_rec_concat_sort {m:basic_model} l1 l2 r1 r2 :
    bindings_type l1 r1 → bindings_type l2 r2 →
    bindings_type (rec_concat_sort l1 l2) (rec_concat_sort r1 r2) .

  Lemma typed_oql_query_program_yields_typed_data {m:basic_model} {τc τdefls} {τenv τout} c (defls env:list (string ×data)) (q:oql_query_program):
    bindings_type c τ c →
    bindings_type defls τ defls →
    bindings_type env τ env →
    (oql_query_program_type τ c τ defls τ env q τ out ) →
    (∃ x, (oql_query_program_interp brand_relation_brands c defls q env = Some x ∧ (x ▹ τ out ))).

Main typing soundness theorem for OQL

  Theorem typed_oql_yields_typed_data {m:basic_model} {τc} {τout} c (q:oql_query_program):
    bindings_type c τ c →
    oql_type τ c q τ out →
    (∃ x, (oql_interp brand_relation_brands c q = Some x ∧ (x ▹ τ out ))).

End TOQL.