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"

您会看到，除了您在原始定义中（在语言环境内）提供的单个参数之外，还有一个额外的参数（但只有 1 而不是 2，因为定义不依赖于B）。

Now, after your interpretation (since you did not explicitly provide a name, the constants of localTest will be in scope without qualifier) we have

term concatA

with output

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

That is, localTest.concatA ''a'' is already of type string => string. You additionally add ''b'' and obtain type string, but your type annotation says string => string. So there is really a clash of types and the reason was that you gave too many arguments to localTest.concatA. Try using

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

instead.

于 2013-03-10T04:09:00.477 回答