(* ========================================================================== *)
(* FLYSPECK - BOOK FORMALIZATION                                              *)
(*                                                                            *)
(* Chapter: general                                                       *)
(* Author: Thomas C. Hales                                                    *)
(* Date: 2010-02-13                                                           *)
(* ========================================================================== *)


module State_manager:sig
  val neutralize_state:unit->unit
  end = struct 

(*
not neutralized:
set_jrh_lexer;;
installed printers...

binders, infixes, and prefixes add on July 18, 2010.
*)

(*
Bring conversions back to the following state of hol_version 2.20+ 100110:

basic_convs();;
val it : (string * (term * conv)) list =
  [("FUN_ONEPATTERN_CONV", (`_FUNCTION (\y z. P y z) x`, <fun>));
   ("MATCH_ONEPATTERN_CONV", (`_MATCH x (\y z. P y z)`, <fun>));
   ("FUN_SEQPATTERN_CONV", (`_FUNCTION (_SEQPATTERN r s) x`, <fun>));
   ("MATCH_SEQPATTERN_CONV", (`_MATCH x (_SEQPATTERN r s)`, <fun>));
   ("GEN_BETA_CONV", (`GABS (\a. b) c`, <fun>))]

We cannot restore the list above if someone changes it before this file is read.
The following checking can easily be defeated.  An honor system is in place.  *)


  let neutralize_basic_convs = 
    let bc = basic_convs() in
    let msg = "conversions beyond hol_version 2.20+ 100110.  Cannot neutralize state" in
    let original=["FUN_ONEPATTERN_CONV"; "MATCH_ONEPATTERN_CONV"; 
		  "FUN_SEQPATTERN_CONV";
		  "MATCH_SEQPATTERN_CONV"; "GEN_BETA_CONV"] in
    let _ = if not(List.length(bc)=5)   then failwith ("Added "^msg) in
    let _ =	if not(map fst bc=original)  then failwith ("Changed "^msg) in
      fun () ->    set_basic_convs(bc);;

(*
34 basic rewrites 

val rewrites : thm list =
  [|- FST (x,y) = x; |- SND (x,y) = y; |- FST x,SND x = x;
   |- (if x = x then y else z) = y; |- (if T then t1 else t2) = t1;
   |- (if F then t1 else t2) = t2; |- ~ ~t <=> t; |- (@y. y = x) = x;
   |- x = x <=> T; |- (T <=> t) <=> t; |- (t <=> T) <=> t;
   |- (F <=> t) <=> ~t; |- (t <=> F) <=> ~t; |- ~T <=> F; |- ~F <=> T;
   |- T /\ t <=> t; |- t /\ T <=> t; |- F /\ t <=> F; |- t /\ F <=> F;
   |- t /\ t <=> t; |- T \/ t <=> T; |- t \/ T <=> T; |- F \/ t <=> t;
   |- t \/ F <=> t; |- t \/ t <=> t; |- T ==> t <=> t; |- t ==> T <=> T;
   |- F ==> t <=> T; |- t ==> t <=> T; |- t ==> F <=> ~t; |- (!x. t) <=> t;
   |- (?x. t) <=> t; |- (\x. f x) y = f y; |- x = x ==> p <=> p]

Again, we do not really check that this list is the one above.
*)

  let neutralize_basic_rewrites= 
    let bw = basic_rewrites() in
    let msg = "Added rewrites beyond hol_version 2.20+ 100110.  Cannot neutralize" in
    let _ = if not(List.length(bw)=34) then failwith msg in
      fun () ->  set_basic_rewrites(bw);;

(*
16 Basic congruences

  [|- (!x. ~(x = a) ==> f x = g x)
      ==> (((\x. f x) --> l) (at a within s) <=> (g --> l) (at a within s));
   |- (!x. ~(x = a) ==> f x = g x)
      ==> (((\x. f x) --> l) (at a) <=> (g --> l) (at a));
   |- (!x. x IN s ==> f x = g x) ==> product s (\i. f i) = product s g;
   |- (!i. a <= i /\ i <= b ==> f i = g i)
      ==> product (a..b) (\i. f i) = product (a..b) g;
   |- (!x. p x ==> f x = g x)
      ==> product {y | p y} (\i. f i) = product {y | p y} g;
   |- (!x. x IN s ==> f x = g x) ==> vsum s (\i. f i) = vsum s g;
   |- (!i. a <= i /\ i <= b ==> f i = g i)
      ==> vsum (a..b) (\i. f i) = vsum (a..b) g;
   |- (!x. p x ==> f x = g x) ==> vsum {y | p y} (\i. f i) = vsum {y | p y} g;
   |- (!x. x IN s ==> f x = g x) ==> sum s (\i. f i) = sum s g;
   |- (!i. a <= i /\ i <= b ==> f i = g i)
      ==> sum (a..b) (\i. f i) = sum (a..b) g;
   |- (!x. p x ==> f x = g x) ==> sum {y | p y} (\i. f i) = sum {y | p y} g;
   |- (!x. x IN s ==> f x = g x) ==> nsum s (\i. f i) = nsum s g;
   |- (!i. a <= i /\ i <= b ==> f i = g i)
      ==> nsum (a..b) (\i. f i) = nsum (a..b) g;
   |- (!x. p x ==> f x = g x) ==> nsum {y | p y} (\i. f i) = nsum {y | p y} g;
   |- (g <=> g')
      ==> (g' ==> t = t')
      ==> (~g' ==> e = e')
      ==> (if g then t else e) = (if g' then t' else e');
   |- (p <=> p') ==> (p' ==> (q <=> q')) ==> (p ==> q <=> p' ==> q')]


*)

  let neutralize_basic_congs= 
    let bc = basic_congs() in
    let msg = "Added "^string_of_int(List.length bc)^
      " congruences.  Cannot neutralize. " in
    let _ = if not(List.length(bc)=16) then 
      (let _ = map print_thm bc in failwith msg) in
      fun () ->  set_basic_congs(bc);;

  let default_overload_skeletons =  (* unchanged since July 31 2009 *)
    [("real_interval", `:A`); ("segment", `:A`); ("interval", `:A`);
     ("**", `:A->B->C`); ("norm", `:A->real`); ("gcd", `:A#A->A`);
     ("coprime", `:A#A->bool`); ("mod", `:A->A->A->bool`);
     ("divides", `:A->A->bool`); ("&", `:num->A`); ("min", `:A->A->A`);
     ("max", `:A->A->A`); ("abs", `:A->A`); ("inv", `:A->A`);
     ("pow", `:A->num->A`); ("--", `:A->A`); (">=", `:A->A->bool`);
     (">", `:A->A->bool`); ("<=", `:A->A->bool`); ("<", `:A->A->bool`);
     ("/", `:A->A->A`); ("*", `:A->A->A`); ("-", `:A->A->A`);
     ("+", `:A->A->A`)];;
  
  let neutralize_overload_skeletons()=
    the_overload_skeletons:= default_overload_skeletons;;
  
  
  let the_default_interface = (* set on Feb 12 2010 *)
    [("+", ("real_add", `:real->real->real`));
     ("-", ("real_sub", `:real->real->real`));
     ("*", ("real_mul", `:real->real->real`));
     ("/", ("real_div", `:real->real->real`));
     ("<", ("real_lt", `:real->real->bool`));
     ("<=", ("real_le", `:real->real->bool`));
     (">", ("real_gt", `:real->real->bool`));
     (">=", ("real_ge", `:real->real->bool`));
     ("--", ("real_neg", `:real->real`));
     ("pow", ("real_pow", `:real->num->real`));
     ("inv", ("real_inv", `:real->real`));
     ("abs", ("real_abs", `:real->real`));
     ("max", ("real_max", `:real->real->real`));
     ("min", ("real_min", `:real->real->real`));
     ("&", ("real_of_num", `:num->real`));
     ("mod", ("real_mod", `:real->real->real->bool`));
     ("+", ("vector_add", `:real^N->real^N->real^N`));
     ("-", ("vector_sub", `:real^N->real^N->real^N`));
     ("--", ("vector_neg", `:real^N->real^N`));
     ("norm", ("vector_norm", `:real^N->real`));
     ("**", ("vector_matrix_mul", `:real^M->real^N^M->real^N`));
     ("+", ("+", `:num->num->num`)); ("-", ("-", `:num->num->num`));
     ("*", ("*", `:num->num->num`)); ("<", ("<", `:num->num->bool`));
     ("<=", ("<=", `:num->num->bool`)); (">", (">", `:num->num->bool`));
     (">=", (">=", `:num->num->bool`));
     ("divides", ("num_divides", `:num->num->bool`));
     ("mod", ("num_mod", `:num->num->num->bool`));
     ("coprime", ("num_coprime", `:num#num->bool`));
     ("gcd", ("num_gcd", `:num#num->num`));
     ("+", ("int_add", `:int->int->int`));
     ("-", ("int_sub", `:int->int->int`));
     ("*", ("int_mul", `:int->int->int`));
     ("<", ("int_lt", `:int->int->bool`));
     ("<=", ("int_le", `:int->int->bool`));
     (">", ("int_gt", `:int->int->bool`));
     (">=", ("int_ge", `:int->int->bool`)); ("--", ("int_neg", `:int->int`));
     ("pow", ("int_pow", `:int->num->int`)); ("abs", ("int_abs", `:int->int`));
     ("max", ("int_max", `:int->int->int`));
     ("min", ("int_min", `:int->int->int`));
     ("&", ("int_of_num", `:num->int`));
     ("divides", ("int_divides", `:int->int->bool`));
     ("mod", ("int_mod", `:int->int->int->bool`));
     ("coprime", ("int_coprime", `:int#int->bool`));
     ("gcd", ("int_gcd", `:int#int->int`));
     ("inv", ("complex_inv", `:real^2->real^2`));
     ("pow", ("complex_pow", `:real^2->num->real^2`));
     ("/", ("complex_div", `:real^2->real^2->real^2`));
     ("*", ("complex_mul", `:real^2->real^2->real^2`));
     ("-", ("vector_sub", `:real^2->real^2->real^2`));
     ("+", ("vector_add", `:real^2->real^2->real^2`));
     ("--", ("vector_neg", `:real^2->real^2`));
     ("vol", ("measure", `:(real^3->bool)->real`));
     ("NULLSET", ("negligible", `:(real^3->bool)->bool`));
     ("real_interval",
      ("closed_real_interval", `:(real#real)list->real->bool`));
     ("real_interval", ("open_real_interval", `:real#real->real->bool`));
     ("segment", ("closed_segment", `:(real^A#real^A)list->real^A->bool`));
     ("segment", ("open_segment", `:real^A#real^A->real^A->bool`));
     ("interval", ("closed_interval", `:(real^A#real^A)list->real^A->bool`));
     ("interval", ("open_interval", `:real^A#real^A->real^A->bool`));
     ("**", ("matrix_vector_mul", `:real^N^M->real^N->real^M`));
     ("**", ("matrix_mul", `:real^N^M->real^P^N->real^P^M`));
     ("-", ("matrix_sub", `:real^N^M->real^N^M->real^N^M`));
     ("+", ("matrix_add", `:real^N^M->real^N^M->real^N^M`));
     ("--", ("matrix_neg", `:real^N^M->real^N^M`));
     ("dist", ("distance", `:real^N#real^N->real`));
     ("&", ("hreal_of_num", `:num->hreal`));
     ("<=>", ("=", `:bool->bool->bool`))];;
  
  let neutralize_interface()=
    the_interface:= the_default_interface;;

let set_parsel f g h xl = 
   (let _ = map f (h()) in let _ =  map g xl in ());;

let neutralize_binders() = 
  let bind = ["\\"; "!"; "?"; "?!"; "@"; "minimal"; "lambda"] in
  set_parsel unparse_as_binder parse_as_binder binders bind;;

let neutralize_prefixes() = 
  let pre = ["~"; "--"; "mod"] in
  set_parsel unparse_as_prefix parse_as_prefix prefixes pre;;

let neutralize_infixes() =
  let inf =   [("<=>", (2, "right")); ("==>", (4, "right")); ("\\/", (6, "right"));
   ("/\\", (8, "right")); ("==", (10, "right")); ("===", (10, "right"));
   ("treal_eq", (10, "right")); ("IN", (11, "right"));
   ("--->", (12, "right")); ("-->", (12, "right")); ("<", (12, "right"));
   ("<<", (12, "right"));
   ("<<<", (12, "right")); ("<<=", (12, "right")); ("<=", (12, "right"));
  ("<=_c", (12, "right"));
    ("<_c", (12, "right")); 
   ("=", (12, "right")); ("=_c", (12, "right")); (">", (12, "right"));
  (">=", (12, "right"));
  (">=_c", (12, "right"));
    (">_c", (12, "right"));
   ("HAS_SIZE", (12, "right")); ("PSUBSET", (12, "right"));
   ("SUBSET", (12, "right")); ("absolutely_integrable_on", (12, "right"));
   ("absolutely_real_integrable_on", (12, "right"));
   ("analytic_on", (12, "right")); ("complex_differentiable", (12, "right"));
   ("continuous", (12, "right")); ("continuous_on", (12, "right"));
   ("convex_on", (12, "right")); ("differentiable", (12, "right"));
   ("differentiable_on", (12, "right")); ("divides", (12, "right"));
   ("division_of", (12, "right")); ("edge_of", (12, "right"));
   ("exposed_face_of", (12, "right")); ("extreme_point_of", (12, "right"));
   ("face_of", (12, "right")); ("facet_of", (12, "right"));
   ("fine", (12, "right")); ("has_complex_derivative", (12, "right"));
   ("has_derivative", (12, "right")); ("has_integral", (12, "right"));
   ("has_integral_compact_interval", (12, "right"));
   ("has_measure", (12, "right")); ("has_real_derivative", (12, "right"));
   ("has_real_integral", (12, "right")); ("has_real_measure", (12, "right"));
   ("has_vector_derivative", (12, "right"));
   ("holomorphic_on", (12, "right")); ("homeomorphic", (12, "right"));
   ("inseg", (12, "right")); ("integrable_on", (12, "right"));
   ("limit_point_of", (12, "right")); ("permutes", (12, "right"));
   ("real_continuous", (12, "right")); ("real_continuous_on", (12, "right"));
   ("real_convex_on", (12, "right")); ("real_differentiable", (12, "right"));
   ("real_differentiable_on", (12, "right"));
   ("real_integrable_on", (12, "right")); ("real_sums", (12, "right"));
   ("real_uniformly_continuous_on", (12, "right"));
   ("retract_of", (12, "right")); ("simplex", (12, "right"));
   ("sums", (12, "right")); ("tagged_division_of", (12, "right"));
   ("tagged_partial_division_of", (12, "right"));
   ("treal_le", (12, "right")); ("uniformly_continuous_on", (12, "right"));
   (",", (14, "right")); ("in_direction", (14, "right"));
   ("within", (14, "right")); ("..", (15, "right")); ("+", (16, "right"));
   ("++", (16, "right")); 
   ("+_c", (16, "right"));  ("UNION", (16, "right"));
   ("treal_add", (16, "right")); ("-", (18, "left")); 
    ("DIFF", (18, "left")); ("*", (20, "right"));
   ("**", (20, "right")); 
   ("*_c", (20, "right")); ("INTER", (20, "right"));
   ("cross", (20, "right")); ("dot", (20, "right"));
   ("treal_mul", (20, "right")); ("%", (21, "right"));
   ("INSERT", (21, "right")); ("DELETE", (21, "left"));
   ("hull", (21, "left")); ("CROSS", (22, "right"));
    ("/", (22, "left")); ("DIV", (22, "left"));
   ("MOD", (22, "left")); ("div", (22, "left")); ("rem", (22, "left"));
   ("POWER",(24,"right"));
   ("EXP", (24, "left")); ("cpow", (24, "left")); ("pow", (24, "left"));
   ("$", (25, "left")); ("o", (26, "right"))]
    in
  set_parsel (fun (a,_) -> unparse_as_infix a) parse_as_infix infixes inf ;;


  
  (* What we cannot neutralize we destroy *)
  
  let neutralize_axioms() =
    if not(List.length(axioms()) =3) then failwith ("Further axioms are not allowed");;
  
  
  let neutralize_state()=
    (
      current_goalstack := ([]:goalstack);
      neutralize_overload_skeletons();
      neutralize_interface();
      neutralize_basic_congs();
      neutralize_basic_convs();
      neutralize_basic_rewrites();
      neutralize_binders();
      neutralize_prefixes();
      neutralize_infixes();
      neutralize_axioms();
    );;
  
end;;