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です。第3引数と第4引数の両方を生成するためにvaluesを実行するにはどうすればよいですか？

Answer 1

一般に、inductiveを使用して、簡単に関数として表現できるものを定義することをお勧めします。述語コンパイラには帰納的定義の計算上の意味を理解するための多くの鐘と笛がありますが、それは非常に複雑なので多くの問題が発生します。あなたの場合、問題は行にあります

Γ⇩B = map_comp foo_to_bar_type Γ⇩F 

あなたは2つの機能を比較しようとしています。述語コンパイラは、それが「定義式」とみなされることは知らない。ある意味では、述語コンパイラには不可能な問題を解決するように求めています。

foo_to_barが関数（または単純な定義）として定義されていると、人生ははるかに簡単になります。これは、コードジェネレータを使って自由に動作します。