src/Pure/IsaPlanner/isaplib.ML
author wenzelm
Thu Jun 02 09:11:32 2005 +0200 (2005-06-02)
changeset 16179 fa7e70be26b0
parent 16004 031f56012483
child 17796 86daafee72d6
permissions -rw-r--r--
header;
     1 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) 
     2 (*  Title:      Pure/IsaPlanner/isaplib.ML
     3     ID:		$Id$
     4     Author:     Lucas Dixon, University of Edinburgh
     5                 lucasd@dai.ed.ac.uk
     6 *)
     7 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) 
     8 (*  DESCRIPTION:
     9 
    10     A few useful system-independent utilities.
    11 *)
    12 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) 
    13 signature ISAP_LIB =
    14 sig
    15   (* ints *)
    16   val max : int * int -> int
    17 
    18   (* seq operations *)
    19   val ALL_BUT_LAST : ('a -> 'b Seq.seq) -> 'a -> 'b Seq.seq
    20   val FST : ('a -> 'b Seq.seq) -> 'a -> 'b Seq.seq
    21   val NTH : int -> ('a -> 'b Seq.seq) -> 'a -> 'b Seq.seq
    22   val all_but_last_of_seq : 'a Seq.seq -> 'a Seq.seq
    23   val nat_seq : int Seq.seq
    24   val nth_of_seq : int -> 'a Seq.seq -> 'a option
    25   val pair_seq : 'a Seq.seq -> 'b Seq.seq -> ('a * 'b) Seq.seq
    26   val seq_is_empty : 'a Seq.seq -> bool
    27   val number_seq : 'a Seq.seq -> (int * 'a) Seq.seq
    28 
    29   datatype 'a skipseqT = 
    30            skipmore of int
    31          | skipseq of 'a Seq.seq Seq.seq;
    32   val skipto_seqseq : int -> 'a Seq.seq Seq.seq -> 'a skipseqT
    33   val seqflat_seq : 'a Seq.seq Seq.seq -> 'a Seq.seq 
    34 
    35   (* lists *)
    36   val mk_num_list : int -> int list
    37   val number_list : int -> 'a list -> (int * 'a) list
    38   val repeated_list : int -> 'a -> 'a list
    39   val all_pairs : 'a list -> 'b list -> ('a * 'b) list
    40 	val get_ends_of : ('a * 'a -> bool) ->
    41 										('a * 'a) -> 'a list -> ('a * 'a)
    42   val flatmap : ('a -> 'b list) -> 'a list -> 'b list
    43 
    44 	val lrem : ('a * 'b -> bool) -> 'a list -> 'b list -> 'b list
    45   val forall_list : ('a -> bool) -> 'a list -> bool
    46 
    47   (* the list of lists with one of each of the original sublists *)
    48   val one_of_each : 'a list list -> 'a list list
    49 
    50   (* type changing *)
    51   exception NOT_A_DIGIT of string
    52   val int_of_string : string -> int
    53 
    54   (* string manipulations *)
    55   val remove_end_spaces : string -> string
    56   val str_indent : string -> string
    57   val string_of_intlist : int list -> string
    58   val string_of_list : ('a -> string) -> 'a list -> string
    59 
    60   (* options *)
    61   val aptosome : 'a option -> ('a -> 'b) -> 'b option
    62   val seq_mapfilter : ('a -> 'b option) -> 'a Seq.seq -> 'b Seq.seq
    63   val seq_map_to_some_filter : ('a -> 'b) -> 'a option Seq.seq 
    64                                -> 'b Seq.seq
    65 end;
    66 
    67 
    68 
    69 structure IsaPLib :> ISAP_LIB = 
    70 struct
    71  
    72 (* Int *)
    73 fun max (x,y) = if x > y then x else y;
    74 
    75 (* Seq *)
    76 fun seq_map_to_some_filter f s0 =
    77     let 
    78       fun recf s () = 
    79           case (Seq.pull s) of 
    80             NONE => NONE
    81           | SOME (NONE,s') => recf s' ()
    82           | SOME (SOME d, s') => 
    83             SOME (f d, Seq.make (recf s'))
    84     in Seq.make (recf s0) end;
    85 
    86 fun seq_mapfilter f s0 =
    87     let 
    88       fun recf s () = 
    89           case (Seq.pull s) of 
    90             NONE => NONE
    91           | SOME (a,s') => 
    92             (case f a of NONE => recf s' ()
    93                        | SOME b => SOME (b, Seq.make (recf s')))
    94     in Seq.make (recf s0) end;
    95 
    96 
    97 
    98 (* a simple function to pair with each element of a list, a number *)
    99 fun number_list i [] = []
   100 	| number_list i (h::t) = 
   101 		(i,h)::(number_list (i+1) t)
   102 
   103 (* check to see if a sequence is empty *)
   104 fun seq_is_empty s = is_none (Seq.pull s);
   105 
   106 (* the sequence of natural numbers *)
   107 val nat_seq = 
   108       let fun nseq i () = SOME (i, Seq.make (nseq (i+1)))
   109       in Seq.make (nseq 1)
   110       end;
   111 
   112 (* create a sequence of pairs of the elements of the two sequences
   113    If one sequence becomes empty, then so does the pairing of them. 
   114    
   115    This is particularly useful if you wish to perform counting or
   116    other repeated operations on a sequence and you want to combvine
   117    this infinite sequence with a possibly finite one.
   118 
   119    behaviour: 
   120    s1: a1, a2, ... an
   121    s2: b1, b2, ... bn ...
   122 
   123    pair_seq s1 s2: (a1,b1), (a2,b2), ... (an,bn)
   124 *)
   125 fun pair_seq seq1 seq2 = 
   126     let
   127       fun pseq s1 s2 () = 
   128 	        case Seq.pull s1 of 
   129 	          NONE => NONE
   130 	        | SOME (s1h, s1t) => 
   131 	          case Seq.pull s2 of 
   132 		          NONE => NONE
   133 	          | SOME (s2h, s2t) =>
   134 		          SOME ((s1h, s2h), Seq.make (pseq s1t s2t))
   135     in
   136       Seq.make (pseq seq1 seq2)
   137     end;
   138 
   139 (* number a sequence *)
   140 fun number_seq s = pair_seq nat_seq s;
   141 
   142 (* cuts off the last element of a sequence *)
   143 fun all_but_last_of_seq s = 
   144     let 
   145       fun f () = 
   146 	  case Seq.pull s of
   147 	    NONE => NONE
   148 	  | SOME (a, s2) => 
   149 	    (case Seq.pull s2 of 
   150 	       NONE => NONE
   151 	     | SOME (a2,s3) => 
   152 	       SOME (a, all_but_last_of_seq (Seq.cons (a2,s3))))
   153     in
   154       Seq.make f
   155     end;
   156 
   157  fun ALL_BUT_LAST r st = all_but_last_of_seq (r st);
   158 
   159 
   160   (* nth elem for sequenes, return none if out of bounds *)
   161   fun nth_of_seq i l = 
   162            if (seq_is_empty l) then NONE 
   163            else if i <= 1 then SOME (Seq.hd l)
   164            else nth_of_seq (i-1) (Seq.tl l);
   165 
   166   (* for use with tactics... gives no_tac if element isn't there *)
   167   fun NTH n f st = 
   168       let val r = nth_of_seq n (f st) in 
   169         if (is_none r) then Seq.empty else (Seq.single (valOf r))
   170       end;
   171  
   172   (* First result of a tactic... uses NTH, so if there is no elements,
   173 
   174      then no_tac is returned. *)
   175   fun FST f = NTH 1 f;
   176 
   177 datatype 'a skipseqT = skipmore of int
   178   | skipseq of 'a Seq.seq Seq.seq;
   179 (* given a seqseq, skip the first m non-empty seq's *)
   180 fun skipto_seqseq m s = 
   181     let 
   182       fun skip_occs n sq = 
   183           case Seq.pull sq of 
   184             NONE => skipmore n
   185           | SOME (h,t) => 
   186             (case Seq.pull h of NONE => skip_occs n t
   187              | SOME _ => if n <= 1 then skipseq (Seq.cons (h, t))
   188                          else skip_occs (n - 1) t)
   189     in (skip_occs m s) end;
   190 
   191 (* handy function for re-arranging Sequence operations *)
   192 (* [[a,b,c],[d,e],...] => flatten [[a,d,...], [b,e,...], [c, ...]] *)
   193 fun seqflat_seq ss = 
   194     let 
   195       fun pulltl LL () = 
   196           (case Seq.pull LL of 
   197              NONE => NONE
   198            | SOME (hL,tLL) => 
   199              (case Seq.pull hL of 
   200                 NONE => pulltl tLL ()
   201               | SOME (h,tL) => 
   202                 SOME (h, Seq.make (recf (tLL, (Seq.single tL))))))
   203       and recf (fstLL,sndLL) () = 
   204           (case Seq.pull fstLL of 
   205              NONE => pulltl sndLL ()
   206            | SOME (hL, tLL) => 
   207              (case Seq.pull hL of 
   208                 NONE => recf (tLL, sndLL) ()
   209               | SOME (h,tL) => 
   210                 SOME (h, Seq.make (recf (tLL, Seq.append (sndLL, Seq.single tL))))))
   211     in Seq.make (pulltl ss) end;
   212 (* tested with: 
   213 val ss = Seq.of_list [Seq.of_list [1,2,3], Seq.of_list [4,5], Seq.of_list [7,8,9,10]];
   214 Seq.list_of (seqflat_seq ss);
   215 val it = [1, 4, 7, 2, 5, 8, 3, 9, 10] : int list
   216 *)
   217 
   218 
   219 
   220   (* create a list opf the form (n, n-1, n-2, ... ) *)
   221   fun mk_num_list n =  
   222       if n < 1 then [] else (n :: (mk_num_list (n-1))); 
   223 
   224   fun repeated_list n a =  
   225       if n < 1 then [] else (a :: (repeated_list (n-1) a)); 
   226 
   227   (* create all possible pairs with fst element from the first list
   228      and snd element from teh second list *)
   229   fun all_pairs xs ys = 
   230       let 
   231         fun all_pairs_aux yss [] _ acc = acc
   232           | all_pairs_aux yss (x::xs) [] acc = 
   233             all_pairs_aux yss xs yss acc
   234           | all_pairs_aux yss (xs as (x1::x1s)) (y::ys) acc = 
   235                                all_pairs_aux yss xs ys ((x1,y)::acc)
   236       in
   237         all_pairs_aux ys xs ys []
   238       end;
   239 
   240 
   241   (* create all possible pairs with fst element from the first list
   242      and snd element from teh second list *)
   243   (* FIXME: make tail recursive and quick *)
   244   fun one_of_each [] = []
   245     | one_of_each [[]] = []
   246     | one_of_each [(h::t)] = [h] :: (one_of_each [t])
   247     | one_of_each ([] :: xs) = []
   248     | one_of_each ((h :: t) :: xs) = 
   249       (map (fn z => h :: z) (one_of_each xs)) 
   250       @ (one_of_each (t :: xs));
   251 
   252 
   253 (* function to get the upper/lower bounds of a list 
   254 given: 
   255 gr : 'a * 'a -> bool  = greater than check
   256 e as (u,l) : ('a * 'a) = upper and lower bits
   257 l : 'a list = the list to get the upper and lower bounds of
   258 returns a pair ('a * 'a) of the biggest and lowest value w.r.t "gr"
   259 *)
   260 fun get_ends_of gr (e as (u,l)) [] = e
   261   | get_ends_of gr (e as (u,l)) (h :: t) = 
   262     if gr(h,u) then get_ends_of gr (h,l) t
   263     else if gr(l,h) then get_ends_of gr (u,h) t
   264     else get_ends_of gr (u,l) t;
   265 
   266 fun flatmap f = List.concat o map f;
   267 
   268   (* quick removal of "rs" elements from "ls" when (eqf (r,l)) is true 
   269 		 Ignores ordering. *)
   270   fun lrem eqf rs ls = 
   271 			let fun list_remove rs ([],[]) = []
   272 						| list_remove [] (xs,_) = xs
   273 						| list_remove (r::rs) ([],leftovers) = 
   274 							list_remove rs (leftovers,[])
   275 						| list_remove (r1::rs) ((x::xs),leftovers) = 
   276 							if eqf (r1, x) then list_remove (r1::rs) (xs,leftovers)
   277 							else list_remove (r1::rs) (xs, x::leftovers)
   278 			in
   279 				list_remove rs (ls,[])
   280 			end;
   281 
   282 fun forall_list f [] = true
   283   | forall_list f (a::t) = f a orelse forall_list f t;
   284 
   285 
   286   (* crappy string indeter *)
   287   fun str_indent s = 
   288     implode (map (fn s => if s = "\n" then "\n  " else s) (explode s));
   289       
   290 
   291   fun remove_end_spaces s = 
   292       let 
   293 				fun rem_starts [] = [] 
   294 					| rem_starts (" " :: t) = rem_starts t
   295 					| rem_starts ("\t" :: t) = rem_starts t
   296 					| rem_starts ("\n" :: t) = rem_starts t
   297 					| rem_starts l = l
   298 				fun rem_ends l = rev (rem_starts (rev l))
   299       in
   300 				implode (rem_ends (rem_starts (explode s)))
   301       end;
   302 
   303 (* convert a string to an integer *)
   304   exception NOT_A_DIGIT of string;
   305 
   306   fun int_of_string s = 
   307       let 
   308 				fun digits_to_int [] x = x
   309 					| digits_to_int (h :: t) x = digits_to_int t (x * 10 + h);
   310 	
   311 				fun char_to_digit c = 
   312 						case c of 
   313 							"0" => 0
   314 						| "1" => 1
   315 						| "2" => 2
   316 						| "3" => 3
   317 						| "4" => 4
   318 						| "5" => 5
   319 						| "6" => 6
   320 						| "7" => 7
   321 						| "8" => 8
   322 						| "9" => 9
   323 						| _ => raise NOT_A_DIGIT c
   324       in
   325 				digits_to_int (map char_to_digit (explode (remove_end_spaces s))) 0
   326       end;
   327 
   328   (* Debugging/printing code for this datatype *)
   329   fun string_of_list f l = 
   330       let 
   331 				fun auxf [] = ""
   332 					| auxf [a] = (f a)
   333 					| auxf (h :: (t as (h2 :: t2))) = (f h) ^ ", " ^ (auxf t)
   334       in
   335 				"[" ^ (auxf l) ^ "]"
   336       end;
   337 
   338    val string_of_intlist = string_of_list string_of_int;
   339 
   340 
   341   (* options *)
   342   fun aptosome NONE f = NONE
   343     | aptosome (SOME x) f = SOME (f x);
   344 
   345 end;