Разбор простого императивного языка в Coq - PullRequest
Новая
       5

Разбор простого императивного языка в Coq

1 голос
/ 31 марта 2020

Я пытаюсь проанализировать следующий простой императивный язык в Coq: 

Set Warnings "-notation-overridden,-parsing".
From Coq Require Import Bool.Bool.
From Coq Require Import Init.Nat.
From Coq Require Import Arith.Arith.
From Coq Require Import Arith.EqNat.
From Coq Require Import omega.Omega.
From Coq Require Import Lists.List.
From Coq Require Import Strings.String.
Import ListNotations.

Definition vname := string.
Definition val := Z.

Inductive type :=
| Int: type.

Inductive expr :=
| var : vname -> expr
| int : val -> expr
| add : expr -> expr -> expr.

Inductive com :=
| Skip : com
| Seq : com -> com -> com
| Bind : vname -> type -> com -> com
| Assign : vname -> expr -> com.

Bind Scope move_scope with com.
Notation "'SKIP'" :=
  Skip : move_scope.
Notation "c1 ;; c2" :=
  (Seq c1 c2) (at level 80, right associativity) : move_scope.
Notation "'LET' x ':' t 'IN' b 'END'" :=
  (Bind x t b) (at level 80, right associativity) : move_scope.
Notation "x '::=' e" :=
  (Assign x e) (at level 60) : move_scope.

Definition prog0 : com := SKIP.

Definition prog1 : com := (LET "x" : Int IN SKIP END).

Однако попытка синтаксического анализа выражения let дает ошибку:

Синтаксическая ошибка: ':' ожидается после [constr: operconstr level 200] (в [constr: operconstr]).

Почему это происходит? Как я могу решить это?

1 Ответ

3 голосов
/ 31 марта 2020

Проблема в : - зарезервированное ключевое слово Coq. К сожалению, :: (объединяет начало и конец списка) также зарезервировано. Вы можете использовать ::: - или любую другую запись, которая вам нравится - 

Notation "'LET' x ':::' t 'IN' b 'END'" :=
  (Bind x t b) (at level 40, right associativity) : move_scope.
Definition prog1 : com := (LET "x" ::: Int IN SKIP END).
...