(* tests for sml/calcelems.sml

   author: Walther Neuper 060113

*)

"--------------------------------------------------------";

"--------------------------------------------------------";

"table of contents --------------------------------------";

"--------------------------------------------------------";

"-------- Unsynchronized.ref doesn't work any more ------";

"-------- fun thmID_of_derivation_name ------------------";

"-------- fun term2str ----------------------------------";

"-------- fun thmID_of_derivation_name 000---------------";

"--------------------------------------------------------";

"--------------------------------------------------------";

"--------------------------------------------------------";

"-------- Unsynchronized.ref doesn't work any more ------";

"-------- Unsynchronized.ref doesn't work any more ------";

"-------- Unsynchronized.ref doesn't work any more ------";

(* this code resembles what would be needed to intermediately save original data ... *)

val ref_ = Unsynchronized.ref "original-data";

(* save intermediately *) val val_ = ! ref_;

ref_ := "test-data";

(* restore original    *) ref_ := val_;

if ! ref_ = "original-data"

then writeln "~~~~~ that's what we want"

else writeln "===== why not original ?";

(* ... which works in this simple case. But the same did not work with 

  --- fun insert_errpats ---, see changeset 90f3855dee3b *)

"-------- fun thmID_of_derivation_name ----------------";

"-------- fun thmID_of_derivation_name ----------------";

"-------- fun thmID_of_derivation_name ----------------";

val thm = @{thm radd_0};

val dn = Thm.derivation_name thm;

if dn = "Test.radd_0" then () 

else error "calcelems.sml Thm.derivation_name changed 1";

val thmID = thmID_of_derivation_name dn;

val thyID = thyID_of_derivation_name dn;

if thmID = "radd_0" andalso thyID = "Test" then ()

else error "calcelems.sml Thm.derivation_name changed 2";

"--- thm2 --";

val thm = @{thm add_divide_distrib}

val dn = Thm.derivation_name thm;

val thmID = thmID_of_derivation_name dn;

val thyID = thyID_of_derivation_name dn;

if thmID = "add_divide_distrib" andalso thyID = "Fields" then ()

else error "calcelems.sml Thm.derivation_name changed 3";

"-------- fun term2str ----------------------------------";

"-------- fun term2str ----------------------------------";

"-------- fun term2str ----------------------------------";

(*Quick notes from Makarius.1003

 @{term "2::int"} 

 term "(1.24444) :: real"

 numbers_to_string @{term "%x. (-9993::int) + x + 1"} 

 Toplevel.debug := true;

 literal types:

 PolyML.addPrettyPrinter

  (fn _ => fn _ => ml_pretty o Pretty.to_ML o raw_pp_typ);

pretty types:

 PolyML.addPrettyPrinter

   (fn _ => fn _ => ml_pretty o Pretty.to_ML o Proof_Display.pp_typ Pure.thy);

 print_depth 3;

*)

"===== extend parse to string with markup===";

(*

fun parse thy str = 

  (let val t = (typ_a2real o numbers_to_string) 

		   (Syntax.read_term_global thy str)

   in SOME (cterm_of thy t) end) (*FIXXXXME 10.8.02: return term !!!*)

     handle _ => NONE;

*)

"-------- fun thmID_of_derivation_name 000---------------";

"-------- fun thmID_of_derivation_name 000---------------";

"-------- fun thmID_of_derivation_name 000---------------";

val long_id = Thm.get_name_hint @{thm mult_1_left};

if long_id = "Groups.monoid_mult_class.mult_1_left" then ()

else error "fun Thm.get_name_hint or @{thm mult_1_left} changed";

if thmID_of_derivation_name long_id = "mult_1_left" then ()

else error "fun thmID_of_derivation_name broken";

if thyID_of_derivation_name long_id = "Groups" then ()

else error "fun thyID_of_derivation_name broken";