I’m having a hard time extracting ascii and strings into ocaml without exposing the ascii internal representation, in particular in a match expression that is matching over ascii characters. Should I replace the matches with if then else clauses? That is really inconvenient for my purposes.
Here’s a simple example of the kind of thing that I’m doing.
Require Extraction.
Require Import Coq.extraction.ExtrOcamlString Coq.extraction.ExtrOcamlNatInt Coq.extraction.ExtrOcamlZInt.
Definition check_a_b_c (x : ascii) : option ascii :=
match x with
| "a"%char => Some "a"%char
| "b"%char => Some "b"%char
| "c"%char => Some "c"%char
| _ => None
end.
Extraction check_a_b_c.
Extracts to
let check_a_b_c x =
(* If this appears, you're using Ascii internals. Please don't *)
(fun f c ->
let n = Char.code c in
let h i = (n land (1 lsl i)) <> 0 in
f (h 0) (h 1) (h 2) (h 3) (h 4) (h 5) (h 6) (h 7))
(fun b b0 b1 b2 b3 b4 b5 b6 ->
if b
then if b0
then if b1
then None
else if b2
then None
else if b3
then None
else if b4
then if b5
then if b6 then None else Some 'c'
else None
else None
else if b1
then None
else if b2
then None
else if b3
then None
else if b4
then if b5
then if b6 then None else Some 'a'
else None
else None
else if b0
then if b1
then None
else if b2
then None
else if b3
then None
else if b4
then if b5
then if b6 then None else Some 'b'
else None
else None
else None)
x
Any suggestions? Thanks