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

なぜ私はそのようなことをしたいのですか？私は、eg hereに似ているが有限localeのコンテキストで a を使用しています。グラフが有効かどうかのテストは簡単です。ここで、グラフ アルゴリズムのコードを Scala にエクスポートしたいと考えています。もちろん、コードは任意の有効なグラフで実行する必要があります。valid_graph

次のような Scala の例えを考えています。

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

2 に答える 2

2

これを解決する 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 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

I found a method, thanks to chris' tips.

Define a function to test the prerequisites/assumptions to instantiate a MyTest

definition "can_instance_MyTest L = distinct L"

The command term MyTest reveals that MyTest is of type string list => bool, this means that MyTest is a predicate that takes a parameter and tests if this parameter fulfills MyTest's assumptions. We introduce a code equation ([code]) that replaces MyTest with the executable instance tester. The code generator can now produce code for occurrences of e.g., 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 -

We yield (I replaced List[Char] with String for readability):

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)

More readable pseudo-code:

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

Now we need executable code for isInL. We utilize the predefined constant undefined. This code throws an exception if L is not distinct.

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 -

We yield:

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

We just need to show that the code_isInL is correct:

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 に答える