Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

reorganize xlib.ml #125

Merged
merged 1 commit into from
Apr 11, 2024
Merged

reorganize xlib.ml #125

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
115 changes: 68 additions & 47 deletions xlib.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -9,23 +9,6 @@ REMOVE*)
open Xprelude
open Fusion

let open_file n = log_gen n; open_out n;;

let create_file n f = let oc = open_file n in f oc; close_out oc;;

let command s =
if Sys.command s <> 0 then (log "Error: \"%s\" failed.\n" s; exit 1);;

let concat f1 f2 f3 =
log "generate %s ...\n%!" f3;
command (Printf.sprintf "cat %s %s > %s && rm -f %s %s" f1 f2 f3 f1 f2)
;;

let rename f1 f2 =
log "rename %s into %s ...\n%!" f1 f2;
Sys.rename f1 f2
;;

(****************************************************************************)
(* Ranges of proof indexes. *)
(****************************************************************************)
Expand All @@ -52,44 +35,33 @@ let iter_parts nb_proofs nb_parts f =
;;

(****************************************************************************)
(* Functions on basic data structures. *)
(* Functions on numbers. *)
(****************************************************************************)

let percent k n = (100 * k) / n;;

let part i = "_part_" ^ string_of_int i;;
(****************************************************************************)
(* Functions on system calls. *)
(****************************************************************************)

(* [get_part s suffix] returns [Some(n,k)] if [s=n^suffix^part(k)],
and [None] otherwise. *)
let get_part s suffix =
try
let len_s = String.length s in
let i = ref (len_s - 1) in
(* compute part number *)
let k =
while !i >= 0 && s.[!i] <> '_' do decr i done;
if !i < 0 then raise Exit;
int_of_string (String.sub s (!i+1) (len_s - 1 - !i))
in
(* compute theorem name *)
let len_suffix = String.length suffix + String.length "_part_" in
if !i < len_suffix then raise Exit;
let n = String.sub s 0 (!i - len_suffix + 1) in
Some(n,k)
with Exit -> None
;;
let command s =
if Sys.command s <> 0 then (log "Error: \"%s\" failed.\n" s; exit 1);;

(* [pos_first f l] returns the position (counting from 0) of the first
element of [l] satisfying [f]. Raises Not_found if there is no such
element. *)
let pos_first f =
let rec aux k l =
match l with
| [] -> raise Not_found
| y::l -> if f y then k else aux (k+1) l
in aux 0
(****************************************************************************)
(* Functions on files. *)
(****************************************************************************)

let open_file n = log_gen n; open_out n;;

let create_file n f = let oc = open_file n in f oc; close_out oc;;

let concat f1 f2 f3 =
log "generate %s ...\n%!" f3;
command (Printf.sprintf "cat %s %s > %s && rm -f %s %s" f1 f2 f3 f1 f2)
;;

let rename f1 f2 = log "rename %s into %s ...\n%!" f1 f2; Sys.rename f1 f2;;

(* [string_of_file f] puts the contents of file [f] in a string. *)
let string_of_file f =
let ic = open_in f in
Expand All @@ -115,6 +87,36 @@ let write_val dump_file v =
output_value oc v;
close_out oc

(****************************************************************************)
(* Functions on strings. *)
(****************************************************************************)

let add_prefix prefix f x = prefix^f x;;

let concat_map f xs = String.concat "" (List.map f xs);;

let part i = "_part_" ^ string_of_int i;;

(* [get_part s suffix] returns [Some(n,k)] if [s=n^suffix^part(k)],
and [None] otherwise. *)
let get_part s suffix =
try
let len_s = String.length s in
let i = ref (len_s - 1) in
(* compute part number *)
let k =
while !i >= 0 && s.[!i] <> '_' do decr i done;
if !i < 0 then raise Exit;
int_of_string (String.sub s (!i+1) (len_s - 1 - !i))
in
(* compute theorem name *)
let len_suffix = String.length suffix + String.length "_part_" in
if !i < len_suffix then raise Exit;
let n = String.sub s 0 (!i - len_suffix + 1) in
Some(n,k)
with Exit -> None
;;

(* [replace c1 c2 s] returns a new string identical to [s] but with
every character [c1] replaced by [c2]. *)
let replace c1 c2 s =
Expand Down Expand Up @@ -159,6 +161,25 @@ let rec change_prefixes l s =
if starts_with p s then q ^ String.sub s n (String.length s - n)
else change_prefixes l s

(****************************************************************************)
(* Functions on lists. *)
(****************************************************************************)

(* [pos_first f l] returns the position (counting from 0) of the first
element of [l] satisfying [f]. Raises Not_found if there is no such
element. *)
let pos_first f =
let rec aux k l =
match l with
| [] -> raise Not_found
| y::l -> if f y then k else aux (k+1) l
in aux 0
;;

(****************************************************************************)
(* Functions on hash tables. *)
(****************************************************************************)

(* [bindings ht] returns the list of bindings in the hash table [ht]. *)
let bindings ht = Hashtbl.fold (fun x y acc -> (x,y)::acc) ht [];;
let sorted_bindings ht = List.sort Stdlib.compare (bindings ht);;
Expand Down