Commit d05676b3 authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan

[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.
parent 1a96b802
......@@ -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
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment