From 0c28da26d0d120632b94e5834b9524eccd8fe3a9 Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Wed, 10 Apr 2024 16:15:47 +0100 Subject: [PATCH] Coq: warn that -grouped-regstate isn't supported here --- src/sail_coq_backend/sail_plugin_coq.ml | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/src/sail_coq_backend/sail_plugin_coq.ml b/src/sail_coq_backend/sail_plugin_coq.ml index 7527bf123..795283a69 100644 --- a/src/sail_coq_backend/sail_plugin_coq.ml +++ b/src/sail_coq_backend/sail_plugin_coq.ml @@ -231,8 +231,16 @@ let output libs files = ) files +let ignore_grouped_regstate () = + if !State.opt_type_grouped_regstate then begin + Reporting.simple_warn "-grouped-regstate option not supported in the Coq back-end, ignoring"; + State.opt_type_grouped_regstate := false + end + let coq_target _ _ out_file ast effect_info env = let out_file = match out_file with Some f -> f | None -> "out" in output !opt_libs_coq [(out_file, effect_info, env, ast)] -let _ = Target.register ~name:"coq" ~options:coq_options ~rewrites:coq_rewrites ~asserts_termination:true coq_target +let _ = + Target.register ~name:"coq" ~options:coq_options ~pre_parse_hook:ignore_grouped_regstate ~rewrites:coq_rewrites + ~asserts_termination:true coq_target