neuper@37906: (* use"library.sml"; neuper@37906: WN.22.10.99 neuper@37906: for both, math-engine and isa-98-1-HOL-plus neuper@37906: however, functions closely related to original isabelle-98-1 functions neuper@37906: are in isa-98-1-HOL-plus/rewrite-parse/library_G neuper@37906: *) neuper@37906: neuper@37906: (* Isabelle2002 -> Isabelle2009 library changed: neuper@37906: signature LIBRARY = neuper@37906: sig neuper@37906: include BASIC_LIBRARY neuper@37906: val foldl: ('a * 'b -> 'a) -> 'a * 'b list -> 'a neuper@37906: val foldr: ('a * 'b -> 'b) -> 'a list * 'b -> 'b neuper@37906: val foldl_map: ('a * 'b -> 'a * 'c) -> 'a * 'b list -> 'a * 'c list neuper@37906: val take: int * 'a list -> 'a list neuper@37906: val drop: int * 'a list -> 'a list neuper@37906: val last_elem: 'a list -> 'a neuper@37906: end; neuper@37906: FIXME: overwritten again...*) neuper@37906: fun foldl (f: 'a * 'b -> 'a) : 'a * 'b list -> 'a = (*FIXME.2009*) neuper@37906: let fun itl (e, []) = e neuper@37906: | itl (e, a::l) = itl (f(e, a), l) neuper@37906: in itl end; neuper@37906: fun foldr f (l, e) = (*FIXME.2009*) neuper@37906: let fun itr [] = e neuper@37906: | itr (a::l) = f(a, itr l) neuper@37906: in itr l end; neuper@37906: fun take (n, []) = [] (*FIXME.2009*) neuper@37906: | take (n, x :: xs) = neuper@37906: if n > 0 then x :: take (n - 1, xs) else []; neuper@37906: fun drop (n, []) = [] (*FIXME.2009*) neuper@37906: | drop (n, x :: xs) = neuper@37906: if n > 0 then drop (n - 1, xs) else x :: xs; neuper@38011: neuper@37906: (*exn LIST has disappeared in 2009 ... replaced by error...*) neuper@38031: fun last_elem [] = error "last_elem" (*FIXME.2009*) neuper@37906: | last_elem [x] = x neuper@37906: | last_elem (_ :: xs) = last_elem xs; neuper@37906: neuper@37906: fun gen_mem eq (x, []) = false (*FIXME.2009*) neuper@37906: | gen_mem eq (x, y :: ys) = eq (x, y) orelse gen_mem eq (x, ys); neuper@37906: fun gen_insert (les : 'a * 'a -> bool) ([], a) = [a] neuper@37906: | gen_insert les (x::xs, a) = if les (x, a) then x::(gen_insert les (xs, a)) neuper@37906: else a::x::xs; neuper@37906: fun gen_sort les xs = foldl (gen_insert les) (xs, []); neuper@37906: fun gen_distinct eq lst = neuper@37906: let neuper@37906: val memb = gen_mem eq; neuper@37906: neuper@37906: fun dist (rev_seen, []) = rev rev_seen neuper@37906: | dist (rev_seen, x :: xs) = neuper@37906: if memb (x, rev_seen) then dist (rev_seen, xs) neuper@37906: else dist (x :: rev_seen, xs); neuper@37906: in neuper@37906: dist ([], lst) neuper@37906: end; neuper@37906: fun gen_rems eq (xs, ys) = filter_out (fn x => gen_mem eq (x, ys)) xs; neuper@37906: fun distinct l = gen_distinct (op =) l; neuper@37906: neuper@37906: neuper@37906: neuper@37906: (*.see 'fun (y :: ys) \ x' in Pure/library.ML.*) neuper@37906: fun gen_dif eq (y :: ys, x) = if eq (y, x) then ys neuper@37906: else y :: (gen_dif eq (ys, x)) neuper@37906: | gen_dif eq ([], x) = []; neuper@37906: (* val (eq, (y :: ys, x)) = ();*) neuper@37906: neuper@37906: (*.see 'fun ys \\ xs' in Pure/library.ML.*) neuper@37906: fun gen_diff eq (ys, xs) = foldl (gen_dif eq) (ys,xs); neuper@37906: (* val (eq, (ys, xs)) = (eq_thmI, (isacrlsthms, isacthms)); neuper@37906: *) neuper@37906: (* gen_diff op= ([1,2,3,4,5,6,7],[2,3,5]); neuper@37906: val it = [1, 4, 6, 7] : int list*) neuper@37906: neuper@37906: neuper@37906: (*an indulgent version of Isabelle/src/Pure/library.ML ~~*) neuper@37906: infix ~~~; neuper@37906: fun xs ~~~ ys = neuper@37906: let fun aaa xys [] [] = xys neuper@37906: | aaa xys [] (y :: ys) = xys neuper@37906: | aaa xys (x :: xs) [] = xys neuper@37906: | aaa xys (x :: xs) (y :: ys) = aaa (xys @ [(x, y)]) xs ys neuper@37906: in aaa [] xs ys end; neuper@37906: (*[1,2,3] ~~~ ["1","2","3"]; neuper@37906: val it = [(1, "1"), (2, "2"), (3, "3")] : (int * string) list neuper@37906: > [1,2] ~~~ ["1","2","3"]; neuper@37906: val it = [(1, "1"), (2, "2")] : (int * string) list neuper@37906: > [1,2,3] ~~~ ["1","2"]; neuper@37906: val it = [(1, "1"), (2, "2")] : (int * string) list*) neuper@37906: neuper@37906: (*from Isabelle2002/src/Pure/library.ML; has changed in 2009 FIXME replace*) neuper@37906: fun gen_ins eq (x, xs) = if gen_mem eq (x, xs) then xs else x :: xs; neuper@37906: fun gen_insI eq pr (x, xs) = neuper@37906: if gen_mem eq (x, xs) neuper@38015: then (tracing ("### occurs twice: "^(pr x)); xs) neuper@37906: else x :: xs; neuper@37906: fun gen_union eq pr (xs, []) = xs neuper@37906: | gen_union eq pr ([], ys) = ys neuper@37906: | gen_union eq pr (x :: xs, ys) = gen_union eq pr (xs, gen_ins eq (x, ys)); neuper@37906: neuper@37906: fun cons2 (f,g) x = (f x, g x); (*PL softwareparadigmen*) neuper@37906: neuper@38031: fun nth _ [] = error "nth _ []" neuper@37906: | nth 1 (x::_) = x neuper@37906: | nth n (_::xs) = nth (n-1) xs; neuper@37906: (*WN050106 quick for test: doesn't check for exns*) neuper@37906: fun drop_nth ls (_, []) = ls neuper@37906: | drop_nth ls (n, x :: xs) = neuper@37906: if n = 1 neuper@37906: then ls @ xs neuper@37906: else drop_nth (ls @ [x]) (n - 1, xs); neuper@37906: (*> drop_nth [] (3,[1,2,3,4,5]); neuper@37906: val it = [1, 2, 4, 5] : int list neuper@37906: > drop_nth [] (1,[1,2,3,4,5]); neuper@37906: val it = [2, 3, 4, 5] : int list neuper@37906: > drop_nth [] (5,[1,2,3,4,5]); neuper@37906: val it = [1, 2, 3, 4] : int list *) neuper@37906: neuper@37906: fun and_ (b1,b2) = b1 andalso b2;(* ~/Design.98/ModelSpec.sml/library_G.sml *) neuper@37906: fun or_ (b1,b2) = b1 orelse b2; neuper@37906: neuper@37906: neuper@37906: fun takerest (i, ls) = (rev o take) (length ls - i, rev ls); neuper@37906: (*> takerest (3, ["normalize","polynomial","univariate","equation"]); neuper@37906: val it = ["equation"] : string list neuper@37906: *) neuper@37906: fun takelast (i, ls) = (rev o take) (i, rev ls); neuper@37906: (* > takelast (2, ["normalize","polynomial","univariate","equation"]); neuper@37906: val it = ["univariate", "equation"] : pblID neuper@37906: > takelast (2, ["equation"]); neuper@37906: val it = ["equation"] : pblID neuper@37906: > takelast (3, ["normalize","polynomial","univariate","equation"]); neuper@37906: val it = ["polynomial", "univariate", "equation"]*) neuper@37906: fun split_nlast (i, ls) = neuper@37906: let val rv = rev ls neuper@37906: in (rev (takelast (i - 1, rv)), rev (take (i, rv))) end; neuper@37906: neuper@37906: fun split_nlast (i, ls) = (take (length ls - i, ls), rev (take (i, rev ls))); neuper@37906: (* val (a, b) = split_nlast (3, ["a","b","[",".","]"]); neuper@37906: val a = ["a", "b"] : string list neuper@37906: val b = ["[", ".", "]"] : string list neuper@37906: > val (a, b) = split_nlast (3, [".","]"]); neuper@37906: val a = [] : string list neuper@37906: val b = [".", "]"] : string list *) neuper@37906: neuper@37906: (*.analoguous to dropwhile in Pure/libarary.ML.*) neuper@37906: fun dropwhile P [] = [] neuper@37906: | dropwhile P (ys as x::xs) = if P x then dropwhile P xs else ys; neuper@37906: fun takewhile col P [] = col neuper@37906: | takewhile col P (ys as x::xs) = if P x then takewhile (col @ [x]) P xs neuper@37906: else col; neuper@37906: (* > takewhile [] (not o (curry op= 4)) [1,2,3,4,5,6,7]; neuper@37906: val it = [1, 2, 3] : int list*) neuper@37906: fun dropuntil P [] = [] neuper@37906: | dropuntil P (ys as x::xs) = if P x then ys else dropuntil P xs; neuper@37906: neuper@37906: neuper@37906: neuper@37906: fun pair2tri ((a,b),c) = (a,b,c); neuper@37906: fun fst3 (a,_,_) = a; neuper@37906: fun snd3 (_,b,_) = b; neuper@37906: fun thd3 (_,_,c) = c; neuper@37906: neuper@37906: fun skip_blanks strl = neuper@37906: let neuper@37906: fun skip strl [] = strl neuper@37906: | skip strl (" "::ss) = skip strl ss neuper@37906: | skip strl ( s ::ss) = skip (strl @ [s]) ss neuper@37906: in skip [] strl end; neuper@37906: neuper@37906: neuper@37906: neuper@37906: fun de_quote str = neuper@37906: let fun scan ss' [] = ss' neuper@37906: | scan ss' ("\""::ss) = scan ss' ss neuper@37906: | scan ss' (s::ss) = scan (ss' @ [s]) ss; neuper@37906: in (implode o (scan []) o explode) str end; neuper@37906: (*> de_quote "\"d_d ?bdv (?u + ?v) = d_d ?bdv ?u + d_d ?bdv ?v\""; neuper@37906: val it = "d_d ?bdv (?u + ?v) = d_d ?bdv ?u + d_d ?bdv ?v" : string*) neuper@37906: neuper@37906: neuper@37906: neuper@37906: (* conversions to (quoted) strings neuper@37906: FIXME: rename *2str --> *2strq (quoted elems) neuper@37906: now *2str' (elems NOT quoted) instead of *2str *) neuper@37906: neuper@37906: val commas = space_implode ","; neuper@37906: neuper@37906: fun strs2str strl = "[" ^ (commas (map quote strl)) ^ "]"; neuper@38015: (*> val str = strs2str ["123","asd"]; tracing str; neuper@37906: val it = "[\"123\", \"asd\"]" : string neuper@37906: "123", "asd"] *) neuper@37906: fun strs2str' strl = "[" ^ (commas strl) ^ "]"; neuper@37906: fun list2str strl = "[" ^ (commas strl) ^ "]"; neuper@38015: (*> val str = list2str ["123","asd"]; tracing str; neuper@37906: val str = "[123, asd]" : string neuper@37906: [123, asd] *) neuper@37906: fun spair2str (s1,s2) = "(" ^ (quote s1) ^ ", " ^ (quote s2) ^ ")"; neuper@37906: fun pair2str (s1,s2) = "(" ^ s1 ^ ", " ^ s2 ^ ")"; neuper@37906: (*16.11.00 neuper@37906: fun subs2str (subs:(string * string) list) = neuper@37906: (list2str o (map pair2str)) subs;*) neuper@37906: fun subs2str (subs: string list) = list2str subs; neuper@37906: (*> val sss = ["(bdv,x)","(err,#0)"]; neuper@37906: > subs2str sss; neuper@37906: val it = "[(bdv,x),(err,#0)]" : string*) neuper@37906: fun subs2str' (subs:(string * string) list) = (*12.12.99???*) neuper@37906: (list2str o (map pair2str)) subs; neuper@38015: (*> val subs = subs2str [("bdv","x")]; tracing subs; neuper@37906: val subs = "[(\"bdv\", \"x\")]" : string neuper@37906: [("bdv", "x")] *) neuper@37906: fun con2str land_lor = quote " &| "; neuper@37906: val int2str = string_of_int; neuper@37906: fun ints2str ints = (strs2str o (map string_of_int)) ints; neuper@37906: fun ints2str' ints = (strs2str' o (map string_of_int)) ints; neuper@37906: neuper@37906: neuper@37906: (* use"library.sml"; neuper@37906: *) neuper@37906: neuper@37906: neuper@37906: (*needed in Isa + ME*) neuper@37906: fun get_thy str = neuper@37906: let fun get strl [] = strl neuper@37906: | get strl ("."::ss) = strl neuper@37906: | get strl ( s ::ss) = get (strl @ [s]) ss neuper@37906: in implode( get [] (explode str)) end; neuper@37906: neuper@37906: fun strip_thy str = neuper@37906: let fun strip bdVar [] = implode (rev bdVar) neuper@37906: | strip bdVar ("."::_ ) = implode (rev bdVar) neuper@37906: | strip bdVar (c ::cs) = strip (bdVar @[c]) cs neuper@37906: in strip [] (rev(explode str)) end; neuper@37906: neuper@37906: fun id_of (Var ((id,ix),_)) = if ix=0 then id else id^(string_of_int ix) neuper@37906: | id_of (Free (id ,_)) = id neuper@37906: | id_of (Const(id ,_)) = id neuper@37906: | id_of _ = ""; (* never such an identifier *) neuper@37906: neuper@37906: fun ids_of t = neuper@37906: let fun con ss (Const (s,_)) = s::ss neuper@37906: | con ss (Free (s,_)) = s::ss neuper@37906: | con ss (Abs (s,_,b)) = s::(con ss b) neuper@37906: | con ss (t1 $ t2) = (con ss t1) @ (con ss t2) neuper@37906: | con ss _ = ss neuper@37906: in map strip_thy ((distinct o (con [])) t) end; neuper@37906: (* neuper@37906: > val t = (term_of o the o (parse thy)) neuper@37906: "solve_univar (R, [univar, equation], no_met) (a = b + #1) a"; neuper@37906: > ids_of t; neuper@37906: ["solve'_univar","Pair","R","Cons","univar","equation","Nil",...]*) neuper@37906: neuper@37906: neuper@37906: (*FIXME.WN090819 fun overwrite missing in ..2009/../library.ML*) neuper@37906: fun overwrite (al, p as (key, _)) = (*FIXME.2009*) neuper@37906: let fun over ((q as (keyi, _)) :: pairs) = neuper@37906: if keyi = key then p :: pairs else q :: (over pairs) neuper@37906: | over [] = [p] neuper@37906: in over al end; neuper@37906: fun overwritel (al, []) = al neuper@37906: | overwritel (al, b::bl) = overwritel (overwrite (al, b), bl); neuper@37906: (*> val aaa = [(1,11),(2,22),(3,33)]; neuper@37906: > overwritel (aaa, [(2,2222),(4,4444)]); neuper@37906: val it = [(1,11),(2,2222),(3,33),(4,4444)] : (int * int) list*) neuper@37906: neuper@37906: neuper@37906: local neuper@37906: fun intsto1 0 = [] neuper@37906: | intsto1 n = (intsto1 (n-1)) @ [n] neuper@37906: in neuper@38031: fun intsto n = if n < 0 then (error "intsto < 0") else intsto1 n neuper@37906: end; neuper@37906: neuper@37906: neuper@37906: type 'a stack = 'a list; neuper@37906: fun top ((x::xs):'a stack) = x neuper@38031: | top _ = error "top called for empty list"; neuper@37906: fun pop ((x::xs):'a stack) = xs:'a stack neuper@38031: | pop _ = error "pop called for empty list"; neuper@37906: fun push x (xs:'a stack) = x::xs:'a stack; neuper@37906: neuper@37906: neuper@37906: fun drop_last l = ((rev o tl o rev) l); neuper@37906: fun drop_last_n n l = rev (takerest (n, rev l)); neuper@37906: (*> drop_last_n 2 [1,2,3,4,5]; neuper@37906: val it = [1, 2, 3] : int list neuper@37906: > drop_last_n 3 [1,2,3,4,5]; neuper@37906: val it = [1, 2] : int list neuper@37906: > drop_last_n 7 [1,2,3,4,5]; neuper@37906: val it = [] : int list neuper@37906: *) neuper@37906: neuper@37906: fun bool2str true = "true" neuper@37906: | bool2str false = "false"; neuper@37906: neuper@37906: (*.take elements from b to e including both.*) neuper@37906: fun take_fromto from to l = neuper@38031: if from > to then error ("take_fromto from="^string_of_int from^ neuper@37906: " > to="^string_of_int to) neuper@37906: else drop (from - 1, take (to, l)); neuper@37906: (*> take_fromto 3 5 [1,2,3,4,5,6,7]; neuper@37906: val it = [3,4,5] : int list neuper@37906: > take_fromto 3 3 [1,2,3,4,5,6,7]; neuper@37906: val it = [3] : int list*) neuper@37906: neuper@37906: neuper@37906: fun idt str 0 = " " neuper@37906: | idt str n = str ^ idt str (n-1); neuper@37906: (*fun indt 0 = "" neuper@37906: | indt n = " " ^ indt (n-1);---------does not terminate with negatives*) neuper@37906: fun indt n = if n <= 0 then "" else " " ^ indt (n-1); neuper@37906: fun indent 0 = "" neuper@37906: | indent n = ". " ^ indent(n-1); neuper@37906: neuper@37906: fun dashs i = if 0 neuper@38022: (TextIO.output (stream, (strip_specials s)); neuper@38022: TextIO.output (stream, "\n"); neuper@38022: TextIO.flushOut stream)); neuper@38022: fun redirect_tracing path = redir (TextIO.openOut path);