package linksem

  1. Overview
  2. Docs
A formalisation of the core ELF and DWARF file formats written in Lem

Install 

dune-project
 Dependency

github.com Edit opam file Versions (2)

Authors

  1. S
    Stephen Kell
  2. D
    Dominic Mulligan
  3. P
    Peter Sewell

Maintainers

  1. L
    Linksem Devs <cl-linksem-dev@lists.cam.ac.uk>

Sources

0.8.tar.gz
md5=2075c56715539b3b8f54ae65cc808b8c
sha512=f7c16e4036a1440a6a8d13707a43f0f9f9db0c68489215f948cc300b6a164dba5bf852e58f89503e9d9f38180ee658d9478156ca1a1ef64d6861eec5f9cf43d2

doc/linksem_zarith/Error/index.html

Module ErrorSource

Sourcetype 'a error =
  1. | Success of 'a
  2. | Fail of string

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.

Sourceval return : 'a -> 'a error

return is the monadic lifting function for error, representing a successful * computation.

Sourceval with_success : 'a error -> 'b -> ('a -> 'b) -> 'b
Sourceval fail : string -> 'a error

fail err represents a failing computation, with error message err.

Sourceval bind : 'a error -> ('a -> 'b error) -> 'b error

(>>=) is the monadic binding function for error.

as_maybe e drops an error value into a maybe value, throwing away * error information.

Sourceval as_maybe : 'a error -> 'a option
Sourceval of_maybe : string -> 'a option -> 'a error
Sourceval repeatM'' : Nat_big_num.num -> 'a error -> 'a list error -> 'a list error

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.

Sourceval repeatM : Nat_big_num.num -> 'a error -> 'a list error
Sourceval repeatM' : Nat_big_num.num -> 'b -> ('b -> ('a * 'b) error) -> ('a list * 'b) error

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.

Sourceval mapM' : ('a -> 'b error) -> 'a list -> 'b list error -> 'b list error

mapM f xs maps f across xs, failing if f fails on any element of xs.

Sourceval mapM : ('a -> 'b error) -> 'a list -> 'b list error
Sourceval foldM : ('a -> 'b -> 'a error) -> 'a -> 'b list -> 'a error

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.

Sourceval string_of_error : 'a Show.show_class -> 'a error -> string

string_of_error err produces a string representation of err.

Sourceval instance_Show_Show_Error_error_dict : 'a Show.show_class -> 'a error Show.show_class