Ошибка сортировки по массе... не равна

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

Вы пытаетесь сравнить две функции. Компилятор предикатов не знает, что его можно рассматривать как "определяющее уравнение". В некотором смысле вы просите компилятор предикатов решить невозможную проблему.

Ваша жизнь будет намного проще, если foo_to_bar вместо этого определяется как функция (или простое определение). Это будет работать из коробки с генератором кода.