我希望直接從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
}
使用2月12日CODEGEN-DOC 2013年的版本,第3.3節不非常容易理解(並且從第一句話中的錯字開始......)。 – corny 2013-03-19 23:37:46
'morphisms undlist dlist'做什麼? – corny 2013-03-19 23:41:18
檢查生成的代碼,我可以自由創建一個不明顯的'dlist',並將它傳遞給'isInL'。這怎麼能被阻止?在我最初的例子中,代碼在執行'isInL'之前測試了獨特性。 – corny 2013-03-19 23:55:23