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