diff -r 81d6dc597559 -r 5181e317e9ff src/Pure/IsaPlanner/isaplib.ML --- a/src/Pure/IsaPlanner/isaplib.ML Sun Jun 11 00:28:18 2006 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,317 +0,0 @@ -(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) -(* Title: Pure/IsaPlanner/isaplib.ML - ID: $Id$ - Author: Lucas Dixon, University of Edinburgh - lucasd@dai.ed.ac.uk -*) -(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) -(* DESCRIPTION: - - A few useful system-independent utilities. -*) -(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) -signature ISAP_LIB = -sig - (* seq operations *) - val ALL_BUT_LAST : ('a -> 'b Seq.seq) -> 'a -> 'b Seq.seq - val FST : ('a -> 'b Seq.seq) -> 'a -> 'b Seq.seq - val NTH : int -> ('a -> 'b Seq.seq) -> 'a -> 'b Seq.seq - val all_but_last_of_seq : 'a Seq.seq -> 'a Seq.seq - val nat_seq : int Seq.seq - val nth_of_seq : int -> 'a Seq.seq -> 'a option - val pair_seq : 'a Seq.seq -> 'b Seq.seq -> ('a * 'b) Seq.seq - val number_seq : 'a Seq.seq -> (int * 'a) Seq.seq - - datatype 'a skipseqT = - skipmore of int - | skipseq of 'a Seq.seq Seq.seq; - val skipto_seqseq : int -> 'a Seq.seq Seq.seq -> 'a skipseqT - val seqflat_seq : 'a Seq.seq Seq.seq -> 'a Seq.seq - - (* lists *) - val mk_num_list : int -> int list - val number_list : int -> 'a list -> (int * 'a) list - val repeated_list : int -> 'a -> 'a list - val all_pairs : 'a list -> 'b list -> ('a * 'b) list - val get_ends_of : ('a * 'a -> bool) -> - ('a * 'a) -> 'a list -> ('a * 'a) - val flatmap : ('a -> 'b list) -> 'a list -> 'b list - - val lrem : ('a * 'b -> bool) -> 'a list -> 'b list -> 'b list - val forall_list : ('a -> bool) -> 'a list -> bool - - (* the list of lists with one of each of the original sublists *) - val one_of_each : 'a list list -> 'a list list - - (* type changing *) - exception NOT_A_DIGIT of string - val int_of_string : string -> int - - (* string manipulations *) - val remove_end_spaces : string -> string - val str_indent : string -> string - val string_of_intlist : int list -> string - val string_of_list : ('a -> string) -> 'a list -> string - - (* options *) - val aptosome : 'a option -> ('a -> 'b) -> 'b option - val seq_mapfilter : ('a -> 'b option) -> 'a Seq.seq -> 'b Seq.seq - val seq_map_to_some_filter : ('a -> 'b) -> 'a option Seq.seq - -> 'b Seq.seq -end; - - - -structure IsaPLib : ISAP_LIB = -struct - -(* Seq *) -fun seq_map_to_some_filter f = Seq.map_filter (Option.map f); -fun seq_mapfilter f = Seq.map_filter f; - -(* the sequence of natural numbers *) -val nat_seq = - let fun nseq i () = SOME (i, Seq.make (nseq (i+1))) - in Seq.make (nseq 1) - end; - -(* a simple function to pair with each element of a list, a number *) -fun number_list i [] = [] - | number_list i (h::t) = - (i,h)::(number_list (i+1) t) - -(* create a sequence of pairs of the elements of the two sequences - If one sequence becomes empty, then so does the pairing of them. - - This is particularly useful if you wish to perform counting or - other repeated operations on a sequence and you want to combvine - this infinite sequence with a possibly finite one. - - behaviour: - s1: a1, a2, ... an - s2: b1, b2, ... bn ... - - pair_seq s1 s2: (a1,b1), (a2,b2), ... (an,bn) -*) -fun pair_seq seq1 seq2 = - let - fun pseq s1 s2 () = - case Seq.pull s1 of - NONE => NONE - | SOME (s1h, s1t) => - case Seq.pull s2 of - NONE => NONE - | SOME (s2h, s2t) => - SOME ((s1h, s2h), Seq.make (pseq s1t s2t)) - in - Seq.make (pseq seq1 seq2) - end; - -(* number a sequence *) -fun number_seq s = pair_seq nat_seq s; - -(* cuts off the last element of a sequence *) -fun all_but_last_of_seq s = - let - fun f () = - case Seq.pull s of - NONE => NONE - | SOME (a, s2) => - (case Seq.pull s2 of - NONE => NONE - | SOME (a2,s3) => - SOME (a, all_but_last_of_seq (Seq.cons a2 s3))) - in - Seq.make f - end; - - fun ALL_BUT_LAST r st = all_but_last_of_seq (r st); - - - (* nth elem for sequenes, return none if out of bounds *) - fun nth_of_seq i l = - (case Seq.pull l of - NONE => NONE - | SOME (x, xq) => - if i <= 1 then SOME x - else nth_of_seq (i - 1) xq); - - (* for use with tactics... gives no_tac if element isn't there *) - fun NTH n f st = - (case nth_of_seq n (f st) of - NONE => Seq.empty - | SOME r => Seq.single r); - - (* First result of a tactic... uses NTH, so if there is no elements, - - then no_tac is returned. *) - fun FST f = NTH 1 f; - -datatype 'a skipseqT = skipmore of int - | skipseq of 'a Seq.seq Seq.seq; -(* given a seqseq, skip the first m non-empty seq's *) -fun skipto_seqseq m s = - let - fun skip_occs n sq = - case Seq.pull sq of - NONE => skipmore n - | SOME (h,t) => - (case Seq.pull h of NONE => skip_occs n t - | SOME _ => if n <= 1 then skipseq (Seq.cons h t) - else skip_occs (n - 1) t) - in (skip_occs m s) end; - -(* handy function for re-arranging Sequence operations *) -(* [[a,b,c],[d,e],...] => flatten [[a,d,...], [b,e,...], [c, ...]] *) -fun seqflat_seq ss = - let - fun pulltl LL () = - (case Seq.pull LL of - NONE => NONE - | SOME (hL,tLL) => - (case Seq.pull hL of - NONE => pulltl tLL () - | SOME (h,tL) => - SOME (h, Seq.make (recf (tLL, (Seq.single tL)))))) - and recf (fstLL,sndLL) () = - (case Seq.pull fstLL of - NONE => pulltl sndLL () - | SOME (hL, tLL) => - (case Seq.pull hL of - NONE => recf (tLL, sndLL) () - | SOME (h,tL) => - SOME (h, Seq.make (recf (tLL, Seq.append (sndLL, Seq.single tL)))))) - in Seq.make (pulltl ss) end; -(* tested with: -val ss = Seq.of_list [Seq.of_list [1,2,3], Seq.of_list [4,5], Seq.of_list [7,8,9,10]]; -Seq.list_of (seqflat_seq ss); -val it = [1, 4, 7, 2, 5, 8, 3, 9, 10] : int list -*) - - - - (* create a list opf the form (n, n-1, n-2, ... ) *) - fun mk_num_list n = - if n < 1 then [] else (n :: (mk_num_list (n-1))); - - fun repeated_list n a = - if n < 1 then [] else (a :: (repeated_list (n-1) a)); - - (* create all possible pairs with fst element from the first list - and snd element from teh second list *) - fun all_pairs xs ys = - let - fun all_pairs_aux yss [] _ acc = acc - | all_pairs_aux yss (x::xs) [] acc = - all_pairs_aux yss xs yss acc - | all_pairs_aux yss (xs as (x1::x1s)) (y::ys) acc = - all_pairs_aux yss xs ys ((x1,y)::acc) - in - all_pairs_aux ys xs ys [] - end; - - - (* create all possible pairs with fst element from the first list - and snd element from teh second list *) - (* FIXME: make tail recursive and quick *) - fun one_of_each [] = [] - | one_of_each [[]] = [] - | one_of_each [(h::t)] = [h] :: (one_of_each [t]) - | one_of_each ([] :: xs) = [] - | one_of_each ((h :: t) :: xs) = - (map (fn z => h :: z) (one_of_each xs)) - @ (one_of_each (t :: xs)); - - -(* function to get the upper/lower bounds of a list -given: -gr : 'a * 'a -> bool = greater than check -e as (u,l) : ('a * 'a) = upper and lower bits -l : 'a list = the list to get the upper and lower bounds of -returns a pair ('a * 'a) of the biggest and lowest value w.r.t "gr" -*) -fun get_ends_of gr (e as (u,l)) [] = e - | get_ends_of gr (e as (u,l)) (h :: t) = - if gr(h,u) then get_ends_of gr (h,l) t - else if gr(l,h) then get_ends_of gr (u,h) t - else get_ends_of gr (u,l) t; - -fun flatmap f = maps f; - - (* quick removal of "rs" elements from "ls" when (eqf (r,l)) is true - Ignores ordering. *) - fun lrem eqf rs ls = - let fun list_remove rs ([],[]) = [] - | list_remove [] (xs,_) = xs - | list_remove (r::rs) ([],leftovers) = - list_remove rs (leftovers,[]) - | list_remove (r1::rs) ((x::xs),leftovers) = - if eqf (r1, x) then list_remove (r1::rs) (xs,leftovers) - else list_remove (r1::rs) (xs, x::leftovers) - in - list_remove rs (ls,[]) - end; - -fun forall_list f [] = true - | forall_list f (a::t) = f a orelse forall_list f t; - - - (* crappy string indeter *) - fun str_indent s = - implode (map (fn s => if s = "\n" then "\n " else s) (explode s)); - - - fun remove_end_spaces s = - let - fun rem_starts [] = [] - | rem_starts (" " :: t) = rem_starts t - | rem_starts ("\t" :: t) = rem_starts t - | rem_starts ("\n" :: t) = rem_starts t - | rem_starts l = l - fun rem_ends l = rev (rem_starts (rev l)) - in - implode (rem_ends (rem_starts (explode s))) - end; - -(* convert a string to an integer *) - exception NOT_A_DIGIT of string; - - fun int_of_string s = - let - fun digits_to_int [] x = x - | digits_to_int (h :: t) x = digits_to_int t (x * 10 + h); - - fun char_to_digit c = - case c of - "0" => 0 - | "1" => 1 - | "2" => 2 - | "3" => 3 - | "4" => 4 - | "5" => 5 - | "6" => 6 - | "7" => 7 - | "8" => 8 - | "9" => 9 - | _ => raise NOT_A_DIGIT c - in - digits_to_int (map char_to_digit (explode (remove_end_spaces s))) 0 - end; - - (* Debugging/printing code for this datatype *) - fun string_of_list f l = - let - fun auxf [] = "" - | auxf [a] = (f a) - | auxf (h :: (t as (h2 :: t2))) = (f h) ^ ", " ^ (auxf t) - in - "[" ^ (auxf l) ^ "]" - end; - - val string_of_intlist = string_of_list string_of_int; - - - (* options *) - fun aptosome opt f = Option.map f opt; - -end;