package lambdapi
Proof assistant for the λΠ-calculus modulo rewriting
Install
Dune Dependency
Authors
Maintainers
Sources
lambdapi-2.5.0.tbz
sha256=9bc8ae3694dd51bd5742e7aba760bd2878c4b0e5ef9b3d4a7b06f3cd303b611d
sha512=c812c3129b3d85b0c4d7e741d11137dbb4fe2a0aaba3a5968409080b742924ecb506280c19ad83ef6bc910346db96d87780313fa7683c29345edae16ae79c704
doc/src/lambdapi.lplib/extra.ml.html
Source file extra.ml
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105
(** Functional maps with [int] keys. *) module IntMap = Map.Make (Base.Int) (** Functional sets of integers. *) module IntSet = Set.Make (Base.Int) (** Functional maps with [string] keys. *) module StrMap = Map.Make (String) (** Functional sets of strings. *) module StrSet = Set.Make (String) (** [get_safe_prefix p strings] returns a string starting with [p] and so that there is no non-negative integer [k] such that [p ^ string_of_int k] belongs to [strings]. *) let get_safe_prefix : string -> StrSet.t -> string = fun head set -> let head_len = String.length head in let f s acc = let s_len = String.length s in if head_len <= s_len && String.equal head (String.sub s 0 head_len) then try let curr_int = int_of_string (String.sub s head_len (s_len - 1)) in if acc < curr_int then curr_int else acc with Failure _ -> acc else acc in let res = StrSet.fold f set (-1) in if res = -1 then head else head ^ string_of_int (res + 1) (** [time f x] times the application of [f] to [x], and returns the evaluation time in seconds together with the result of the application. *) let time : ('a -> 'b) -> 'a -> float * 'b = fun f x -> let t = Sys.time () in let r = f x in (Sys.time () -. t, r) (** Exception raised by the [with_timeout] function on a timeout. *) exception Timeout (** [with_timeout nbs f x] computes [f x] with a timeout of [nbs] seconds. The exception [Timeout] is raised if the computation takes too long, otherwise everything goes the usual way. *) let with_timeout : int -> ('a -> 'b) -> 'a -> 'b = fun nbs f x -> let sigalrm_handler = Sys.Signal_handle (fun _ -> raise Timeout) in let old_behavior = Sys.signal Sys.sigalrm sigalrm_handler in let reset_sigalrm () = let _ = Unix.alarm 0 in Sys.set_signal Sys.sigalrm old_behavior in try let _ = Unix.alarm nbs in let res = f x in reset_sigalrm (); res with e -> reset_sigalrm (); raise e (** [input_lines ic] reads the input channel [ic] line by line and returns its contents. The trailing newlines are removed in lines. The input channel is not closed by the function. *) let input_lines : in_channel -> string list = fun ic -> let lines = ref [] in try while true do lines := input_line ic :: !lines done; assert false with End_of_file -> List.rev !lines (** [run_process cmd] runs the command [cmd] and returns the list of the lines that it printed to its standard output (if the command was successful). If the command failed somehow, then [None] is returned. *) let run_process : string -> string list option = fun cmd -> let oc, ic, ec = Unix.open_process_full cmd (Unix.environment ()) in let res = input_lines oc in match Unix.close_process_full (oc, ic, ec) with | Unix.WEXITED 0 -> Some res | _ -> None (** [file_time fname] returns the modification time of file [fname] represented as a [float]. [neg_infinity] is returned if the file does not exist. *) let file_time : string -> float = fun fname -> if Sys.file_exists fname then Unix.((stat fname).st_mtime) else neg_infinity (** [more_recent source target] checks whether the [target] (produced from the [source] file) should be produced again. This is the case when [source] is more recent than [target]. *) let more_recent : string -> string -> bool = fun source target -> file_time source > file_time target (** [files f d] returns all the filenames in [d] and its sub-directories recursively satisfying the function [f], assuming that [d] is a directory. *) let files : (string -> bool) -> string -> string list = fun chk -> let rec files acc dirs = match dirs with | [] -> acc | d::dirs -> let f (fnames, dnames) s = let s = Filename.concat d s in if Sys.is_directory s then (fnames, s::dnames) else if chk s then (s::fnames, dnames) else (fnames, dnames) in let acc, dirs = Array.fold_left f (acc, dirs) (Sys.readdir d) in files acc dirs in fun d -> files [] [d]
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>