Как использовать оператор, который определяется локалью в типе данных - PullRequest
Новая
       2

Как использовать оператор, который определяется локалью в типе данных

0 голосов
/ 06 марта 2019

Моя работа посвящена процедурной алгебраической семантике.
Теперь я определил некоторые алгебраические семантические операторы и хочу использовать их в типе данных, потому что мне нужно создать полную семантику программы.
Это мой код: 

datatype 'a prog_expr =
   Const_expr "'a" |
   if_then_else_expr "'a prog_expr" bool "'a prog_expr" |
   sequential_expr "'a prog_expr" "'a prog_expr" |
   nondeterm_choice_expr "'a prog_expr" bool "'a prog_expr" 

primrec val_prog_expr :: "'a prog_expr ⇒ ('a ⇒ 'a prog_expr) ⇒ 'a prog_expr" where
"val_prog_expr (Const_expr P) s = s P" |
"val_prog_expr (if_then_else_expr P b Q) s = (val_prog_expr P s ◃ b ▹⇩? val_prog_expr Q s)" |
"val_prog_expr (sequential_expr P Q) s = (val_prog_expr P s ; val_prog_expr Q s)" |
"val_prog_expr (nondetem_choice_expr P Q) s = (val_prog_expr p s  ⊓  val_prog_expr Q s)"

сейчас, в этой строке: 

"val_prog_expr (if_then_else_expr P b Q) s = (val_prog_expr P s ◃ b ▹⇩? val_prog_expr Q s)" |

есть ошибка: 

Inner lexical error⌂
Failed to parse prop

Я думаю, что это оиспользовали операторы локали.
Затем я добавляю контекст locale_name begin .... end, там есть новая ошибка: 

Undefined type name: "prog_expr"⌂
Failed to parse type

Итак, что мне делать? Надеюсь, кто-томожете дать мне некоторое руководство.

...