From d05676b344c7415e49e8a09cfcea8ef665fa43cb Mon Sep 17 00:00:00 2001 From: Jacques-Henri Jourdan Date: Sun, 4 Nov 2018 17:28:32 +0100 Subject: [PATCH] [Coq backend] Surjection without matching on int31 literal Instead, we convert the int31 to Z, and perform pattenr matching in Z. The reason for that change is that pattern-matching on int31 will disappear when native 63 bits integers will be introduced in Coq. --- src/coqBackend.ml | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/src/coqBackend.ml b/src/coqBackend.ml index 30035e58..605a811c 100644 --- a/src/coqBackend.ml +++ b/src/coqBackend.ml @@ -128,9 +128,11 @@ module Run (T: sig end) = struct write_optimized_int31 f k ); fprintf f "\n end;\n"; - fprintf f " surj := (fun n => match n return _ with "; + (* Pattern matching on int31 litterals will disappear when + native 63 bits integers will be introduced in Coq. *) + fprintf f " surj := (fun n => match Int31.phi n return _ with "; iteri (fprintf f "\n | %d => %s "); - fprintf f "\n | _ => %s\n end)%%int31;\n" (List.hd constrs); + fprintf f "\n | _ => %s\n end)%%Z;\n" (List.hd constrs); fprintf f " inj_bound := %d%%int31 }.\n" (List.length constrs); end else -- GitLab