The Coq mailing list

[Konstantinos Kallas <kallas AT seas.upenn.edu>]

Hi all,

We are trying to define the syntax of a simple imperative language using the Custom entries feature but we are encountering some problems. Some of the problems might not be related to custom entries per se, but might be caused by some misuse of the notation feature (due to my lack of understanding of parsing in Coq).

I have attached a file that contains the definitions, some examples that work as expected, and some examples where the parser gets confused (that are annotated with "Question:" comments).

It would be great if someone could give us some hints about what could be the problem or how should we go about solving it.

Thanks,

Konstantinos

(* This is a definition of a simple imperative programming language,
   called Imp. We wanted to use custom entries to have cleaner
   language syntax, but we encountered some problems...

   Our concerns are noted in "Question:" comments below *)

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.

(* -------------------------------------------------------------------------- *)
(* Arithmetic expressions *)

Inductive aexp : Type :=
  | ANum (n : nat)        (* Constant *)
  | AId (x : string)      (* Variable *)
  | APlus (a1 a2 : aexp)  (* + *)
  | AMinus (a1 a2 : aexp) (* - *)
  | AMult (a1 a2 : aexp). (* * *)

(* We define a set of variable names that we use often so that we
   don't write variables as strings in Imp programs. *)
Definition W : string := "W".
Definition X : string := "X".
Definition Y : string := "Y".
Definition Z : string := "Z".

(* Notations *)
Declare Custom Entry string.
Notation "x" := x (in custom string at level 0, x global).
Declare Custom Entry aexp.
Notation "[[a e ]]" := e (e custom aexp at level 0).
Notation "( x )" := x (in custom aexp, x at level 10).
Coercion AId : string >-> aexp.
Coercion ANum : nat >-> aexp.
Notation "x" := x (in custom aexp at level 0, x constr at level 0).
Notation "x + y" := (APlus x y) (in custom aexp at level 2, left associativity).
Notation "x - y" := (AMinus x y) (in custom aexp at level 2, left associativity).
Notation "x * y" := (AMult x y) (in custom aexp at level 1, left associativity).

(* Some aexp examples *)
Definition example_aexp : aexp := [[a 3 + (X * 2) ]].
Check [[a 1 + 2 ]].

(* Question: It seems from the documentation that we have to choose
   different sets of brackets for aexps, bexps, and commands -- e.g.,
   here we've written [[a ...]] for aexps -- instead of just writing
   them all with the same brackets [[...]].  Can this really be true?
   It seems like a big limitation.  (And, intuitively, it seems like
   it should not be needed, since it is always easy to tell whether an
   expression in the Imp grammar represents an arithmetic expression,
   a boolean expression, or a command.) *)

(* -------------------------------------------------------------------------- *)
(* Boolean expressions *)

Inductive bexp : Type :=
  | BTrue
  | BFalse
  | BEq (a1 a2 : aexp)
  | BLe (a1 a2 : aexp)
  | BNot (b : bexp)
  | BAnd (b1 b2 : bexp).

Declare Custom Entry bexp.
Notation "[[b e ]]" := e (e custom bexp at level 0).
Notation "( x )" := x (in custom bexp, x at level 10).
Notation "'true'"  := (BTrue) (in custom bexp at level 0).
Notation "'false'"  := (BFalse) (in custom bexp at level 0).
Notation "x <= y" := (BLe x y)
                       (in custom bexp at level 3,
                           x custom aexp at level 0, y custom aexp at level 0,
                           no associativity).
Notation "x = y"  := (BEq x y)
                       (in custom bexp at level 3,
                           x custom aexp at level 0, y custom aexp at level 0,
                           no associativity).
Notation "x && y" := (BAnd x y)
                       (in custom bexp at level 2, left associativity).
Notation "'~' b"  := (BNot b) (in custom bexp at level 1, right associativity).

(* Examples *)
Definition example_bexp : bexp := [[b true && ~(X <= 4) ]].
Check [[b 2 = 1 ]].

(* -------------------------------------------------------------------------- *)
(* Commands *)

Inductive com : Type :=
  | CSkip
  | CAss (x : string) (a : aexp)
  | CSeq (c1 c2 : com)
  | CIf (b : bexp) (c1 c2 : com)
  | CWhile (b : bexp) (c : com).

Declare Custom Entry com.
Notation "[[ e ]]" := e (e custom com at level 0).
Notation "'skip'"  := (CSkip) (in custom com at level 0).
Notation "x :=  y" := (CAss x y)
                      (in custom com at level 4, x custom string at level 0,
                       y custom aexp at level 2, no associativity).
Notation "x ; y" := (CSeq x y) (in custom com at level 10, right associativity).
Notation "'if' x 'then' y 'else' z" :=
                      (CIf x y z)
                      (in custom com at level 10, right associativity, x custom bexp).
Notation "'while' x 'do' y 'end'" :=
                      (CWhile x y)
                      (in custom com at level 10, right associativity, x custom bexp).

(* Some com examples *)
Check [[ skip ]].
Check [[ skip ; skip ]].
Check [[ Z := X ]].


Definition fact_in_coq : com :=
  [[ Z := X;
     Y := 1;
     while ~(Z = 0) do
       Y := Y * Z;
       Z := Z - 1
     end ]].

Definition plus2 : com :=
  [[ X := X + 2 ]].

Definition XtimesYinZ : com :=
  [[ Z := X * Y ]].

Definition subtract_slowly_body : com :=
  [[ Z := Z - 1 ;
     X := X - 1 ]].

(* Question: This fails, but we don't understand why: We managed to do
   it by adding a [Notation "x" := x (in custom com at level 0, x
   global).], but then the parser gets confused with the left hand
   side of assignments... *)
Definition subtract_slowly : com :=
  [[ while ~(X = 0) do
       subtract_slowly_body
     end ]].

(* Question: Similarly the `;` cannot be parsed correctly in the
   definition below. *)
Fixpoint identity (c : com) : com :=
  match c with
    | [[ skip ]] =>
      [[ skip ]]
    | [[ x := a1 ]] =>
      [[ x := a1 ]]
    | [[ c1 ; c2 ]] =>
      [[ c1 ; c2 ]]
    | [[ if b then c1 else c2 ]] =>
      [[ if b then c1 else c2 ]]
    | [[ while b do c end ]] =>
      [[ while b do c end ]]
  end.