code_predと値の使い方は？

Question

Tobias NipkowとGerwin Klein、第7.2.2節の「具体的セマンティクス」にcode_predの使用例があります。

私は例をもとに、簡単な言語を実装していると私は式の値を計算してみてください。

theory BooLang 
    imports Main 
begin 

type_synonym id = string 
type_synonym 'a Env = "id ⇒ 'a" 

datatype BooBoolExp = 
    BooLiteralExp bool | 
    BooLetExp id BooBoolExp BooBoolExp | 
    BooVarExp id | 
    BooAndExp BooBoolExp BooBoolExp 

datatype BooVal = Bv bool 

type_synonym BooEnv = "BooVal Env" 

inductive tbooval :: "BooBoolExp × BooEnv ⇒ BooVal ⇒ bool" (infix "⇒" 55) where 
    Literal: "(BooLiteralExp b, env) ⇒ Bv b" | 
    And: "⟦(a, env) ⇒ Bv av; (b, env) ⇒ Bv bv⟧ ⟹ (BooAndExp a b, env) ⇒ Bv (av ∧ bv)" | 
    Var: "(BooVarExp v, env) ⇒ env v" | 
    Let: "⟦(val, env) ⇒ b; (body, env(v := b)) ⇒ x⟧ ⟹ (BooLetExp v val body, env) ⇒ x" 

code_pred tbooval . 

values "{t. True}" 

values "{t. (BooLiteralExp true, λ_. Bv false) ⇒ t}" 

end 

しかし、第一の値の呼び出しのために、私はエラーを取得する：「値の評価が可能ではありませんcode_predでのコンパイルが呼び出されなかったため "です。

2番目のエラーについては、「理解不可能なモードはありません{t。（BooLiteralExp true、λ_。Bv false）⇒t}」と表示されます。

私の理論には何が問題なのですか？

Answer 1

最初のコマンドvalues {t. True}は、このコマンドがタイプ変数'aであると推定されるタイプtのすべての値を列挙するように要求するため、機能しません。これはできません。

2番目のコマンドでは、TrueとFalseのスペルが間違っています。つまり、trueとfalseはブール定数ではなくブール変数であると推定されます。 valueとは異なり、コマンドvaluesはIsabelle2016-1でのシンボリック実行をサポートしていません。つまり、誘導述部へのすべての入力引数は、変数なしの基底値でなければなりません。あなたの例では、code_predは、2つの実行モードを推測します。1つはすべてが入力として与えられ、もう1つは入力として与えられます。あなたは、あなたがcode generator tutorialでcode_predとvaluesにさらにいくつかのドキュメントを見つけることができます

code_pred [show_modes] tboolval . 

によう[show_modes]オプションを渡すことによって推測されたモードを見ることができます。