從沒有解釋的語言環境生成代碼

Question

我希望直接從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 

爲什麼我想要做這樣的事情？ 我在valid_graph的環境中與locale一起工作，類似於例如here但有限。測試一個圖是否有效很容易。現在我想將我的圖算法的代碼導出到Scala中。當然，代碼應該在任意有效的圖上運行。

我想斯卡拉比喻像這樣類似的事情：要解決這是使用不變量的數據類型細化

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

Answer 1

的一種方式（見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 dlist s）。

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 - 

Answer 2

由於chris的提示，我找到了一種方法。

定義一個函數來測試的先決條件/假設實例化一個MyTest

definition "can_instance_MyTest L = distinct L" 

命令term MyTest表明MyTest是string list => bool類型， 的這意味着MyTest是採用如果一個參數和測試謂詞這個參數滿足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)