TFL/utils.sml
author paulson
Mon, 26 May 1997 12:27:58 +0200
changeset 3330 ab7161e593c8
parent 3302 404fe31fd8d2
child 3391 5e45dd3b64e9
permissions -rw-r--r--
Deleted unused functions
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
3302
404fe31fd8d2 New headers and other minor changes
paulson
parents: 3245
diff changeset
     1
(*  Title:      TFL/utils
404fe31fd8d2 New headers and other minor changes
paulson
parents: 3245
diff changeset
     2
    ID:         $Id$
404fe31fd8d2 New headers and other minor changes
paulson
parents: 3245
diff changeset
     3
    Author:     Konrad Slind, Cambridge University Computer Laboratory
404fe31fd8d2 New headers and other minor changes
paulson
parents: 3245
diff changeset
     4
    Copyright   1997  University of Cambridge
2112
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
     5
3302
404fe31fd8d2 New headers and other minor changes
paulson
parents: 3245
diff changeset
     6
Basic utilities
404fe31fd8d2 New headers and other minor changes
paulson
parents: 3245
diff changeset
     7
*)
3245
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 3191
diff changeset
     8
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 3191
diff changeset
     9
structure Utils = 
2112
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    10
struct
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    11
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    12
(* Standard exception for TFL. *)
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    13
exception ERR of {module:string,func:string, mesg:string};
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    14
fun UTILS_ERR{func,mesg} = ERR{module = "Utils",func=func,mesg=mesg};
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    15
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    16
local 
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    17
fun info_string s {module,func,mesg} =
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    18
       (s^" at "^module^"."^func^":\n"^mesg^"\n")
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    19
in
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    20
val ERR_string = info_string "Exception raised"
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    21
val MESG_string = info_string "Message"
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    22
end;
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    23
3245
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 3191
diff changeset
    24
fun Raise (e as ERR sss) = (TextIO.output(TextIO.stdOut, ERR_string sss);  
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 3191
diff changeset
    25
                            raise e)
2112
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    26
  | Raise e = raise e;
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    27
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    28
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    29
(* Simple combinators *)
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    30
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    31
fun C f x y = f y x
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    32
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    33
fun itlist f L base_value =
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    34
   let fun it [] = base_value
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    35
         | it (a::rst) = f a (it rst)
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    36
   in it L 
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    37
   end;
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    38
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    39
fun rev_itlist f =
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    40
   let fun rev_it [] base = base
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    41
         | rev_it (a::rst) base = rev_it rst (f a base)
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    42
   in rev_it
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    43
   end;
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    44
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    45
fun end_itlist f =
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    46
   let fun endit [] = raise UTILS_ERR{func="end_itlist", mesg="list too short"}
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    47
         | endit alist = 
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    48
            let val (base::ralist) = rev alist
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    49
            in itlist f (rev ralist) base
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    50
            end
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    51
   in endit
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    52
   end;
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    53
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    54
fun itlist2 f L1 L2 base_value =
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    55
 let fun it ([],[]) = base_value
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    56
       | it ((a::rst1),(b::rst2)) = f a b (it (rst1,rst2))
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    57
       | it _ = raise UTILS_ERR{func="itlist2",mesg="different length lists"}
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    58
 in  it (L1,L2)
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    59
 end;
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    60
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    61
fun mapfilter f alist = itlist (fn i=>fn L=> (f i::L) handle _ => L) alist [];
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    62
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    63
fun pluck p  =
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    64
  let fun remv ([],_) = raise UTILS_ERR{func="pluck",mesg = "item not found"}
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    65
        | remv (h::t, A) = if p h then (h, rev A @ t) else remv (t,h::A)
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    66
  in fn L => remv(L,[])
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    67
  end;
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    68
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    69
fun front_back [] = raise UTILS_ERR{func="front_back",mesg="empty list"}
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    70
  | front_back [x] = ([],x)
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    71
  | front_back (h::t) = 
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    72
       let val (L,b) = front_back t
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    73
       in (h::L,b)
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    74
       end;
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    75
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    76
fun take f =
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    77
  let fun grab(0,L) = []
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    78
        | grab(n, x::rst) = f x::grab(n-1,rst)
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    79
  in grab
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    80
  end;
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    81
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    82
fun zip3 [][][] = []
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    83
  | zip3 (x::l1) (y::l2) (z::l3) = (x,y,z)::zip3 l1 l2 l3
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    84
  | zip3 _ _ _ = raise UTILS_ERR{func="zip3",mesg="different lengths"};
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    85
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    86
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    87
fun can f x = (f x ; true) handle _ => false;
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    88
fun holds P x = P x handle _ => false;
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    89
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    90
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    91
(* Set ops *)
3245
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 3191
diff changeset
    92
nonfix mem;  (* Gag Barf Choke *)
2112
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    93
fun mem eq_func i =
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    94
   let val eqi = eq_func i
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    95
       fun mm [] = false
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    96
         | mm (a::rst) = eqi a orelse mm rst
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    97
   in mm
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    98
   end;
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    99
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   100
fun mk_set eq_func =
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   101
   let val mem = mem eq_func
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   102
       fun mk [] = []
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   103
         | mk (a::rst) = if (mem a rst) then mk rst else a::(mk rst)
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   104
   in mk
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   105
   end;
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   106
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   107
(* All the elements in the first set that are not also in the second set. *)
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   108
fun set_diff eq_func S1 S2 = filter (fn x => not (mem eq_func x S2)) S1
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   109
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   110
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   111
fun sort R = 
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   112
let fun part (m, []) = ([],[])
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   113
      | part (m, h::rst) =
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   114
         let val (l1,l2) = part (m,rst)
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   115
         in if (R h m) then (h::l1, l2)
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   116
                       else (l1,  h::l2) end
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   117
    fun qsort [] = []
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   118
      | qsort (h::rst) = 
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   119
        let val (l1,l2) = part(h,rst)
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   120
        in qsort l1@ [h] @qsort l2
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   121
        end
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   122
in qsort
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   123
end;
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   124
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   125
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   126
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   127
end; (* Utils *)