Email Gateway (Aug 18 2022 at 13:43): Email Gateway (Aug 18 2022 at 13:43):From: Peter Lammich <peter.lammich@uni-muenster.de>
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".
*)
Email Gateway (Aug 18 2022 at 13:43):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
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:
Then everything should work fine.
Hope this helps,
Florian
Peter Lammich schrieb:
signature.asc
Last updated: May 03 2024 at 08:18 UTC