如何使用类或区域设置?
问题描述:
我试图定义一种编程语言的通用操作:如何使用类或区域设置?
type_synonym vname = "string"
type_synonym 'a env = "vname ⇒ 'a option"
locale language =
fixes big_step :: "'exp × 'val env ⇒ 'val ⇒ bool" (infix "⇒" 55)
fixes typing :: "'type env ⇒ 'exp ⇒ 'type ⇒ bool" ("(1_/ ⊢/ (_ :/ _))" [50,0,50] 50)
例如,这是一个特殊的语言:
datatype foo_exp =
FooBConst bool |
FooLet vname foo_exp foo_exp |
FooVar vname |
FooAnd foo_exp foo_exp
datatype foo_val = FooBValue bool | FooIValue int
type_synonym foo_env = "foo_val env"
datatype foo_type = FooBType | FooIType
type_synonym foo_tenv = "foo_type env"
inductive foo_big_step :: "foo_exp × foo_env ⇒ foo_val ⇒ bool"
inductive foo_typing :: "foo_tenv ⇒ foo_exp ⇒ foo_type ⇒ bool"
如何使它language
语言环境的实例?
在一个理论中是否可以对不同的语言使用相同的符号(⇒
和_ ⊢ _ : _
)?这种表示法可能是多态的吗?
答
专门区域设置的参数,你需要做一个解释为
interpretation foo: language foo_big_step foo_typing .
这将产生一个缩写foo.f
在现场每个定义f
language
专门到foo_big_step
和foo_typing
和每一个定理thm
language
变得专门到foo.thm
。参数和语言环境中的所有常量的mixfix语法注释将不会被继承。
在此上下文中不能使用类型类,因为您的语言环境依赖于多个类型变量,并且Isabelle中的类型类只支持一个类型变量。
如果您想为大步语义和类型判断使用某种多态符号,Adhoc_Overloading
可能会起作用,前提是Isabelle的解析器可以静态解析唯一的重载。以下是这可能工作:
theory Language imports Main "~~/src/Tools/Adhoc_Overloading" begin
type_synonym 'a env = "vname ⇒ 'a option"
consts
big_step :: "'exp × 'val env ⇒ 'val ⇒ bool" (infix "⇒" 55)
typing :: "'type env ⇒ 'exp ⇒ 'type ⇒ bool" ("(1_/ ⊢/ (_ :/ _))" [50,0,50] 50)
locale language =
fixes big_step :: "'exp × 'val env ⇒ 'val ⇒ bool"
fixes typing :: "'type env ⇒ 'exp ⇒ 'type ⇒ bool"
begin
adhoc_overloading Language.big_step big_step
adhoc_overloading Language.typing typing
end
的解释后,你必须注册foo
的语义和类型判断常数即席与句法常数big_step
和typing
再次超载foo_big_step
和foo_typing
。
interpretation foo: language foo_big_step foo_typing .
adhoc_overloading Language.big_step foo_big_step
adhoc_overloading Language.typing foo_typing
所以,当你写
term "(x :: foo_exp, E) ⇒ v"
后,伊莎贝尔的解析器将通过此指foo_big_step
类型找出和场景Language
内,term "(x :: 'exp, E) ⇒ v"
解析为区域设置参数big_step
。
这应该也适用于区域设置Language
的多种解释,只要类型足以唯一地解决超载问题。如果没有,你会得到错误信息,这并不总是很容易理解。
感谢您的回答!有用。但是我得到以下警告:“模糊输入⌂产生3个分析树:... Language.big_step ... Language.language.foo_big_step ... Language.language.bar_big_step ...”如果我删除了'foo_big_step'的符号和“bar_big_step”,然后我得到以下错误:“无法解析adhoc常量重载 big_step ::”foo.foo_exp×(char list⇒foo.foo_val选项)⇒foo.foo_val⇒bool“ 在术语”(foo.FooAnd (foo.FooBConst True)(foo.FooBConst False),e)⇒foo。FooBValue False“ no instances” – Denis
@Denis:我误解了'interpre''不会重复'adhoc_overlaoding'声明。我相应地编辑了我的帖子。解释之后,您必须重新发布专门用于“foo”实例的'adhoc_overlaoding'命令。然后,你不再需要'foo_big_step'上的语法注释,语法也不再含糊不清了。 –