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



Hi Peter,

the problem you have run into is ML's infamous value restriction (c.f.
http://users.cs.fiu.edu/~smithg/cop4555/valrestr.html).  There are at
least two ways to circumvent this problem:

* specialise the type to pt_ts to something monomorphic
* add a unit closure to pt_ts

Then everything should work fine.

Hope this helps,
	Florian

Peter Lammich schrieb:
> 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".
> *)
> 

Attachment: signature.asc
Description: OpenPGP digital signature



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