(* use"library.sml";

   WN.22.10.99

   for both, math-engine and isa-98-1-HOL-plus

   however, functions closely related to original isabelle-98-1 functions

            are in isa-98-1-HOL-plus/rewrite-parse/library_G

*)

(* Isabelle2002 -> Isabelle2009 library changed:

signature LIBRARY =

sig

  include BASIC_LIBRARY

  val foldl: ('a * 'b -> 'a) -> 'a * 'b list -> 'a

  val foldr: ('a * 'b -> 'b) -> 'a list * 'b -> 'b

  val foldl_map: ('a * 'b -> 'a * 'c) -> 'a * 'b list -> 'a * 'c list

  val take: int * 'a list -> 'a list

  val drop: int * 'a list -> 'a list

  val last_elem: 'a list -> 'a

end;

FIXME: overwritten again...*)

fun foldl (f: 'a * 'b -> 'a) : 'a * 'b list -> 'a = (*FIXME.2009*)

  let fun itl (e, [])  = e

        | itl (e, a::l) = itl (f(e, a), l)

  in  itl end;

fun foldr f (l, e) = (*FIXME.2009*)

  let fun itr [] = e

        | itr (a::l) = f(a, itr l)

  in  itr l  end;

fun take (n, []) = [] (*FIXME.2009*)

  | take (n, x :: xs) =

      if n > 0 then x :: take (n - 1, xs) else [];

fun drop (n, []) = [] (*FIXME.2009*)

  | drop (n, x :: xs) =

      if n > 0 then drop (n - 1, xs) else x :: xs;

(*exn LIST has disappeared in 2009 ... replaced by error...*)

fun last_elem [] = error "last_elem" (*FIXME.2009*)

  | last_elem [x] = x

  | last_elem (_ :: xs) = last_elem xs;

fun gen_mem eq (x, []) = false (*FIXME.2009*)

  | gen_mem eq (x, y :: ys) = eq (x, y) orelse gen_mem eq (x, ys);

fun gen_insert (les : 'a * 'a -> bool) ([], a) = [a]

  | gen_insert les (x::xs, a) = if les (x, a) then x::(gen_insert les (xs, a)) 

			    else a::x::xs;

fun gen_sort les xs = foldl (gen_insert les) (xs, []);

fun gen_distinct eq lst =

  let

    val memb = gen_mem eq;

    fun dist (rev_seen, []) = rev rev_seen

      | dist (rev_seen, x :: xs) =

          if memb (x, rev_seen) then dist (rev_seen, xs)

          else dist (x :: rev_seen, xs);

  in

    dist ([], lst)

  end;

fun gen_rems eq (xs, ys) = filter_out (fn x => gen_mem eq (x, ys)) xs;

fun distinct l = gen_distinct (op =) l;

(*.see 'fun (y :: ys) \ x' in Pure/library.ML.*)

fun gen_dif eq (y :: ys, x) = if eq (y, x) then ys 

			      else y :: (gen_dif eq (ys, x))

  | gen_dif eq ([], x) = [];

(* val (eq, (y :: ys, x)) = ();*)

(*.see 'fun ys \\ xs' in Pure/library.ML.*)

fun gen_diff eq (ys, xs) = foldl (gen_dif eq) (ys,xs);

(* val (eq, (ys, xs)) = (eq_thmI, (isacrlsthms, isacthms));

 *)

(* gen_diff op= ([1,2,3,4,5,6,7],[2,3,5]);

val it = [1, 4, 6, 7] : int list*)

(*an indulgent version of Isabelle/src/Pure/library.ML ~~*)

infix ~~~;

fun xs ~~~ ys =

    let fun aaa xys []        []        = xys

	  | aaa xys []        (y :: ys) = xys

	  | aaa xys (x :: xs) []        = xys

	  | aaa xys (x :: xs) (y :: ys) = aaa (xys @ [(x, y)]) xs ys

    in aaa [] xs ys end;

(*[1,2,3] ~~~ ["1","2","3"];

val it = [(1, "1"), (2, "2"), (3, "3")] : (int * string) list

> [1,2] ~~~ ["1","2","3"];

val it = [(1, "1"), (2, "2")] : (int * string) list

> [1,2,3] ~~~ ["1","2"];

val it = [(1, "1"), (2, "2")] : (int * string) list*)

(*from Isabelle2002/src/Pure/library.ML; has changed in 2009 FIXME replace*)

fun gen_ins eq (x, xs) = if gen_mem eq (x, xs) then xs else x :: xs;

fun gen_insI eq pr (x, xs) = 

    if gen_mem eq (x, xs) 

    then (tracing ("### occurs twice: "^(pr x)); xs) 

    else x :: xs;

fun gen_union eq pr (xs, []) = xs

  | gen_union eq pr ([], ys) = ys

  | gen_union eq pr (x :: xs, ys) = gen_union eq pr (xs, gen_ins eq (x, ys));

fun cons2 (f,g) x = (f x, g x); (*PL softwareparadigmen*)

fun nth _ []      = error "nth _ []"

  | nth 1 (x::_) = x

  | nth n (_::xs) = nth (n-1) xs;

(*WN050106 quick for test: doesn't check for exns*)

fun drop_nth ls (_, []) = ls

  | drop_nth ls (n, x :: xs) = 

      if n = 1 

      then ls @ xs

      else drop_nth (ls @ [x]) (n - 1, xs);

(*> drop_nth [] (3,[1,2,3,4,5]); 

val it = [1, 2, 4, 5] : int list

 > drop_nth [] (1,[1,2,3,4,5]); 

val it = [2, 3, 4, 5] : int list

 > drop_nth [] (5,[1,2,3,4,5]); 

val it = [1, 2, 3, 4] : int list *)

fun and_ (b1,b2) = b1 andalso b2;(* ~/Design.98/ModelSpec.sml/library_G.sml *) 

fun or_ (b1,b2) = b1 orelse b2;

fun takerest (i, ls) = (rev o take) (length ls - i, rev ls);

(*> takerest (3, ["normalize","polynomial","univariate","equation"]);

val it = ["equation"] : string list

*)

fun takelast (i, ls) = (rev o take) (i, rev ls);

(* > takelast (2, ["normalize","polynomial","univariate","equation"]);

val it = ["univariate", "equation"] : pblID

> takelast (2, ["equation"]);

val it = ["equation"] : pblID

> takelast (3, ["normalize","polynomial","univariate","equation"]);

val it = ["polynomial", "univariate", "equation"]*)

fun split_nlast (i, ls) =

    let val rv = rev ls

    in (rev (takelast (i - 1, rv)), rev (take (i, rv))) end;

fun split_nlast (i, ls) = (take (length ls - i, ls), rev (take (i, rev ls)));

(* val (a, b) = split_nlast (3, ["a","b","[",".","]"]);

val a = ["a", "b"] : string list

val b = ["[", ".", "]"] : string list

>  val (a, b) = split_nlast (3, [".","]"]);

val a = [] : string list

val b = [".", "]"] : string list   *)

(*.analoguous to dropwhile in Pure/libarary.ML.*)

fun dropwhile P [] = []

  | dropwhile P (ys as x::xs) = if P x then dropwhile P xs else ys;

fun takewhile col P [] = col

  | takewhile col P (ys as x::xs) = if P x then takewhile (col @ [x]) P xs

				     else col;

(* > takewhile [] (not o (curry op= 4)) [1,2,3,4,5,6,7];

   val it = [1, 2, 3] : int list*)

fun dropuntil P [] = []

  | dropuntil P (ys as x::xs) = if P x then ys else dropuntil P xs;

fun pair2tri ((a,b),c) = (a,b,c);

fun fst3 (a,_,_) = a;

fun snd3 (_,b,_) = b;

fun thd3 (_,_,c) = c;

fun skip_blanks strl = 

  let 

    fun skip strl []        = strl

      | skip strl (" "::ss) = skip strl ss

      | skip strl ( s ::ss) = skip (strl @ [s]) ss

  in skip [] strl end;

fun de_quote str =

  let fun scan ss' [] = ss'

	| scan ss' ("\""::ss) = scan ss' ss

	| scan ss' (s::ss) = scan (ss' @ [s]) ss;

  in (implode o (scan []) o explode) str end;

(*> de_quote "\"d_d ?bdv (?u + ?v) = d_d ?bdv ?u + d_d ?bdv ?v\"";

val it = "d_d ?bdv (?u + ?v) = d_d ?bdv ?u + d_d ?bdv ?v" : string*)

(* conversions to (quoted) strings 

   FIXME: rename *2str --> *2strq (quoted elems) 

             now *2str' (elems NOT quoted) instead of *2str *)

val commas = space_implode ",";

fun strs2str strl = "[" ^ (commas (map quote strl)) ^ "]";

(*> val str = strs2str ["123","asd"]; tracing str;

val it = "[\"123\", \"asd\"]" : string

"123", "asd"] *)

fun strs2str' strl = "[" ^ (commas strl) ^ "]";

fun list2str strl = "[" ^ (commas strl) ^ "]";

(*> val str = list2str ["123","asd"]; tracing str;

val str = "[123, asd]" : string

[123, asd] *)

fun spair2str (s1,s2) =   "(" ^ (quote s1) ^ ", " ^ (quote s2) ^ ")";

fun pair2str (s1,s2) =   "(" ^ s1 ^ ", " ^ s2 ^ ")";

(*16.11.00

fun subs2str (subs:(string * string) list) = 

  (list2str o (map pair2str)) subs;*)

fun subs2str (subs: string list) = list2str  subs;

(*> val sss = ["(bdv,x)","(err,#0)"];

> subs2str sss;

val it = "[(bdv,x),(err,#0)]" : string*)

fun subs2str' (subs:(string * string) list) = (*12.12.99???*)

  (list2str o (map pair2str)) subs;

(*> val subs = subs2str [("bdv","x")]; tracing subs;

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

[("bdv", "x")] *)

fun con2str land_lor = quote " &| ";

val int2str = string_of_int;

fun ints2str ints = (strs2str o (map string_of_int)) ints;

fun ints2str' ints = (strs2str' o (map string_of_int)) ints;

(* use"library.sml";

   *)

(*needed in Isa + ME*)

fun get_thy str = 

  let fun get strl []        = strl

	| get strl ("."::ss) = strl

	| get strl ( s ::ss) = get (strl @ [s]) ss

  in implode( get [] (explode str)) end;

fun strip_thy str =

  let fun strip bdVar []        = implode (rev bdVar)

	| strip bdVar ("."::_ ) = implode (rev bdVar)

	| strip bdVar (c  ::cs) = strip (bdVar @[c]) cs

  in strip [] (rev(explode str)) end;

fun id_of (Var ((id,ix),_)) = if ix=0 then id else id^(string_of_int ix)

  | id_of (Free (id    ,_)) = id

  | id_of (Const(id    ,_)) = id

  | id_of _                 = ""; (* never such an identifier *)

fun ids_of t =

  let fun con ss (Const (s,_)) = s::ss

	| con ss (Free (s,_)) = s::ss

	| con ss (Abs (s,_,b)) = s::(con ss b)

	| con ss (t1 $ t2) = (con ss t1) @ (con ss t2)

	| con ss _ = ss

  in map strip_thy ((distinct o (con [])) t) end;

(*

> val t = (term_of o the o (parse thy))

  "solve_univar (R, [univar, equation], no_met) (a = b + #1) a";

> ids_of t;

["solve'_univar","Pair","R","Cons","univar","equation","Nil",...]*)

(*FIXME.WN090819 fun overwrite missing in ..2009/../library.ML*)

fun overwrite (al, p as (key, _)) =               (*FIXME.2009*)

  let fun over ((q as (keyi, _)) :: pairs) =

            if keyi = key then p :: pairs else q :: (over pairs)

        | over [] = [p]

  in over al end;

fun overwritel (al, []) = al

  | overwritel (al, b::bl) = overwritel (overwrite (al, b), bl);

(*> val aaa = [(1,11),(2,22),(3,33)];

> overwritel (aaa, [(2,2222),(4,4444)]);

val it = [(1,11),(2,2222),(3,33),(4,4444)] : (int * int) list*)

local

fun intsto1 0 = []

  | intsto1 n = (intsto1 (n-1)) @ [n]

in

fun intsto n  = if n < 0 then (error "intsto < 0") else intsto1 n

end;

type 'a stack = 'a list;

fun top ((x::xs):'a stack) = x

  | top _ = error "top called for empty list";

fun pop ((x::xs):'a stack) = xs:'a stack

  | pop _ = error "pop called for empty list";

fun push x (xs:'a stack) = x::xs:'a stack;

fun drop_last l = ((rev o tl o rev) l);

fun drop_last_n n l = rev (takerest (n, rev l));

(*> drop_last_n 2 [1,2,3,4,5];

val it = [1, 2, 3] : int list

> drop_last_n 3 [1,2,3,4,5];

val it = [1, 2] : int list

> drop_last_n 7 [1,2,3,4,5];

val it = [] : int list

*)

fun bool2str true = "true"

  | bool2str false = "false";

(*.take elements from b to e including both.*)

fun take_fromto from to l = 

    if from > to then error ("take_fromto from="^string_of_int from^

				  " > to="^string_of_int to)

    else drop (from - 1, take (to, l));

(*> take_fromto 3 5 [1,2,3,4,5,6,7];

val it = [3,4,5] : int list 

> take_fromto 3 3  [1,2,3,4,5,6,7];

val it = [3] : int list*)

fun idt str 0 = " "

  | idt str n = str ^ idt str (n-1);

(*fun indt 0 = ""

  | indt n = " " ^ indt (n-1);---------does not terminate with negatives*)

fun indt n = if n <= 0 then "" else " " ^ indt (n-1);

fun indent 0 = ""

  | indent n = ". " ^ indent(n-1);

fun dashs i = if 0<i then "-"^ dashs (i-1) else "";

fun dots i = if 0<i then "."^ dots (i-1) else "";

fun assoc ([], key) = NONE(*cp 2002 Pure/library.ML FIXXXME take AList.lookup*)

  | assoc ((keyi, xi) :: pairs, key) =

      if key = keyi then SOME xi else assoc (pairs, key);

(*association list lookup, optimized version for strings*)

fun assoc_string ([], (key:string)) = NONE

  | assoc_string ((keyi, xi) :: pairs, key) =

      if key = keyi then SOME xi else assoc_string (pairs, key);

fun if_none NONE y = y (*cp from 2002 Pure/library.ML FIXXXME replace*)

  | if_none (SOME x) _ = x;

(* redirect tracing, following The Isabelle Cookbook *)

(* TODO: how redirect tracing to emacs buffer again ? *)

val strip_specials =

    let

        fun strip ("\^A" :: _ :: cs) = strip cs

          | strip (c :: cs) = c :: strip cs

          | strip [] = [];

    in

        implode o strip o explode

    end

fun redir stream =

    Output.tracing_fn := (fn s =>

                             (TextIO.output (stream, (strip_specials s));

                              TextIO.output (stream, "\n");

                              TextIO.flushOut stream));

fun redirect_tracing path = redir (TextIO.openOut path);