0

codegenのドキュメント セクション「7.3 ロケールと解釈」によると、ロケールからのコードのエクスポートは少しトリッキーですが、実現可能です。次の例は正常に機能します。

locale localTest =
  fixes A :: "string"
begin
  fun concatA :: "string ⇒ string" where "concatA x = x@A"
  definition concatAA :: "string ⇒ string" where "concatAA x = x@A@A"
end

definition localtest_concatA :: "string ⇒ string " where
[code del]: "localtest_concatA = localTest.concatA ''a''"
definition localtest_concatAA :: "string ⇒ string " where
[code del]: "localtest_concatAA = localTest.concatAA ''a''"

interpretation localTest "''a''"
  where "localTest.concatA ''a'' = localtest_concatA"
  and "localTest.concatAA ''a'' = localtest_concatAA"
  apply unfold_locales
  apply(simp_all add: localtest_concatA_def localtest_concatAA_def)
  done

export_code localtest_concatA localtest_concatAA in Scala file -

複数のパラメーターを持つロケールのコードをエクスポートするにはどうすればよいですか? 以下を考えるとlocale：

locale localTest =
  fixes A :: "string"
  fixes B :: "string"
begin
  fun concatA :: "string ⇒ string" where "concatA x = x@A"
  definition concatB :: "string ⇒ string" where "concatB x = x@B"
end

私はそれを解釈することができます

interpretation localTest "''a''" "''b''" .

しかし、この解釈を定義に使用することはできません

definition localtest_concatA :: "string ⇒ string " where
[code del]: "localtest_concatA = localTest.concatA ''a'' ''b''"

で失敗します

Type unification failed: Clash of types "_ list" and "_ ⇒ _"

Type error in application: incompatible operand type

Operator:  op = localtest_concatA :: (char list ⇒ char list) ⇒ bool
Operand:   localTest.concatA ''a'' ''b'' :: char list
4

1 に答える 1

2

たとえば、termコマンドによって、導入された定数を調べます。我々は持っています

term localTest.concatA

出力あり

"localTest.concatA" :: "char list ⇒ char list ⇒ char list"

元の定義 (ロケール内) で指定した単一のパラメーターに加えて、追加のパラメーターがあることがわかります (ただし、定義は に依存していないため、2 ではなく 1 のみBです)。

さて、あなたの解釈の後（名前を明示的に指定しなかったため、の定数はlocalTest修飾子なしでスコープ内になります）

term concatA

出力あり

"localTest.concatA ''a''" :: "char list ⇒ char list"

つまり、localTest.concatA ''a''すでに 型string => stringです。さらに type を追加''b''して取得stringしますが、型注釈には と書かれていますstring => string。したがって、実際には型の衝突があり、その理由は に与えた引数が多すぎるためlocalTest.concatAです。使ってみて

definition localtest_concatA :: "string ⇒ string " where
  [code del]: "localtest_concatA = concatA

代わりは。

于 2013-03-10T04:09:00.477 に答える