Module Qcert.NRAEnv.Typing.TNRAEnv


Section TNRAEnv.
  Require Import String.
  Require Import List.
  Require Import Compare_dec.
  Require Import Program.
  Require Import Utils.
  Require Import CommonSystem.
  Require Import cNRAEnvSystem.
  Require Import NRAEnv.
  Require Import NRAEnvEq.

  Local Open Scope nraenv_scope.
  
Typing for NRA
  Section typ.
    Context {m:basic_model}.
    Contextconstants:list (string*rtype)).
    Definition nraenv_type (q:nraenv) : rtype -> rtype -> rtype -> Prop :=
      @nraenv_core_type m τconstants (nraenv_to_nraenv_core q).

  End typ.

  Notation "Op ▷ₓ A >=> BC ; E" := (nraenv_type C Op E A B) (at level 70).

Type lemmas for individual algebraic expressions

  Section prop.
    Context {m:basic_model}.
  
Main typing soundness theorem for the NRA

    Lemma typed_nraenv_yields_typed_nraenv_corec τenv τin τout} (op:nraenv):
      (op ▷ₓ τin >=> τout ⊣ τcenv) -> nraenv_core_type τc (nraenv_to_nraenv_core op) τenv τin τout.
Proof.
      unfold nraenv_type; intro; assumption.
    Qed.

    Lemma typed_nraenv_core_yields_typed_nraenvc τenv τin τout} (op:nraenv):
      nraenv_core_type τc (nraenv_to_nraenv_core op) τenv τin τout -> (op ▷ₓ τin >=> τout ⊣ τcenv).
Proof.
      revert τin τout τenv.
      induction op; intros;
      (* Takes care of all core operators *)
      unfold nraenv_type; assumption;
      try (solve[inversion H; clear H; subst; repeat econstructor; eauto]).
    Qed.
    
    Theorem typed_nraenv_core_iff_typed_nraenvc τenv τin τout} (op:nraenv):
      (op ▷ₓ τin >=> τout ⊣ τcenv) <-> nraenv_core_type τc (nraenv_to_nraenv_core op) τenv τin τout.
Proof.
      split.
      apply typed_nraenv_yields_typed_nraenv_core.
      apply typed_nraenv_core_yields_typed_nraenv.
    Qed.
    
    Theorem typed_nraenv_yields_typed_datac τenv τin τout} c (env:data) (d:data) (op:nraenv):
      bindings_type c τc ->
      (env ▹ τenv) -> (d ▹ τin) -> (op ▷ₓ τin >=> τout ⊣ τcenv) ->
      (exists x, (nraenv_eval brand_relation_brands c op env d = Some x /\ (x ▹ τout))).
Proof.
      intros.
      unfold nraenv_eval.
      apply (@typed_nraenv_core_yields_typed_data m τc τenv τin τout); try assumption.
    Qed.

Corrolaries of the main type soudness theorem

    Definition typed_nraenv_totalc τenv τin τout} (op:nraenv) (HOpT: op ▷ₓ τin >=> τout ⊣ τcenv) c (env:data) (d:data):
      bindings_type c τc ->
      (env ▹ τenv) ->
      (d ▹ τin) ->
      { x:data | x ▹ τout }.
Proof.
      intros Hc Henv.
      intros HdT.
      generalize (typed_nraenv_yields_typed_data c env d op Hc Henv HdT HOpT).
      intros.
      destruct (nraenv_eval brand_relation_brands c op env d).
      assert (data_type d0 τout).
      - inversion H. inversion H0. inversion H1. trivial.
      - exists d0. trivial.
      - cut False. intuition. inversion H.
        destruct H0. inversion H0.
    Defined.

    Definition tnraenv_evalc τenv τin τout} (op:nraenv) (HOpT: op ▷ₓ τin >=> τout ⊣ τcenv) c (env:data) (d:data):
      bindings_type c τc ->
      (env ▹ τenv) -> (d ▹ τin) -> data.
Proof.
      intros Hc Henv.
      intros HdT.
      destruct (typed_nraenv_total op HOpT c env d Hc Henv HdT).
      exact x.
    Defined.
  End prop.

End TNRAEnv.


Notation "Op ▷ₓ A >=> BC ; E" := (nraenv_type C Op E A B) (at level 70).
Notation "Op @▷ₓ dC ; e" := (tnraenv_eval C Op e d) (at level 70).

  
Hint Unfold nraenv_type.
Hint Constructors unary_op_type.
Hint Constructors binary_op_type.

Ltac nraenv_inferer :=
  unfold nraenv_type in *;
  unfold nraenv_eval; simpl in *;
  try nraenv_core_inverter; subst; try eauto.

Ltac nraenv_input_well_typed :=
  repeat progress
         match goal with
           | [HO:?op ▷ₓ ?τin >=> ?τout ⊣ ?τc ; ?τenv,
              HI:?x ▹ ?τin,
              HE:?env ▹ ?τenv,
              HC:bindings_type ?cc
              |- context [(nraenv_eval ?h ?c ?op ?env ?x)]] =>
             let xout := fresh "dout" in
             let xtype := freshout" in
             let xeval := fresh "eout" in
             destruct (typed_nraenv_yields_typed_data _ _ _ op HC HE HI HO)
               as [xout [xeval xtype]]; rewrite xeval in *; simpl
         end; input_well_typed.