[isabelle] String.explode in generated code

Dear all,

In Isabelle2009-2, the code generator translated the theory String into the module Stringa. In Isabelle2011, it uses String. Consequently, the SML translations in HOL/Library/Code_Char for String.implode and String.explode to String.implode and String.explode no longer refer to ML's built-in implode and explode functions, but are captured by the new String module, which does not declare such functions. Consequently, PolyML 5.4 rejects generated code that uses String.implode and String.explode.

Surprisingly, with the @{code} antiquotation, everything seems to work fine.
Here's a small example:

theory Test imports Main Code_Char begin
definition foo where "foo = String.explode (STR ''abc'')"
export_code foo in SML file "test.ML"
ML {* @{code foo} *}

If I adjust the translation to

code_const explode (SML "explode")

then the raw polyml accepts the code produced by export_code, but the antiquotation no longer works.

What do I have to do such that both work?


Karlsruher Institut für Technologie
IPD Snelting

Andreas Lochbihler
wissenschaftlicher Mitarbeiter
Adenauerring 20a, Geb. 50.41, Raum 023
76131 Karlsruhe

Telefon: +49 721 608-48352
Fax: +49 721 608-48457
E-Mail: andreas.lochbihler at kit.edu
KIT - Universität des Landes Baden-Württemberg und nationales Forschungszentrum in der Helmholtz-Gemeinschaft

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.