从语言环境生成代码而无需解释 [英] Generating code from locales without interpretation

问题描述

我希望直接从区域设置定义生成代码，而无需进行解释。示例：

I would love to generate code from locale definitions directly, without interpretation. Example:

(* A locale, from the code point of view, similar to a class *)
locale MyTest =
  fixes L :: "string list"
  assumes distinctL: "distinct L"
  begin
    definition isInL :: "string => bool" where
      "isInL s = (s ∈ set L)"
  end

实例化 MyTest 是可执行文件，我可以为其生成代码

The assumptions to instantiate MyTest are executable and I can generate code for them

definition "can_instance_MyTest L = distinct L"  
lemma "can_instance_MyTest L = MyTest L"
  by(simp add: MyTest_def can_instance_MyTest_def)
export_code can_instance_MyTest in Scala file -

我可以定义一个函数，对任意 MyTest执行 isInL 定义。

I can define a function to execute the isInL definition for arbitrary MyTest.

definition code_isInL :: "string list ⇒ string ⇒ bool option" where
"code_isInL L s = (if can_instance_MyTest L then Some (MyTest.isInL L s) else None)"

lemma "code_isInL L s = Some b ⟷ MyTest L ∧ MyTest.isInL L s = b"
  by(simp add: code_isInL_def MyTest_def can_instance_MyTest_def)

但是，代码导出失败：

export_code code_isInL in Scala file -
No code equations for MyTest.isInL

为什么要这样做事情？
我在 valid_graph 的上下文中使用区域设置，例如此处但有限。测试图形是否有效很容易。现在，我想将图形算法的代码导出到Scala中。当然，代码应该在任意有效的图形上运行。

Why do I want to do such a thing? I'm working with a locale in the context of a valid_graph similar to e.g. here but finite. Testing that a graph is valid is easy. Now I want to export the code of my graph algorithms into Scala. Of course, the code should run on arbitrary valid graphs.

我在考虑类似这样的Scala类：

I'm thinking of the Scala analogy similar to something like this:

class MyTest(L: List[String]) {
require(L.distinct)
def isInL(s: String): Bool = L contains s
}

推荐答案

解决的方法是使用不变量精炼数据类型（请参见 isabelle doc codegen 第3.3节）。因此，可以将有效性假设（在您的情况下为 distinct L ）转移到新类型中。考虑下面的示例：

One way to solve this is datatype refinement using invariants (see isabelle doc codegen section 3.3). Thereby the validity assumption (distinct L, in your case) can be moved into a new type. Consider the following example:

typedef 'a dlist = "{xs::'a list. distinct xs}"
morphisms undlist dlist
proof
  show "[] ∈ ?dlist" by auto
qed

这定义了一个新类型，其元素都是具有不同元素的列表。我们必须为代码生成器显式设置这种新类型。

This defines a new type whose elements are all lists with distinct elements. We have to explicitly set up this new type for the code generator.

lemma [code abstype]: "dlist (undlist d) = d"
  by (fact undlist_inverse)

然后，在语言环境中我们有一个假设免费（因为新类型的每个元素都可以保证；但是，在某些时候，我们必须将基本操作集从具有不同元素的列表中提升到'a dlist s）。

Then, in the locale we have the assumption "for free" (since every element of the new type guarantees it; however, at some point we have to lift a basic set of operations from lists with distinct element to 'a dlists).

locale MyTest =
  fixes L :: "string dlist"
begin
  definition isInL :: "string => bool" where
    "isInL s = (s ∈ set (undlist L))"
end

至此，我们可以将（无条件的）方程式提供给代码生成器。

At this point, we are able to give (unconditional) equations to the code generator.

lemma [code]: "MyTest.isInL L s ⟷ s ∈ set (undlist L)"
  by (fact MyTest.isInL_def)

export_code MyTest.isInL in Haskell file -

这篇关于从语言环境生成代码而无需解释的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！