Stream: Miscellaneous

Topic: fancy exception modules


view this post on Zulip Gaëtan Gilbert (Jul 13 2020 at 09:10):

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

view this post on Zulip Emilio Jesús Gallego Arias (Jul 13 2020 at 14:22):

@Gaëtan Gilbert did you see https://github.com/coq/coq/pull/12602 ?

view this post on Zulip Emilio Jesús Gallego Arias (Jul 13 2020 at 14:22):

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: Aug 19 2022 at 21:02 UTC