some fancy modules to declare exceptions together with a printer
doing it with modules lets us access the exception by whatever name we want
probably too verbose to be useful
module type A = sig
type contents
val pp : contents -> string
end
module type X = sig
type contents
exception E of contents
end
module type B = sig
type contents
module type T
module Mk : functor (X:X with type contents := contents) -> T
end
module F (A:A) (B:B with type contents := A.contents) () : B.T =
B.Mk(struct
exception E of A.contents
let () = Printexc.register_printer (function
| E c -> Some (A.pp c)
| _ -> None)
end)
(* usage *)
module EE = F (struct type contents = int let pp i = "hello " ^ string_of_int i end)
(struct
module type T = sig exception BadInt of int end
module Mk(X:X with type contents := int) = struct exception BadInt = X.E end
end)
()
let raise_badint i = raise (EE.BadInt i)
let () = raise_badint 0
@Gaëtan Gilbert did you see https://github.com/coq/coq/pull/12602 ?
I don't find that approach verbose, main problem I'm stuck with that one is that some exceptions ought to carry a decoration [sigma / env for example] so the layering is a bit tricky to organize
Last updated: Sep 30 2023 at 17:01 UTC