The Coq mailing list

[AUGER Cédric <sedrikov AT gmail.com>]

Le Sun, 3 Feb 2013 14:55:04 +0200,
Dmitry Grebeniuk 
<gdsfh1 AT gmail.com>
 a écrit :

> Hello.
> 
> > I did the following.
> 
>   And I've understood your code and rewrote it to Coq 8.3.
> The result is not very beautiful, I had to pass eq_refl to some
> matches, some tactics didn't solve the goals and so on.

Hmm, I can still try to improve your code to avoid the eq_refl tricks.

> Good reason to upgrade to 8.4, but I can't do it now.
> 
>   Good idea about tree.  Also useful for "unchecked
> exceptions" we've discussed on #coq about an year ago.

Yes, I immediately thought of that when I wrote this code.
I think it is a rather common trick along languages to deal bitwise
with complex structures. It looks a lot like Marshall in Ocaml, or JSon
(although I never used any of them). Agda has reflection (ie. you have
access to the AST inside the language), and so on… But it seems that in
Coq, not much effort has been done for that kind of thing.

> 
>   Nice that the code allows me to build OrderedType from
> almost any datastructure, writing only [un]serialize function.

and proving it correct! (unserialize∘serialize=id)

I do not know if you knew the term "section" for serialize and
"retraction" for unserialize.

http://en.wikipedia.org/wiki/Section_(category_theory)

> 
>   But one thing bothers me: extracted code for SAscii
> has comments:
> 
> module SAscii =
>  struct
> [...]
>   let serialize a =
>     (* If this appears, you're using Ascii internals. Please don't *)

I didn't thought of that. Well that occurs only if you import
ExtrOcamlStrings. But I think it is okay to use it, just that the code
is rather ugly, and not much efficient.

> 
>   I think I can use your code from CoqIde, but what should
> I do when I'll need to extract it?
>   Maybe I should write an axiomatized OrderedType on
> ascii datatype, that uses OCaml Pervasives' eq/compare?
> (now it's an easy task since you showed me the type that
> OrderedType modules should have.)

That is a possibility, but in that case, do it directly for strings,
skip the module for ascii.

You may also consider defining an ocaml array of "256 data", so that
serialize will be an access to this array.

>   Also maybe Ascii and ExtrOcamlString should have "lt"
> function for ascii characters?

Well in fact, I do not really advise use of Coq strings/ascii.
They are "wrong" in the sense that they are not well designed, and
suffer of many downsides. Plus that means that you have no support for
unicode in general, which becomes more and more useful in developers
world.

I do not know what exactly you need.

I mean, that if you work with a fixed set of strings, you can define a
type Inductive strings := String1 | String2 |…, and then work with it,
just that the printing will use a table to map each constructor to the
given string.

You can also define (in OCaml) a function of type "string → t list"
where t is a coq type similar to:

1. (if you want to really work with strings, ie. parse them and so on)

Inductive t :=
| Alpha : bool (*upper/lower case*) → alpha → t
| Dig : digit → t
| Sym : sym → t.

Inductive alpha := A | B | C | … | X | Y | Z. (*or a five bits record
to avoid big pattern matchings*)
Inductive digit := D0 | D1 | … | D8 | D9. (*or a 4 bits record,
allowing hexadecimal*)
Inductive sym := … (*all the symbols which can occur in your strings*)

or 2. (if you just want a way to have identifiers)

Inductive t := Q0 | Q1 | Q2 | Q3.
(* then an ascii is a list of 4 t; I use 4 just because it avoids a
lot of overhead with using bool, and pattern matching won't be too big*)

And then never use string/ascii in the ascii code, just t.
When you have a string, you first convert it in a "t list" and then
pass it to a Coq extracted function. The Coq part will be safe (and
even safer than tricking with "Extract Constant"). You just need the
usual extra-care when difining your "string → t list".
And of course, you also need a "t list → string", and check that when
given a valid string, converting it to a t list and reconverting it to
a string, you get the first string.