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