Source file protect.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
module Error = struct
  type 'l payload = 'l option * Pp.t

  type 'l t =
    | User of 'l payload
    | Anomaly of 'l payload

  let map ~f = function
    | User e -> User (f e)
    | Anomaly e -> Anomaly (f e)
end

module R = struct
  type ('a, 'l) t =
    | Completed of ('a, 'l Error.t) result
    | Interrupted (* signal sent, eval didn't complete *)

  let error e = Completed (Error (Error.User (None, e)))

  let map ~f = function
    | Completed (Result.Ok r) -> Completed (Result.Ok (f r))
    | Completed (Result.Error r) -> Completed (Result.Error r)
    | Interrupted -> Interrupted

  let map_error ~f = function
    | Completed (Error e) -> Completed (Error (Error.map ~f e))
    | Completed (Ok r) -> Completed (Ok r)
    | Interrupted -> Interrupted

  let map_loc ~f =
    let f (loc, msg) = (Option.map f loc, msg) in
    map_error ~f
end

(* Eval and reify exceptions *)
let eval_exn ~token ~f x =
  match Limits.limit ~token ~f x with
  | Ok res -> R.Completed (Ok res)
  | Error _ ->
    Vernacstate.invalidate_cache ();
    R.Interrupted
  | exception exn ->
    let e, info = Exninfo.capture exn in
    let loc = Loc.(get_loc info) in
    let msg = CErrors.iprint (e, info) in
    Vernacstate.invalidate_cache ();
    if CErrors.is_anomaly e then R.Completed (Error (Anomaly (loc, msg)))
    else R.Completed (Error (User (loc, msg)))

let _bind_exn ~f x =
  match x with
  | R.Interrupted -> R.Interrupted
  | R.Completed (Error e) -> R.Completed (Error e)
  | R.Completed (Ok r) -> f r

let fb_queue : Loc.t Message.t list ref = ref []

module E = struct
  type ('a, 'l) t =
    { r : ('a, 'l) R.t
    ; feedback : 'l Message.t list
    }

  let eval ~token ~f x =
    let r = eval_exn ~token ~f x in
    let feedback = List.rev !fb_queue in
    let () = fb_queue := [] in
    { r; feedback }

  let map ~f { r; feedback } = { r = R.map ~f r; feedback }
  let map_message ~f (loc, lvl, msg) = (Option.map f loc, lvl, msg)

  let map_loc ~f { r; feedback } =
    { r = R.map_loc ~f r; feedback = List.map (map_message ~f) feedback }

  let bind ~f { r; feedback } =
    match r with
    | R.Interrupted -> { r = R.Interrupted; feedback }
    | R.Completed (Error e) -> { r = R.Completed (Error e); feedback }
    | R.Completed (Ok r) ->
      let { r; feedback = fb2 } = f r in
      { r; feedback = feedback @ fb2 }

  let ok v = { r = Completed (Ok v); feedback = [] }
  let error err = { r = R.error err; feedback = [] }

  module O = struct
    let ( let+ ) x f = map ~f x
    let ( let* ) x f = bind ~f x
  end
end

(* Eval with reified exceptions and feedback *)
let eval ~token ~f x = E.eval ~token ~f x