wneuper/isa: test/Tools/isac/BaseDefinitions/calcelems.sml@68883c046963

     1 (* Title:  BaseDefinitions/calcelems.sml

     2    Author: Walther Neuper 060113

     3    (c) due to copyright terms

     4 *)

     6 "--------------------------------------------------------";

     7 "--------------------------------------------------------";

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

     9 "--------------------------------------------------------";

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

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

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

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

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

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

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

    17 "--------------------------------------------------------";

    18 "--------------------------------------------------------";

    19 "--------------------------------------------------------";

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

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

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

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

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

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

    28 ref_ := "test-data";

    29 (* restore original    *) ref_ := val_;

    30 if ! ref_ = "original-data"

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

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

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

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

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

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

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

    41 val thm = @{thm radd_0};

    42 val dn = Thm.derivation_name thm;

    43 if dn = "Test.radd_0" then ()

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

    46 val thmID = ThmC.cut_id dn;

    47 val thyID = ThyC.cut_id dn;

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

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

    51 "--- thm2 --";

    52 val thm = @{thm add_divide_distrib}

    53 val dn = Thm.derivation_name thm;

    54 val thmID = ThmC.cut_id dn;

    55 val thyID = ThyC.cut_id dn;

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

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

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

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

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

    62 (*Quick notes from Makarius.1003

    64  @{term "2::int"}

    66  term "(1.24444) :: real"

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

    70  Toplevel.debug := true;

    72  literal types:

    73  PolyML.addPrettyPrinter

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

    76 pretty types:

    77  PolyML.addPrettyPrinter

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

    79  (*default_print_depth 3;*)

    80 *)

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

    82 (*

    83 fun parse thy str =

    84   (let val t = (typ_a2real o ThmC_Def.num_to_Free)

    85 		   (Syntax.read_term_global thy str)

    86    in SOME (Thm.global_cterm_of thy t) end) (*FIXXXXME 10.8.02: return term !!!*)

    87      handle _ => NONE;

    88 *)

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

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

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

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

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

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

    97 if ThmC.cut_id long_id = "mult_1_left" then ()

    98 else error "fun ThmC.cut_id broken";

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

   101 else error "fun ThyC.cut_id broken";

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

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

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

   106 (*theory Thy_2 imports Thy_1*)

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

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

   109 (*theory Thy_2b imports Thy_1*)

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

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

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

   114 ;

   115 case rules of

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

   117 | _ => error "Rule_Set.merge changed"

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

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

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

   122 val pty = [

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

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

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

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

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

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

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

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

   132 val ID = ["ddd"];

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

   135 val ID = ["ccc"];

   136 if Store.update ID ID 99999 pty =

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

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

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

   140   Store.Node ("ccc", [99999], [])]

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

   143 val ID = ["aaa"];

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

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

   147 if Store.update ID ID 99999 pty =

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

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

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

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

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

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

   155 if Store.update ID ID 99999 pty =

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

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

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

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

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

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

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

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

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

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

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

   168 *)

author	Walther Neuper <walther.neuper@jku.at>
	Tue, 21 Apr 2020 15:42:50 +0200
changeset 59898	68883c046963
parent 59897	8cba439d0454
child 60230	0ca0f9363ad3
permissions	-rw-r--r--