(* Title:  CalcElements/calcelems.sml

   Author: Walther Neuper 060113

   (c) due to copyright terms

*)

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

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

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

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

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

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

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

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

"-------- fun merge_rlss -----------------------------------------------------";

"-------- fun update_ptyps --------------------------------------------------";

"-------- fun subst2str' -----------------------------------------------------------------------";

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

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

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

"-------- 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);

 (*default_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 (Thm.global_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";

"-------- fun merge_rlss -----------------------------------------------------";

"-------- fun merge_rlss -----------------------------------------------------";

"-------- fun merge_rlss -----------------------------------------------------";

(*theory Thy_2 imports Thy_1*)

val rlss2 = [("test_list_rls", (Context.theory_name @{theory},

  append_rls "test_list_rls" e_rls [Thm ("refl", @{thm refl}), Thm ("subst", @{thm subst})]))]

(*theory Thy_2b imports Thy_1*)

val rlss2b = [("test_list_rls", (Context.theory_name @{theory},

  append_rls "test_list_rls" e_rls [Thm ("False_def", @{thm False_def})]))]

val [(_, (_, Rls {rules, ...}))] = merge_rlss (rlss2, rlss2b)

;

case rules of

  [Thm ("subst", _), Thm ("refl", _), Thm ("False_def", _)] => ()

| _ => error "merge_rlss changed"

"-------- fun update_ptyps --------------------------------------------------";

"-------- fun update_ptyps --------------------------------------------------";

"-------- fun update_ptyps --------------------------------------------------";

val pty = [

  Ptyp ("aaa", [1], [

    Ptyp ("aaa-1", [11], [])]),

  Ptyp ("bbb", [2], [

    Ptyp ("bbb-1", [21], []),

    Ptyp ("bbb-2", [22], [

      Ptyp ("bbb-21", [221], []),

      Ptyp ("bbb-22", [222], [])])]),

  Ptyp ("ccc", [3], [])] : int ptyp list

val ID = ["ddd"];

(*update_ptyps ID ID 99999 pty; ERROR update_ptyps: [aaa] does not exist*)

val ID = ["ccc"];

if update_ptyps ID ID 99999 pty = 

  [Ptyp ("aaa", [1], [Ptyp ("aaa-1", [11], [])]), 

  Ptyp ("bbb", [2], [Ptyp ("bbb-1", [21], []), 

    Ptyp ("bbb-2", [22], [Ptyp ("bbb-21", [221], []), Ptyp ("bbb-22", [222], [])])]),

  Ptyp ("ccc", [99999], [])] 

  then () else error "update_ptyps has changed 1";

val ID = ["aaa"];

(*update_ptyps ID ID 99999 pty; ERROR update_ptyps: [aaa] has descendants*)

val ID = ["bbb", "bbb-2", "bbb-21"];

if update_ptyps ID ID 99999 pty = 

  [Ptyp ("aaa", [1], [Ptyp ("aaa-1", [11], [])]), 

  Ptyp ("bbb", [2], [Ptyp ("bbb-1", [21], []), Ptyp ("bbb-2", [22], 

    [Ptyp ("bbb-21", [99999], []), Ptyp ("bbb-22", [222], [])])]), 

  Ptyp ("ccc", [3], [])] 

then () else error "update_ptyps has changed 2";

val ID = ["bbb", "bbb-2", "bbb-22"];

if update_ptyps ID ID 99999 pty = 

  [Ptyp ("aaa", [1], [Ptyp ("aaa-1", [11], [])]), 

  Ptyp ("bbb", [2], [Ptyp ("bbb-1", [21], []), 

      Ptyp ("bbb-2", [22], [Ptyp ("bbb-21", [221], []), Ptyp ("bbb-22", [99999], [])])]), 

  Ptyp ("ccc", [3], [])] 

then () else error "update_ptyps has changed 3";

"----------- fun subst2str' --------------------------------------------------------------------";

"----------- fun subst2str' --------------------------------------------------------------------";

"----------- fun subst2str' --------------------------------------------------------------------";

(*> subst2str' [(str2term "bdv", str2term "x"),

		(str2term "bdv_2", str2term "y")];

val it = "[(bdv, x)]" : string

*)