(* library extending Isabelle's library.

    Author: Walther Neuper 1999

    (c) copyright due to lincense terms

 Note: Here many functions reflect changes since Isabelle 98. Changes frequently were resolved

    quick and dirty by additing Isabelle's old version to the library below.

 TODO:

  * remove unused functions

  * review duplicates with other signatures and re-locate respectively

  * move unparsing ("*_t0_str", "*2str", etc) somewhere else in ThydataC/

  * apply Isabelle's coding standards and remove warnings

  * rename "library.sml" to "libraryC.sml" like many other files, where struct <> filename.

 *)

 infix 1 ~~~

 signature LIBRARY_C =

 sig

   val and_: bool * bool -> bool

   val cand_: bool -> bool -> bool

   val or_: bool * bool -> bool

   val cor_: bool -> bool -> bool

   val assoc: (''a * 'b) list * ''a -> 'b option

   val assoc_string: (string * 'a) list * string -> 'a option

   val bool2str: bool -> string

   val commas: string list -> string

   val dashs: int -> string

   val de_quote: string -> string

   val dots: int -> string

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

   val drop_last: 'a list -> 'a list

   val drop_last_n: int -> 'a list -> 'a list

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

   val dropuntil: ('a -> bool) -> 'a list -> 'a list

   val dropwhile: ('a -> bool) -> 'a list -> 'a list

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

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

   val fst3: 'a * 'b * 'c -> 'a

   val gen_mem: ('a * 'b -> bool) -> 'a * 'b list -> bool

   val gen_rems: ('a * 'b -> bool) -> 'a list * 'b list -> 'a list

   val if_none: 'a option -> 'a -> 'a

   val indent: int -> string

   val indt: int -> string

   val idt: string -> int -> string

   val int2str: int -> string

   val ints2str': int list -> string

   val intsto: int -> int list

   val last_elem: 'a list -> 'a

   val list2str: string list -> string

   val list_update: 'a list -> int -> 'a -> 'a list

   val maxl: int list -> int

   val member_swap: ('a * 'b -> bool) -> 'a -> 'b list -> bool

   val nos: string list -> string

   val nth: int -> 'a list -> 'a

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

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

   val pair2str: string * string -> string

   val pair2str_: string * string -> string

   val pair2tri: ('a * 'b) * 'c -> 'a * 'b * 'c

   val snd3: 'a * 'b * 'c -> 'b

   val spair2str: string * string -> string

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

   val string_to_bool: string -> bool

   val strs2str: string list -> string

   val strs2str': string list -> string

   val strs2str_: string list -> string                                 (* duplicates in Rule *)

   val strslist2strs: string list list -> string

   type subst = (term * term) list

   val take: int * 'a list -> 'a list (*conflict with Library.take: int -> 'a list -> 'a list *)

   val take_fromto: int -> int -> 'a list -> 'a list

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

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

   val takewhile: 'a list -> ('a -> bool) -> 'a list -> 'a list

   val termless: term * term -> bool

   val thd3: 'a * 'b * 'c -> 'c

   val triple2pair: 'a * 'b * 'c -> 'a * 'b

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

   val linefeed: string -> string

   val dropwhile' : ('a -> 'b -> bool) -> 'a list -> 'b list -> 'a list * 'b list

 \<^isac_test>\<open>

   val enumerate_strings: string list -> string list

   val quad2pair: 'a * 'b * 'c * 'd -> 'a * 'b

 \<close>

 (*///------------------------------>>> thy ------------------------------------------------\\\*)

     val get_thy: string -> string

     val strip_thy: string -> string

 (*\\\------------------------------>>> thy ------------------------------------------------///*)

 (*///------------------------------>>> term -----------------------------------------------\\\*)

   val subs2str: string list -> string

   val id_of: term -> string

   val ids_of: term -> string list

 (*\\\------------------------------>>> term -----------------------------------------------///*)

 end;                                                      

 (**)

 structure LibraryC(**): LIBRARY_C(**) =

 struct

 (**)

 val foldl = Library.foldl

 val foldr = Library.foldr

 fun take (n, xs) = Library.take n xs;;

 fun drop (n, xs) = Library.drop n xs;

 fun last_elem [] = raise ERROR "last_elem"

   | last_elem [x] = x

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

 fun member_swap eq x xs = member eq xs x

 fun gen_mem _ (_, []) = false

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

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

 (*fun nth n xs = Library.nth xs n; exn behaviour different*)

 fun nth _ []      = raise ERROR "nth _ []" (*Isabelle2002, still saved the hours of update*)

   | nth 1 (x :: _) = x

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

 fun list_update [] _ _ = []

   | list_update (x :: xs) i v = 

       case i of 

         0 => v :: xs

       | j => x :: list_update xs (j - 1) v

 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);

 fun and_ (b1, b2) = b1 andalso b2;

 fun cand_ b1 b2 = b1 andalso b2;

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

 fun cor_ b1 b2 = b1 orelse b2;

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

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

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

 fun dropwhile _ [] = []

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

 fun takewhile col _ [] = col

   | takewhile col P (x::xs) =

     if P x then takewhile (col @ [x]) P xs else col;

 fun dropuntil _ [] = []

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

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

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

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

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

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

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

 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 Symbol.explode) str end;

 val commas = Library.space_implode ", ";

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

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

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

 val nos = space_implode "#";

 fun strs2str_ strl = "#" ^ (nos strl) ^ "#";

 fun strslist2strs strslist = map strs2str strslist |> strs2str';

 type subst = (term * term) list;

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

 fun pair2str_ (s1, s2) =   s1 ^ "#" ^ s2;

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

 val int2str = Library.string_of_int;

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

 fun overwrite (al, p as (key, _)) =

   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);

 (* TODO replace by Library.upto *)

 local

 fun intsto1 0 = []

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

 in

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

 end;

 fun bool2str true = "true"

   | bool2str false = "false";

 fun string_to_bool "true" = true

   | string_to_bool "false" = false

   | string_to_bool str = raise ERROR ("string_to_bool: arg = " ^ str)

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

 fun take_fromto from to l = 

   if from > to

   then raise ERROR ("take_fromto from=" ^ string_of_int from ^ " > to=" ^ string_of_int to)

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

 fun idt _ 0 = "@"

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

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

 fun indent i = fold (curry op ^) (replicate i ". ") ""

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

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

 fun assoc ([], _) = 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);

 (* optimized version for strings *)

 fun assoc_string ([], (_ : 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;

 fun triple2pair (a, b, _) = (a, b);

 \<^isac_test>\<open>

 fun quad2pair (a, b, _, _) = (a, b);

 \<close>

 (* append a counter to a string list *)

 \<^isac_test>\<open>

 fun enumerate_strings strs =

   let fun enum _ [] = []

         | enum i (s :: ss) = (s ^ "--" ^ string_of_int i) :: (enum (i + 1) ss)

   in enum 1 strs end

 \<close>

 fun maxl [] = raise ERROR "maxl of []"

   | maxl (y :: ys) =

     let

       fun mx x [] = x

         | mx x (y :: ys) = if x < (y: int) then mx y ys else mx x ys

   in mx y ys end

 fun xs ~~~ ys =

     let fun aaa xys []        [] = xys

 	  | aaa xys []        (_ :: _) = xys

 	  | aaa xys (_ :: _) []        = xys

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

     in aaa [] xs ys end;

 (*///------------------------------>>> thy ------------------------------------------------\\\*)

 fun get_thy str = 

   let

     fun get strl [] = strl

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

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

   in implode (get [] (Symbol.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 (Symbol.explode str)) end;

 (*\\\------------------------------>>> thy ------------------------------------------------///*)

 (*///------------------------------>>>  term ----------------------------------------------\\\*)

 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 op =) o (con [])) t) end;

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

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

 > subs2str sss;

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

 (*\\\------------------------------>>>  term ----------------------------------------------///*)

 fun termless tu = (Term_Ord.term_ord tu = LESS);

 val linefeed = curry op ^ "\n"; (* ?\<longrightarrow> libraryC ?*)

 (*the lists contain eq-al elem-pairs at the beginning;

   return first list reverted (again) - ie. in order as required subsequently*)

 fun dropwhile' equal (f1::f2::fs) (i1::i2::is) =

     if equal f1 i1 then

       if equal f2 i2 then dropwhile' equal (f2 :: fs) (i2 :: is)

       else (rev (f1 :: f2 :: fs), i1 :: i2 :: is)

     else raise ERROR "dropwhile': did not start with equal elements"

   | dropwhile' equal (f::fs) [i] =

     if equal f i then

       (rev (f::fs), [i])

     else raise ERROR "dropwhile': did not start with equal elements"

   | dropwhile' equal [f] (i::is) =

     if equal f i then

       ([f], i::is)

     else raise ERROR "dropwhile': did not start with equal elements"

   | dropwhile' _ _ _ = raise ERROR "dropwhile': uncovered case"

 end; (*struct*) open LibraryC