0

我很想locale直接从定义中生成代码，而不需要解释。例子：

(* 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是可执行的，我可以为它们生成代码

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 -

我可以定义一个函数来执行isInL任意的定义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

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

我正在考虑类似于这样的 Scala 类比：

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

2 回答 2

2

解决这个问题的一种方法是使用不变量进行数据类型细化（参见isabelle doc codegen第 3.3 节）。因此，可以将有效性假设（distinct L在您的情况下为 ）移至新类型。考虑以下示例：

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

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

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

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

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

在这一点上，我们可以给代码生成器（无条件）方程。

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

export_code MyTest.isInL in Haskell file -
于 2013-03-10T04:59:22.990 回答
0

多亏了克里斯的提示，我找到了一种方法。

定义一个函数来测试先决条件/假设以实例化一个MyTest

definition "can_instance_MyTest L = distinct L"

该命令term MyTest显示MyTest是 type string list => bool，这意味着 thatMyTest是一个谓词，它接受一个参数并测试该参数是否满足MyTest的假设。我们引入了一个代码方程 ( [code])，它用MyTest可执行实例测试器代替。代码生成器现在可以为出现的情况生成代码，例如，MyTest [a,b,c]

lemma [code]: "MyTest = can_instance_MyTest"
  by(simp add:fun_eq_iff MyTest_def can_instance_MyTest_def)

export_code MyTest in Scala file -

我们屈服（为了可读性，我替换List[Char]为String）：

def can_instance_MyTest[A : HOL.equal](l: List[A]): Boolean =
  Lista.distinct[A](l)

def myTest: (List[String]) => Boolean =
  (a: List[String]) => can_instance_MyTest[String](a)

更易读的伪代码：

def myTest(l: List[String]): Boolean = l.isDistinct

现在我们需要isInL. 我们利用预定义的常量undefined。L如果不是不同的，此代码将引发异常。

definition code_isInL :: "string list ⇒ string ⇒ bool" where
"code_isInL L s = (if can_instance_MyTest L then s ∈ set L else undefined)"

export_code code_isInL in Scala file -

我们产生：

def code_isInL(l: List[String], s:String): Boolean =
  (if (can_instance_MyTest[String](l)) Lista.member[String](l, s)
    else sys.error("undefined"))*)

我们只需要证明code_isInL是正确的：

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


(* Unfortunately, the other direction does not hold. The price of undefined. *)
lemma "¬ MyTest L  ⟹ code_isInL L s = undefined"
  by(simp add: code_isInL_def can_instance_MyTest_def MyTest_def)
于 2013-03-20T00:50:31.487 回答