diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/initial_check.ml | 7 | ||||
| -rw-r--r-- | src/initial_check.mli | 14 | ||||
| -rw-r--r-- | src/pp.ml | 76 | ||||
| -rw-r--r-- | src/pp.mli | 54 | ||||
| -rw-r--r-- | src/process_file.ml | 5 | ||||
| -rw-r--r-- | src/process_file.mli | 1 | ||||
| -rw-r--r-- | src/type_internal.ml | 57 | ||||
| -rw-r--r-- | src/type_internal.mli | 52 | ||||
| -rw-r--r-- | src/util.ml | 259 | ||||
| -rw-r--r-- | src/util.mli | 193 |
10 files changed, 717 insertions, 1 deletions
diff --git a/src/initial_check.ml b/src/initial_check.ml new file mode 100644 index 00000000..8f474f26 --- /dev/null +++ b/src/initial_check.ml @@ -0,0 +1,7 @@ +open Type_internal +open Ast + +type 'a envs = 'a * Nameset.t * kind Kindmap.t * t Typmap.t + +let rec to_ast (bound_names : Nameset.t) (kind_env : kind Kindmap.t) (typ_env : t Typmap.t) partial_defs defs = + (Defs []) diff --git a/src/initial_check.mli b/src/initial_check.mli new file mode 100644 index 00000000..39b955b5 --- /dev/null +++ b/src/initial_check.mli @@ -0,0 +1,14 @@ + +open Type_internal +open Ast + +type 'a envs = 'a * Nameset.t * kind Kindmap.t * t Typmap.t + +val to_ast : Nameset.t -> kind Kindmap.t -> t Typmap.t -> tannot def list -> Parse_ast.defs -> tannot defs +(*val to_ast_def : nameset -> kind kindmap -> t typmap -> tannot def list -> Parse_ast.defs -> (annot def) envs * annot def list +val to_ast_fun : nameset -> kind kindmap -> t typmap -> Parse_ast.fundef -> (annot fundef) envs +val to_ast_expr : nameset -> kind kindmap -> t typmap -> Parse_ast.exp -> (annot exp) envs +val to_ast_targ : nameset -> kind kindmap -> t typmap -> Parse_ast.atyp -> (annot typ_arg) envs +val to_ast_typ : nameset -> kind kindmap -> t typmap -> Parse_ast.atyp -> (annot typ) envs +val to_ast_nexp : nameset -> kind kindmap -> t typmap -> Parse_ast.atyp -> (annot nexp) envs +*) diff --git a/src/pp.ml b/src/pp.ml new file mode 100644 index 00000000..0fa8636a --- /dev/null +++ b/src/pp.ml @@ -0,0 +1,76 @@ +(**************************************************************************) +(* Lem *) +(* *) +(* Dominic Mulligan, University of Cambridge *) +(* Francesco Zappa Nardelli, INRIA Paris-Rocquencourt *) +(* Gabriel Kerneis, University of Cambridge *) +(* Kathy Gray, University of Cambridge *) +(* Peter Boehm, University of Cambridge (while working on Lem) *) +(* Peter Sewell, University of Cambridge *) +(* Scott Owens, University of Kent *) +(* Thomas Tuerk, University of Cambridge *) +(* *) +(* The Lem sources are copyright 2010-2013 *) +(* by the UK authors above and Institut National de Recherche en *) +(* Informatique et en Automatique (INRIA). *) +(* *) +(* All files except ocaml-lib/pmap.{ml,mli} and ocaml-libpset.{ml,mli} *) +(* are distributed under the license below. The former are distributed *) +(* under the LGPLv2, as in the LICENSE file. *) +(* *) +(* *) +(* Redistribution and use in source and binary forms, with or without *) +(* modification, are permitted provided that the following conditions *) +(* are met: *) +(* 1. Redistributions of source code must retain the above copyright *) +(* notice, this list of conditions and the following disclaimer. *) +(* 2. Redistributions in binary form must reproduce the above copyright *) +(* notice, this list of conditions and the following disclaimer in the *) +(* documentation and/or other materials provided with the distribution. *) +(* 3. The names of the authors may not be used to endorse or promote *) +(* products derived from this software without specific prior written *) +(* permission. *) +(* *) +(* THIS SOFTWARE IS PROVIDED BY THE AUTHORS ``AS IS'' AND ANY EXPRESS *) +(* OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED *) +(* WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE *) +(* ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHORS BE LIABLE FOR ANY *) +(* DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL *) +(* DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE *) +(* GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS *) +(* INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER *) +(* IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR *) +(* OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN *) +(* IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. *) +(**************************************************************************) + +(** pretty printing utilities *) + +open Format + +let pp_str ppf s = + fprintf ppf "%s" s + +let rec lst sep f ppf = function + | [] -> () + | [x] -> + fprintf ppf "%a" + f x + | (h::t) -> + f ppf h; + fprintf ppf sep; + lst sep f ppf t + +let opt f ppf = function + | None -> + fprintf ppf "None" + | Some(x) -> + fprintf ppf "Some(%a)" + f x + +let pp_to_string pp = + let b = Buffer.create 16 in + let f = formatter_of_buffer b in + pp f; + pp_print_flush f (); + Buffer.contents b diff --git a/src/pp.mli b/src/pp.mli new file mode 100644 index 00000000..2c7d6777 --- /dev/null +++ b/src/pp.mli @@ -0,0 +1,54 @@ +(**************************************************************************) +(* Lem *) +(* *) +(* Dominic Mulligan, University of Cambridge *) +(* Francesco Zappa Nardelli, INRIA Paris-Rocquencourt *) +(* Gabriel Kerneis, University of Cambridge *) +(* Kathy Gray, University of Cambridge *) +(* Peter Boehm, University of Cambridge (while working on Lem) *) +(* Peter Sewell, University of Cambridge *) +(* Scott Owens, University of Kent *) +(* Thomas Tuerk, University of Cambridge *) +(* *) +(* The Lem sources are copyright 2010-2013 *) +(* by the UK authors above and Institut National de Recherche en *) +(* Informatique et en Automatique (INRIA). *) +(* *) +(* All files except ocaml-lib/pmap.{ml,mli} and ocaml-libpset.{ml,mli} *) +(* are distributed under the license below. The former are distributed *) +(* under the LGPLv2, as in the LICENSE file. *) +(* *) +(* *) +(* Redistribution and use in source and binary forms, with or without *) +(* modification, are permitted provided that the following conditions *) +(* are met: *) +(* 1. Redistributions of source code must retain the above copyright *) +(* notice, this list of conditions and the following disclaimer. *) +(* 2. Redistributions in binary form must reproduce the above copyright *) +(* notice, this list of conditions and the following disclaimer in the *) +(* documentation and/or other materials provided with the distribution. *) +(* 3. The names of the authors may not be used to endorse or promote *) +(* products derived from this software without specific prior written *) +(* permission. *) +(* *) +(* THIS SOFTWARE IS PROVIDED BY THE AUTHORS ``AS IS'' AND ANY EXPRESS *) +(* OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED *) +(* WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE *) +(* ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHORS BE LIABLE FOR ANY *) +(* DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL *) +(* DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE *) +(* GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS *) +(* INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER *) +(* IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR *) +(* OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN *) +(* IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. *) +(**************************************************************************) + +open Format +val pp_str : formatter -> string -> unit + +val lst : ('a, formatter, unit) format -> (formatter -> 'b -> unit) -> formatter -> 'b list -> unit + +val opt : (formatter -> 'a -> unit) -> formatter -> 'a option -> unit + +val pp_to_string : (formatter -> 'a) -> string diff --git a/src/process_file.ml b/src/process_file.ml index 4284a252..8c996c14 100644 --- a/src/process_file.ml +++ b/src/process_file.ml @@ -44,7 +44,7 @@ (* IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. *) (**************************************************************************) -(* XXX: for debugging the developing code: open Coq_ast *) +open Type_internal (* let r = Ulib.Text.of_latin1 *) @@ -69,6 +69,9 @@ let parse_file (f : string) : Parse_ast.defs = | Lexer.LexError(s,p) -> raise (Reporting_basic.Fatal_error (Reporting_basic.Err_lex (p, s))) +let convert_ast (defs : Parse_ast.defs) : Type_internal.tannot Ast.defs = + Initial_check.to_ast Nameset.empty Kindmap.empty Typmap.empty [] defs + (* type instances = Types.instance list Types.Pfmap.t let check_ast (ts : Typed_ast.Targetset.t) (mod_path : Name.t list) diff --git a/src/process_file.mli b/src/process_file.mli index 1622d902..f01aa251 100644 --- a/src/process_file.mli +++ b/src/process_file.mli @@ -47,6 +47,7 @@ (* open Typed_ast *) val parse_file : string -> Parse_ast.defs +val convert_ast : Parse_ast.defs -> Type_internal.tannot Ast.defs (* type instances = Types.instance list Types.Pfmap.t diff --git a/src/type_internal.ml b/src/type_internal.ml new file mode 100644 index 00000000..8b68934e --- /dev/null +++ b/src/type_internal.ml @@ -0,0 +1,57 @@ +module Kindmap = Finite_map.Fmap_map(String) +module Nameset' = Set.Make(String) +module Nameset = struct + include Nameset' + let pp ppf nameset = + Format.fprintf ppf "{@[%a@]}" + (Pp.lst ",@ " Pp.pp_str) + (Nameset'.elements nameset) +end + +module Typmap = Finite_map.Fmap_map(String) + +type t = { mutable t : t_aux } +and t_aux = + | Tvar of string + | Tfn of t * t * effect + | Ttup of t list + | Tapp of string * t_arg list + | Tuvar of t_uvar +and t_uvar = { index : int; mutable subst : t option } +and nexp = { mutable nexp : nexp_aux } +and nexp_aux = + | Nvar of string + | Nconst of int + | Nadd of nexp * nexp + | Nmult of nexp * nexp + | N2n of nexp + | Nneg of nexp (* Unary minus for representing new vector sizes after vector slicing *) + | Nuvar of n_uvar +and n_uvar = { nindex : int; mutable nsubst : t option } +and effect = { mutable effect : effect_aux } +and effect_aux = + | Evar of string + | Eset of Ast.efct_aux list + | Euvar of e_uvar +and e_uvar = { eindex : int; mutable esubst : t option } +and order = { mutable order : order_aux } +and order_aux = + | Ovar of string + | Oinc + | Odec + | Ouvar of o_uvar +and o_uvar = { oindex : int; mutable osubst : t option } +and t_arg = + | TA_typ of t + | TA_nexp of nexp + | TA_eft of effect + | TA_ord of order + +(* Constraints for nexps, plus the location which added the constraint, each nexp is either <= 0 = 0 or >= 0 *) +type nexp_range = + | LtEq of Parse_ast.l * nexp + | Eq of Parse_ast.l * nexp + | GtEq of Parse_ast.l * nexp + | In of Parse_ast.l * nexp * nexp list + +type tannot = (t * nexp_range list) option diff --git a/src/type_internal.mli b/src/type_internal.mli new file mode 100644 index 00000000..cfa12a75 --- /dev/null +++ b/src/type_internal.mli @@ -0,0 +1,52 @@ +module Kindmap : Finite_map.Fmap with type k = string +module Typmap : Finite_map.Fmap with type k = string +module Nameset : sig + include Set.S with type elt = string + val pp : Format.formatter -> t -> unit +end + +type t_uvar +type n_uvar +type e_uvar +type o_uvar +type t = { mutable t : t_aux } +and t_aux = + | Tvar of string + | Tfn of t * t * effect + | Ttup of t list + | Tapp of string * t_arg list + | Tuvar of t_uvar +and nexp = { mutable nexp : nexp_aux } +and nexp_aux = + | Nvar of string + | Nconst of int + | Nadd of nexp * nexp + | Nmult of nexp * nexp + | N2n of nexp + | Nneg of nexp (* Unary minus for representing new vector sizes after vector slicing *) + | Nuvar of n_uvar +and effect = { mutable effect : effect_aux } +and effect_aux = + | Evar of string + | Eset of Ast.efct_aux list + | Euvar of e_uvar +and order = { mutable order : order_aux } +and order_aux = + | Ovar of string + | Oinc + | Odec + | Ouvar of o_uvar +and t_arg = + | TA_typ of t + | TA_nexp of nexp + | TA_eft of effect + | TA_ord of order + +(* Constraints for nexps, plus the location which added the constraint, each nexp is either <= 0 = 0 or >= 0 *) +type nexp_range = + | LtEq of Parse_ast.l * nexp + | Eq of Parse_ast.l * nexp + | GtEq of Parse_ast.l * nexp + | In of Parse_ast.l * nexp * nexp list + +type tannot = (t * nexp_range list) option diff --git a/src/util.ml b/src/util.ml new file mode 100644 index 00000000..28b56f22 --- /dev/null +++ b/src/util.ml @@ -0,0 +1,259 @@ +(**************************************************************************) +(* Lem *) +(* *) +(* Dominic Mulligan, University of Cambridge *) +(* Francesco Zappa Nardelli, INRIA Paris-Rocquencourt *) +(* Gabriel Kerneis, University of Cambridge *) +(* Kathy Gray, University of Cambridge *) +(* Peter Boehm, University of Cambridge (while working on Lem) *) +(* Peter Sewell, University of Cambridge *) +(* Scott Owens, University of Kent *) +(* Thomas Tuerk, University of Cambridge *) +(* *) +(* The Lem sources are copyright 2010-2013 *) +(* by the UK authors above and Institut National de Recherche en *) +(* Informatique et en Automatique (INRIA). *) +(* *) +(* All files except ocaml-lib/pmap.{ml,mli} and ocaml-libpset.{ml,mli} *) +(* are distributed under the license below. The former are distributed *) +(* under the LGPLv2, as in the LICENSE file. *) +(* *) +(* *) +(* Redistribution and use in source and binary forms, with or without *) +(* modification, are permitted provided that the following conditions *) +(* are met: *) +(* 1. Redistributions of source code must retain the above copyright *) +(* notice, this list of conditions and the following disclaimer. *) +(* 2. Redistributions in binary form must reproduce the above copyright *) +(* notice, this list of conditions and the following disclaimer in the *) +(* documentation and/or other materials provided with the distribution. *) +(* 3. The names of the authors may not be used to endorse or promote *) +(* products derived from this software without specific prior written *) +(* permission. *) +(* *) +(* THIS SOFTWARE IS PROVIDED BY THE AUTHORS ``AS IS'' AND ANY EXPRESS *) +(* OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED *) +(* WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE *) +(* ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHORS BE LIABLE FOR ANY *) +(* DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL *) +(* DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE *) +(* GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS *) +(* INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER *) +(* IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR *) +(* OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN *) +(* IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. *) +(**************************************************************************) + +module Duplicate(S : Set.S) = struct + +type dups = + | No_dups of S.t + | Has_dups of S.elt + +let duplicates (x : S.elt list) : dups = + let rec f x acc = match x with + | [] -> No_dups(acc) + | s::rest -> + if S.mem s acc then + Has_dups(s) + else + f rest (S.add s acc) + in + f x S.empty +end + +let remove_duplicates l = + let l' = List.sort Pervasives.compare l in + let rec aux acc l = match (acc, l) with + (_, []) -> List.rev acc + | ([], x :: xs) -> aux [x] xs + | (y::ys, x :: xs) -> if (x = y) then aux (y::ys) xs else aux (x::y::ys) xs + in + aux [] l' + +let rec compare_list f l1 l2 = + match (l1,l2) with + | ([],[]) -> 0 + | (_,[]) -> 1 + | ([],_) -> -1 + | (x::l1,y::l2) -> + let c = f x y in + if c = 0 then + compare_list f l1 l2 + else + c + +let map_changed_default d f l = + let rec g = function + | [] -> ([],false) + | x::y -> + let (r,c) = g y in + match f x with + | None -> ((d x)::r,c) + | Some(x') -> (x'::r,true) + in + let (r,c) = g l in + if c then + Some(r) + else + None + +let map_changed f l = map_changed_default (fun x -> x) f l + +let rec map_filter (f : 'a -> 'b option) (l : 'a list) : 'b list = + match l with [] -> [] + | x :: xs -> + let xs' = map_filter f xs in + match (f x) with None -> xs' + | Some x' -> x' :: xs' + +let list_index p l = + let rec aux i l = + match l with [] -> None + | (x :: xs) -> if p x then Some i else aux (i+1) xs + in + aux 0 l + +let option_get_exn e = function + | Some(o) -> o + | None -> raise e + +let option_default d = function + | None -> d + | Some(o) -> o + +let option_cases op f1 f2 = match op with + | Some(o) -> f1 o + | None -> f2 () + +let option_map f = function + | None -> None + | Some(o) -> Some(f o) + +let option_bind f = function + | None -> None + | Some(o) -> f o + +let changed2 f g x h y = + match (g x, h y) with + | (None,None) -> None + | (Some(x'),None) -> Some(f x' y) + | (None,Some(y')) -> Some(f x y') + | (Some(x'),Some(y')) -> Some(f x' y') + +let rec map_all (f : 'a -> 'b option) (l : 'a list) : 'b list option = + match l with [] -> Some [] + | x :: xs -> + match (f x) with None -> None + | Some x' -> option_map (fun xs' -> x' :: xs') (map_all f xs) + +let rec option_first f xL = + match xL with + [] -> None + | (x :: xs) -> match f x with None -> option_first f xs | Some s -> Some s + +let list_to_front n l = + if n <= 0 then l else + let rec aux acc n l = + match (n, l) with + (0, x::xs) -> (x :: (List.rev_append acc xs)) + | (n, x::xs) -> aux (x :: acc) (n-1) xs + | (_, []) -> (* should not happen *) raise (Failure "list_to_front") + in aux [] n l + +let undo_list_to_front n l = + if n <= 0 then l else + let rec aux acc n y l = + match (n, l) with + (0, xs) -> List.rev_append acc (y::xs) + | (n, x::xs) -> aux (x :: acc) (n-1) y xs + | (_, []) -> List.rev_append acc [y] + in match l with [] -> l | y::xs -> aux [] n y xs + +let split_after n l = + if n < 0 then raise (Failure "negative argument to split_after") else + let rec aux acc n ll = match (n, ll) with + (0, _) -> (List.rev acc, ll) + | (n, x :: xs) -> aux (x :: acc) (n-1) xs + | _ -> raise (Failure "index too large") + in aux [] n l + +let list_mapi (f : int -> 'a -> 'b) (l : 'a list) : 'b list = + let rec aux f i l = + match l with + [] -> [] + | (x :: xs) -> ((f i x) :: (aux f (i + 1) xs)) + in + aux f 0 l + +let rec list_iter_sep (sf : unit -> unit) (f : 'a -> unit) l : unit = + match l with + | [] -> () + | [x0] -> f x0 + | (x0 :: x1 :: xs) -> (f x0; sf(); list_iter_sep sf f (x1 :: xs)) + +let string_to_list s = + let rec aux i acc = + if i < 0 then acc + else aux (i-1) (s.[i] :: acc) + in aux (String.length s - 1) [] + +module IntSet = Set.Make( + struct + let compare = Pervasives.compare + type t = int + end ) + +module IntIntSet = Set.Make( + struct + let compare = Pervasives.compare + type t = int * int + end ) + + +module ExtraSet = functor (S : Set.S) -> + struct + let add_list s l = List.fold_left (fun s x -> S.add x s) s l + let from_list l = add_list S.empty l + let list_union l = List.fold_left S.union S.empty l + let list_inter = function s :: l -> List.fold_left S.inter s l + | [] -> raise (Failure "ExtraSet.list_inter") + end;; + + +let copy_file src dst = + let len = 5096 in + let b = String.make len ' ' in + let read_len = ref 0 in + let i = open_in_bin src in + let o = open_out_bin dst in + while (read_len := input i b 0 len; !read_len <> 0) do + output o b 0 !read_len + done; + close_in i; + close_out o + +let move_file src dst = + if (Sys.file_exists dst) then Sys.remove dst; + try + (* try efficient version *) + Sys.rename src dst + with Sys_error _ -> + begin + (* OK, do it the the hard way *) + copy_file src dst; + Sys.remove src + end + +let same_content_files file1 file2 : bool = + (Sys.file_exists file1) && (Sys.file_exists file2) && + begin + let s1 = Stream.of_channel (open_in_bin file1) in + let s2 = Stream.of_channel (open_in_bin file2) in + let stream_is_empty s = (try Stream.empty s; true with Stream.Failure -> false) in + try + while ((Stream.next s1) = (Stream.next s2)) do () done; + false + with Stream.Failure -> stream_is_empty s1 && stream_is_empty s2 + end + diff --git a/src/util.mli b/src/util.mli new file mode 100644 index 00000000..29c68a0d --- /dev/null +++ b/src/util.mli @@ -0,0 +1,193 @@ +(**************************************************************************) +(* Lem *) +(* *) +(* Dominic Mulligan, University of Cambridge *) +(* Francesco Zappa Nardelli, INRIA Paris-Rocquencourt *) +(* Gabriel Kerneis, University of Cambridge *) +(* Kathy Gray, University of Cambridge *) +(* Peter Boehm, University of Cambridge (while working on Lem) *) +(* Peter Sewell, University of Cambridge *) +(* Scott Owens, University of Kent *) +(* Thomas Tuerk, University of Cambridge *) +(* *) +(* The Lem sources are copyright 2010-2013 *) +(* by the UK authors above and Institut National de Recherche en *) +(* Informatique et en Automatique (INRIA). *) +(* *) +(* All files except ocaml-lib/pmap.{ml,mli} and ocaml-libpset.{ml,mli} *) +(* are distributed under the license below. The former are distributed *) +(* under the LGPLv2, as in the LICENSE file. *) +(* *) +(* *) +(* Redistribution and use in source and binary forms, with or without *) +(* modification, are permitted provided that the following conditions *) +(* are met: *) +(* 1. Redistributions of source code must retain the above copyright *) +(* notice, this list of conditions and the following disclaimer. *) +(* 2. Redistributions in binary form must reproduce the above copyright *) +(* notice, this list of conditions and the following disclaimer in the *) +(* documentation and/or other materials provided with the distribution. *) +(* 3. The names of the authors may not be used to endorse or promote *) +(* products derived from this software without specific prior written *) +(* permission. *) +(* *) +(* THIS SOFTWARE IS PROVIDED BY THE AUTHORS ``AS IS'' AND ANY EXPRESS *) +(* OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED *) +(* WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE *) +(* ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHORS BE LIABLE FOR ANY *) +(* DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL *) +(* DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE *) +(* GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS *) +(* INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER *) +(* IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR *) +(* OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN *) +(* IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. *) +(**************************************************************************) + +(** Mixed useful things *) +module Duplicate(S : Set.S) : sig + type dups = + | No_dups of S.t + | Has_dups of S.elt + val duplicates : S.elt list -> dups +end + +(** [remove_duplicates l] removes duplicate elements from + the list l. As a side-effect, the list might be reordered. *) +val remove_duplicates : 'a list -> 'a list + +(** {2 Option Functions} *) + +(** [option_map f None] returns [None], whereas + [option_map f (Some x)] returns [Some (f x)]. *) +val option_map : ('a -> 'b) -> 'a option -> 'b option + +(** [option_cases None f_s f_n] returns [f_n], whereas + [option_cases (Some x) f_s f_n] returns [f_s x]. *) +val option_cases : 'a option -> ('a -> 'b) -> (unit -> 'b) -> 'b + +(** [option_bind f None] returns [None], whereas + [option_bind f (Some x)] returns [f x]. *) +val option_bind : ('a -> 'b option) -> 'a option -> 'b option + +(** [option_default d None] returns the default value [d], + whereas [option_default d (Some x)] returns [x]. *) +val option_default : 'a -> 'a option -> 'a + +(** [option_get_exn exn None] throws the exception [exn], + whereas [option_get_exn exn (Some x)] returns [x]. *) +val option_get_exn : exn -> 'a option -> 'a + +(** [changed2 f g x h y] applies [g] to [x] and [h] to [y]. + If both function applications return [None], then [None] is + returned. Otherwise [f] is applied to the results. For this + application of [f], [x] is used in case [g x] returns [None] and + similarly [y] in case [h y] returns [None]. *) +val changed2 : ('a -> 'b -> 'c) -> ('a -> 'a option) -> 'a -> ('b -> 'b option) -> 'b -> 'c option + + +(** {2 List Functions} *) + +(** [list_index p l] returns the first index [i] such that + the predicate [p (l!i)] holds. If no such [i] exists, + [None] is returned. *) +val list_index: ('a -> bool) -> 'a list -> int option + +(** [option_first f l] searches for the first element [x] of [l] such + that the [f x] is not [None]. If such an element exists, [f x] is + returned, otherwise [None]. *) +val option_first: ('a -> 'b option) -> 'a list -> 'b option + +(** [map_changed f l] maps [f] over [l]. + If for all elements of [l] the + function [f] returns [None], then [map_changed f l] returns [None]. + Otherwise, it uses [x] for all elements, where [f x] returns [None], + and returns the resulting list. *) +val map_changed : ('a -> 'a option) -> 'a list -> 'a list option + +(** [map_changed_default d f l] maps [f] over [l]. + If for all elements of [l] the + function [f] returns [None], then [map_changed f l] returns [None]. + Otherwise, it uses [d x] for all elements [x], where [f x] returns [None], + and returns the resulting list. *) +val map_changed_default : ('a -> 'b) -> ('a -> 'b option) -> 'a list -> 'b list option + +(** [list_mapi f l] maps [f] over [l]. In contrast to the standard + [map] function, [f] gets the current index of the list as an extra + argument. Counting starts at [0]. *) +val list_mapi : (int -> 'a -> 'b) -> 'a list -> 'b list + +(** [list_iter sf f [a1; ...; an]] applies function [f] in turn to [a1; ...; an] and + calls [sf ()] in between. It is equivalent to [begin f a1; sf(); f a2; sf(); ...; f an; () end]. *) +val list_iter_sep : (unit -> unit) -> ('a -> unit) -> 'a list -> unit + +(** [map_filter f l] maps [f] over [l] and removes all entries [x] of [l] + with [f x = None]. *) +val map_filter : ('a -> 'b option) -> 'a list -> 'b list + +(** [map_all f l] maps [f] over [l]. If at least one entry is [None], [None] is returned. Otherwise, + the [Some] function is removed from the list. *) +val map_all : ('a -> 'b option) -> 'a list -> 'b list option + +(** [list_to_front i l] resorts the list [l] by bringing the element at index [i] + to the front. + @throws Failure if [i] is not smaller than the length of [l]*) +val list_to_front : int -> 'a list -> 'a list + +(** [undo_list_to_front i l] resorts the list [l] by moving the head element to index index [i] + It's the inverse of [list_to_front i l]. *) +val undo_list_to_front : int -> 'a list -> 'a list + +(** [split_after n l] splits the first [n] elemenst from list [l], i.e. it returns two lists + [l1] and [l2], with [length l1 = n] and [l1 @ l2 = l]. Fails if n is too small or large. *) +val split_after : int -> 'a list -> 'a list * 'a list + +val compare_list : ('a -> 'b -> int) -> 'a list -> 'b list -> int + + +(** {2 Files} *) + +(** [copy_file src dst] copies file [src] to file [dst]. Only files are supported, + no directories. *) +val copy_file : string -> string -> unit + +(** [move_file src dst] moves file [src] to file [dst]. In contrast to [Sys.rename] no error is + produced, if [dst] already exists. Moreover, in case [Sys.rename] fails for some reason (e.g. because + it does not work over filesystem boundaries), [copy_file] and [Sys.remove] are used as + fallback. *) +val move_file : string -> string -> unit + +(** [same_content_files file1 file2] checks, whether the files [file1] and [file2] have the same content. +If at least one of the files does not exist, [false] is returned. [same_content_files] throws an exception, +if one of the files exists, but cannot be read. *) +val same_content_files : string -> string -> bool + +(** {2 Strings} *) + +(** [string_to_list l] translates the string [l] to the list of its characters. *) +val string_to_list : string -> char list + +(** {2 Useful Sets} *) + +(** Sets of Integers *) +module IntSet : Set.S with type elt = int +module IntIntSet : Set.S with type elt = int * int + +(** Some useful extra functions for sets *) +module ExtraSet : functor (S : Set.S) -> + sig + (** Add a list of values to an existing set. *) + val add_list : S.t -> S.elt list -> S.t + + (** Construct a set from a list. *) + val from_list : S.elt list -> S.t + + (** Builds the union of a list of sets *) + val list_union : S.t list -> S.t + + (** Builds the intersection of a list of sets. + If the list is empty, a match exception is thrown. *) + val list_inter : S.t list -> S.t + end + + |