package lambdapi
Proof assistant for the λΠ-calculus modulo rewriting
Install
Dune Dependency
Authors
Maintainers
Sources
lambdapi-2.6.0.tbz
sha256=d01e5f13db2eaba6e4fe330667149e0059d4886c651ff9d6b672db2dfc9765ed
sha512=33b68c972aca37985ed73c527076198e7d4961c7e27c89cdabfe4d1cff97cd41ccfb85ae9499eb98ad9a0aefd920bc55555df6393fc441ac2429e4d99cddafa8
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)"
>