package linksem

  1. Overview
  2. Docs
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

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)})
OCaml

Innovation. Community. Security.