src/HOL/Tools/res_lib.ML
author paulson
Wed Oct 05 11:18:06 2005 +0200 (2005-10-05 ago)
changeset 17764 fde495b9e24b
parent 17525 ae5bb6001afb
child 17775 2679ba74411f
permissions -rw-r--r--
improved process handling. tidied
     1 (*  Title:      HOL/Tools/res_lib.ML
     2     Author:     Jia Meng, Cambridge University Computer Laboratory
     3     ID:         $Id$
     4     Copyright   2004 University of Cambridge
     5 
     6 Some auxiliary functions frequently used by files in this directory.
     7 *)
     8 
     9 signature RES_LIB =
    10 sig
    11 val flat_noDup : ''a list list -> ''a list
    12 val helper_path : string -> string -> string
    13 val no_rep_add : ''a -> ''a list -> ''a list
    14 val no_rep_app : ''a list -> ''a list -> ''a list
    15 val intOfPid : Posix.Process.pid -> Int.int
    16 val pidOfInt : Int.int -> Posix.Process.pid
    17 end;
    18 
    19 
    20 structure ResLib : RES_LIB =
    21 struct
    22 
    23 fun no_rep_add x []     = [x]
    24   | no_rep_add x (y::z) = if x=y then y::z else y::(no_rep_add x z);
    25 
    26 fun no_rep_app l1 []     = l1
    27   | no_rep_app l1 (x::y) = no_rep_app (no_rep_add x l1) y;
    28 
    29 fun flat_noDup []     = []
    30   | flat_noDup (x::y) = no_rep_app x (flat_noDup y);
    31 
    32  
    33 (*Return the path to a "helper" like SPASS or tptp2X, first checking that
    34   it exists. --lcp *)  
    35 fun helper_path evar base =
    36   case getenv evar of
    37       "" => error  ("Isabelle environment variable " ^ evar ^ " not defined")
    38     | home => 
    39         let val path = home ^ "/" ^ base
    40         in  if File.exists (File.unpack_platform_path path) then path 
    41 	    else error ("Could not find the file " ^ path)
    42 	end;  
    43 
    44 (*** Converting between process ids and integers ***)
    45 
    46 fun intOfPid pid = Word.toInt (Word.fromLargeWord (Posix.Process.pidToWord pid));
    47 
    48 fun pidOfInt n = Posix.Process.wordToPid (Word.toLargeWord (Word.fromInt n));
    49 
    50 end;