Wellsortedness 错误 ... 排序不相等

Question

这是从语言 foo 到 bar 的简单翻译器：

type_synonym vname = "string"
type_synonym 'a env = "vname ⇒ 'a option"

datatype foo_exp = FooBConst bool
datatype foo_type = FooBType | FooIType | FooSType

datatype bar_exp = BarBConst bool
datatype bar_type = BarBType | BarIType

fun foo_to_bar_type :: "foo_type ⇒ bar_type option" where
  "foo_to_bar_type FooBType = Some BarBType" |
  "foo_to_bar_type FooIType = Some BarIType" |
  "foo_to_bar_type _ = None"

inductive foo_to_bar :: "foo_type env ⇒ foo_exp ⇒ bar_type env ⇒ bar_exp ⇒ bool" where
"Γ⇩B = map_comp foo_to_bar_type Γ⇩F ⟹
 foo_to_bar Γ⇩F (FooBConst c) Γ⇩B (BarBConst c)"

code_pred [show_modes] foo_to_bar .

values "{t. foo_to_bar Map.empty (FooBConst True) Map.empty t}"

最后一行导致以下错误：

Wellsortedness error
(in code equation foo_to_bar_i_i_i_o ?x ?xa ?xb ≡
                  Predicate.bind (Predicate.single (?x, ?xa, ?xb))
                   (λ(Γ⇩F_, aa, Γ⇩B_).
                       case aa of
                       FooBConst c_ ⇒
                         Predicate.bind (eq_i_i Γ⇩B_ (foo_to_bar_type ∘⇩m Γ⇩F_))
                          (λ(). Predicate.single (BarBConst c_))),
with dependency "Pure.dummy_pattern" -> "foo_to_bar_i_i_i_o"):
Type char list ⇒ bar_type option not of sort equal
No type arity list :: enum

你能建议我如何解决吗？

还有 foo_to_bar 有模式 i => i => o => o => boolpos。我应该如何执行 values 来生成第 3 个和第 4 个参数？

Answer 1

一般来说，我建议不要使用 inductive 来定义可以轻松表示为函数的内容。虽然谓词编译器附带了很多花里胡哨的东西来使归纳定义具有计算意义，但由于它太复杂了，所以可能会出现很多问题。在你的情况下，问题出在行

Γ⇩B = map_comp foo_to_bar_type Γ⇩F

您正在尝试比较两个函数。谓词编译器不知道它可以被看作是 "defining equation"。从某种意义上说，您是在要求谓词编译器解决一个不可能的问题。

如果将 foo_to_bar 定义为函数（或简单定义），您的生活将会轻松得多。它将与代码生成器一起开箱即用。

Wellsortedness 错误 ... 排序不相等

Wellsortedness error ... not of sort equal

isabelle