Module Qcert.cNRAEnv.Typing.TcNRAEnv

Require Import Bool.
Require Import String.
Require Import List.
Require Import Compare_dec.
Require Import Eqdep_dec.
Require Import Program.
Require Import Utils.
Require Import DataSystem.
Require Import cNRAEnv.
Require Import cNRAEnvEq.
Require Import NRASystem.

Import ListNotations.
Local Open Scope list_scope.

Section TcNRAEnv.
  Local Open Scope nraenv_core_scope.
  
  Section typ.
    Context {m:basic_model}.
    Context (τconstants:tbindings).
  
  Inductive nraenv_core_type : nraenv_core -> rtype -> rtype -> rtype -> Prop :=
  | type_cNRAEnvGetConstant {τenv τin τout} s :
      tdot τconstants s = Some τout ->
      nraenv_core_type (cNRAEnvGetConstant s) τenv τin τout
  | type_cNRAEnvID {τenv τ} :
      nraenv_core_type cNRAEnvID τenv τ τ
  | type_cNRAEnvConst {τenv τin τout} c :
      data_type (normalize_data brand_relation_brands c) τout -> nraenv_core_type (cNRAEnvConst c) τenv τin τout
  | type_cNRAEnvBinop {τenv τin τ₁ τ₂ τout} b op1 op2 :
      binary_op_type b τ₁ τ₂ τout ->
      nraenv_core_type op1 τenv τin τ₁ ->
      nraenv_core_type op2 τenv τin τ₂ ->
      nraenv_core_type (cNRAEnvBinop b op1 op2) τenv τin τout
  | type_cNRAEnvUnop {τenv τin τ τout} u op :
      unary_op_type u τ τout ->
      nraenv_core_type op τenv τin τ ->
      nraenv_core_type (cNRAEnvUnop u op) τenv τin τout
  | type_cNRAEnvMap {τenv τin τ₁ τ₂} op1 op2 :
      nraenv_core_type op1 τenv τ₁ τ₂ ->
      nraenv_core_type op2 τenv τin (Coll τ₁) ->
      nraenv_core_type (cNRAEnvMap op1 op2) τenv τin (Coll τ₂)
  | type_cNRAEnvMapProduct {τenv τin τ₁ τ₂ τ₃} op1 op2 pf1 pf2 pf3 :
      nraenv_core_type op1 τenv (Rec Closed τ₁ pf1) (Coll (Rec Closed τ₂ pf2)) ->
      nraenv_core_type op2 τenv τin (Coll (Rec Closed τ₁ pf1)) ->
      rec_concat_sort τ₁ τ₂ = τ₃ ->
      nraenv_core_type (cNRAEnvMapProduct op1 op2) τenv τin (Coll (Rec Closed τ₃ pf3))
  | type_cNRAEnvProduct {τenv τin τ₁ τ₂ τ₃} op1 op2 pf1 pf2 pf3 :
      nraenv_core_type op1 τenv τin (Coll (Rec Closed τ₁ pf1)) ->
      nraenv_core_type op2 τenv τin (Coll (Rec Closed τ₂ pf2)) ->
      rec_concat_sort τ₁ τ₂ = τ₃ ->
      nraenv_core_type (cNRAEnvProduct op1 op2) τenv τin (Coll (Rec Closed τ₃ pf3))
  | type_cNRAEnvSelect {τenv τin τ} op1 op2 :
      nraenv_core_type op1 τenv τ Bool ->
      nraenv_core_type op2 τenv τin (Coll τ) ->
      nraenv_core_type (cNRAEnvSelect op1 op2) τenv τin (Coll τ)
  | type_cNRAEnvDefault {τenv τin τ} op1 op2 :
      nraenv_core_type op1 τenv τin (Coll τ) ->
      nraenv_core_type op2 τenv τin (Coll τ) ->
      nraenv_core_type (cNRAEnvDefault op1 op2) τenv τin (Coll τ)
  | type_cNRAEnvEither {τenv τl τr τout} opl opr :
      nraenv_core_type opl τenv τl τout ->
      nraenv_core_type opr τenv τr τout ->
      nraenv_core_type (cNRAEnvEither opl opr) τenv (Either τl τr) τout
  | type_cNRAEnvEitherConcat {τenv τin rll pfl rlr pfr rlo pfo lo ro} op1 op2 pflo pfro :
      nraenv_core_type op1 τenv τin (Either (Rec Closed rll pfl) (Rec Closed rlr pfr)) ->
      nraenv_core_type op2 τenv τin (Rec Closed rlo pfo) ->
      rec_concat_sort rll rlo = lo ->
      rec_concat_sort rlr rlo = ro ->
      nraenv_core_type (cNRAEnvEitherConcat op1 op2) τenv τin (Either (Rec Closed lo pflo) (Rec Closed ro pfro))
  | type_cNRAEnvApp {τenv τin τ1 τ2} op2 op1 :
      nraenv_core_type op1 τenv τin τ1 ->
      nraenv_core_type op2 τenv τ1 τ2 ->
      nraenv_core_type (cNRAEnvApp op2 op1) τenv τin τ2
  | type_cNRAEnvEnv {τenv τin} :
      nraenv_core_type cNRAEnvEnv τenv τin τenv
  | type_cNRAEnvAppEnv {τenv τenv' τin τ2} op2 op1 :
      nraenv_core_type op1 τenv τin τenv' ->
      nraenv_core_type op2 τenv' τin τ2 ->
      nraenv_core_type (cNRAEnvAppEnv op2 op1) τenv τin τ2
  | type_cNRAEnvMapEnv {τenv τin τ₂} op1 :
      nraenv_core_type op1 τenv τin τ₂ ->
      nraenv_core_type (cNRAEnvMapEnv op1) (Coll τenv) τin (Coll τ₂).
  End typ.

  Notation "Op ▷ A >=> B ⊣ C ; E" := (nraenv_core_type C Op E A B) (at level 70).


  Context {m:basic_model}.
  
  Lemma lift_map_typed {τc} {τenv τ₁ τ₂ : rtype} c (op1 : nraenv_core) (env:data) (dl : list data) :
    (bindings_type c τc) ->
    (env ▹ τenv) ->
    (Forall (fun d : data => data_type d τ₁) dl) ->
    (op1 ▷ τ₁ >=> τ₂ ⊣ τc; τenv) ->
    (forall d : data,
       data_type d τ₁ -> exists x : data, brand_relation_brands ⊢ₑ op1 @ₑ d ⊣ c; env = Some x /\ x ▹ τ₂) ->
    exists x : list data, (lift_map (nraenv_core_eval brand_relation_brands c op1 env) dl = Some x) /\ data_type (dcoll x) (Coll τ₂).

  Lemma lift_map_env_typed {τc} {τenv τ₁ τ₂ : rtype} c (op1 : nraenv_core) (x0:data) (dl : list data) :
    bindings_type c τc ->
    (x0 ▹ τ₁) ->
    (Forall (fun d : data => data_type d τenv) dl) ->
    (op1 ▷ τ₁ >=> τ₂ ⊣ τc;τenv) ->
    (forall env : data,
       data_type env τenv ->
       forall d : data,
         data_type d τ₁ ->
         exists x : data, brand_relation_brands ⊢ₑ op1 @ₑ d ⊣ c;env = Some x /\ data_type x τ₂) ->
    exists x : list data, (lift_map (fun env' => (nraenv_core_eval brand_relation_brands c op1 env' x0)) dl = Some x) /\ data_type (dcoll x) (Coll τ₂).

  Lemma recover_rec k d r τ pf:
    data_type d r ->
    ` r =
    Rec₀ k
      (map
         (fun x : string * {τ₀ : rtype₀ | wf_rtype₀ τ₀ = true} =>
            (fst x, ` (snd x))) τ) ->
    data_type d (Rec k τ pf).

  Lemma recover_rec_forall k l r τ pf:
    Forall (fun d : data => data_type d r) l ->
    ` r =
    Rec₀ k
      (map
         (fun x : string * {τ₀ : rtype₀ | wf_rtype₀ τ₀ = true} =>
            (fst x, ` (snd x))) τ) ->
    Forall (fun d : data => data_type d (Rec k τ pf)) l.

  Lemma omap_concat_typed_env
        (τenv:rtype) (τ₁ τ₂ τ₃: list (string * rtype)) (env:data) (dl2: list data)
        (x : list (string * data)) pf1 pf2 pf3:
    (data_type env τenv) ->
    (forall x : data, In x dl2 -> data_type x (Rec Closed τ₂ pf2)) ->
    rec_concat_sort τ₁ τ₂ = τ₃ ->
    data_type (drec x) (Rec Closed τ₁ pf1) ->
    (exists y : list data,
       lift_map (fun x1 : data => orecconcat (drec x) x1) dl2
       = Some y /\ data_type (dcoll y) (Coll (Rec Closed τ₃ pf3))).

  Lemma oproduct_typed_env {τ₁ τ₂ τ₃: list (string * rtype)} (dl dl0: list data) pf1 pf2 pf3:
    Forall (fun d : data => data_type d (Rec Closed τ₂ pf2)) dl0 ->
    Forall (fun d : data => data_type d (Rec Closed τ₁ pf1)) dl ->
    rec_concat_sort τ₁ τ₂ = τ₃ ->
    exists x : list data, (oproduct dl dl0 = Some x) /\ data_type (dcoll x) (Coll (Rec Closed τ₃ pf3)).
  
  Lemma data_type_concat l1 l2 τ:
    data_type (dcoll l1) (Coll τ) ->
    data_type (dcoll l2) (Coll τ) ->
    data_type (dcoll (l1 ++ l2)) (Coll τ).

  Lemma omap_product_typed_env {τc} {τenv:rtype} {τ₁ τ₂ τ₃ : list (string * rtype)} (op1 : nraenv_core) c (env:data) (dl: list data) pf1 pf2 pf3:
    bindings_type c τc ->
    env ▹ τenv ->
    rec_concat_sort τ₁ τ₂ = τ₃ ->
    Forall (fun d : data => data_type d (Rec Closed τ₁ pf1)) dl ->
    (op1 ▷ Rec Closed τ₁ pf1 >=> Coll (Rec Closed τ₂ pf2) ⊣ τc;τenv) ->
    (forall d : data,
                data_type d (Rec Closed τ₁ pf1) ->
                exists x : data,
                   brand_relation_brands ⊢ₑ op1 @ₑ d ⊣ c;env = Some x /\ data_type x (Coll (Rec Closed τ₂ pf2))) ->
    exists x : list data, (omap_product (nraenv_core_eval brand_relation_brands c op1 env) dl = Some x) /\ data_type (dcoll x) (Coll (Rec Closed τ₃ pf3)).

  Lemma omap_product_typed2_env {τc} {τenv:rtype} {τ₁ τ₂ τ₃ : list (string * rtype)} τin c (op1 : nraenv_core) (env:data) y (dl: list data) pf1 pf2 pf3:
    bindings_type c τc ->
    env▹ τenv ->
    rec_concat_sort τ₁ τ₂ = τ₃ ->
    Forall (fun d : data => data_type d (Rec Closed τ₁ pf1)) dl ->
    (op1 ▷ τin >=> Coll (Rec Closed τ₂ pf2) ⊣ τc;τenv) ->
    (forall d : data,
                data_type d (Rec Closed τ₁ pf1) ->
                exists x : data,
                   brand_relation_brands ⊢ₑ op1 @ₑ y ⊣ c;env = Some x /\ data_type x (Coll (Rec Closed τ₂ pf2))) ->
    exists x : list data, (omap_product (fun z => brand_relation_brands ⊢ₑ op1@ₑ y ⊣ c;env) dl = Some x) /\ data_type (dcoll x) (Coll (Rec Closed τ₃ pf3)).


  Theorem typed_nraenv_core_yields_typed_data {τc} {τenv τin τout} c (env:data) (d:data) (op:nraenv_core):
    bindings_type c τc ->
    (env ▹ τenv) -> (d ▹ τin) -> (op ▷ τin >=> τout ⊣ τc;τenv) ->
    (exists x, (brand_relation_brands ⊢ₑ op @ₑ d ⊣ c;env = Some x /\ (x ▹ τout))).


  Local Hint Constructors nra_type unary_op_type binary_op_type : qcert.
  Local Hint Resolve ATdot ATnra_data : qcert.

  Definition typed_nraenv_core_total {τc} {τenv τin τout} (op:nraenv_core) (HOpT: op ▷ τin >=> τout ⊣ τc;τenv) c (env:data) (d:data)
    (dt_c: bindings_type c τc) :
    (env ▹ τenv) ->
    (d ▹ τin) ->
    { x:data | x ▹ τout }.

  Definition tnraenv_core_eval {τc} {τenv τin τout} (op:nraenv_core) (HOpT: op ▷ τin >=> τout ⊣ τc;τenv) c (env:data) (d:data)
             (dt_c: bindings_type c τc) :
    (env ▹ τenv) -> (d ▹ τin) -> data.

  Theorem typed_nraenv_core_to_typed_nra {τc} {τenv τin τout} (op:nraenv_core):
    (nraenv_core_type τc op τenv τin τout) -> (nra_type τc (nra_of_nraenv_core op) (nra_context_type τenv τin) τout).

  Lemma fold_nra_context_type (env d: {τ₀ : rtype₀ | wf_rtype₀ τ₀ = true}) pf :
    Rec Closed [("PBIND"%string, env); ("PDATA"%string, d)] pf
    = nra_context_type env d.

  Ltac defst l
    := match l with
       | @nil (string*rtype₀) => constr:(@nil (string*rtype))
       | cons (?x,proj1_sig ?y) ?l' =>
         let l'' := defst l' in
         constr:(cons (x,y) l'')
       end.
  
  Ltac rec_proj_simpler
    := repeat
         match goal with
         | [H: Rec₀ ?k ?l = proj1_sig ?τ |- _ ] => symmetry in H
         | [H: proj1_sig ?τ = Rec₀ ?k ?l |- _ ] =>
           let ll := defst l in
           let HH:=fresh "eqq" in
           generalize (@Rec₀_eq_proj1_Rec _ _ τ k ll); intros HH;
           simpl in HH; specialize (HH H); clear H; destruct HH;
           try subst τ
         end.
  
  Lemma UIP_bool {a b:bool} (pf1 pf2:a = b) : pf1 = pf2.

  Ltac nra_inverter_ext
    :=
      simpl in *; match goal with
                  | [H:@nra_type _ _ (unnest_two _ _ _) _ (Coll _) |- _ ] => apply ATunnest_two_inv in H;
                                                                           destruct H as [? [? [? [? [? [? [?[??]]]]]]]]
                  | [H: prod _ _ |- _ ] => destruct H; simpl in *; try subst
                  | [H: context [Rec Closed [("PBIND"%string, ?env); ("PDATA"%string, ?d)] ?pf ] |- _ ] => unfold rtype in H; rewrite (fold_nra_context_type env d pf) in H
                  | [H: Rec₀ ?k ?l = proj1_sig ?τ |- _ ] => symmetry in H
                  | [H: proj1_sig ?τ = Rec₀ ?k ?l |- _ ] =>
                    let ll := defst l in
                    let HH:=fresh "eqq" in
                    generalize (@Rec₀_eq_proj1_Rec _ _ τ k ll); intros HH;
                    simpl in HH; specialize (HH H); clear H; destruct HH;
                    try subst τ
                  | [H:proj1_sig _ =
                       Rec₀ Closed
                            (map
                               (fun x : string * {τ₀ : rtype₀ | wf_rtype₀ τ₀ = true} =>
                                  (fst x, ` (snd x))) _) |- _ ]
                    => let Hpf := fresh "spf" in
                       apply Rec₀_eq_proj1_Rec in H; destruct H as [? Hpf]
                  | [H1:@eq bool ?a ?b,
                        H2:@eq bool ?a ?b |- _] => destruct (UIP_bool H1 H2)
                  end.

  Ltac nra_inverter2 :=
    repeat (try unfold nra_wrap, nra_wrap_a1, nra_wrap_bind_a1, nra_context, nra_double, nra_bind, nra_wrap in *; (nra_inverter_ext || nra_inverter); try subst).

  Ltac tdot_inverter :=
    repeat
      match goal with
        | [H: tdot _ _ = Some _ |- _ ] =>
          let HH:= fresh "eqq" in
          inversion H as [HH];
            match type of HH with
              | ?x1 = ?x2 => try (subst x2 || subst x1); clear H
              | _ => fail 1
            end
      end.

  Lemma typed_nraenv_core_to_typed_nra_inv' {k τc τenv τin τout pf} (op:nraenv_core):
    nra_type τc (nra_of_nraenv_core op) (Rec k [("PBIND"%string, τenv); ("PDATA"%string, τin)] pf) τout ->
    nraenv_core_type τc op τenv τin τout.
  
  Theorem typed_nraenv_core_to_typed_nra_inv {τc} {τenv τin τout} (op:nraenv_core):
    nra_type τc (nra_of_nraenv_core op) (nra_context_type τenv τin) τout ->
    nraenv_core_type τc op τenv τin τout.

  Lemma typed_nraenv_core_const_sort_f {τc op τenv τin τout} :
    nraenv_core_type (rec_sort τc) op τenv τin τout ->
    nraenv_core_type τc op τenv τin τout.

  Lemma typed_nraenv_core_const_sort_b {τc op τenv τin τout} :
      nraenv_core_type τc op τenv τin τout ->
      nraenv_core_type (rec_sort τc) op τenv τin τout.

  Lemma typed_nraenv_core_const_sort τc op τenv τin τout :
    nraenv_core_type (rec_sort τc) op τenv τin τout <->
    nraenv_core_type τc op τenv τin τout.

End TcNRAEnv.


Notation "Op ▷ A >=> B ⊣ C ; E" := (nraenv_core_type C Op E A B) (at level 70).
Notation "Op @▷ d ⊣ C ; e" := (tnraenv_core_eval C Op e d) (at level 70).

  
Global Hint Constructors nraenv_core_type : qcert.
Global Hint Constructors unary_op_type : qcert.
Global Hint Constructors binary_op_type : qcert.

Ltac nraenv_core_inverter :=
  match goal with
    | [H:Coll _ = Coll _ |- _] => inversion H; clear H
    | [H: `?τ₁ = Coll₀ (`?τ₂) |- _] => rewrite (Coll_right_inv τ₁ τ₂) in H; subst
    | [H: Coll₀ (`?τ₂) = `?τ₁ |- _] => symmetry in H
    | [H:cNRAEnvID ▷ _ >=> _ ⊣ _ ; _ |- _ ] => inversion H; clear H
    | [H:cNRAEnvEnv ▷ _ >=> _ ⊣ _ ;_ |- _ ] => inversion H; clear H
    | [H:cNRAEnvMap _ _ ▷ _ >=> _ ⊣ _ ;_ |- _ ] => inversion H; clear H
    | [H:cNRAEnvMapProduct _ _ ▷ _ >=> _ ⊣ _ ;_ |- _ ] => inversion H; clear H
    | [H:cNRAEnvMapEnv _ ▷ _ >=> _ ⊣ _ ;_ |- _ ] => inversion H; clear H
    | [H:cNRAEnvDefault _ _ ▷ _ >=> _ ⊣ _ ;_ |- _ ] => inversion H; clear H
    | [H:cNRAEnvApp _ _ ▷ _ >=> _ ⊣ _ ;_ |- _ ] => inversion H; clear H
    | [H:cNRAEnvAppEnv _ _ ▷ _ >=> _ ⊣ _ ;_ |- _ ] => inversion H; clear H
    | [H:cNRAEnvEither _ _ ▷ _ >=> _ ⊣ _ ;_ |- _ ] => inversion H; clear H
    | [H:cNRAEnvEitherConcat _ _ ▷ _ >=> _ ⊣ _ ;_ |- _ ] => inversion H; clear H
    | [H:cNRAEnvProduct _ _ ▷ _ >=> _ ⊣ _ ;_ |- _ ] => inversion H; clear H
    | [H:cNRAEnvSelect _ _ ▷ _ >=> _ ⊣ _ ;_ |- _ ] => inversion H; clear H
    | [H:cNRAEnvUnop _ _ ▷ _ >=> _ ⊣ _ ;_ |- _ ] => inversion H; clear H
    | [H:cNRAEnvBinop _ _ _ ▷ _ >=> _ ⊣ _ ;_ |- _ ] => inversion H; clear H
    | [H:cNRAEnvConst _ ▷ _ >=> _ ⊣ _ ;_ |- _ ] => inversion H; clear H
    | [H: (_,_) = (_,_) |- _ ] => inversion H; clear H
    | [H: map (fun x2 : string * {τ₀ : rtype₀ | wf_rtype₀ τ₀ = true} =>
                 (fst x2, ` (snd x2))) ?x0 = [] |- _] => apply (map_rtype_nil x0) in H; simpl in H; subst
    | [H: (map
             (fun x : string * {τ₀ : rtype₀ | wf_rtype₀ τ₀ = true} =>
                (fst x, proj1_sig (snd x))) _)
          =
          (map
             (fun x' : string * {τ₀' : rtype₀ | wf_rtype₀ τ₀' = true} =>
                (fst x', proj1_sig (snd x'))) _) |- _ ] =>
      apply map_rtype_fequal in H; trivial
    | [H:Rec _ _ _ = Rec _ _ _ |- _ ] => generalize (Rec_inv H); clear H; intro H; try subst
    | [H: context [(_::nil) = map
                                (fun x : string * {τ₀ : rtype₀ | wf_rtype₀ τ₀ = true} =>
                                   (fst x, proj1_sig (snd x))) _] |- _] => symmetry in H
                                                                                         
    | [H: context [map
                     (fun x : string * {τ₀ : rtype₀ | wf_rtype₀ τ₀ = true} =>
                        (fst x, proj1_sig (snd x))) _ = (_::nil) ] |- _] => apply map_eq_cons in H;
        destruct H as [? [? [? [??]]]]
    | [H: Coll₀ _ = Coll₀ _ |- _ ] => inversion H; clear H
    | [H: Rec₀ _ _ = Rec₀ _ _ |- _ ] => inversion H; clear H
    | [H: _ ▷ _ >=> snd ?x ⊣ _ ;_ |- _] => destruct x; simpl in *; subst
    | [H:unary_op_type OpBag _ _ |- _ ] => inversion H; clear H; subst
    | [H:unary_op_type OpFlatten _ _ |- _ ] => inversion H; clear H; subst
    | [H:unary_op_type (OpRec _) _ _ |- _ ] => inversion H; clear H; subst
    | [H:unary_op_type (OpDot _) _ _ |- _ ] => inversion H; clear H; subst
    | [H:unary_op_type (OpRecProject _) _ _ |- _ ] => inversion H; clear H; subst
    | [H:unary_op_type (OpRecRemove _) _ _ |- _ ] => inversion H; clear H; subst
    | [H:unary_op_type OpLeft _ _ |- _ ] => inversion H; clear H; subst
    | [H:unary_op_type OpRight _ _ |- _ ] => inversion H; clear H; subst
    | [H:binary_op_type OpRecConcat _ _ _ |- _ ] => inversion H; clear H
    | [H:binary_op_type OpAnd _ _ _ |- _ ] => inversion H; clear H
    | [H:binary_op_type OpRecMerge _ _ _ |- _ ] => inversion H; clear H
  end; try rtype_equalizer; try assumption; try subst; simpl in *; try nraenv_core_inverter.

Ltac nraenv_core_inferer := try nraenv_core_inverter; subst; try qeauto.


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