The Coq mailing list

[Hugo Herbelin <Hugo.Herbelin AT inria.fr>]

Hi,

This is also due to the special status of { } which is predefined at
level 0 with syntax "{ x }". In "(<{ { X > 0 } X := 0 { true } }>)",
the right-hand side of :=, a term at level 0, is parsed as "0 { true }",
that is as 0 applied to the notation "{ true }".

I'm afraid you'd have to renounce to the notation

Notation "f x .. y" := (.. (f x) .. y)
                  (in custom com at level 0, only parsing,
                  f constr at level 0, x constr at level 9,
                  y constr at level 9) : com_scope.

in custom entry com, or to replace it e.g. with a notation of the form
"f ( x , .. , y )", etc.

This special notation "{ x }" was there to implement the "historical"
notations "{ x } + { y }" for sumbool and "x + { y }" for sumor, and
their nesting as in "{ x } + { y } + { z }". We did not find a way
to do it without introducing a stand-alone "{ x }".

Hope it helps,

Hugo

On Sun, Oct 22, 2023 at 04:06:46PM -0400, Benjamin Pierce wrote:
> Many thanks, Gaëtan!  Yes, this works.
> 
> May I trouble you (and/or others) with one further question?  When I scale 
> this
> up to the full Imp language, it seems to get me almost everything I want, 
> but I
> am still puzzled by why I can't omit the parentheses on the very last line
> below.  I've tried tweaking various precedence levels, but have not found 
> the
> right combination...
> 
>    - B
> 
> 
>     From Coq Require Import Strings.String. Import String.
>     From Coq Require Import Bool.Bool.
>     From Coq Require Import Init.Nat.
>     From Coq Require Import Arith.Arith.
>     From Coq Require Import Arith.EqNat. Import Nat.
>     From Coq Require Import Lia.
>     From Coq Require Import Lists.List. Import ListNotations.
>     From PLF Require Import Maps.
> 
>     Declare Custom Entry com.
>     Declare Custom Entry com_aux.
>     Declare Scope com_scope.
>     Open Scope com_scope.
> 
>     Definition state := total_map nat.
> 
>     Inductive aexp : Type :=
>       | ANum (n : nat)
>       | AId (x : string)
>       | APlus (a1 a2 : aexp)
>       | AMinus (a1 a2 : aexp)
>       | AMult (a1 a2 : aexp).
> 
>     Definition W : string := "W".
>     Definition X : string := "X".
>     Definition Y : string := "Y".
>     Definition Z : string := "Z".
> 
>     Inductive bexp : Type :=
>       | BTrue
>       | BFalse
>       | BEq (a1 a2 : aexp)
>       | BNeq (a1 a2 : aexp)
>       | BLe (a1 a2 : aexp)
>       | BGt (a1 a2 : aexp)
>       | BNot (b : bexp)
>       | BAnd (b1 b2 : bexp).
> 
>     Coercion AId : string >-> aexp.
>     Coercion ANum : nat >-> aexp.
> 
>     Notation "<{ e }>" := e (e custom com_aux) : com_scope.
>     Notation "e" := e (in custom com_aux at level 0, e custom com) : 
> com_scope.
> 
>     Notation "( x )" := x (in custom com, x at level 98) : com_scope.
>     Notation "x" := x (in custom com at level 0, x constr at level 0) :
>     com_scope.
>     Notation "f x .. y" := (.. (f x) .. y)
>                       (in custom com at level 0, only parsing,
>                       f constr at level 0, x constr at level 9,
>                       y constr at level 9) : com_scope.
> 
>     Notation "x + y"   := (APlus x y) (in custom com at level 50, left
>     associativity).
>     Notation "x - y"   := (AMinus x y) (in custom com at level 50, left
>     associativity).
>     Notation "x * y"   := (AMult x y) (in custom com at level 40, left
>     associativity).
>     Notation "'true'"  := true (at level 1).
>     Notation "'true'"  := BTrue (in custom com at level 0).
>     Notation "'false'" := false (at level 1).
>     Notation "'false'" := BFalse (in custom com at level 0).
>     Notation "x <= y"  := (BLe x y) (in custom com at level 70, no
>     associativity).
>     Notation "x > y"   := (BGt x y) (in custom com at level 70, no
>     associativity).
>     Notation "x = y"   := (BEq x y) (in custom com at level 70, no
>     associativity).
>     Notation "x <> y"  := (BNeq x y) (in custom com at level 70, no
>     associativity).
>     Notation "x && y"  := (BAnd x y) (in custom com at level 80, left
>     associativity).
>     Notation "'~' b"   := (BNot b) (in custom com at level 75, right
>     associativity).
> 
>     Locate "=".
>     Check <{ X + Y }>.
>     Check <{ X + Y = 0 }>.
>     Check <{ ~ (Y = X) }>.
>     Check <{ X + Y }>.
>     Check <{ ~ (X + Y = Y) && Z = W }>.
> 
>     Inductive com : Type :=
>       | CSkip
>       | CAsgn (x : string) (a : aexp)
>       | CSeq (c1 c2 : com)
>       | CIf (b : bexp) (c1 c2 : com)
>       | CWhile (b : bexp) (c : com).
> 
>     Notation "'skip'"  :=
>              CSkip (in custom com at level 0) : com_scope.
>     Notation "x := y"  :=
>              (CAsgn x y)
>                 (in custom com at level 0, x constr at level 0,
>                  y at level 85, no associativity) : com_scope.
>     Notation "x ; y" :=
>              (CSeq x y)
>                (in custom com at level 90,
>                 right associativity) : com_scope.
>     Notation "'if' x 'then' y 'else' z 'end'" :=
>              (CIf x y z)
>                (in custom com at level 89, x at level 98,
>                 y at level 98, z at level 98) : com_scope.
>     Notation "'while' x 'do' y 'end'" :=
>              (CWhile x y)
>                (in custom com at level 89, x at level 98,
>                 y at level 98) : com_scope.
> 
>     Check <{ skip }>.
>     Check <{ (skip ; skip) ; skip }>.
>     Check <{ 1 + 2 }>.
>     Check <{ 2 = 1 }>.
>     Check <{ Z := X }>.
>     Check <{ Z := X + 3 }>.
>     Definition func (c : com) : com := <{ c ; skip }>.
>     Check <{ skip; func <{ skip }> }>.
>     Definition func2 (c1 c2 : com) : com := <{ c1 ; c2 }>.
>     Check <{ skip ; func2 <{skip}> <{skip}> }>.
>     Check <{ true && ~(false && true) }>.
>     Check <{ if true then skip else skip end }>.
>     Check <{ if true && true then skip; skip else skip; X:=X+1 end }>.
>     Check <{ while Z <> 0 do Y := Y * Z; Z := Z - 1 end }>.
> 
>     Fixpoint aeval (st : state) (* <--- NEW *)
>                    (a : aexp) : nat :=
>       match a with
>       | ANum n => n
>       | AId x => st x                                (* <--- NEW *)
>       | <{a1 + a2}> => (aeval st a1) + (aeval st a2)
>       | <{a1 - a2}> => (aeval st a1) - (aeval st a2)
>       | <{a1 * a2}> => (aeval st a1) * (aeval st a2)
>       end.
> 
>     Fixpoint beval (st : state) (* <--- NEW *)
>                    (b : bexp) : bool :=
>       match b with
>       | <{true}>      => true
>       | <{false}>     => false
>       | <{a1 = a2}>   => (aeval st a1) =? (aeval st a2)
>       | <{a1 <> a2}>  => negb ((aeval st a1) =? (aeval st a2))
>       | <{a1 <= a2}>  => (aeval st a1) <=? (aeval st a2)
>       | <{a1 > a2}>   => negb ((aeval st a1) <=? (aeval st a2))
>       | <{~ b1}>      => negb (beval st b1)
>       | <{b1 && b2}>  => andb (beval st b1) (beval st b2)
>       end.
> 
>     Definition Assertion := state -> Prop.
> 
>     Definition Assert_of_bexp (b : bexp) : Assertion := fun st => beval st 
> b =
>     true.
> 
>     Notation "{ P } e { Q }" :=
>       ((Assert_of_bexp P), e, (Assert_of_bexp Q))
>         (in custom com_aux,
>          e custom com,
>          P custom com,
>          Q custom com) : com_scope.
> 
>     Check (<{ X > 0 }>).
>     Check (<{ X := 0 }>).
>     Check (<{ { X > 0 } (X := 0) { true } }>).
>     Check (<{ { X > 0 } X := 0 { true } }>).
> 
> 
> 
>