The Coq mailing list

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

Fixing a typo:
the right-hand side of :=, a term at level 0
-->
the right-hand side of :=, a com at level 85 eventually expected to be a com 
at level 0

On Mon, Oct 23, 2023 at 01:19:40PM +0200, Hugo Herbelin wrote:
> 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 } }>).
> > 
> > 
> > 
> >