1.1 --- a/src/Tools/isac/KEStore.thy	Mon Mar 26 09:27:24 2018 +0200
     1.2 +++ b/src/Tools/isac/KEStore.thy	Mon Mar 26 10:21:19 2018 +0200
     1.3 @@ -8,7 +8,7 @@
     1.4  begin
     1.5    ML_file "~~/src/Tools/isac/library.sml"
     1.6    ML_file "~~/src/Tools/isac/ThydataC/rule.sml"
     1.7 -ML_file "~~/src/Tools/isac/calcelems.sml"
     1.8 +  ML_file "~~/src/Tools/isac/calcelems.sml"
     1.9  (* TODO: 
    1.10   * separate structures from calcelems.sml in addition to Rule to ThydataC/.
    1.11   * separate structures from rule.sml as noted in the respective signature.

     2.1 --- a/src/Tools/isac/library.sml	Mon Mar 26 09:27:24 2018 +0200
     2.2 +++ b/src/Tools/isac/library.sml	Mon Mar 26 10:21:19 2018 +0200
     2.3 @@ -1,22 +1,110 @@
     2.4 -(* use"library.sml";
     2.5 -   WN.22.10.99
     2.6 -   for both, math-engine and isa-98-1-HOL-plus
     2.7 -   however, functions closely related to original isabelle-98-1 functions
     2.8 -            are in isa-98-1-HOL-plus/rewrite-parse/library_G
     2.9 +(* library extending Isabelle's library.
    2.10 +   Author: Walther Neuper 1999
    2.11 +   (c) copyright due to lincense terms
    2.12 +
    2.13 +Note: Here many functions reflect changes since Isabelle 98. Changes frequently were resolved
    2.14 +   quick and dirty by additing Isabelle's old version to the library below.
    2.15 +TODO:
    2.16 + * move outcommented tests from "src/../library.sml" to "test/../library.sml"
    2.17 + * remove unused functions
    2.18 + * review duplicates with other signatures and re-locate respectively
    2.19 + * move unparsing ("*_t0_str", "*2str", etc) somewhere else in ThydataC/
    2.20 + * apply Isabelle's coding standards and remove warnings
    2.21 + * rename "library.sml" to "libraryC.sml" like many other files, where struct <> filename.
    2.22  *)
    2.23  
    2.24 -(* Isabelle2002 -> Isabelle2009 library changed:
    2.25 -signature LIBRARY =
    2.26 -sig
    2.27 -  include BASIC_LIBRARY
    2.28 -  val foldl: ('a * 'b -> 'a) -> 'a * 'b list -> 'a
    2.29 -  val foldr: ('a * 'b -> 'b) -> 'a list * 'b -> 'b
    2.30 -  val foldl_map: ('a * 'b -> 'a * 'c) -> 'a * 'b list -> 'a * 'c list
    2.31 -  val take: int * 'a list -> 'a list
    2.32 -  val drop: int * 'a list -> 'a list
    2.33 -  val last_elem: 'a list -> 'a
    2.34 -end;
    2.35 -FIXME: overwritten again...*)
    2.36 +infix 1 ~~~
    2.37 +
    2.38 +signature LIBRARYC =
    2.39 +  sig
    2.40 +    val and_: bool * bool -> bool
    2.41 +    val assoc: (''a * 'b) list * ''a -> 'b option
    2.42 +    val assoc_string: (string * 'a) list * string -> 'a option
    2.43 +    val bool2str: bool -> string
    2.44 +    val commas: string list -> string
    2.45 +    val compare_strs: string -> string -> unit list
    2.46 +    val con2str: 'a -> string
    2.47 +    val cons2: ('a -> 'b) * ('a -> 'c) -> 'a -> 'b * 'c
    2.48 +    val dashs: int -> string
    2.49 +    val de_quote: string -> string
    2.50 +    val distinct: ''a list -> ''a list
    2.51 +    val dots: int -> string
    2.52 +    val drop: int * 'a list -> 'a list
    2.53 +    val drop_last: 'a list -> 'a list
    2.54 +    val drop_last_n: int -> 'a list -> 'a list
    2.55 +    val drop_nth: 'a list -> int * 'a list -> 'a list
    2.56 +    val dropuntil: ('a -> bool) -> 'a list -> 'a list
    2.57 +    val dropwhile: ('a -> bool) -> 'a list -> 'a list
    2.58 +    val enumerate_strings: string list -> string list
    2.59 +    val foldl: ('a * 'b -> 'a) -> 'a * 'b list -> 'a
    2.60 +    val foldr: ('a * 'b -> 'b) -> 'a list * 'b -> 'b
    2.61 +    val fst3: 'a * 'b * 'c -> 'a
    2.62 +    val gen_dif: ('a * 'b -> bool) -> 'a list * 'b -> 'a list
    2.63 +    val gen_diff: ('a * 'b -> bool) -> 'a list * 'b list -> 'a list
    2.64 +    val gen_distinct: ('a * 'a -> bool) -> 'a list -> 'a list
    2.65 +    val gen_ins: ('a * 'a -> bool) -> 'a * 'a list -> 'a list
    2.66 +    val gen_insI: ('a * 'a -> bool) -> ('a -> string) -> 'a * 'a list -> 'a list
    2.67 +    val gen_insert: ('a * 'a -> bool) -> 'a list * 'a -> 'a list
    2.68 +    val gen_mem: ('a * 'b -> bool) -> 'a * 'b list -> bool
    2.69 +    val gen_rems: ('a * 'b -> bool) -> 'a list * 'b list -> 'a list
    2.70 +    val gen_sort: ('a * 'a -> bool) -> 'a list -> 'a list
    2.71 +    val gen_union: ('a * 'a -> bool) -> 'b -> 'a list * 'a list -> 'a list
    2.72 +    val get_thy: string -> string
    2.73 +    val id_of: term -> string
    2.74 +    val ids_of: term -> string list
    2.75 +    val idt: string -> int -> string
    2.76 +    val if_none: 'a option -> 'a -> 'a
    2.77 +    val indent: int -> string
    2.78 +    val indt: int -> string
    2.79 +    val int2str: int -> string
    2.80 +    val ints2str: int list -> string
    2.81 +    val ints2str': int list -> string
    2.82 +    val intsto: int -> int list
    2.83 +    val last_elem: 'a list -> 'a
    2.84 +    val list2str: string list -> string
    2.85 +    val list_update: 'a list -> int -> 'a -> 'a list
    2.86 +    val maxl: int list -> int
    2.87 +    val member_swap: ('a * 'b -> bool) -> 'a -> 'b list -> bool
    2.88 +    val nos: string list -> string
    2.89 +    val nth: int -> 'a list -> 'a
    2.90 +    val or_: bool * bool -> bool
    2.91 +    val overwrite: (''a * 'b) list * (''a * 'b) -> (''a * 'b) list
    2.92 +    val overwritel: (''a * 'b) list * (''a * 'b) list -> (''a * 'b) list
    2.93 +    val pair2str: string * string -> string
    2.94 +    val pair2str_: string * string -> string
    2.95 +    val pair2tri: ('a * 'b) * 'c -> 'a * 'b * 'c
    2.96 +    eqtype 'a stack
    2.97 +    val pop: 'a stack -> 'a stack
    2.98 +    val push: 'a -> 'a stack -> 'a stack
    2.99 +    val quad2pair: 'a * 'b * 'c * 'd -> 'a * 'b
   2.100 +    val skip_blanks: string list -> string list
   2.101 +    val snd3: 'a * 'b * 'c -> 'b
   2.102 +    val spair2str: string * string -> string
   2.103 +    val split_nlast: int * 'a list -> 'a list * 'a list
   2.104 +    val string_to_bool: string -> bool
   2.105 +    val strip_thy: string -> string
   2.106 +    val strs2str: string list -> string                                  (* duplicates in Rule *)
   2.107 +    val strs2str': string list -> string                                 (* duplicates in Rule *)
   2.108 +    val strs2str_: string list -> string                                 (* duplicates in Rule *)
   2.109 +    val strslist2strs: string list list -> string                        (* duplicates in Rule *)
   2.110 +    val subs2str: string list -> string
   2.111 +    val subs2str': (string * string) list -> string
   2.112 +    val take: int * 'a list -> 'a list
   2.113 +    val take_fromto: int -> int -> 'a list -> 'a list
   2.114 +    val takelast: int * 'a list -> 'a list
   2.115 +    val takerest: int * 'a list -> 'a list
   2.116 +    val takewhile: 'a list -> ('a -> bool) -> 'a list -> 'a list
   2.117 +    val thd3: 'a * 'b * 'c -> 'c
   2.118 +    val top: 'a stack -> 'a
   2.119 +    val triple2pair: 'a * 'b * 'c -> 'a * 'b
   2.120 +    val ~~~ : 'a list * 'b list -> ('a * 'b) list
   2.121 +  end;
   2.122 +
   2.123 +(**)
   2.124 +structure LibraryC(*: RULE*) =
   2.125 +struct
   2.126 +(**)
   2.127 +
   2.128  fun foldl (f: 'a * 'b -> 'a) : 'a * 'b list -> 'a = (*FIXME.2009*)
   2.129    let fun itl (e, [])  = e
   2.130          | itl (e, a::l) = itl (f(e, a), l)
   2.131 @@ -75,7 +163,6 @@
   2.132  
   2.133  
   2.134  (*an indulgent version of Isabelle/src/Pure/library.ML ~~*)
   2.135 -infix ~~~;
   2.136  fun xs ~~~ ys =
   2.137      let fun aaa xys []        []        = xys
   2.138  	  | aaa xys []        (y :: ys) = xys
   2.139 @@ -377,3 +464,4 @@
   2.140          | mx x (y :: ys) = if x < (y: int) then mx y ys else mx x ys
   2.141    in mx y ys end
   2.142  
   2.143 +end; (*struct*) open LibraryC