Source file `failure.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
open Ppxlib
open Ortac_core.Builder

let eterm t = estring t

let term_kind kind =
  (match kind with
  | `Check -> "Check"
  | `Pre -> "Pre"
  | `Post -> "Post"
  | `XPost -> "XPost"
  | `Invariant -> "Invariant")
  |> lident
  |> fun c -> pexp_construct c None

let register ~register_name e =
  [%expr [%e e] |> Ortac_runtime.Errors.register [%e register_name]]

let violated_condition kind ~term ~register_name =
  let kind = term_kind kind in
  [%expr
    Ortac_runtime.Violated_condition
      { term = [%e eterm term]; term_kind = [%e kind] }]
  |> register ~register_name

let violated_invariant kind ~term ~register_name =
  [%expr
    Ortac_runtime.Violated_invariant
      { term = [%e eterm term]; position = [%e kind] }]
  |> register ~register_name

let violated_axiom ~register_name =
  register ~register_name [%expr Ortac_runtime.Violated_axiom]

let axiom_failure ~exn ~register_name =
  [%expr Ortac_runtime.Axiom_failure { exn = [%e exn] }]
  |> register ~register_name

let invariant_failure kind ~term ~exn ~register_name =
  [%expr
    Ortac_runtime.Specification_failure
      { term = [%e eterm term]; term_kind = [%e kind]; exn = [%e exn] }]
  |> register ~register_name

let spec_failure kind = invariant_failure (term_kind kind)

let unexpected_exn ~allowed_exn ~exn ~register_name =
  let allowed_exn = List.map estring allowed_exn |> elist in
  [%expr
    Ortac_runtime.Unexpected_exception
      { allowed_exn = [%e allowed_exn]; exn = [%e exn] }]
  |> register ~register_name

let uncaught_checks ~term ~register_name =
  [%expr Ortac_runtime.Uncaught_checks { term = [%e eterm term] }]
  |> register ~register_name

let unexpected_checks ~register_name =
  (* let terms = List.map eterm terms |> elist in *)
  [%expr Ortac_runtime.Unexpected_checks { terms = [] }]
  |> register ~register_name

let report ~register_name =
  [%expr Ortac_runtime.Errors.report [%e register_name]]