Hello. I got a strange behavior when I was writing a Coq formatter. Here is a MRE.
(* bin/main.ml *)
exception NotImplemented
let pp_constr_expr CAst.{ v; loc = _ } =
match v with
| Constrexpr.CLambdaN _ -> raise NotImplemented
| Constrexpr.CLetIn _ -> raise NotImplemented
| Constrexpr.CAppExpl _ -> raise NotImplemented
| Constrexpr.CApp _ -> raise NotImplemented
| Constrexpr.CProj _ -> raise NotImplemented
| Constrexpr.CRecord _ -> raise NotImplemented
| Constrexpr.CCases _ -> raise NotImplemented
| Constrexpr.CLetTuple _ -> raise NotImplemented
| Constrexpr.CIf _ -> raise NotImplemented
| Constrexpr.CHole _ -> raise NotImplemented
| Constrexpr.CPatVar _ -> raise NotImplemented
| Constrexpr.CEvar _ -> ()
| Constrexpr.CSort _ -> raise NotImplemented
| _ -> raise NotImplemented
let pp_subast CAst.{ v = Vernacexpr.{ control = _; attrs = _; expr }; loc = _ }
=
match expr with
| VernacInductive
(Inductive_kw, [ (((NoCoercion, (_, None)), ([], None), Some ty, _), []) ])
->
pp_constr_expr ty
| _ -> raise NotImplemented
let pp_ast ast = List.hd ast |> pp_subast
let generate_from_code code =
let mode = Ltac_plugin.G_ltac.classic_proof_mode in
let entry = Pvernac.main_entry (Some mode) in
let parser = Gramlib.Stream.of_string code |> Pcoq.Parsable.make in
let rec f acc =
match Pcoq.Entry.parse entry parser with
| None -> List.rev acc
| Some ast -> f (ast :: acc)
in
f []
let _ = generate_from_code "Inductive foo:Type:=foo|bar." |> pp_ast
; bin/dune
(executable
(public_name coqfmt)
(name main)
(libraries coq-core.plugins.ltac)
(ocamlc_flags -g))
; dune-project
(lang dune 3.9)
(generate_opam_files true)
(package
(name coqfmt)
(depends coq-core dune ocaml))
When I run the program by OCAMLRUNPARAM=b dune exec bin/main.exe
, it fails with an exception raised by the CRef
branch.
%dune clean && OCAMLRUNPARAM=b dune exec bin/main.exe
Fatal error: exception Dune__exe__Main.NotImplemented
Raised at Dune__exe__Main.pp_constr_expr in file "bin/main.ml", line 7, characters 25-45
Called from Dune__exe__Main in file "bin/main.ml", line 45, characters 8-67
Then, removing the branch and running it again fails with the CLambdaN
branch, despite my expectation that it’d fall onto the last catch-all one.
%dune clean && OCAMLRUNPARAM=b dune exec bin/main.exe
Fatal error: exception Dune__exe__Main.NotImplemented
Raised at Dune__exe__Main.pp_constr_expr in file "bin/main.ml", line 7, characters 29-49
Called from Dune__exe__Main in file "bin/main.ml", line 44, characters 8-67
I thought this was a compiler bug at first, but now I’m not sure because I’m a beginner in OCaml, and actually I found a similar case where the cause turned out to be the evaluation order of a tuple.
I also found another related issue, but here another problem is that my code depends on coq-core
which is huge and makes it difficult to examine the actual cause.
Could anyone tell me if it is an expected behavior or a real compiler bug?
I tested the code with Ocaml 4.14.1 and 5.0.0, dune 3.9.2, and coq-core 8.17.1.