The Coq mailing list

[Hugo Herbelin <Hugo.Herbelin AT inria.fr>]

  Dear Vincent,
 
> I would like to manipulate strings in Coq as in any other
> language :
> 
> Definition s := "Hello".
> 
> Does there exist a formalization of strings in Coq and a pretty
> parsing and printing ?

  To my knowledge, there is currently no formalization of strings,
characters, and operations on strings. If somebody has time for it...

  If what you want is to extract program with strings then do as
follows. The following idea comes from Bruno Barras. I suppose he is
OK I show it to you (ask him for more details). The following sequence
of commands should work (you can do a macro, using the primitive
grammar prim:string to gather Parameter, ML Import and Link together,
see below).

    Require Extraction.

    Parameter ml_string : Set.
    ML Import Constant string == string : Set.
    Link ml_string := string.

    Parameter ml_my_first_string : ml_string.
    ML Import Constant "\"my first string\"" == my_first_string : string.
    Link ml_my_first_string := my_first_string.

    Parameter ml_my_second_string : ml_string.
    ML Import Constant "\"my second string\"" == my_second_string : string.
    Link ml_my_second_string := my_second_string.

    Then use ml_my_first_tring, ml_my_second_tring, etc in your development.


                                                  Hugo

----------------------------------------------------------------------
Macro for importing ML strings (for Coq V6.2)

Grammar vernac vernac :=
 def_string
 [ "DefString" prim:var($s) prim:var($mls) ":=" prim:string($str) "." ]
  -> [ (VERNACLIST
         <:vernac:< Parameter $s : ml_string. >>
         <:vernac:< ML Import Constant $str == $mls : string. >>
         <:vernac:< Link $s := $mls. >>) ].

(* This is not supported in V6.3; use "Time" instead of "VERNACLIST"
   (but this give execution time as an undesired side effect...) *)