The Coq mailing list

[Dmitry Grebeniuk <gdsfh1 AT gmail.com>]

Hello.

>>   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.

  Thanks, but it's not needed: 1. I'll upgrade to 8.4 eventually,
2. rewritten code just works, 3. I'm not an aesthete.

> Agda has reflection (ie. you have access to the AST
> inside the language)

  Btw, it could be useful in Coq too, when "quote" tactic
is not enough.

> I do not know if you knew the term "section" for serialize and
> "retraction" for unserialize.
>
> http://en.wikipedia.org/wiki/Section_(category_theory)

  It's a happy coincidence that I know these terms.
  Also http://www.ncatlab.org/ is a good wiki to read about
category theory.  I'm using both wikipedia and ncatlab,
and choosing definition that is easier to understand
(as I am not a scientist).

>>     (* 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've looked at extracted code, found that it should be safe,
but was interesting to know opinion of coq-club members,
so I've asked here.

>>   Maybe I should write an axiomatized OrderedType on
>> ascii datatype, that uses OCaml Pervasives' eq/compare?
>
> That is a possibility, but in that case, do it directly for strings,
> skip the module for ascii.

  Good idea.

> Well in fact, I do not really advise use of Coq strings/ascii.

  There are many advantages in using CoqIde as ide for my
edsl, so I have to put up with Coq strings.

> Plus that means that you have no support for
> unicode in general, which becomes more and more useful
> in developers world.

  In an other Coq+OCaml project I'm using simple axioms
(implemented in OCaml) to work with unicode.  Not very
convenient, but possible, if everything you need from Coq
are extracted .ml files, and not a work with strings to
prove anything.

> 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.

  The set of strings is fixed at each developement step, but:
1. I'll have to modify constructors' set between steps,
2. Anyway I have to generate code with real strings.
  If there were any plugin/extension that could allow me to
automatize maintaining of "Inductive strings" and mapping
from this type to real strings, it would be cool.  But I have no
desire to write a Coq plugin.

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

> Inductive t := Q0 | Q1 | Q2 | Q3.

  I haven't thought about it.  Now I know this way to work
with ascii/strings, that's good.

  Thank you for the long and continuous help!