[isabelle] Code Generator ML error: ... free type variable Found near val ...



Hi all,

I'm having trouble with the code generator of Isabelle 2009 (the one
invoked by export_code-keyword). I boiled it down to the following
example, where I try to export
a record to ML-code.
The code is generated, and I can also write it to a file. However, ML
does not accept the code, it sais:
    > Scratch.tree_struct_rec_ext_type includes a free type variable
Found near val 

What is the problem here? How to fix it?

Many thanks in advance,
  Peter

Attached is the theory where I get the error:

theory Scratch
imports Main
begin
record ('N,'L) tree_struct_rec =
  t_lab :: "'N \<Rightarrow> 'L"        -- "Label of a node"
  t_chn :: "'N \<Rightarrow> 'N list"   -- "Children of a node"

datatype ('P,'\<Gamma>,'L) ptree =
  PTNIL 'P '\<Gamma> |
  PTSPAWN 'L "('P,'\<Gamma>,'L) ptree" "('P,'\<Gamma>,'L) ptree"

datatype ('P,'\<Gamma>,'L) ptree_label =
  PTLNIL 'P '\<Gamma> |
  PTLSPAWN 'L

fun pt_lab where
  "pt_lab (PTNIL p \<gamma>) = PTLNIL p \<gamma>" |
  "pt_lab (PTSPAWN l _ _) = PTLSPAWN l"

fun pt_chn where
  "pt_chn (PTNIL p \<gamma>) = []" |
  "pt_chn (PTSPAWN l ts t) = [ts,t]"

definition "pt_ts == \<lparr> t_lab = pt_lab, t_chn = pt_chn \<rparr>"

export_code pt_lab pt_chn in SML
(* Works !*)

export_code pt_ts in SML
(*
*** Error: Type (('a, 'b, 'c) Scratch.ptree, ('a, 'b, 'c)
Scratch.ptree_label, unit)
*** Scratch.tree_struct_rec_ext_type includes a free type variable Found
near val
***    pt_ts :
***          (('a, 'b, 'c) Scratch.ptree, ('a, ...) Scratch.ptree_label,
unit)
***          Scratch.tree_struct_rec_ext_type
***       =
***       tree_struct_rec_ext(pt_lab)(pt_chn)(()) (line 21 of "generated
code")
*** Exception- Fail "Static errors (pass2)" raised
*** At command "export_code".
*)






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