Re: [isabelle] Code Generation with Locales that Fix Type Parameters



3. You use one of Peter Lammich's tools from Autoref or Monadic
> Refinement Framework thatÂ
> automates step 2. He can tell you more about this.

Unfortunately, the Locale_Code tool Andreas probably refers to does not
work for this particular case.Â

This tool was specifically developed for the needs of the Isabelle
Collection Framework. It's a workaround, and after being told that this
hack is of no general interest as it should be done properly, I did not
invest more work to make it usable in more general cases.

Anyway, 5 years later, the problem of generating code from locale
interpretations *without* writing tons of boilerplate seems still not
solved.

So again, here the idea of my hack:

Before and after interpreting a locale, record the existing Spec_Rules.
After interpreting the locale, make a diff to find the new spec rules,
and process them to automatically set up new code equations.

However, as far as I can remember, the current implementation only
declares new code equations, without defining new constants.Â

SeeÂ"$AFP/Collections/ICF/tools/Locale_Code_Ex" and the Isabelle
Collection Framework for examples where it actually works and the three
linesÂ

setup Locale_Code.open_block
interpretation ...
setup Locale_Code.close_block

declare dozens of code theorems, thus saving dozens of boilerplate declarations as would be required for method 1 or 2.

--
 Peter




> 
> Hope this helps,
> Andreas
> 
> On 16/02/17 14:55, Brandon Bohrer wrote:
> > 
> > Hello All,
> > 
> > I've been trying to generate code for functions that are defined
> > inside a
> > locale, but Isabelle is refusing and the error suggests it is
> > related to
> > the type variables fixed by my locale. Here is a toy example of the
> > problem:
> > 
> > theory "Codegen_Example"
> > Â imports Complex_Main
> > begin
> > Â locale Foo =
> > Â fixes x::"'type_param::finite"
> > Â fixes y::"'type_param::finite"
> > 
> > context Foo begin
> > fun test1 :: "int \<Rightarrow> int" where
> > Â "test1 n = n"
> > 
> > fun test2 :: "'a \<Rightarrow> 'a" where
> > Â "test2 n = n"
> > 
> > fun test3 :: "int \<Rightarrow> 'type_param \<Rightarrow> int"
> > where
> > Â "test3 n _= n"
> > end
> > 
> > interpretation bb: Foo Enum.finite_2.a\<^sub>1
> > Enum.finite_2.a\<^sub>2
> > done
> > 
> > (* Works *)
> > export_code "bb.test1" in SML
> > export_code "bb.test2" in SML
> > 
> > (* Does Not Work*)
> > export_code "bb.test3" in SML
> > end
> > 
> > The last "export_code" line gives the error:
> > 
> > Type
> > int â Enum.finite_2 â int
> > of constant "Codegen_Example.Foo.test3"
> > is too specific compared to declared type
> > int â ?'type_param::{} â int
> > 
> > I don't understand this error, because generating code for a
> > specific
> > instance 'type_param = Enum.finite_2 seems like something that
> > ought to
> > work (and Enum.finite_2 supports the finite typeclass).
> > 
> > Does anyone know a way to convince Isabelle to generate code in
> > such a
> > situation (or fix my confusion as to why this is not supported?).
> > It would
> > actually be more convenient in my case to generate polymorphic code
> > instead
> > of fixing 'type_param = Enum.finite_2, but of course that's
> > cheating in the
> > sense that SML knows nothing about the finite typeclass thus cannot
> > enforce
> > it.
> > 
> > Incidentally, in the real code, the reason for fixing the type
> > parameters
> > like this are (1) I use the assumption 'type_param::finite very
> > frequently
> > and it's nicer to only write it down once and (2) I frequently
> > construct
> > values based on x and y (and a number of other arguments) so it
> > would be
> > quite unwieldy if they were not locale parameters.
> > 
> > Thanks in advance,
> > Brandon
> > 




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