package smtml

  1. Overview
  2. Docs
An SMT solver frontend for OCaml

Install 

dune-project
 Dependency

github.com Readme Changelog Edit opam file Versions (15)

Authors

  1. J
    João Pereira <joaomhmpereira@tecnico.ulisboa.pt>
  2. F
    Filipe Marques <filipe.s.marques@tecnico.ulisboa.pt>
  3. H
    Hichem Rami Ait El Hara <hra@ocamlpro.com>
  4. R
    redianthus <redopam@pm.me>
  5. A
    Arthur Carcano <arthur.carcano@ocamlpro.com>
  6. P
    Pierre Chambart <pierre.chambart@ocamlpro.com>
  7. J
    José Fragoso Santos <jose.fragoso@tecnico.ulisboa.pt>

Maintainers

  1. F
    Filipe Marques <filipe.s.marques@tecnico.ulisboa.pt>

Sources

v0.20.0.tar.gz
md5=25a38c1470173f0214ea3c33e665998c
sha512=bc7c921dd307d5673154c47e00aa3b124621f8651f22ad86ff80cf02eb2aca201ae93a4172e9bb591d1891d5e6a5b9b5649466cf65b456464d98b8544a8b7932

doc/src/smtml.prelude/smtml_prelude.ml.html

Source file smtml_prelude.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
(* SPDX-License-Identifier: MIT *)
(* Copyright (C) 2023-2024 formalsec *)
(* Written by the Smtml programmers *)

include Prelude

module String = struct
  include String

  let hash x = String_hash.seeded_hash 0 x
end

module Int32 = struct
  include Int32

  (* As they are defined in the stdlib *)
  let hash x = Hashtbl.seeded_hash_param 10 100 0 x
end

module Int64 = struct
  include Int64

  (* As they are defined in the stdlib *)
  let hash x = Hashtbl.seeded_hash_param 10 100 0 x
end

module Option = struct
  include Option

  module Syntax = struct
    let ( let* ) v f = bind v f

    let ( let+ ) v f = map f v
  end
end

module Result = struct
  include Result

  module Syntax = struct
    let ( let* ) v f = Result.bind v f

    let ( let+ ) v f = Result.map f v
  end

  let rec list_iter f =
    let open Syntax in
    function
    | [] -> Ok ()
    | hd :: tl ->
      let* () = f hd in
      list_iter f tl

  let list_map f v =
    let open Syntax in
    let rec list_map_cps f v k =
      match v with
      | [] -> k (Ok [])
      | hd :: tl ->
        list_map_cps f tl (fun rest ->
          let* rest in
          let* hd' = f hd in
          k (Ok (hd' :: rest)) )
    in
    list_map_cps f v Fun.id

  let list_filter_map f v =
    let open Syntax in
    let rec list_filter_map_cps f v k =
      match v with
      | [] -> k (Ok [])
      | hd :: tl ->
        list_filter_map_cps f tl (fun rest ->
          let* rest in
          let* v = f hd in
          k (Ok (match v with None -> rest | Some v -> v :: rest)) )
    in
    list_filter_map_cps f v Fun.id
end