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



Hi Brandon,

code_pred does not work inside the locale, but you can use it with global_interpretation. Here's an example:

locale l = fixes x :: 'a assumes "x = x"
inductive (in l) is_x where "is_x x"
global_interpretation i: l "0 :: nat" defines i_is_x = "i.is_x" by unfold_locales simp

declare i.is_x.intros[code_pred_intro]
code_pred i_is_x by(rule i.is_x.cases)
thm i_is_x.equation

The crucial line is the re-declaration of the intro rules.

Hope this helps,
Andreas

On 21/02/17 15:31, Brandon Bohrer wrote:
Hi Andreas,

Thank you for such a detailed response! Solution #2 got export_code to work (my locale has
assumptions, so #1 was not an option). I don't mind the boilerplate code so long as it works.

My locale also has some inductive predicates for which I would like to generate code. Am I
correct that the predicate compiler doesn't work inside locales that have assumptions? The
following thread seems to suggest so:
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2017-January/msg00063.html

If that's the case, it shouldn't be too hard to turn all my predicates into functions. It
just looks cleaner when they're written as inductive predicates, so it would be nice if
code generation for predicates happens to work.

On Fri, Feb 17, 2017 at 7:02 AM, Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch
<mailto:andreas.lochbihler at inf.ethz.ch>> wrote:

    Dear Brandon,

    The underlying reason is not related to type classes. It is simply that you must do
    some work to get the code generator work on interpretations of locales. You have three
    options:

    1. Export the code for the general constant Foo.test3 after having re-declared the
    code equations on the theory level:

    lemmas [code] = Foo.test1.simps Foo.test2.simps Foo.test3.simps

    export_code Foo.test3 in SML

    In addition, if you want to get the specialisation for the interpretation, you must
    define a constant instead of the abbreviation:

    definition "bb_test3 = bb.test3"
    export_code bb_test3 in SML

    This option works only if your locale does not contain or inherit any "assumes" parts.


    2. You define at the time of interpretation new constants for all the terms you ever
    want to execute. You must use global_interpretation instead of interpretation.

    global_interpretation bb: Foo Enum.finite_2.aâ1 Enum.finite_2.aâ2
      defines bb_test1 = bb.test1
        and bb_test2 = bb.test2
        and bb_test3 = bb.test3


    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.

    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.