From 103aa7074a9dd3b1bcb2864d52c89292a2ab7bff Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Mon, 19 Sep 2022 16:28:06 +0200 Subject: Add `Declare Scope` where appropriate (#440) And re-enable the `undeclared-scope` warning. `Declare Scope` has been available since Coq 8.12, which is now the minimal Coq version supported. --- Makefile | 4 ---- MenhirLib/Interpreter.v | 4 ++-- aarch64/Asm.v | 1 + arm/Asm.v | 1 + backend/Allocation.v | 2 ++ backend/CminorSel.v | 1 + backend/Registers.v | 2 ++ cfrontend/Cexec.v | 6 ++++++ cfrontend/SimplExpr.v | 1 + common/Errors.v | 2 ++ common/Globalenvs.v | 2 +- common/Linking.v | 2 ++ common/Separation.v | 1 + common/Smallstep.v | 2 ++ export/Clightdefs.v | 2 ++ export/Csyntaxdefs.v | 2 ++ powerpc/Asm.v | 1 + riscV/Asm.v | 1 + x86/Asm.v | 1 + 19 files changed, 31 insertions(+), 7 deletions(-) diff --git a/Makefile b/Makefile index b3b7a124..48648a0a 100644 --- a/Makefile +++ b/Makefile @@ -44,9 +44,6 @@ endif # Notes on silenced Coq warnings: # -# undeclared-scope: -# warning introduced in 8.12 -# suggested change (use `Declare Scope`) supported since 8.12 # unused-pattern-matching-variable: # warning introduced in 8.13 # the code rewrite that avoids the warning is not desirable @@ -58,7 +55,6 @@ endif # triggered by Menhir-generated files, to be solved upstream in Menhir COQCOPTS ?= \ - -w -undeclared-scope \ -w -unused-pattern-matching-variable \ -w -deprecated-ident-entry diff --git a/MenhirLib/Interpreter.v b/MenhirLib/Interpreter.v index 158bba9f..922d6656 100644 --- a/MenhirLib/Interpreter.v +++ b/MenhirLib/Interpreter.v @@ -84,8 +84,8 @@ CoInductive buffer : Type := Buf_cons { buf_head : token; buf_tail : buffer }. (* Note: Coq 8.12.0 wants a Declare Scope command, - but this breaks compatibility with Coq < 8.10. - Declare Scope buffer_scope. *) + but this breaks compatibility with Coq < 8.10. *) +Declare Scope buffer_scope. Delimit Scope buffer_scope with buf. Bind Scope buffer_scope with buffer. diff --git a/aarch64/Asm.v b/aarch64/Asm.v index c5f4032e..0b5b01b8 100644 --- a/aarch64/Asm.v +++ b/aarch64/Asm.v @@ -96,6 +96,7 @@ Coercion preg_of_iregsp: iregsp >-> preg. (** Conventional name for return address ([RA]) *) +Declare Scope asm. Notation "'RA'" := X30 (only parsing) : asm. (** The instruction set. Most instructions correspond exactly to diff --git a/arm/Asm.v b/arm/Asm.v index 8c902074..f0dd347f 100644 --- a/arm/Asm.v +++ b/arm/Asm.v @@ -94,6 +94,7 @@ Module Pregmap := EMap(PregEq). (** Conventional names for stack pointer ([SP]) and return address ([RA]) *) +Declare Scope asm. Notation "'SP'" := IR13 (only parsing) : asm. Notation "'RA'" := IR14 (only parsing) : asm. diff --git a/backend/Allocation.v b/backend/Allocation.v index 08e0a4f4..4de215b8 100644 --- a/backend/Allocation.v +++ b/backend/Allocation.v @@ -167,6 +167,8 @@ Definition check_succ (s: node) (b: LTL.bblock) : bool := | _ => false end. +Declare Scope option_monad_scope. + Notation "'do' X <- A ; B" := (match A with Some X => B | None => None end) (at level 200, X ident, A at level 100, B at level 200) : option_monad_scope. diff --git a/backend/CminorSel.v b/backend/CminorSel.v index f6f6e34d..97a666bd 100644 --- a/backend/CminorSel.v +++ b/backend/CminorSel.v @@ -54,6 +54,7 @@ with condexpr : Type := | CEcondition : condexpr -> condexpr -> condexpr -> condexpr | CElet: expr -> condexpr -> condexpr. +Declare Scope cminorsel_scope. Infix ":::" := Econs (at level 60, right associativity) : cminorsel_scope. (** Conditional expressions [condexpr] are expressions that are evaluated diff --git a/backend/Registers.v b/backend/Registers.v index 622cddfe..7f7ecb60 100644 --- a/backend/Registers.v +++ b/backend/Registers.v @@ -61,6 +61,8 @@ Definition regmap_setres | _ => rs end. +Declare Scope rtl. + Notation "a # b" := (Regmap.get b a) (at level 1) : rtl. Notation "a ## b" := (List.map (fun r => Regmap.get r a) b) (at level 1) : rtl. Notation "a # b <- c" := (Regmap.set b c a) (at level 1, b at next level) : rtl. diff --git a/cfrontend/Cexec.v b/cfrontend/Cexec.v index 52037ac0..f02da0c8 100644 --- a/cfrontend/Cexec.v +++ b/cfrontend/Cexec.v @@ -25,6 +25,8 @@ Local Open Scope list_scope. (** Error monad with options or lists *) +Declare Scope option_monad_scope. + Notation "'do' X <- A ; B" := (match A with Some X => B | None => None end) (at level 200, X ident, A at level 100, B at level 200) : option_monad_scope. @@ -45,6 +47,8 @@ Notation " 'check' A ; B" := (if A then B else None) (at level 200, A at level 100, B at level 200) : option_monad_scope. +Declare Scope list_monad_scope. + Notation "'do' X <- A ; B" := (match A with Some X => B | None => nil end) (at level 200, X ident, A at level 100, B at level 200) : list_monad_scope. @@ -745,6 +749,8 @@ Definition incontext2 {A1 A2 B: Type} (ctx2: A2 -> B) (ll2: reducts A2) : reducts B := incontext ctx1 ll1 ++ incontext ctx2 ll2. +Declare Scope reducts_monad_scope. + Notation "'do' X <- A ; B" := (match A with Some X => B | None => stuck end) (at level 200, X ident, A at level 100, B at level 200) : reducts_monad_scope. diff --git a/cfrontend/SimplExpr.v b/cfrontend/SimplExpr.v index bb1dbe38..cf5dd6d1 100644 --- a/cfrontend/SimplExpr.v +++ b/cfrontend/SimplExpr.v @@ -55,6 +55,7 @@ Definition bind {A B: Type} (x: mon A) (f: A -> mon B) : mon B := Definition bind2 {A B C: Type} (x: mon (A * B)) (f: A -> B -> mon C) : mon C := bind x (fun p => f (fst p) (snd p)). +Declare Scope gensym_monad_scope. Notation "'do' X <- A ; B" := (bind A (fun X => B)) (at level 200, X ident, A at level 100, B at level 200) : gensym_monad_scope. diff --git a/common/Errors.v b/common/Errors.v index bf72f12b..d9158165 100644 --- a/common/Errors.v +++ b/common/Errors.v @@ -67,6 +67,8 @@ Definition bind2 (A B C: Type) (f: res (A * B)) (g: A -> B -> res C) : res C := (** The [do] notation, inspired by Haskell's, keeps the code readable. *) +Declare Scope error_monad_scope. + Notation "'do' X <- A ; B" := (bind A (fun X => B)) (at level 200, X ident, A at level 100, B at level 200) : error_monad_scope. diff --git a/common/Globalenvs.v b/common/Globalenvs.v index f424a69d..1c5bf4ff 100644 --- a/common/Globalenvs.v +++ b/common/Globalenvs.v @@ -39,9 +39,9 @@ Require Import Zwf. Require Import Axioms Coqlib Errors Maps AST Linking. Require Import Integers Floats Values Memory. +Declare Scope pair_scope. Notation "s #1" := (fst s) (at level 9, format "s '#1'") : pair_scope. Notation "s #2" := (snd s) (at level 9, format "s '#2'") : pair_scope. - Local Open Scope pair_scope. Local Open Scope error_monad_scope. diff --git a/common/Linking.v b/common/Linking.v index 4ef83d42..54d1628e 100644 --- a/common/Linking.v +++ b/common/Linking.v @@ -862,6 +862,8 @@ Inductive Passes: Language -> Language -> Type := | pass_nil: forall l, Passes l l | pass_cons: forall l1 l2 l3, Pass l1 l2 -> Passes l2 l3 -> Passes l1 l3. +Declare Scope linking_scope. + Infix ":::" := pass_cons (at level 60, right associativity) : linking_scope. (** The pass corresponding to the composition of a list of passes. *) diff --git a/common/Separation.v b/common/Separation.v index f41d94c3..2ba6e77b 100644 --- a/common/Separation.v +++ b/common/Separation.v @@ -54,6 +54,7 @@ Record massert : Type := { m_valid: forall m b ofs, m_pred m -> m_footprint b ofs -> Mem.valid_block m b }. +Declare Scope sep_scope. Notation "m |= p" := (m_pred p m) (at level 74, no associativity) : sep_scope. (** Implication and logical equivalence between memory predicates *) diff --git a/common/Smallstep.v b/common/Smallstep.v index 487e7a80..3cbd8934 100644 --- a/common/Smallstep.v +++ b/common/Smallstep.v @@ -552,6 +552,8 @@ Definition Semantics {state funtype vartype: Type} (** Handy notations. *) +Declare Scope smallstep_scope. + Notation " 'Step' L " := (step L (globalenv L)) (at level 1) : smallstep_scope. Notation " 'Star' L " := (star (step L) (globalenv L)) (at level 1) : smallstep_scope. Notation " 'Plus' L " := (plus (step L) (globalenv L)) (at level 1) : smallstep_scope. diff --git a/export/Clightdefs.v b/export/Clightdefs.v index dc4e3491..3a9da8f6 100644 --- a/export/Clightdefs.v +++ b/export/Clightdefs.v @@ -49,6 +49,8 @@ Definition mkprogram (types: list composite_definition) (** ** Notations *) +Declare Scope clight_scope. + Module ClightNotations. (** A convenient notation [$ "ident"] to force evaluation of diff --git a/export/Csyntaxdefs.v b/export/Csyntaxdefs.v index 84ce9f3a..67bc7f51 100644 --- a/export/Csyntaxdefs.v +++ b/export/Csyntaxdefs.v @@ -49,6 +49,8 @@ Definition mkprogram (types: list composite_definition) (** ** Notations *) +Declare Scope csyntax_scope. + Module CsyntaxNotations. (** A convenient notation [$ "ident"] to force evaluation of diff --git a/powerpc/Asm.v b/powerpc/Asm.v index 6b1f2232..ea6f5c92 100644 --- a/powerpc/Asm.v +++ b/powerpc/Asm.v @@ -87,6 +87,7 @@ Module Pregmap := EMap(PregEq). (** Conventional names for stack pointer ([SP]) and return address ([RA]) *) +Declare Scope asm. Notation "'SP'" := GPR1 (only parsing) : asm. Notation "'RA'" := LR (only parsing) : asm. diff --git a/riscV/Asm.v b/riscV/Asm.v index cbe3476a..15c3dab4 100644 --- a/riscV/Asm.v +++ b/riscV/Asm.v @@ -93,6 +93,7 @@ Module Pregmap := EMap(PregEq). (** Conventional names for stack pointer ([SP]) and return address ([RA]). *) +Declare Scope asm. Notation "'SP'" := X2 (only parsing) : asm. Notation "'RA'" := X1 (only parsing) : asm. diff --git a/x86/Asm.v b/x86/Asm.v index b9c4817a..64a835e1 100644 --- a/x86/Asm.v +++ b/x86/Asm.v @@ -312,6 +312,7 @@ Module Pregmap := EMap(PregEq). Definition regset := Pregmap.t val. Definition genv := Genv.t fundef unit. +Declare Scope asm. Notation "a # b" := (a b) (at level 1, only parsing) : asm. Notation "a # b <- c" := (Pregmap.set b c a) (at level 1, b at next level) : asm. -- cgit