(* Title:  BaseDefinitions/calcelems.sml

   Author: Walther Neuper 060113

   (c) due to copyright terms

*)

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

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

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

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

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

"-------- fun ThmC.cut_id ------------------";

"-------- fun UnparseC.term ----------------------------------";

"-------- fun ThmC.cut_id 000---------------";

"-------- fun Rule_Set.merge -----------------------------------------------------";

"-------- 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 ThmC.cut_id ----------------";

"-------- fun ThmC.cut_id ----------------";

"-------- fun ThmC.cut_id ----------------";

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 = ThmC.cut_id dn;

val thyID = ThyC.cut_id 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 = ThmC.cut_id dn;

val thyID = ThyC.cut_id dn;

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

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

"-------- fun UnparseC.term ----------------------------------";

"-------- fun UnparseC.term ----------------------------------";

"-------- fun UnparseC.term ----------------------------------";

(*Quick notes from Makarius.1003

 @{term "2::int"} 

 term "(1.24444) :: real"

 ThmC_Def.num_to_Free @{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;*)

*)

"-------- fun ThmC.cut_id 000---------------";

"-------- fun ThmC.cut_id 000---------------";

"-------- fun ThmC.cut_id 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 ThmC.cut_id long_id = "mult_1_left" then ()

else error "fun ThmC.cut_id broken";

if ThyC.cut_id long_id = "Groups" then ()

else error "fun ThyC.cut_id broken";

"-------- fun Rule_Set.merge -----------------------------------------------------";

"-------- fun Rule_Set.merge -----------------------------------------------------";

"-------- fun Rule_Set.merge -----------------------------------------------------";

(*theory Thy_2 imports Thy_1*)

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

  Rule_Set.append_rules "test_list_rls" Rule_Set.empty [Thm ("refl", @{thm refl}), Thm ("subst", @{thm subst})]))]

(*theory Thy_2b imports Thy_1*)

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

  Rule_Set.append_rules "test_list_rls" Rule_Set.empty [Thm ("False_def", @{thm False_def})]))]

val [(_, (_, Rule_Set.Repeat {rules, ...}))] = Rule_Set.to_kestore (rlss2, rlss2b)

;

case rules of

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

| _ => error "Rule_Set.merge changed"

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

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

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

val pty = [

  Store.Node ("aaa", [1], [

    Store.Node ("aaa-1", [11], [])]),

  Store.Node ("bbb", [2], [

    Store.Node ("bbb-1", [21], []),

    Store.Node ("bbb-2", [22], [

      Store.Node ("bbb-21", [221], []),

      Store.Node ("bbb-22", [222], [])])]),

  Store.Node ("ccc", [3], [])] : int Store.T

val ID = ["ddd"];

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

val ID = ["ccc"];

if Store.update ID ID 99999 pty = 

  [Store.Node ("aaa", [1], [Store.Node ("aaa-1", [11], [])]), 

  Store.Node ("bbb", [2], [Store.Node ("bbb-1", [21], []), 

    Store.Node ("bbb-2", [22], [Store.Node ("bbb-21", [221], []), Store.Node ("bbb-22", [222], [])])]),

  Store.Node ("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 Store.update ID ID 99999 pty = 

  [Store.Node ("aaa", [1], [Store.Node ("aaa-1", [11], [])]), 

  Store.Node ("bbb", [2], [Store.Node ("bbb-1", [21], []), Store.Node ("bbb-2", [22], 

    [Store.Node ("bbb-21", [99999], []), Store.Node ("bbb-22", [222], [])])]), 

  Store.Node ("ccc", [3], [])] 

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

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

if Store.update ID ID 99999 pty = 

  [Store.Node ("aaa", [1], [Store.Node ("aaa-1", [11], [])]), 

  Store.Node ("bbb", [2], [Store.Node ("bbb-1", [21], []), 

      Store.Node ("bbb-2", [22], [Store.Node ("bbb-21", [221], []), Store.Node ("bbb-22", [99999], [])])]), 

  Store.Node ("ccc", [3], [])] 

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

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

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

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

(*> subst2str' [(TermC.parse_test @{context} "bdv", TermC.parse_test @{context} "x"),

		(TermC.parse_test @{context} "bdv_2", TermC.parse_test @{context} "y")];

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

*)