package linksem
A formalisation of the core ELF and DWARF file formats written in Lem
Install
Dune Dependency
Authors
Maintainers
Sources
0.8.tar.gz
md5=2075c56715539b3b8f54ae65cc808b8c
sha512=f7c16e4036a1440a6a8d13707a43f0f9f9db0c68489215f948cc300b6a164dba5bf852e58f89503e9d9f38180ee658d9478156ca1a1ef64d6861eec5f9cf43d2
doc/src/linksem_zarith/error.ml.html
Source file error.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 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121
(*Generated by Lem from error.lem.*) open Lem_basic_classes open Lem_list open Lem_maybe open Lem_num open Lem_string open Show (** [error] is a type used to represent potentially failing computations. [Success] * marks a successful completion of a computation, whilst [Fail err] marks a failure, * with [err] as the reason. *) type 'a error = Success of 'a | Fail of string (** [return] is the monadic lifting function for [error], representing a successful * computation. *) (*val return : forall 'a. 'a -> error 'a*) let return r:'a error= (Success r) (*val with_success : forall 'a 'b. error 'a -> 'b -> ('a -> 'b) -> 'b*) let with_success err fl suc:'b= ((match err with | Success s -> suc s | Fail err -> fl )) (** [fail err] represents a failing computation, with error message [err]. *) (*val fail : forall 'a. string -> error 'a*) let fail err:'a error= (Fail err) (** [(>>=)] is the monadic binding function for [error]. *) (*val >>= : forall 'a 'b. error 'a -> ('a -> error 'b) -> error 'b*) let bind x f:'b error= ((match x with | Success s -> f s | Fail err -> Fail err )) (** [as_maybe e] drops an [error] value into a [maybe] value, throwing away * error information. *) (*val as_maybe : forall 'a. error 'a -> maybe 'a*) let as_maybe e:'a option= ((match e with | Fail err -> None | Success s -> Some s )) (*val of_maybe : forall 'a. string -> maybe 'a -> error 'a*) let of_maybe err_msg m:'a error= ((match m with | Some v -> Success v | None -> Fail err_msg )) (** [repeatM count action] fails if [action] is a failing computation, or * successfully produces a list [count] elements long, where each element is * the value successfully returned by [action]. *) (*val repeatM'' : forall 'a. natural -> error 'a -> error (list 'a) -> error (list 'a)*) let rec repeatM'' count action acc:('a list)error= (if Nat_big_num.equal count( (Nat_big_num.of_int 0)) then acc else repeatM'' ( Nat_big_num.sub_nat count( (Nat_big_num.of_int 1))) action ( bind acc (fun tail -> bind action (fun head -> return (head::tail))))) (*val repeatM : forall 'a. natural -> error 'a -> error (list 'a)*) let repeatM count action:('a list)error= (repeatM'' count action (return [])) (** [repeatM' count seed action] is a variant of [repeatM] that acts like [repeatM] * apart from any successful result returns a tuple whose second component is [seed] * and whose first component is the same as would be returned by [repeatM]. *) (*val repeatM' : forall 'a 'b. natural -> 'b -> ('b -> error ('a * 'b)) -> error ((list 'a) * 'b)*) let rec repeatM' count seed action:('a list*'b)error= (if Nat_big_num.equal count( (Nat_big_num.of_int 0)) then return ([], seed) else bind (action seed) (fun (head, seed) -> bind (repeatM' ( Nat_big_num.sub_nat count( (Nat_big_num.of_int 1))) seed action) (fun (tail, seed) -> return ((head::tail), seed)))) (** [mapM f xs] maps [f] across [xs], failing if [f] fails on any element of [xs]. *) (*val mapM' : forall 'a 'b. ('a -> error 'b) -> list 'a -> error (list 'b) -> error (list 'b)*) let rec mapM' f xs rev_acc:('b list)error= ((match xs with | [] -> bind rev_acc (fun rev_acc -> return (List.rev rev_acc)) | x::xs -> mapM' f xs ( bind rev_acc (fun tl -> bind (f x) (fun hd -> return (hd::tl)))) )) (*val mapM : forall 'a 'b. ('a -> error 'b) -> list 'a -> error (list 'b)*) let mapM f xs:('b list)error= (mapM' f xs (return [])) (** [foldM f e xs] performs a monadic right fold of [f] across [xs] using [e] * as the base case. Fails if any application of [f] fails. *) (*val foldM : forall 'a 'b. ('a -> 'b -> error 'a) -> 'a -> list 'b -> error 'a*) let rec foldM f e xs:'a error= ((match xs with | [] -> return e | x::xs -> bind (f e x) (fun res -> foldM f res xs) )) (** [string_of_error err] produces a string representation of [err]. *) (*val string_of_error : forall 'a. Show 'a => error 'a -> string*) let string_of_error dict_Show_Show_a e:string= ((match e with | Fail err -> "Fail: " ^ err | Success s -> dict_Show_Show_a.show_method s )) let instance_Show_Show_Error_error_dict dict_Show_Show_a:('a error)show_class= ({ show_method = (string_of_error dict_Show_Show_a)})
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>