1.1 --- a/src/Tools/isac/BaseDefinitions/KEStore.thy	Wed Apr 15 18:00:58 2020 +0200
     1.2 +++ b/src/Tools/isac/BaseDefinitions/KEStore.thy	Fri Apr 17 15:12:19 2020 +0200
     1.3 @@ -23,6 +23,18 @@
     1.4  ML_file rule.sml
     1.5  ML_file "error-fill-def.sml" (*rename identifiers by use of struct.id*)
     1.6  ML_file "rule-set.sml"
     1.7 +
     1.8 +ML_file "celem-0.sml"  (**)
     1.9 +ML_file "celem-1.sml"  (**)
    1.10 +ML_file "celem-2.sml"  (**)
    1.11 +ML_file "celem-3.sml"  (**)
    1.12 +ML_file "celem-4.sml"  (**)
    1.13 +ML_file "celem-5.sml"  (**)
    1.14 +ML_file "celem-6.sml"  (**)
    1.15 +ML_file "celem-7.sml"  (**)
    1.16 +ML_file "celem-8.sml"  (**)
    1.17 +ML_file "celem-9.sml"  (**)
    1.18 +
    1.19  ML_file calcelems.sml
    1.20  ML \<open>
    1.21  \<close> ML \<open>

     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/Tools/isac/BaseDefinitions/celem-0.sml	Fri Apr 17 15:12:19 2020 +0200
     2.3 @@ -0,0 +1,72 @@
     2.4 +(* Title:  BaseDefinitions/celem-0.sml
     2.5 +   Author: Walther Neuper
     2.6 +   (c) due to copyright terms
     2.7 +
     2.8 +          *)
     2.9 +signature CALCELEMENT_0 =
    2.10 +(*/------- to Celem0 -------\*)
    2.11 +(*\------- to Celem0 -------/*)
    2.12 +sig
    2.13 +(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
    2.14 +  (*NONE*)
    2.15 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
    2.16 +  (*NONE*)
    2.17 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
    2.18 +end
    2.19 +
    2.20 +(**)
    2.21 +structure Celem0(**): CALCELEMENT_0(**) =
    2.22 +struct
    2.23 +(**)
    2.24 +(*
    2.25 +val get_cas: theory -> Celem.cas_elem list
    2.26 +  val add_cas: Celem.cas_elem list -> theory -> theory
    2.27 +  val get_ptyps: theory -> Celem.ptyps
    2.28 +  val add_pbts: (Celem.pbt * Celem.pblID) list -> theory -> theory
    2.29 +  val get_mets: theory -> Celem.mets
    2.30 +  val add_mets: (Celem.met * Celem.metID) list -> theory -> theory
    2.31 +  val get_thes: theory -> (Celem.thydata Celem.ptyp) list
    2.32 +  val add_thes: (Celem.thydata * Celem.theID) list -> theory -> theory (* thydata dropped at existing elems *)
    2.33 +  val insert_fillpats: (Celem.theID * Error_Fill_Def.fillpat list) list -> theory -> theory 
    2.34 +    type T = (term * (Celem.spec * (term list -> (term * term list) list))) list;
    2.35 +    val merge = merge Celem.cas_eq;
    2.36 +  fun add_cas cas = Data.map (union_overwrite Celem.cas_eq cas)
    2.37 +    type T = Celem.ptyps;
    2.38 +    val empty = [Celem.e_Ptyp];
    2.39 +    val merge = Celem.merge_ptyps;
    2.40 +                (if (!Celem.check_guhs_unique) then Celem.check_pblguh_unique guh (Data.get thy) else ();
    2.41 +                  rev pblID |> Celem.insrt pblID pbt);
    2.42 +    type T = Celem.mets;
    2.43 +    val empty = [Celem.e_Mets];
    2.44 +    val merge = Celem.merge_ptyps;
    2.45 +                (if (!Celem.check_guhs_unique) then Celem.check_metguh_unique guh (Data.get thy) else ();
    2.46 +                  Celem.insrt metID met metID);
    2.47 +    type T = (Celem.thydata Celem.ptyp) list;
    2.48 +    val merge = Celem.merge_ptyps; (* relevant for store_thm, store_rls *)
    2.49 +    fun add_the (thydata, theID) = Celem.add_thydata ([], theID) thydata
    2.50 +          val hthm = Celem.get_py (Data.get thy) theID theID
    2.51 +          val hthm' = Celem.update_hthm hthm fillpats
    2.52 +        in Celem.update_ptyps theID theID hthm' end
    2.53 +  [(Celem.Html {guh = Celem.part2guh ["IsacKnowledge"], html = "",
    2.54 +  (Celem.Html {guh = Celem.part2guh ["Isabelle"], html = "",
    2.55 +  (Celem.Html {guh = Celem.part2guh ["IsacScripts"], html = "",
    2.56 +fun check_kestore_cas ((t, (s, _)) : Celem.cas_elem) =
    2.57 +  (Proof_Context.init_global @{theory})))) t ^ ", " ^ Celem.spec2str s ^ ")";
    2.58 +  | count_kestore_ptyps ((Celem.Ptyp (_, _, ps)) :: ps') =
    2.59 +fun check_kestore_ptyp' strfun (Celem.Ptyp (key, pbts, pts)) = "Ptyp (" ^ (quote key) ^ ", " ^
    2.60 +      (strfun pbts) ^ ", " ^ (map (check_kestore_ptyp' strfun) pts |> list2str) ^ ")" |> Celem.linefeed;
    2.61 +val check_kestore_ptyp = check_kestore_ptyp' Celem.pbts2str;
    2.62 +fun ptyp_ord ((Celem.Ptyp (s1, _, _)), (Celem.Ptyp (s2, _, _))) = string_ord (s1, s2);
    2.63 +fun pbt_ord ({guh = guh'1, ...} : Celem.pbt, {guh = guh'2, ...} : Celem.pbt) = string_ord (guh'1, guh'2);
    2.64 +  | sort_kestore_ptyp' ordfun ((Celem.Ptyp (key, pbts, ps)) :: ps') =
    2.65 +     ((Celem.Ptyp (key, sort ordfun pbts, sort_kestore_ptyp' ordfun ps |> sort ptyp_ord))
    2.66 +fun metguh2str ({guh,...} : Celem.met) = guh : string;
    2.67 +fun check_kestore_met (mp: Celem.met Celem.ptyp) =
    2.68 +fun met_ord ({guh = guh'1, ...} : Celem.met, {guh = guh'2, ...} : Celem.met) = string_ord (guh'1, guh'2);
    2.69 +fun check_kestore_thes thes = ((map writeln) o (map (check_kestore_ptyp' Celem.thes2str))) thes
    2.70 +    |> map (fn (id, the) => (Celem.theID2str id, Celem.the2str the))
    2.71 +*)
    2.72 +(*/------- to Celem0 -------\*)
    2.73 +(*\------- to Celem0 -------/*)
    2.74 +
    2.75 +(**)end(**)

     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/Tools/isac/BaseDefinitions/celem-1.sml	Fri Apr 17 15:12:19 2020 +0200
     3.3 @@ -0,0 +1,25 @@
     3.4 +(* Title:  BaseDefinitions/celem-1.sml
     3.5 +   Author: Walther Neuper
     3.6 +   (c) due to copyright terms
     3.7 +
     3.8 +          *)
     3.9 +signature CALCELEMENT_1 =
    3.10 +(*/------- to Celem1 -------\*)
    3.11 +(*\------- to Celem1 -------/*)
    3.12 +sig
    3.13 +(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
    3.14 +  (*NONE*)
    3.15 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
    3.16 +  (*NONE*)
    3.17 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
    3.18 +end
    3.19 +
    3.20 +(**)
    3.21 +structure Celem1(**): CALCELEMENT_1(**) =
    3.22 +struct
    3.23 +(**)
    3.24 +
    3.25 +(*/------- to Celem1 -------\*)
    3.26 +(*\------- to Celem1 -------/*)
    3.27 +
    3.28 +(**)end(**)

     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/Tools/isac/BaseDefinitions/celem-2.sml	Fri Apr 17 15:12:19 2020 +0200
     4.3 @@ -0,0 +1,25 @@
     4.4 +(* Title:  BaseDefinitions/celem-2.sml
     4.5 +   Author: Walther Neuper
     4.6 +   (c) due to copyright terms
     4.7 +
     4.8 +          *)
     4.9 +signature CALCELEMENT_2 =
    4.10 +(*/------- to Celem2 -------\*)
    4.11 +(*\------- to Celem2 -------/*)
    4.12 +sig
    4.13 +(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
    4.14 +  (*NONE*)
    4.15 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
    4.16 +  (*NONE*)
    4.17 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
    4.18 +end
    4.19 +
    4.20 +(**)
    4.21 +structure Celem2(**): CALCELEMENT_2(**) =
    4.22 +struct
    4.23 +(**)
    4.24 +
    4.25 +(*/------- to Celem2 -------\*)
    4.26 +(*\------- to Celem2 -------/*)
    4.27 +
    4.28 +(**)end(**)

     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/Tools/isac/BaseDefinitions/celem-3.sml	Fri Apr 17 15:12:19 2020 +0200
     5.3 @@ -0,0 +1,25 @@
     5.4 +(* Title:  BaseDefinitions/celem-3.sml
     5.5 +   Author: Walther Neuper
     5.6 +   (c) due to copyright terms
     5.7 +
     5.8 +          *)
     5.9 +signature CALCELEMENT_3 =
    5.10 +(*/------- to Celem3 -------\*)
    5.11 +(*\------- to Celem3 -------/*)
    5.12 +sig
    5.13 +(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
    5.14 +  (*NONE*)
    5.15 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
    5.16 +  (*NONE*)
    5.17 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
    5.18 +end
    5.19 +
    5.20 +(**)
    5.21 +structure Celem3(**): CALCELEMENT_3(**) =
    5.22 +struct
    5.23 +(**)
    5.24 +
    5.25 +(*/------- to Celem3 -------\*)
    5.26 +(*\------- to Celem3 -------/*)
    5.27 +
    5.28 +(**)end(**)

     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/Tools/isac/BaseDefinitions/celem-4.sml	Fri Apr 17 15:12:19 2020 +0200
     6.3 @@ -0,0 +1,25 @@
     6.4 +(* Title:  BaseDefinitions/celem-4.sml
     6.5 +   Author: Walther Neuper
     6.6 +   (c) due to copyright terms
     6.7 +
     6.8 +          *)
     6.9 +signature CALCELEMENT_4 =
    6.10 +(*/------- to Celem4 -------\*)
    6.11 +(*\------- to Celem4 -------/*)
    6.12 +sig
    6.13 +(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
    6.14 +  (*NONE*)
    6.15 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
    6.16 +  (*NONE*)
    6.17 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
    6.18 +end
    6.19 +
    6.20 +(**)
    6.21 +structure Celem4(**): CALCELEMENT_4(**) =
    6.22 +struct
    6.23 +(**)
    6.24 +
    6.25 +(*/------- to Celem4 -------\*)
    6.26 +(*\------- to Celem4 -------/*)
    6.27 +
    6.28 +(**)end(**)

     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/src/Tools/isac/BaseDefinitions/celem-5.sml	Fri Apr 17 15:12:19 2020 +0200
     7.3 @@ -0,0 +1,25 @@
     7.4 +(* Title:  BaseDefinitions/celem-5.sml
     7.5 +   Author: Walther Neuper
     7.6 +   (c) due to copyright terms
     7.7 +
     7.8 +          *)
     7.9 +signature CALCELEMENT_5 =
    7.10 +(*/------- to Celem5 -------\*)
    7.11 +(*\------- to Celem5 -------/*)
    7.12 +sig
    7.13 +(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
    7.14 +  (*NONE*)
    7.15 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
    7.16 +  (*NONE*)
    7.17 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
    7.18 +end
    7.19 +
    7.20 +(**)
    7.21 +structure Celem5(**): CALCELEMENT_5(**) =
    7.22 +struct
    7.23 +(**)
    7.24 +
    7.25 +(*/------- to Celem5 -------\*)
    7.26 +(*\------- to Celem5 -------/*)
    7.27 +
    7.28 +(**)end(**)

     8.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.2 +++ b/src/Tools/isac/BaseDefinitions/celem-6.sml	Fri Apr 17 15:12:19 2020 +0200
     8.3 @@ -0,0 +1,25 @@
     8.4 +(* Title:  BaseDefinitions/celem-6.sml
     8.5 +   Author: Walther Neuper
     8.6 +   (c) due to copyright terms
     8.7 +
     8.8 +          *)
     8.9 +signature CALCELEMENT_6 =
    8.10 +(*/------- to Celem6 -------\*)
    8.11 +(*\------- to Celem6 -------/*)
    8.12 +sig
    8.13 +(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
    8.14 +  (*NONE*)
    8.15 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
    8.16 +  (*NONE*)
    8.17 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
    8.18 +end
    8.19 +
    8.20 +(**)
    8.21 +structure Celem6(**): CALCELEMENT_6(**) =
    8.22 +struct
    8.23 +(**)
    8.24 +
    8.25 +(*/------- to Celem6 -------\*)
    8.26 +(*\------- to Celem6 -------/*)
    8.27 +
    8.28 +(**)end(**)

     9.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.2 +++ b/src/Tools/isac/BaseDefinitions/celem-7.sml	Fri Apr 17 15:12:19 2020 +0200
     9.3 @@ -0,0 +1,25 @@
     9.4 +(* Title:  BaseDefinitions/celem-7.sml
     9.5 +   Author: Walther Neuper
     9.6 +   (c) due to copyright terms
     9.7 +
     9.8 +          *)
     9.9 +signature CALCELEMENT_7 =
    9.10 +(*/------- to Celem7 -------\*)
    9.11 +(*\------- to Celem7 -------/*)
    9.12 +sig
    9.13 +(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
    9.14 +  (*NONE*)
    9.15 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
    9.16 +  (*NONE*)
    9.17 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
    9.18 +end
    9.19 +
    9.20 +(**)
    9.21 +structure Celem7(**): CALCELEMENT_7(**) =
    9.22 +struct
    9.23 +(**)
    9.24 +
    9.25 +(*/------- to Celem7 -------\*)
    9.26 +(*\------- to Celem7 -------/*)
    9.27 +
    9.28 +(**)end(**)

    10.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    10.2 +++ b/src/Tools/isac/BaseDefinitions/celem-8.sml	Fri Apr 17 15:12:19 2020 +0200
    10.3 @@ -0,0 +1,25 @@
    10.4 +(* Title:  BaseDefinitions/celem-8.sml
    10.5 +   Author: Walther Neuper
    10.6 +   (c) due to copyright terms
    10.7 +
    10.8 +          *)
    10.9 +signature CALCELEMENT_8 =
   10.10 +(*/------- to Celem8 -------\*)
   10.11 +(*\------- to Celem8 -------/*)
   10.12 +sig
   10.13 +(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
   10.14 +  (*NONE*)
   10.15 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
   10.16 +  (*NONE*)
   10.17 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
   10.18 +end
   10.19 +
   10.20 +(**)
   10.21 +structure Celem8(**): CALCELEMENT_8(**) =
   10.22 +struct
   10.23 +(**)
   10.24 +
   10.25 +(*/------- to Celem8 -------\*)
   10.26 +(*\------- to Celem8 -------/*)
   10.27 +
   10.28 +(**)end(**)

    11.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    11.2 +++ b/src/Tools/isac/BaseDefinitions/celem-9.sml	Fri Apr 17 15:12:19 2020 +0200
    11.3 @@ -0,0 +1,25 @@
    11.4 +(* Title:  BaseDefinitions/celem-9.sml
    11.5 +   Author: Walther Neuper
    11.6 +   (c) due to copyright terms
    11.7 +
    11.8 +          *)
    11.9 +signature CALCELEMENT_9 =
   11.10 +(*/------- to Celem9 -------\*)
   11.11 +(*\------- to Celem9 -------/*)
   11.12 +sig
   11.13 +(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
   11.14 +  (*NONE*)
   11.15 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
   11.16 +  (*NONE*)
   11.17 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
   11.18 +end
   11.19 +
   11.20 +(**)
   11.21 +structure Celem9(**): CALCELEMENT_9(**) =
   11.22 +struct
   11.23 +(**)
   11.24 +
   11.25 +(*/------- to Celem9 -------\*)
   11.26 +(*\------- to Celem9 -------/*)
   11.27 +
   11.28 +(**)end(**)

    12.1 --- a/src/Tools/isac/BaseDefinitions/libraryC.sml	Wed Apr 15 18:00:58 2020 +0200
    12.2 +++ b/src/Tools/isac/BaseDefinitions/libraryC.sml	Fri Apr 17 15:12:19 2020 +0200
    12.3 @@ -78,6 +78,8 @@
    12.4      val thd3: 'a * 'b * 'c -> 'c
    12.5      val triple2pair: 'a * 'b * 'c -> 'a * 'b
    12.6      val ~~~ : 'a list * 'b list -> ('a * 'b) list
    12.7 +    val linefeed: string -> string
    12.8 +
    12.9  (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
   12.10      (* NONE *)
   12.11  (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
   12.12 @@ -300,4 +302,6 @@
   12.13  
   12.14  fun termless tu = (Term_Ord.term_ord tu = LESS);
   12.15  
   12.16 +val linefeed = curry op ^ "\n"; (* ?\<longrightarrow> libraryC ?*)
   12.17 +
   12.18  end; (*struct*) open LibraryC

    13.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    13.2 +++ b/src/Tools/isac/BaseDefinitions/tracing.sml	Fri Apr 17 15:12:19 2020 +0200
    13.3 @@ -0,0 +1,41 @@
    13.4 +(* Title:  BaseDefinitions/tracing.sml
    13.5 +   Author: Walther Neuper
    13.6 +   (c) due to copyright terms
    13.7 +
    13.8 +This structure could be dropped due to improved reflection in Isabelle;
    13.9 +but ThmC.sym_thm requires still an identifying string thm_id.
   13.10 +*)
   13.11 +signature TRACING =
   13.12 +sig
   13.13 +(*/------- to Trace from Celem -------\*)
   13.14 +    val trace_calc: bool Unsynchronized.ref
   13.15 +    val trace_rewrite: bool Unsynchronized.ref
   13.16 +(*\------- to Trace from Celem --------/*)
   13.17 +(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
   13.18 +  (*NONE*)
   13.19 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
   13.20 +  (*NONE*)
   13.21 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
   13.22 +end
   13.23 +
   13.24 +(**)
   13.25 +structure Trace(**): TRACING(**) =
   13.26 +struct
   13.27 +(**)
   13.28 +
   13.29 +(*/------- to Trace from Celem -------\*)
   13.30 +(* trace internal steps of isac's numeral calculations *)
   13.31 +val trace_calc = Unsynchronized.ref false;
   13.32 +(* trace internal steps of isac's rewriter *)
   13.33 +val trace_rewrite = Unsynchronized.ref false;
   13.34 +(* depth of recursion in traces of the rewriter, if trace_rewrite:=true *)
   13.35 +val depth = Unsynchronized.ref 99999;
   13.36 +(* no of rewrites exceeding this int -> NO rewrite *)
   13.37 +val lim_deriv = Unsynchronized.ref 100;
   13.38 +(* switch for checking guhs unique before storing a pbl or met;
   13.39 +   set true at startup (done at begin of ROOT.ML)
   13.40 +   set false for editing IsacKnowledge (done at end of ROOT.ML) *)
   13.41 +val check_guhs_unique = Unsynchronized.ref true;
   13.42 +(*\------- to Trace from Celem --------/*)
   13.43 +
   13.44 +(**)end(**)

    14.1 --- a/src/Tools/isac/TODO.thy	Wed Apr 15 18:00:58 2020 +0200
    14.2 +++ b/src/Tools/isac/TODO.thy	Fri Apr 17 15:12:19 2020 +0200
    14.3 @@ -29,7 +29,17 @@
    14.4    \item ML_file "rule-set.sml" KEStore -> MathEngBasic (=ThmC, Rewrite)
    14.5      probably first review calcelems.sml
    14.6    \item xxx
    14.7 +  \item replace src/ Erls Rule_Set.Empty
    14.8    \item xxx
    14.9 +  \item rename exec-def.sml -> eval_def.sml
   14.10 +               calculate.sml _> evaluate.sml (struct Eval -> Evaluate?!?)
   14.11 +  \item xxx
   14.12 +  \item rename KEStore -> Know_Store KNOWLEDGE_STORE + file.sml
   14.13 +               Build_Thydata -> Build_Knowledge
   14.14 +  \item xxx
   14.15 +  \item rename ptyps.sml -> specify-etc.sml
   14.16 +        rename Specify -> Specify_Etc
   14.17 +        rename SpecifyNEW -> Specify
   14.18    \item xxx
   14.19    \item xxx
   14.20    \item xxx