The Coq mailing list

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

Thanks a lot for the suggestions Jasper. I managed to make it work using your hints. I attach the working file :)

Best,

Konstantinos

On Tue, Sep 24, 2019 at 4:06 PM Jasper Hugunin <jasperh AT cs.washington.edu> wrote:

Hello,

That you need different brackets for each quotation is indeed annoying; I've struggled with it myself.

Making "x := y" a level 0 command fixed the second question you have in that file, along with adding the invisible antiquotation you mention.

I found this by trying replacing [x custom string at level 4] with [x ident], and then Coq told me that notations starting with an atomic _expression_ must be at level 0.

Those changes also let the final question get further (past the ; case), but it now fails in the "if" case on "then", apparently thinking b is an aexp and then looking for a <= or =. Playing around with making the level of "a = a2" and "a <= a2" zero, and adding invisible antiquotations for global bexps makes different things succeed and fail, so there may be something possible there. This feels like a similar problem to the second question, in a slightly different guise.

Making the inside of the quotations look for things of level 10 or so rather than 0 may help avoid weird things, since you are writing [ x + y ] rather than [ ( x + y ) ].

Best of luck,

- Jasper Hugunin

On Tue, Sep 24, 2019 at 3:06 PM Jim Fehrle <jim.fehrle AT gmail.com> wrote:

I don't know too much about notations, but perhaps this is not completely useless:

It appears that com doesn't have a constructor to represent calling or referencing another com such as subtract_slowly_body.  And presumably that would need its own notation.

You can reproduce the problem with the following simpler example:

Definition foo : com :=

  [[subtract_slowly_body]].

I suppose defining a notation like "'call' x" might be a way to get around parsing limitations.

--Jim

On Tue, Sep 24, 2019 at 4:05 AM Benjamin C. Pierce <bcpierce AT cis.upenn.edu> wrote:

Any suggestions from the community on how to make custom entries work better here would be greatly appreciated.  We would like to use the new features in the next release of Software Foundations (for which the timeline is rather tight), but right now we are blocked on several things that appear to be either inconveniently rigid in the design or not working as documented.  :-(

Thanks!

    - Benjamin

> On Sep 22, 2019, at 1:33 PM, Konstantinos Kallas <kallas AT seas.upenn.edu> wrote:
>
> 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 "x" := x (in custom bexp at level 0, x global).
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 1, y custom aexp at level 1,
                           no associativity).
Notation "x = y"  := (BEq x y)
                       (in custom bexp at level 3,
                           x custom aexp at level 1, y custom aexp at level 1,
                           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 "x" := x (in custom com at level 0, x global).
Notation "'skip'"  := (CSkip) (in custom com at level 0).
Notation "x :=  y" := (CAss x y)
                      (in custom com at level 0, 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 at level 0).
Notation "'while' x 'do' y 'end'" :=
                      (CWhile x y)
                      (in custom com at level 10, right associativity, x custom bexp at level 0).

(* 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 ]].

Definition subtract_slowly : com :=
  [[ while ~(X = 0) do
       subtract_slowly_body
     end ]].

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.