Module TNNRC

Section TNNRC.

  Require Import String.
  Require Import List.
  Require Import Arith.
  Require Import Program.
  Require Import EquivDec Morphisms.

  Require Import Utils BasicSystem.
  Require Import cNNRC NNRC.
  Require Import TcNNRC.

  Section typ.

    Context {m:basic_model}.
    Definition nnrc_ext_type (env:tbindings) (n:nnrc) (t:rtype) : Prop :=
      nnrc_type env (nnrc_ext_to_nnrc n) t.
  End typ.
  

  Theorem typed_nnrc_ext_yields_typed_data {m:basic_model} {τ} (env:bindings) (tenv:tbindings) (e:nnrc) :
    bindings_type env tenv ->
    nnrc_ext_type tenv e τ ->
    (exists x, (@nnrc_ext_eval _ brand_relation_brands env e) = Some x /\ (data_type x τ)).

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

End TNNRC.

Ltac nnrc_ext_inverter :=
  unfold nnrc_ext_type, nnrc_ext_to_nnrc in *; simpl in *; try nnrc_inverter.

Ltac nnrc_ext_input_well_typed :=
  repeat progress
         match goal with
         | [HO:nnrc_ext_type ?Γ ?op ?τout,
               HE:bindings_type ?env ?Γ
            |- context [(nnrc_ext_eval brand_relation_brands ?env ?op)]] =>
           let xout := fresh "dout" in
           let xtype := fresh "τout" in
           let xeval := fresh "eout" in
           destruct (typed_nnrc_ext_yields_typed_data env Γ op HE HO)
             as [xout [xeval xtype]]; rewrite xeval in *; simpl
         end.