CristalCaveGem » LustreC

(* This file is part of the Kind 2 model checker.

   Copyright (c) 2015 by the Board of Trustees of the University of Iowa

   Licensed under the Apache License, Version 2.0 (the "License"); you

   may not use this file except in compliance with the License.  You

   may obtain a copy of the License at

   http://www.apache.org/licenses/LICENSE-2.0 

   Unless required by applicable law or agreed to in writing, software

   distributed under the License is distributed on an "AS IS" BASIS,

   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or

   implied. See the License for the specific language governing

   permissions and limitations under the License. 

*)

open Format

(* ********************************************************************** *)

(* Helper functions                                                       *)

(* ********************************************************************** *)

(* Identity function. *)

let identity anything = anything

(* Prints the first argument and returns the second. *)

let print_pass s whatever =

  printf "%s@." s ;

  whatever

(* Returns true when given unit. *)

let true_of_unit () = true

(* Returns false when given unit. *)

let false_of_unit () = false

(* Returns None when given unit. *)

let none_of_unit () = None

(* Returns true *)

let true_of_any _ = true

(* Returns false s*)

let false_of_any _ = false

(* Creates a directory if it does not already exist. *)

let mk_dir dir =

  try Unix.mkdir dir 0o740 with Unix.Unix_error(Unix.EEXIST, _, _) -> ()

(* ********************************************************************** *)

(* Arithmetic functions                                                   *)

(* ********************************************************************** *)

(* Compute [m * h + i] and make sure that the result does not overflow

   to a negtive number *)

let safe_hash_interleave h m i = abs(i + (m * h) mod max_int)

(* ********************************************************************** *)

(* List functions                                                         *)

(* ********************************************************************** *)

(* Add element to the head of the list if the option value is not [None] *)

let ( @:: ) = 

    function

    | None -> (function l -> l)

    | Some e -> (function l -> e :: l)

(* Creates a size-n list equal to [f 0; f 1; ... ; f (n-1)] *)

let list_init f n =

  if n = 0 then [] else

    let rec init_aux i =

      if i = n-1 then

        [f i]

      else

        (f i) :: (init_aux (i+1))

    in

    init_aux 0

(* Returns the maximum element of a non-empty list *)

let list_max l =

  assert (List.length l > 0);

  let rec list_max_aux l acc =

    match l with

    | [] ->

       acc

    | hd :: tl ->

       list_max_aux tl (max hd acc)

  in

  list_max_aux l (List.hd l)

(* Return the index of the first element that satisfies the predicate [p] *)

let list_index p = 

  let rec list_index p i = function

    | [] -> raise Not_found

    | x :: l -> if p x then i else list_index p (succ i) l

  in

  list_index p 0 

(* [list_indexes l1 l2] returns the indexes in list [l2] of elements in

   list [l1] *)

let rec list_indexes' accum pos l = function 

  | [] -> List.rev accum

  | h :: tl -> 

    if List.mem h l then 

      list_indexes' (pos :: accum) (succ pos) l tl

    else

      list_indexes' accum (succ pos) l tl

let list_indexes l1 l2 = list_indexes' [] 0 l1 l2

(* [list_filter_nth l [p1; p2; ...]] returns the elements [l] at positions [p1], [p2] etc. *)

let rec list_filter_nth' current_pos accum = 

  function 

    | [] -> (function _ -> List.rev accum)

    | h :: list_tl -> 

      (function 

        | next_pos :: positions_tl when current_pos = next_pos -> 

          (match positions_tl with

            | next_pos' :: _ when next_pos >= next_pos' -> 

              raise 

                (Invalid_argument

                   "list_filter_nth: list of position is not sorted")

            | _ -> 

              list_filter_nth' 

                (succ current_pos) 

                (h :: accum) 

                list_tl 

                positions_tl)

        | positions -> 

          list_filter_nth' (succ current_pos) accum list_tl positions)

let list_filter_nth l p = list_filter_nth' 0 [] l p

let list_extract_nth l i =

  let rec aux acc l i = match i, l with

    | 0, x :: r -> x, List.rev_append acc r

    | i, x :: r when i > 0 -> aux (x :: acc) r (i - 1) 

    | _ -> raise (Invalid_argument "list_extract_nth")

  in

  aux [] l i

(* [chain_list \[e1; e2; ...\]] is \[\[e1; e2\]; \[e2; e3\]; ... \]]*)

let chain_list = function 

  | [] 

  | _ :: [] -> invalid_arg "chain_list"

  | h :: tl -> 

    let rec chain_list (accum, last) curr = ([last; curr] :: accum, curr) in

    List.rev (fst (List.fold_left chain_list ([], h) tl))

(* Return a list containing all values in the first list that are not

    in the second list *)

let list_subtract l1 l2 = 

  List.filter

    (function e -> not (List.mem e l2))

    l1

(* From a sorted list return a list with physical duplicates removed *)

let list_uniq l = 

  let rec list_uniq accum = function 

    | [] -> List.rev accum

    | h1 :: tl -> 

      match accum with 

        | [] -> list_uniq [h1] tl

        | h2 :: _ -> 

          if h1 == h2 then list_uniq accum tl else list_uniq (h1 :: accum) tl

  in

  list_uniq [] l

(* Merge two sorted lists without physical duplicates to a sorted list without

   physical duplicates *)

let list_merge_uniq cmp l1 l2 = 

  let rec list_merge_uniq cmp accum l1 l2 = match l1, l2 with

    (* One of the lists is empty: reverse accumulator, append

       other list and return *)

    | [], l 

    | l, [] -> List.rev_append accum l

    (* First and second head elements are physically equal: remove

       head element from second list *)

    | h1 :: _, h2 :: tl when h1 == h2 -> list_merge_uniq cmp accum l1 tl

    (* First head element is smaller than second: add first head

       element to accumulator *)

    | h1 :: tl, h2 :: _ when cmp h1 h2 < 0 -> 

      list_merge_uniq cmp (h1 :: accum) tl l2

    (* First head element is greater than second: add second head

       element to accumulator *)

    | h1 :: _, h2 :: tl when cmp h1 h2 > 0 -> 

      list_merge_uniq cmp (h2 :: accum) l1 tl

    (* Head elements are structurally but not physically equal: keep

       both in original order *)

    | h1 :: tl1, h2 :: tl2 -> 

      list_merge_uniq cmp (h2 :: h1 :: accum) tl1 tl2

  in

  list_merge_uniq cmp [] l1 l2

(* From two sorted lists without physical duplicates return a sorted

   list without physical duplicates containing elements in both lists *)

let list_inter_uniq cmp l1 l2 = 

  let rec list_inter_uniq cmp accum l1 l2 = match l1, l2 with 

    (* One of the lists is empty: reverse accumulator and return *)

    | [], l

    | l, [] -> List.rev accum

    (* First and second head elements are physically equal: add first

       head element to accumulator *)

    | h1 :: tl1, h2 :: tl2 when h1 == h2 -> 

      list_inter_uniq cmp (h1 :: accum) tl1 tl2

    (* First head element is smaller than second: remove first head

       element from list *)

    | h1 :: tl, h2 :: _ when cmp h1 h2 < 0 -> 

      list_inter_uniq cmp accum tl l2

    (* First head element is greater than or structurally but not

       physically equal to second: remove second head element from

       list *)

    | h1 :: _, h2 :: tl ->

      list_inter_uniq cmp accum l1 tl

  in

  list_inter_uniq cmp [] l1 l2

(* From two sorted lists without physical duplicates return a sorted

   list without physical duplicates containing elements in the first

   but not in the second list *)

let list_diff_uniq cmp l1 l2 = 

  let rec list_diff_uniq cmp accum l1 l2 = match l1, l2 with 

    (* First list is empty: reverse accumulator and return *)

    | [], l -> List.rev accum

    (* Second list is empty: reverse accumulator, append first list

       and return *)

    | l, [] -> List.rev_append accum l

    (* First and second head elements are physically equal: remove

       both head elements *)

    | h1 :: tl1, h2 :: tl2 when h1 == h2 -> 

      list_diff_uniq cmp accum tl1 tl2

    (* First head element is smaller than second: add first head

       element to accumulator *)

    | h1 :: tl, h2 :: _ when cmp h1 h2 < 0 -> 

      list_diff_uniq cmp (h1 :: accum) tl l2

    (* First head element is greater than second: remove first head

       element from list *)

    | h1 :: _, h2 :: tl ->

      list_diff_uniq cmp accum l1 tl

  in

  list_diff_uniq cmp [] l1 l2

(* For two sorted lists without physical duplicates return true if the

   first list contains a physically equal element for each element in

   the second list *)

let rec list_subset_uniq cmp l1 l2 = match l1, l2 with 

  (* Both lists are empty: return true *)

  | [], [] -> true

  (* First list is empty, but second list not: return true *)

  | [], _ -> true

  (* Second list is empty, but first list not: return false *)

  | _, [] -> false

  (* First and second head elements are physically equal: remove

     both head elements *)

  | h1 :: tl1, h2 :: tl2 when h1 == h2 -> list_subset_uniq cmp tl1 tl2

  (* First head element is smaller than second: return false *)

  | h1 :: tl, h2 :: _ when cmp h1 h2 < 0 -> false

  (* First head element is greater than the second or structurally

     but not physically equal: remove first head element *)

  | h1 :: _, h2 :: tl -> list_subset_uniq cmp l1 tl

(* Lexicographic comparison of pairs *)

let compare_pairs cmp_a cmp_b (a1, b1) (a2, b2) =

  let c_a = cmp_a a1 a2 in if c_a = 0 then cmp_b b1 b2 else c_a

(* Lexicographic comparison of lists *)

let rec compare_lists f l1 l2 = 

    match l1, l2 with 

      (* Two empty lists are equal *)

      | [], [] -> 0

      (* An empty list is smaller than a non-empty list *)

      | [], _ -> -1 

      (* An non-empty list is greater than an empty list *)

      | _, [] -> 1

      (* Compare two non-empty lists *)

      | h1 :: tl1, h2 :: tl2 -> 

        (* Compare head elements of lists *)

        let c = f h1 h2 in

        (* If head elements are equal, compare tails of lists,

           otherwise return comparison of head elements *)

        if c = 0 then compare_lists f tl1 tl2 else c

(* Given two ordered association lists with identical keys, push the

   values of each element of the first association list to the list of

   elements of the second association list. 

   The returned association list is in the order of the input lists,

   the function [equal] is used to compare keys. *)

let list_join equal l1 l2 = 

  let rec list_join' equal accum l1 l2 = match l1, l2 with

    (* Both lists consumed, return in original order *)

    | [], [] -> List.rev accum 

    (* Keys of head elements in both lists equal *)

    | (((k1, v1) :: tl1), ((k2, v2) :: tl2)) when equal k1 k2 -> 

      (* Add to accumulator and continue *)

      list_join' equal ((k1, (v1 :: v2)) :: accum) tl1 tl2

    (* Keys of head elements different, or one of the lists is empty *)

    | _ -> failwith "list_join"

  in

  (* Second list is empty? *)

  match l2 with 

    (* Initialize with singleton elements from first list *)

    | [] -> List.map (fun (k, v) -> (k, [v])) l1

    (* Call recursive function with initial accumulator *)

    | _ -> list_join' equal [] l1 l2

(* ********************************************************************** *)

(* Array functions                                                        *)

(* ********************************************************************** *)

(* Returns the maximum element of a non-empty array *)

let array_max a =

  assert (Array.length a > 0);

  let max_val = ref a.(0) in

  Array.iter (fun x -> if x > !max_val then max_val := x else ()) a;

  !max_val

(* ********************************************************************** *)

(* Set functions                                                          *)

(* ********************************************************************** *)

(* Set of integers *)

module IntegerSet = 

  Set.Make

  (struct

    type t = int

    let compare = Pervasives.compare

    let equal = (=)

   end)

(* Hashtable of integers *)

module IntegerHashtbl =

  Hashtbl.Make

    (struct

      type t = int

      let hash i = i

      let equal = (=)

     end)

(* ********************************************************************** *)

(* Generic pretty-printing                                                 *)

(* ********************************************************************** *)

(* Pretty-print an array *)

let pp_print_arrayi pp sep ppf array  =

  let n = Array.length array in

  let print_element i =

    if i = n-1 then

      pp ppf i array.(i)

    else

      (pp ppf i array.(i);

       fprintf ppf sep)

  in

  let indices = list_init (fun i -> i) n in  

  List.iter print_element indices

(* Pretty-print a list *)

let rec pp_print_list pp sep ppf = function 

  (* Output nothing for the empty list *) 

  | [] -> ()

  (* Output a single element in the list  *) 

  | e :: [] -> 

    pp ppf e

  (* Output a single element and a space *) 

  | e :: tl -> 

    (* Output one element *)

    pp_print_list pp sep ppf [e]; 

    (* Output separator *)

    fprintf ppf sep; 

    (* Output the rest of the list *)

    pp_print_list pp sep ppf tl

(* Pretty-print a list with a counter of its elements *)

let rec pp_print_listi' pp sep ppf = function 

  (* Output nothing for the empty list *) 

  | (_, []) -> ()

  (* Output a single element in the list  *) 

  | (i, e :: []) -> pp ppf i e

  (* Output a single element and a space *) 

  | (i, e :: tl) -> 

    (* Output one element *)

    pp ppf i e;

    (* Output separator *)

    fprintf ppf sep; 

    (* Output the rest of the list *)

    pp_print_listi' pp sep ppf (succ i, tl)

(* Pretty-print a list with a counter of its elements *)

let pp_print_listi pp sep ppf l = pp_print_listi' pp sep ppf (0, l)

let rec pp_print_list2i' pp sep ppf = function 

  | _, [], [] -> ()

  | i, [e1], [e2] -> pp ppf i e1 e2

  | i, e1 :: tl1, e2 :: tl2 -> 

    pp ppf i e1 e2;

    (* Output separator *)

    fprintf ppf sep; 

    (* Output the rest of the two lists *)

    pp_print_list2i' pp sep ppf (succ i, tl1, tl2)

  | _ -> invalid_arg "pp_print_list2i"

(* Pretty-print two lists of the same length with a counter of their

   elements *)

let pp_print_list2i pp sep ppf l1 l2 = pp_print_list2i' pp sep ppf (0, l1, l2)

(* Pretty-print a list wrapped in parentheses *)

let pp_print_paren_list ppf list = 

  (* Begin expression with opening parenthesis *)

  pp_print_string ppf "(";

  (* Output elements of list *)

  pp_print_list pp_print_string "@ " ppf list;

  (* End expression with closing parenthesis *)

  pp_print_string ppf ")"

(* Pretty-print an option type *)

let pp_print_option pp ppf = function 

  | None -> fprintf ppf "None"

  | Some s -> fprintf ppf "@[<hv>Some@ %a@]" pp s

(* Print if list is not empty *)

let pp_print_if_not_empty s ppf = function 

  | [] -> ()

  | _ -> fprintf ppf s

(* Pretty-print into a string *)

let string_of_t pp t = 

  (* Create a buffer *)

  let buf = Buffer.create 80 in

  (* Create a formatter printing into the buffer *)

  let ppf = formatter_of_buffer buf in

  (* Output into buffer *)

  pp ppf t;

  (* Flush the formatter *)

  pp_print_flush ppf ();

  (* Return the buffer contents *)

  Buffer.contents buf

(* Return the strings as a parenthesized and space separated list *)

let paren_string_of_string_list list =

  string_of_t pp_print_paren_list list

(* Return the width of the string, meaning the wisth of it's longest line *)

let width_of_string s =

  let lines = Str.split (Str.regexp "\n") s in

  List.fold_left (fun max_width s ->

      max max_width (String.length s)

    ) 0 lines

(* ********************************************************************** *)

(* Option types                                                           *)

(* ********************************************************************** *)

(* Return the value of an option type, raise [Invalid_argument "get"]

   if the option value is [None] *)

let get = function None -> raise (Invalid_argument "get") | Some x -> x

(* ********************************************************************** *)

(* String                                                                 *)

(* ********************************************************************** *)

(* Return true if the first characters of [s1] up to the length of

   [s2] are ientical to [s2]. Return false if [s2] is longer than

   [s1]. *)

let string_starts_with s1 s2 = 

  (String.length s1 >= String.length s2) &&

  (String.sub s1 0 (String.length s2) = s2)

(* ********************************************************************** *)

(* Log levels                                                             *)

(* ********************************************************************** *)

(* Levels of log messages *)

type log_level =

  | L_off

  | L_fatal

  | L_error

  | L_warn

  | L_note

  | L_info

  | L_debug

  | L_trace

(* Default log level. *)

let default_log_level = L_note

(* Associate an integer with each level to induce a total ordering *)

let int_of_log_level = function 

  | L_off -> -1 

  | L_fatal -> 0

  | L_error -> 1

  | L_warn -> 2

  | L_note -> 3

  | L_info -> 4

  | L_debug -> 5

  | L_trace -> 6

let log_level_of_int = function 

  | -1 -> L_off 

  | 0 -> L_fatal

  | 1 -> L_error

  | 2 -> L_warn

  | 3 -> L_note

  | 4 -> L_info

  | 5 -> L_debug

  | 6 -> L_trace

  | _ -> raise (Invalid_argument "log_level_of_int")

let string_of_log_level = function

  | L_off -> "off"

  | L_fatal -> "fatal"

  | L_error -> "error"

  | L_warn -> "warn"

  | L_note -> "note"

  | L_info -> "info"

  | L_debug -> "debug"

  | L_trace -> "trace"

(* Compare two levels *)

let compare_levels l1 l2 = 

  Pervasives.compare (int_of_log_level l1) (int_of_log_level l2)

(* Current log level *)

let log_level = ref L_warn

(* Set log level *)

let set_log_level l = log_level := l

(* Log level *)

let get_log_level () = !log_level

(* Level is of higher or equal priority than current log level? *)

let output_on_level level = compare_levels level !log_level <= 0

(* Return fprintf if level is is of higher or equal priority

   than current log level, otherwise return ifprintf *)

let ignore_or_fprintf level = 

  if output_on_level level then fprintf else ifprintf

(* ********************************************************************** *)

(* Output target                                                          *)  

(* ********************************************************************** *)

(* Current formatter for output *)

let log_ppf = ref std_formatter

(* Set file to write log messages to *)

let log_to_file f = 

  (* Open channel to logfile *)

  let oc = 

    try open_out f with

      | Sys_error _ -> failwith "Could not open logfile"

  in 

  (* Create and store formatter for logfile *)

  log_ppf := formatter_of_out_channel oc

(* Write messages to standard output *)

let log_to_stdout () = log_ppf := std_formatter

(* ********************************************************************** *)

(* System functions                                                       *)

(* ********************************************************************** *)

(* let pp_print_banner ppf () = *)

(*     fprintf ppf "%s %s" Kind2Config.package_name Version.version *)

(* let pp_print_version ppf = pp_print_banner ppf () *)

(* Kind modules *)

type kind_module = 

  [ `IC3 

  | `BMC

  | `IND

  | `IND2

  | `INVGEN

  | `INVGENOS

  | `INVGENINT

  | `INVGENINTOS

  | `INVGENREAL

  | `INVGENREALOS

  | `C2I

  | `Interpreter

  | `Supervisor

  | `Parser

  | `Certif  ]

(* Pretty-print the type of the process *)

let pp_print_kind_module ppf = function

  | `IC3 -> fprintf ppf "property directed reachability"

  | `BMC -> fprintf ppf "bounded model checking"

  | `IND -> fprintf ppf "inductive step"

  | `IND2 -> fprintf ppf "2-induction"

  | `INVGEN -> fprintf ppf "two state invariant generator (bool)"

  | `INVGENOS -> fprintf ppf "one state invariant generator (bool)"

  | `INVGENINT -> fprintf ppf "two state invariant generator (int)"

  | `INVGENINTOS -> fprintf ppf "one state invariant generator (int)"

  | `INVGENREAL -> fprintf ppf "two state invariant generator (real)"

  | `INVGENREALOS -> fprintf ppf "one state invariant generator (real)"

  | `C2I -> fprintf ppf "c2i"

  | `Interpreter -> fprintf ppf "interpreter"

  | `Supervisor -> fprintf ppf "invariant manager"

  | `Parser -> fprintf ppf "parser"

  | `Certif -> Format.fprintf ppf "certificate"

(* String representation of a process type *)

let string_of_kind_module = string_of_t pp_print_kind_module

(* Return a short representation of kind module *)

let short_name_of_kind_module = function

 | `IC3 -> "ic3"

 | `BMC -> "bmc"

 | `IND -> "ind"

 | `IND2 -> "ind2"

 | `INVGEN -> "invgents"

 | `INVGENOS -> "invgenos"

 | `INVGENINT -> "invgenintts"

 | `INVGENINTOS -> "invgenintos"

 | `INVGENREAL -> "invgenintts"

 | `INVGENREALOS -> "invgenintos"

 | `C2I -> "c2i"

 | `Interpreter -> "interp"

 | `Supervisor -> "super"

 | `Parser -> "parse"

 | `Certif -> "certif"

(* Process type of a string *)

let kind_module_of_string = function 

  | "IC3" -> `IC3

  | "BMC" -> `BMC

  | "IND" -> `IND

  | "IND2" -> `IND2

  | "INVGEN" -> `INVGEN

  | "INVGENOS" -> `INVGENOS

  | "INVGENINT" -> `INVGENINT

  | "INVGENINTOS" -> `INVGENINTOS

  | "INVGENREAL" -> `INVGENREAL

  | "INVGENREALOS" -> `INVGENREALOS

  | "C2I" -> `C2I

  | _ -> raise (Invalid_argument "kind_module_of_string")

let int_of_kind_module = function

  | `Certif -> -4

  | `Parser -> -3

  | `Interpreter -> -2

  | `Supervisor -> -1

  | `BMC -> 1

  | `IND -> 2

  | `IND2 -> 3

  | `IC3 -> 4

  | `INVGEN -> 5

  | `INVGENOS -> 6

  | `INVGENINT -> 7

  | `INVGENINTOS -> 8

  | `INVGENREAL -> 9

  | `INVGENREALOS -> 10

  | `C2I -> 11

(* Timeouts *)

exception TimeoutWall

exception TimeoutVirtual

(* System signal caught *)

exception Signal of int

(* String representation of signal *)

let string_of_signal = function 

  | s when s = Sys.sigabrt -> "SIGABRT"

  | s when s = Sys.sigalrm -> "SIGALRM"

  | s when s = Sys.sigfpe -> "SIGFPE"

  | s when s = Sys.sighup -> "SIGHUP"

  | s when s = Sys.sigill -> "SIGILL"

  | s when s = Sys.sigint -> "SIGINT"

  | s when s = Sys.sigkill -> "SIGKILL"

  | s when s = Sys.sigpipe -> "SIGPIPE"

  | s when s = Sys.sigquit -> "SIGQUIT"

  | s when s = Sys.sigsegv -> "SIGSEGV"

  | s when s = Sys.sigterm -> "SIGTERM"

  | s when s = Sys.sigusr1 -> "SIGUSR1"

  | s when s = Sys.sigusr2 -> "SIGUSR2"

  | s when s = Sys.sigchld -> "SIGCHLD"

  | s when s = Sys.sigcont -> "SIGCONT"

  | s when s = Sys.sigstop -> "SIGSTOP"

  | s when s = Sys.sigtstp -> "SIGTSTP"

  | s when s = Sys.sigttin -> "SIGTTIN"

  | s when s = Sys.sigttou -> "SIGTTOU"

  | s when s = Sys.sigvtalrm -> "SIGVTALRM"

  | s when s = Sys.sigprof -> "SIGPROF"

  | s -> string_of_int s

let pp_print_signal ppf s = fprintf ppf "%s" (string_of_signal s)

(* Pretty-print the termination status of a process *)

let pp_print_process_status ppf = function 

  | Unix.WEXITED s -> fprintf ppf "exited with return code %d" s

  | Unix.WSIGNALED s -> 

    fprintf ppf "killed by signal %a" pp_print_signal s

  | Unix.WSTOPPED s -> 

    fprintf ppf "stopped by signal %a" pp_print_signal s

(* Raise exception on signal *)

let exception_on_signal signal = 

  (* printf "Signal %a caught" pp_print_signal signal; *)

  raise (Signal signal)

(* (\* Sleep for seconds, resolution is in ms *\) *)

(* let minisleep sec = *)

(*   try  *)

(*     (\* Sleep for the given seconds, yield to other threads *\) *)

(*     Thread.delay sec  *)

(*   with  *)

(*     (\* Signal caught while in kernel *\) *)

(*     | Unix.Unix_error(Unix.EINTR, _, _) ->  *)

(*       (\* Cannot find out signal number *\) *)

(*       raise (Signal 0) *)

(* Return full path to executable, search PATH environment variable

   and current working directory *)

let find_on_path exec = 

  let rec find_on_path' exec path = 

    (* Terminate on empty path *)

    if path = "" then raise Not_found;

    (* Split path at first colon *)

    let path_hd, path_tl = 

      try 

        (* Position of colon in string *)

        let colon_index = String.index path ':' in

        (* Length of string *)

        let path_len = String.length path in

        (* Return string up to colon *)

        (String.sub path 0 colon_index, 

         (* Return string after colon *)

         String.sub path (colon_index + 1) (path_len - colon_index - 1))

      (* Colon not found, return whole string and empty string *)

      with Not_found -> path, ""

    in

    (* Combine path and filename *)

    let exec_path = Filename.concat path_hd exec in

    if 

      (* Check if file exists on path *)

      Sys.file_exists exec_path 

    then 

      (* Return full path to file 

         TODO: Check if file is executable here? *)

      exec_path 

    else 

      (* Continue on remaining path entries *)

      find_on_path' exec path_tl

  in

  try 

    if Filename.is_relative exec then 

      (* Return filename on path, fail with Not_found if path is empty

         or [exec] not found on path *)

      find_on_path' exec (Unix.getenv "PATH")

    else if 

      (* Check if file exists on path *)

      Sys.file_exists exec

    then 

      (* Return full path to file 

         TODO: Check if file is executable here? *)

      exec

    else 

      raise Not_found

  with Not_found -> 

    (* Check current directory as last resort *)

    let exec_path = Filename.concat (Sys.getcwd ()) exec in 

    (* Return full path if file exists, fail otherwise *)

    if Sys.file_exists exec_path then exec_path else raise Not_found

(* ********************************************************************** *)

(* Parser and lexer functions                                             *)

(* ********************************************************************** *)

(* A position in a file

   The column is the actual colum number, not an offset from the

   beginning of the file as in Lexing.position *)

type position =

  { pos_fname : string; pos_lnum: int; pos_cnum: int }

(* Comparision on positions *)

let compare_pos 

    { pos_fname = p1; pos_lnum = l1; pos_cnum = c1 }  

    { pos_fname = p2; pos_lnum = l2; pos_cnum = c2 } =