Set Implicit Arguments.
Require Export AbstractSign Analysers.
Require Export LibList.
Require Export Shared.

Notation " [ ] " := nil : list_scope.
Notation " [ x ] " := (cons x nil) : list_scope.
Notation " [ x ; .. ; y ] " := (cons x .. (cons y nil) ..) : list_scope.

Section General.

Let analyser_result := analyser_result sign_asem.
Coercion sign_analyser_found := analyser_found sign_asem : sign_ares → analyser_result.
Let analyser_correct := analyser_correct (asem := sign_asem) _ _.
Let correct_analyser_result := correct_analyser_result (asem := sign_asem) _ _.

Definition analyser_match (ar : analyser_result) A (found : sign_ares → A)
    (failed : list (terms × sign_ast) → list (terms × sign_ast × sign_ares) → A) : A :=
  match ar with
  | analyser_found r ⇒ found r
  | analyser_failed lf lo ⇒ failed lf lo
  end.

Global Instance abort_ares_decidable : ∀ r,
    Decidable (abort_ares r).
  introv. applys decidable_make
    (decide (sign_ares_expr (⊥♯, ⊤♯) ⊑♯ r ∨ sign_ares_stat (⊥♯, ⊤♯) ⊑♯ r)).
  rewrite decide_spec. apply eq_isTrue. iff A.
   inverts A as A; constructor (exact A).
   inverts× A.
Defined.

Global Instance abort_ast_decidable : ∀ sigma,
    Decidable (abort_ast sigma).
  destruct sigma as [aEv|aEv aEf|aEv aEf|aEv ar|av ar|aEv ar|aC aEv ar
                     |aEv aEf ar|aC aEf ar|aEv aEf ar|aEv aEf ar| |];
  try solve [ applys decidable_make false; fold_bool; rew_refl; intro A; inverts A ];
  applys decidable_make (decide (abort_ares ar));
  rewrite decide_spec; apply eq_isTrue; iff A; try solve [ constructors¬ ]; inverts× A.
Defined.

Global Instance sign_acond_Decidable : ∀ n sigma,
    Decidable (sign_acond n sigma).
  destruct n; destruct sigma as [aEv|aEv aEf|aEv aEf|aEv ar|av ar|aEv ar|aC aEv ar
                                |aEv aEf ar|aC aEf ar|aEv aEf ar|aEv aEf ar| |];
    try typeclass;
    destruct aEv as [aE aC]; try typeclass;
    destruct aC as [[[[? ?]|]|]|];
    repeat first [ typeclass | apply not_decidable | apply and_decidable ]; simpl;
    try solve [ applys decidable_make false; fold_bool; rew_refl; introv (?&?); auto¬ ];
    try solve [ applys decidable_make true; fold_bool; rew_refl; ∃¬ Sign.zero ];
    try solve [
      set_eq b: (decide (v = v0)); applys decidable_make b; destruct b;
        fold_bool; rew_refl in *; substs;
       [ eexists; splits~; apply Sign.order_refl; auto×
       | introv (?&?&?); false× ] ];
    try solve [
      match goal with
      | |- Decidable (?A → ?B) ⇒
        applys decidable_make (decide B); rew_refl; simpl; fold_bool; rew_refl~;
        let A := fresh in introv A; forwards~: A Sign.zero
      end ].
   set_eq b: (decide (v ≠ v0)); applys decidable_make b; destruct b;
     fold_bool; rew_refl in *; substs.
    introv A. intuit. false¬.
    introv A. apply (A a). splits.
     apply Sign.order_refl. auto×.
     rew_logic¬ in EQb.
Defined.

Definition sign_applicable_names (t : terms) (sigma : sign_ast) :=
  'let f := fun n ⇒ decide (sign_acond n sigma) in
  option_map (filter f)
    match t with
    | expr_cst c ⇒ Some ([ name_cst c ])
    | expr_var x ⇒ Some ([ name_var x; name_varCxt x; name_varUndef x ])
    | expr_add e1 e2 ⇒ Some ([ name_add e1 e2 ])
    | expr_add_1 e2 ⇒ Some ([ name_add_1 e2; name_abort_ext_expr (expr_add_1 e2) ])
    | expr_add_2 ⇒ Some ([ name_add_2; name_abort_ext_expr expr_add_2 ])
    | stat_skip ⇒ Some ([ name_skip ])
    | stat_throw ⇒ Some ([ name_throw ])
    | stat_asgn x e ⇒ Some ([ name_asgn x e ])
    | stat_asgn_1 x ⇒ Some ([ name_asgn_1 x; name_abort_ext_stat (stat_asgn_1 x);
                               name_asgn_1_immutable x ])
    | stat_seq s1 s2 ⇒ Some ([ name_seq s1 s2 ])
    | stat_seq_1 s2 ⇒ Some ([ name_seq_1 s2; name_abort_ext_stat (stat_seq_1 s2) ])
    | stat_if e s1 s2 ⇒ Some ([ name_if e s1 s2 ])
    | stat_if_1 s1 s2 ⇒ Some ([ name_if_1_true s1 s2; name_if_1_false s1 s2;
                                 name_abort_ext_stat (stat_if_1 s1 s2) ])
    | stat_while e s ⇒ Some ([ name_while e s ])
    | stat_while_1 e s ⇒ Some ([ name_while_1 e s; name_abort_ext_stat (stat_while_1 e s) ])
    | stat_while_2 e s ⇒ Some ([ name_while_2_true e s; name_while_2_false e s;
                                  name_abort_ext_stat (stat_while_2 e s) ])
    | stat_proc_call f e ⇒ Some ([ name_proc_call f e ])
    | stat_proc_call_1 f ⇒
      let abort := name_abort_ext_stat (stat_proc_call_1 f) in
      match sigma with
      | sign_ast_proc_call_1 aEv aEf ar ⇒
        match readF_env aEf f with
        | FlatLatticeDec.TB_Top ⇒ None

        | FlatLatticeDec.TB_Bot ⇒
          Some ([ abort ])

        | FlatLatticeDec.TB_Elem proc ⇒
          match proc with
          | Some (x, s) ⇒ Some ([ name_proc_call_1 f x s; abort ])
          | None ⇒ Some ([ name_proc_call_1_undef f; abort ])
          end
        end
      | _ ⇒ None
      end
    | prog_proc_decl f x s p ⇒ Some ([ name_proc_decl f x s p ])
    | prog_stat s ⇒ Some ([ name_prog_stat s ])
    end.

Lemma sign_applicable_names_correct : ∀ l t sigma n,
  sign_applicable_names t sigma = Some l →
  (while_left n = t ∧ sign_acond n sigma) ↔ List.In n l.
Proof.
  introv E. unfolds in E. let_name. forwards (l0&E1&E2): option_map_out (rm E). iff I.
   lets (T&C): (rm I). subst l. apply filter_in. splits.
    destruct t as [()|()|()|()|()]; destruct n; simpls~; tryfalse; inverts T;
      repeat inverts E1 as E1; try solve [ repeat (solve [ left¬ ] || right) ];
      try solve [
        destruct sigma as [| | | | | | | | | |aEv aEf ar| |]; tryfalse;
        destruct (readF_env aEf p) as [| |[[x' s']|]] eqn:Er; inverts E1;
        try (lets (E&Aar): (rm C); inverts E);
        try solve [ repeat (solve [ left¬ ] || right) ] ].
    substs. rewrite decide_spec. rew_refl¬.
   subst l. apply filter_in in I. lets (I0&C): (rm I). substs. splits.
     clear C. destruct t as [()|()|()|()|()]; destruct n; simpls~; tryfalse;
       inverts E1 as E1; repeat inverts I0 as I0; tryfalse; auto~;
       try solve [
         destruct sigma as [| | | | | | | | | |aEv aEf ar| |]; tryfalse;
         destruct (readF_env aEf p) as [| |[[x' s']|]] eqn:Er;
         inverts E1 as E1; repeat inverts I0 as I0; tryfalse; auto¬ ].
    rewrite decide_spec in C. rew_refl¬ in C.
Qed.

Definition sign_failing_analyser : terms → sign_ast → analyser_result :=
  failing_analyser sign_asem.

Lemma sign_failing_analyser_correct : analyser_correct sign_failing_analyser.
Proof. apply failing_analyser_correct. Qed.

Definition sign_trivial_analyser : terms → sign_ast → analyser_result := trivial_analyser sign_asem _ _.

Lemma sign_trivial_analyser_correct : analyser_correct sign_trivial_analyser.
Proof. applys trivial_analyser_correct sign_arule_format_correct sign_asemantics_full. Qed.

Definition sign_analyse_step : (terms → sign_ast → analyser_result) → terms → sign_ast → analyser_result :=
  analyse_step (asem := sign_asem) _ _ sign_applicable_names.

Lemma sign_analyse_step_correct : ∀ analyser,
  analyser_correct analyser →
  analyser_correct (sign_analyse_step analyser).
Proof.
  applys analyse_step_correct sign_arule_format_correct sign_asemantics_full sign_applicable_names_correct.
Qed.

Definition sign_analyse_fuel : (terms → sign_ast → analyser_result) → nat
                             → terms → sign_ast → analyser_result :=
  analyse_fuel (asem := sign_asem) _ _ sign_applicable_names.

Lemma sign_analyse_fuel_correct : ∀ analyser fuel,
  analyser_correct analyser →
  analyser_correct (sign_analyse_fuel analyser fuel).
Proof.
  introv C.
  applys analyse_fuel_correct sign_arule_format_correct sign_asemantics_full sign_applicable_names_correct C.
Qed.

Inductive is_looping_branch : terms → terms → Prop :=
  | is_looping_branch_while : ∀ e s,
    is_looping_branch (stat_while_1 e s) (stat_while_2 e s)
  | is_looping_branch_call : ∀ f e,
    is_looping_branch (stat_proc_call_1 f) (stat_proc_call f e)
  .

Global Instance is_looping_branch_Decidable : ∀ p1 p2,
  Decidable (is_looping_branch p1 p2).
Proof.
  introv. destruct p1 as [()|()|()|()|()]; destruct p2 as [()|()|()|()|()];
    try solve [ applys decidable_make false; fold_bool; rew_refl; intro A; inverts A ].
   applys decidable_make (decide (e = e0 ∧ s = s0)). rewrite decide_def.
    cases_if as I; fold_bool; rew_refl.
     destruct I. substs. constructors.
     intro A. inverts× A.
   applys decidable_make (decide (p = p0)). rewrite decide_def.
    cases_if as I; fold_bool; rew_refl.
     destruct I. substs. constructors.
     intro A. inverts× A.
Qed.

Definition sign_prev_term_not_looping :=
  prev_term_not_looping while_str is_looping_branch.

Lemma sign_prev_term_not_looping_wf : well_founded sign_prev_term_not_looping.
Proof.
  asserts Ae: (∀ e : expr, Acc sign_prev_term_not_looping e).
   induction e; repeat (constructors; intros y (P&?); inverts P as E1 E2;
                        destruct n; tryfalse; inverts E1; inverts¬ E2).
  asserts As: (∀ s : stat, Acc sign_prev_term_not_looping s).
   induction s; do 3 (constructors; let L := fresh "L" in intros y (P&L);
      inverts P as E1 E2; destruct n; tryfalse; inverts E1; inverts¬ E2;
      try (solve [ false L; constructors ] || solve [ false L1; constructors ])).
  intro p. destruct¬ p as [?|()|?|()|()]; try solve [ do 3 (constructors;
    let L := fresh "L" in intros y (P&L); inverts P as E1 E2; destruct n; tryfalse;
    inverts E1; inverts¬ E2;
    try (solve [ false L0; constructors ] || solve [ false L1; constructors ])) ].
   gen p v s. induction p0; introv.
    constructors. introv (P&L). inverts P as E1 E2; destruct n; tryfalse.
     inverts E1. inverts¬ E2.
    do 2 (constructors; let L := fresh "L" in intros y (P&L);
     inverts P as E1 E2; destruct n; tryfalse; inverts E1; inverts¬ E2).
Qed.

Definition sign_analyse_step_prev_term_loops :=
  analyse_step_prev_term_loops (asem := sign_asem) _ _ _ sign_applicable_names_correct.

Lemma sign_analyse_step_prev_term_loops_correct : ∀ p following sigma ra,
  (∀ p' (P : prev_term while_str p' p) sigma' ra',
    following _ P sigma' = ra' →
    correct_analyser_result p' sigma' ra') →
  sign_analyse_step_prev_term_loops following sigma = ra →
  correct_analyser_result p sigma ra.
Proof.
  applys analyse_step_prev_term_loops_correct sign_arule_format_correct sign_asemantics_full.
  apply sign_asem.
Qed.

Definition sign_analyse_deep_fuel : (terms → sign_ast → analyser_result)
    → nat → terms → sign_ast → analyser_result :=
  analyse_deep_fuel (asem := sign_asem) _ _ _ sign_applicable_names_correct
    is_looping_branch_Decidable sign_prev_term_not_looping_wf.

Lemma sign_analyse_deep_fuel_correct : ∀ fuel fallback_analyser,
  analyser_correct fallback_analyser →
  analyser_correct (sign_analyse_deep_fuel fallback_analyser fuel).
Proof.
  introv C.
  applys analyse_deep_fuel_correct sign_arule_format_correct sign_asemantics_full C.
   apply sign_asem.
Qed.

Definition sign_guess_step : heap terms (list (sign_ast × sign_ares))
                             → (terms → sign_ast → analyser_result)
                             → (terms → sign_ast → analyser_result) :=
  fun oracle ⇒
    guess_step (asem := sign_asem) _ _ sign_applicable_names
      (read_oracle_meet sign_asem _ _ _ _ oracle).

Definition sign_deep_guess_step : nat
                             → heap terms (list (sign_ast × sign_ares))
                             → (terms → sign_ast → analyser_result)
                             → (terms → sign_ast → analyser_result) :=
  fun deep oracle ⇒
    deep_guess_step (asem := sign_asem) _ _ _ sign_applicable_names_correct
      (read_oracle_meet sign_asem _ _ _ _ oracle)
      is_looping_branch_Decidable sign_prev_term_not_looping_wf deep.

Definition sign_guess_fuel : heap terms (list (sign_ast × sign_ares))
                             → nat → terms → sign_ast → analyser_result :=
  fun oracle ⇒
    guess_fuel (asem := sign_asem) oracle (sign_guess_step oracle).

Definition sign_analyser_oracle_fuel : nat → heap terms (list (sign_ast × sign_ares))
                                       → terms → sign_ast → analyser_result :=
  analyser_oracle_fuel (asem := sign_asem) _ sign_guess_step.

Lemma sign_analyser_oracle_fuel_correct : ∀ oracle fuel,
  analyser_correct (sign_analyser_oracle_fuel fuel oracle).
Proof.
  introv. apply analyser_oracle_fuel_correct with (normalise := meet_closure _ _ _).
   introv I D. applys¬ meet_closure_impl I D.
   applys Park_normalise_Park_meet_closure sign_asemantics_full sign_acond_monotone.
    apply sign_arules_incr.
   introv. applys guess_step_correct_modulo sign_arule_format_correct sign_asemantics_full.
    apply sign_applicable_names_correct.
    apply read_oracle_meet_correct_modulo.
   introv. applys guess_step_correct sign_arule_format_correct sign_asemantics_full.
    apply sign_applicable_names_correct.
    applys read_oracle_meet_correct sign_asemantics_full.
     apply sign_acond_monotone.
     apply sign_arules_incr.
Qed.

Definition sign_analyser_oracle_deep_fuel : nat → nat
                                       → heap terms (list (sign_ast × sign_ares))
                                       → terms → sign_ast → analyser_result :=
  fun deep ⇒
    analyser_oracle_fuel (asem := sign_asem) _ (sign_deep_guess_step deep).

Lemma sign_deep_analyser_oracle_fuel_correct : ∀ deep oracle fuel,
  analyser_correct (sign_analyser_oracle_deep_fuel deep fuel oracle).
Proof.
  introv. apply analyser_oracle_fuel_correct with (normalise := meet_closure _ _ _).
   introv I D. applys¬ meet_closure_impl I D.
   applys Park_normalise_Park_meet_closure sign_asemantics_full sign_acond_monotone.
    apply sign_arules_incr.
   introv. applys deep_guess_step_correct_modulo.
    apply sign_asem.
    apply sign_arule_format_correct.
    apply sign_asemantics_full.
    apply read_oracle_meet_correct_modulo.
   introv. applys deep_guess_step_correct.
    apply sign_asem.
    apply sign_arule_format_correct.
    apply sign_asemantics_full.
    applys read_oracle_meet_correct sign_asemantics_full.
     apply sign_acond_monotone.
     apply sign_arules_incr.
Qed.

Definition sign_analyser_back_and_forth :
    (heap terms (list (sign_ast × sign_ares)) → terms → sign_ast → analyser_result) →
    (heap terms (list (sign_ast × sign_ares)) → terms → sign_ast →
      heap terms (list (sign_ast × sign_ares))) →
    nat → heap terms (list (sign_ast × sign_ares)) → terms → sign_ast → analyser_result :=
  @analyser_back_and_forth _ sign_asem.

Lemma sign_analyser_back_and_forth_correct : ∀ analyser hint fuel oracle,
  (∀ oracle, analyser_correct (analyser oracle)) →
  analyser_correct (sign_analyser_back_and_forth analyser hint fuel oracle).
Proof. introv C. apply¬ analyser_back_and_forth_correct. Qed.

Definition sign_oracle_unfold : nat → heap terms (list (sign_ast × sign_ares)) → terms → sign_ast →
      heap terms (list (sign_ast × sign_ares)) :=
  oracle_unfold sign_asem _ _ _ _ sign_applicable_names_correct is_looping_branch_Decidable
    sign_prev_term_not_looping_wf.

Definition sign_oracle_loop_unfold : nat → heap terms (list (sign_ast × sign_ares)) → terms → sign_ast →
      heap terms (list (sign_ast × sign_ares)) :=
  oracle_loop_unfold sign_asem _ _ _ _ sign_applicable_names_correct is_looping_branch_Decidable
    sign_prev_term_not_looping_wf.

Section Typed.

Definition sign_type_analyse (p : terms) (sigma : sign_ast) : analyser_result :=
  match p return sign_ares with
  | terms_expr _ | terms_ext_expr _ ⇒ sign_ares_expr (⊤♯)
  | terms_stat _ | terms_ext_stat _ | terms_prog _ ⇒ sign_ares_stat (⊤♯)
  end.

Lemma sign_type_analyse_correct : analyser_correct sign_type_analyse.
Proof.
  introv E. substs. constructors.
    gen t sigma. cofix D. constructors. introv Eq C. substs.
    destruct n; simpls; (constructors; [apply TopDec.prop| |
      first [
         solve [ eapply aapply_step_Ax; reflexivity ]
       | solve [ eapply aapply_step_R1; try reflexivity; apply D; reflexivity ]
       | eapply aapply_step_R2; try reflexivity; [ apply D; reflexivity | apply D; reflexivity ] ] ]);
    let t :=
        first [
           solve [ constructors ]
         | solve [ simpl; rew_refl× ] ] in t || (split; t) || idtac.
Qed.

End Typed.

Definition sign_analyse_fuel_fail :=
  sign_analyse_fuel (failing_analyser sign_asem).

Lemma sign_analyse_fuel_fail_correct : ∀ fuel,
  analyser_correct (sign_analyse_fuel_fail fuel).
Proof. introv. apply sign_analyse_fuel_correct. apply failing_analyser_correct. Qed.

Definition sign_analyse_fuel_type :=
  sign_analyse_fuel sign_type_analyse.

Lemma sign_analyse_fuel_type_correct : ∀ fuel,
  analyser_correct (sign_analyse_fuel_type fuel).
Proof. introv. apply sign_analyse_fuel_correct. apply sign_type_analyse_correct. Qed.

Definition sign_analyse_deep_fuel_fail :=
  sign_analyse_deep_fuel (failing_analyser sign_asem).

Lemma sign_analyse_deep_fuel_fail_correct : ∀ fuel,
  analyser_correct (sign_analyse_deep_fuel_fail fuel).
Proof. introv. apply sign_analyse_deep_fuel_correct. apply failing_analyser_correct. Qed.

Definition sign_analyse_deep_fuel_type :=
  sign_analyse_deep_fuel sign_type_analyse.

Lemma sign_analyse_deep_fuel_type_correct : ∀ fuel,
  analyser_correct (sign_analyse_deep_fuel_type fuel).
Proof. introv. apply sign_analyse_deep_fuel_correct. apply sign_type_analyse_correct. Qed.

Definition sign_analyse_oracle_back_and_forth oracle_fuel unfold_fuel fuel :=
  sign_analyser_back_and_forth (sign_analyser_oracle_fuel oracle_fuel)
                               (sign_oracle_unfold unfold_fuel) fuel HeapList.empty.

Lemma sign_analyse_oracle_back_and_forth_correct : ∀ oracle_fuel unfold_fuel fuel,
  analyser_correct (sign_analyse_oracle_back_and_forth oracle_fuel unfold_fuel fuel).
Proof. introv. apply sign_analyser_back_and_forth_correct. introv. apply sign_analyser_oracle_fuel_correct. Qed.

Definition sign_analyse_oracle_back_and_forth_loop oracle_fuel unfold_fuel fuel :=
  sign_analyser_back_and_forth (sign_analyser_oracle_fuel oracle_fuel)
                               (sign_oracle_loop_unfold unfold_fuel) fuel HeapList.empty.

Lemma sign_analyse_oracle_back_and_forth_loop_correct : ∀ oracle_fuel unfold_fuel fuel,
  analyser_correct (sign_analyse_oracle_back_and_forth_loop oracle_fuel unfold_fuel fuel).
Proof. introv. apply sign_analyser_back_and_forth_correct. introv. apply sign_analyser_oracle_fuel_correct. Qed.

Definition sign_analyse_oracle_back_and_forth_deep deep_fuel oracle_fuel unfold_fuel fuel :=
  sign_analyser_back_and_forth (sign_analyser_oracle_deep_fuel deep_fuel oracle_fuel)
                               (sign_oracle_unfold unfold_fuel) fuel HeapList.empty.

Lemma sign_analyse_oracle_back_and_forth_deep_correct : ∀ deep_fuel oracle_fuel unfold_fuel fuel,
  analyser_correct (sign_analyse_oracle_back_and_forth_deep deep_fuel oracle_fuel unfold_fuel fuel).
Proof. introv. apply sign_analyser_back_and_forth_correct. introv. apply sign_deep_analyser_oracle_fuel_correct. Qed.

Definition sign_analyse_oracle_back_and_forth_deep_loop deep_fuel oracle_fuel unfold_fuel fuel :=
  sign_analyser_back_and_forth (sign_analyser_oracle_deep_fuel deep_fuel oracle_fuel)
                               (sign_oracle_loop_unfold unfold_fuel) fuel HeapList.empty.

Lemma sign_analyse_oracle_back_and_forth_deep_loop_correct : ∀ deep_fuel oracle_fuel unfold_fuel fuel,
  analyser_correct (sign_analyse_oracle_back_and_forth_deep_loop deep_fuel oracle_fuel unfold_fuel fuel).
Proof. introv. apply sign_analyser_back_and_forth_correct. introv. apply sign_deep_analyser_oracle_fuel_correct. Qed.

End General.

Extraction Language Ocaml.

Require Import ExtrOcamlBasic.
Require Import ExtrOcamlNatInt.
Require Import ExtrOcamlZInt.
Require Import ExtrOcamlString.

Definition eq_aValVar (v1 v2 : aValVar) := decide (v1 =♯ v2).

Extraction Inline arbitrary.

Extraction "Abstract.ml"
  prog_test0 prog_test1 prog_test2 prog_test3
  prog_test4 prog_test5 prog_test6 prog_test7
  prog_test8 prog_test9 prog_test10 prog_test11
  prog_test12 prog_test13 prog_test14 prog_test15
  prog_test16 prog_test17 prog_test18 prog_test19
  prog_test20 prog_test21 prog_test22
  initialV initialF eq_aValVar analyser_match
  sign_trivial_analyser sign_failing_analyser sign_type_analyse
  sign_analyse_fuel_fail sign_analyse_fuel_type
  sign_analyse_deep_fuel_fail sign_analyse_deep_fuel_type
  sign_analyse_oracle_back_and_forth sign_analyse_oracle_back_and_forth_deep
  sign_analyse_oracle_back_and_forth_loop sign_analyse_oracle_back_and_forth_deep_loop.