aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--doc/changelog/02-specification-language/11261-master+implicit-type-used-printing.rst5
-rw-r--r--doc/changelog/03-notations/11590-master+fix9741-only-printing-does-not-reserve-keyword.rst4
-rw-r--r--doc/sphinx/language/gallina-extensions.rst7
-rw-r--r--interp/constrextern.ml92
-rw-r--r--parsing/notation_gram.ml5
-rw-r--r--parsing/notgram_ops.ml6
-rw-r--r--parsing/notgram_ops.mli4
-rw-r--r--parsing/ppextend.ml3
-rw-r--r--test-suite/bugs/closed/bug_9741.v21
-rw-r--r--test-suite/output/Implicit.out5
-rw-r--r--test-suite/output/Implicit.v10
-rw-r--r--test-suite/output/ImplicitTypes.out26
-rw-r--r--test-suite/output/ImplicitTypes.v37
-rw-r--r--vernac/himsg.ml16
-rw-r--r--vernac/metasyntax.ml44
15 files changed, 220 insertions, 65 deletions
diff --git a/doc/changelog/02-specification-language/11261-master+implicit-type-used-printing.rst b/doc/changelog/02-specification-language/11261-master+implicit-type-used-printing.rst
new file mode 100644
index 0000000000..51818c666b
--- /dev/null
+++ b/doc/changelog/02-specification-language/11261-master+implicit-type-used-printing.rst
@@ -0,0 +1,5 @@
+- **Added:**
+ :cmd:`Implicit Types` are now taken into account for printing. To inhibit it,
+ unset the :flag:`Printing Use Implicit Types` flag
+ (`#11261 <https://github.com/coq/coq/pull/11261>`_,
+ by Hugo Herbelin, granting `#10366 <https://github.com/coq/coq/pull/10366>`_).
diff --git a/doc/changelog/03-notations/11590-master+fix9741-only-printing-does-not-reserve-keyword.rst b/doc/changelog/03-notations/11590-master+fix9741-only-printing-does-not-reserve-keyword.rst
new file mode 100644
index 0000000000..1d94cbf21b
--- /dev/null
+++ b/doc/changelog/03-notations/11590-master+fix9741-only-printing-does-not-reserve-keyword.rst
@@ -0,0 +1,4 @@
+- **Fixed:**
+ Notations in onlyprinting mode do not uselessly reserve parsing keywords
+ (`#11590 <https://github.com/coq/coq/pull/11590>`_,
+ by Hugo Herbelin, fixes `#9741 <https://github.com/coq/coq/pull/9741>`_).
diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst
index f0bbaed8f3..9686500a35 100644
--- a/doc/sphinx/language/gallina-extensions.rst
+++ b/doc/sphinx/language/gallina-extensions.rst
@@ -2208,6 +2208,13 @@ or :g:`m` to the type :g:`nat` of natural numbers).
Adds blocks of implicit types with different specifications.
+.. flag:: Printing Use Implicit Types
+
+ By default, the type of bound variables is not printed when
+ the variable name is associated to an implicit type which matches the
+ actual type of the variable. This feature can be deactivated by
+ turning this flag off.
+
.. _implicit-generalization:
Implicit generalization
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 0a3ee59f4e..38dc10a9b3 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -63,6 +63,28 @@ let print_universes = Detyping.print_universes
(* This suppresses printing of primitive tokens (e.g. numeral) and notations *)
let print_no_symbol = ref false
+(* This tells to skip types if a variable has this type by default *)
+let print_use_implicit_types =
+ Goptions.declare_bool_option_and_ref
+ ~depr:false
+ ~key:["Printing";"Use";"Implicit";"Types"]
+ ~value:true
+
+(**********************************************************************)
+
+let hole = CAst.make @@ CHole (None, IntroAnonymous, None)
+
+let is_reserved_type na t =
+ not !Flags.raw_print && print_use_implicit_types () &&
+ match na with
+ | Anonymous -> false
+ | Name id ->
+ try
+ let pat = Reserve.find_reserved_type id in
+ let _ = match_notation_constr false t ([],pat) in
+ true
+ with Not_found | No_match -> false
+
(**********************************************************************)
(* Turning notations and scopes on and off for printing *)
module IRuleSet = Set.Make(struct
@@ -790,6 +812,12 @@ let rec flatten_application c = match DAst.get c with
end
| a -> c
+let same_binder_type ty nal c =
+ match nal, DAst.get c with
+ | _::_, GProd (_,_,ty',_) -> glob_constr_eq ty ty'
+ | [], _ -> true
+ | _ -> assert false
+
(**********************************************************************)
(* mapping glob_constr to numerals (in presence of coercions, choose the *)
(* one with no delimiter if possible) *)
@@ -939,12 +967,10 @@ let rec extern inctx scopes vars r =
extern inctx scopes (add_vname vars na) c)
| GProd (na,bk,t,c) ->
- let t = extern_typ scopes vars t in
- factorize_prod scopes (add_vname vars na) na bk t c
+ factorize_prod scopes vars na bk t c
| GLambda (na,bk,t,c) ->
- let t = extern_typ scopes vars t in
- factorize_lambda inctx scopes (add_vname vars na) na bk t c
+ factorize_lambda inctx scopes vars na bk t c
| GCases (sty,rtntypopt,tml,eqns) ->
let vars' =
@@ -973,17 +999,19 @@ let rec extern inctx scopes vars r =
) x))
tml
in
- let eqns = List.map (extern_eqn inctx scopes vars) (factorize_eqns eqns) in
+ let eqns = List.map (extern_eqn (inctx || rtntypopt <> None) scopes vars) (factorize_eqns eqns) in
CCases (sty,rtntypopt',tml,eqns)
| GLetTuple (nal,(na,typopt),tm,b) ->
- CLetTuple (List.map CAst.make nal,
+ let inctx = inctx || typopt <> None in
+ CLetTuple (List.map CAst.make nal,
(Option.map (fun _ -> (make na)) typopt,
Option.map (extern_typ scopes (add_vname vars na)) typopt),
sub_extern false scopes vars tm,
extern inctx scopes (List.fold_left add_vname vars nal) b)
| GIf (c,(na,typopt),b1,b2) ->
+ let inctx = inctx || typopt <> None in
CIf (sub_extern false scopes vars c,
(Option.map (fun _ -> (CAst.make na)) typopt,
Option.map (extern_typ scopes (add_vname vars na)) typopt),
@@ -1006,7 +1034,7 @@ let rec extern inctx scopes vars r =
| Some x -> Some (CAst.make @@ CStructRec (CAst.make @@ Name.get_id (List.nth assums x)))
in
((CAst.make fi), n, bl, extern_typ scopes vars0 ty,
- extern false scopes vars1 def)) idv
+ sub_extern true scopes vars1 def)) idv
in
CFix (CAst.(make ?loc idv.(n)), Array.to_list listdecl)
| GCoFix n ->
@@ -1017,7 +1045,7 @@ let rec extern inctx scopes vars r =
let vars0 = List.fold_right (Name.fold_right Id.Set.add) ids vars in
let vars1 = List.fold_right (Name.fold_right Id.Set.add) ids vars' in
((CAst.make fi),bl,extern_typ scopes vars0 tyv.(i),
- sub_extern false scopes vars1 bv.(i))) idv
+ sub_extern true scopes vars1 bv.(i))) idv
in
CCoFix (CAst.(make ?loc idv.(n)),Array.to_list listdecl))
@@ -1043,7 +1071,10 @@ and extern_typ (subentry,(_,scopes)) =
and sub_extern inctx (subentry,(_,scopes)) = extern inctx (subentry,(None,scopes))
-and factorize_prod scopes vars na bk aty c =
+and factorize_prod scopes vars na bk t c =
+ let implicit_type = is_reserved_type na t in
+ let aty = extern_typ scopes vars t in
+ let vars = add_vname vars na in
let store, get = set_temporary_memory () in
match na, DAst.get c with
| Name id, GCases (Constr.LetPatternStyle, None, [(e,(Anonymous,None))],(_::_ as eqns))
@@ -1060,18 +1091,25 @@ and factorize_prod scopes vars na bk aty c =
| _ -> CProdN ([binder],b))
| _ -> assert false)
| _, _ ->
- let c = extern_typ scopes vars c in
- match na, c.v with
+ let c' = extern_typ scopes vars c in
+ match na, c'.v with
| Name id, CProdN (CLocalAssum(nal,Default bk',ty)::bl,b)
- when binding_kind_eq bk bk' && constr_expr_eq aty ty
- && not (occur_var_constr_expr id ty) (* avoid na in ty escapes scope *) ->
- CProdN (CLocalAssum(make na::nal,Default bk,aty)::bl,b)
+ when binding_kind_eq bk bk'
+ && not (occur_var_constr_expr id ty) (* avoid na in ty escapes scope *)
+ && (constr_expr_eq aty ty || (constr_expr_eq ty hole && same_binder_type t nal c)) ->
+ let ty = if implicit_type then ty else aty in
+ CProdN (CLocalAssum(make na::nal,Default bk,ty)::bl,b)
| _, CProdN (bl,b) ->
- CProdN (CLocalAssum([make na],Default bk,aty)::bl,b)
+ let ty = if implicit_type then hole else aty in
+ CProdN (CLocalAssum([make na],Default bk,ty)::bl,b)
| _, _ ->
- CProdN ([CLocalAssum([make na],Default bk,aty)],c)
+ let ty = if implicit_type then hole else aty in
+ CProdN ([CLocalAssum([make na],Default bk,ty)],c')
-and factorize_lambda inctx scopes vars na bk aty c =
+and factorize_lambda inctx scopes vars na bk t c =
+ let implicit_type = is_reserved_type na t in
+ let aty = extern_typ scopes vars t in
+ let vars = add_vname vars na in
let store, get = set_temporary_memory () in
match na, DAst.get c with
| Name id, GCases (Constr.LetPatternStyle, None, [(e,(Anonymous,None))],(_::_ as eqns))
@@ -1088,16 +1126,20 @@ and factorize_lambda inctx scopes vars na bk aty c =
| _ -> CLambdaN ([binder],b))
| _ -> assert false)
| _, _ ->
- let c = sub_extern inctx scopes vars c in
- match c.v with
+ let c' = sub_extern inctx scopes vars c in
+ match c'.v with
| CLambdaN (CLocalAssum(nal,Default bk',ty)::bl,b)
- when binding_kind_eq bk bk' && constr_expr_eq aty ty
- && not (occur_name na ty) (* avoid na in ty escapes scope *) ->
+ when binding_kind_eq bk bk'
+ && not (occur_name na ty) (* avoid na in ty escapes scope *)
+ && (constr_expr_eq aty ty || (constr_expr_eq ty hole && same_binder_type t nal c)) ->
+ let aty = if implicit_type then ty else aty in
CLambdaN (CLocalAssum(make na::nal,Default bk,aty)::bl,b)
| CLambdaN (bl,b) ->
- CLambdaN (CLocalAssum([make na],Default bk,aty)::bl,b)
+ let ty = if implicit_type then hole else aty in
+ CLambdaN (CLocalAssum([make na],Default bk,ty)::bl,b)
| _ ->
- CLambdaN ([CLocalAssum([make na],Default bk,aty)],c)
+ let ty = if implicit_type then hole else aty in
+ CLambdaN ([CLocalAssum([make na],Default bk,ty)],c')
and extern_local_binder scopes vars = function
[] -> ([],[],[])
@@ -1111,15 +1153,17 @@ and extern_local_binder scopes vars = function
Option.map (extern false scopes vars) ty) :: l)
| GLocalAssum (na,bk,ty) ->
+ let implicit_type = is_reserved_type na ty in
let ty = extern_typ scopes vars ty in
(match extern_local_binder scopes (Name.fold_right Id.Set.add na vars) l with
(assums,ids,CLocalAssum(nal,k,ty')::l)
- when constr_expr_eq ty ty' &&
+ when (constr_expr_eq ty ty' || implicit_type && constr_expr_eq ty' hole) &&
match na with Name id -> not (occur_var_constr_expr id ty')
| _ -> true ->
(na::assums,na::ids,
CLocalAssum(CAst.make na::nal,k,ty')::l)
| (assums,ids,l) ->
+ let ty = if implicit_type then hole else ty in
(na::assums,na::ids,
CLocalAssum([CAst.make na],Default bk,ty) :: l))
diff --git a/parsing/notation_gram.ml b/parsing/notation_gram.ml
index 2fa9a496b7..427505c199 100644
--- a/parsing/notation_gram.ml
+++ b/parsing/notation_gram.ml
@@ -34,7 +34,4 @@ type one_notation_grammar = {
notgram_prods : grammar_constr_prod_item list list;
}
-type notation_grammar = {
- notgram_onlyprinting : bool;
- notgram_rules : one_notation_grammar list
-}
+type notation_grammar = one_notation_grammar list
diff --git a/parsing/notgram_ops.ml b/parsing/notgram_ops.ml
index 382a890425..b6699493bb 100644
--- a/parsing/notgram_ops.ml
+++ b/parsing/notgram_ops.ml
@@ -15,16 +15,16 @@ open Notation
open Constrexpr
(* Register the level of notation for parsing and printing
- (we also register a precomputed parsing rule) *)
+ (also register the parsing rule if not onlyprinting) *)
let notation_level_map = Summary.ref ~name:"notation_level_map" NotationMap.empty
-let declare_notation_level ntn ~onlyprint parsing_rule level =
+let declare_notation_level ntn parsing_rule level =
try
let _ = NotationMap.find ntn !notation_level_map in
anomaly (str "Notation " ++ pr_notation ntn ++ str " is already assigned a level.")
with Not_found ->
- notation_level_map := NotationMap.add ntn (onlyprint,parsing_rule,level) !notation_level_map
+ notation_level_map := NotationMap.add ntn (parsing_rule,level) !notation_level_map
let level_of_notation ntn =
NotationMap.find ntn !notation_level_map
diff --git a/parsing/notgram_ops.mli b/parsing/notgram_ops.mli
index 44c3f3bbdf..d8b7e8e4c1 100644
--- a/parsing/notgram_ops.mli
+++ b/parsing/notgram_ops.mli
@@ -17,8 +17,8 @@ val entry_relative_level_eq : entry_relative_level -> entry_relative_level -> bo
(** {6 Declare and test the level of a (possibly uninterpreted) notation } *)
-val declare_notation_level : notation -> onlyprint:bool -> notation_grammar -> level -> unit
-val level_of_notation : notation -> bool (* = onlyprint *) * notation_grammar * level
+val declare_notation_level : notation -> notation_grammar option -> level -> unit
+val level_of_notation : notation -> notation_grammar option * level
(** raise [Not_found] if not declared *)
(** Returns notations with defined parsing/printing rules *)
diff --git a/parsing/ppextend.ml b/parsing/ppextend.ml
index 369db81497..393ab8a302 100644
--- a/parsing/ppextend.ml
+++ b/parsing/ppextend.ml
@@ -60,7 +60,8 @@ let rec unparsing_eq unp1 unp2 = match (unp1,unp2) with
| (UnpMetaVar _ | UnpBinderMetaVar _ | UnpListMetaVar _ |
UnpBinderListMetaVar _ | UnpTerminal _ | UnpBox _ | UnpCut _), _ -> false
-(* Concrete syntax for symbolic-extension table *)
+(* Register generic and specific printing rules *)
+
let generic_notation_printing_rules =
Summary.ref ~name:"generic-notation-printing-rules" (NotationMap.empty : (unparsing_rule * bool * extra_unparsing_rules) NotationMap.t)
diff --git a/test-suite/bugs/closed/bug_9741.v b/test-suite/bugs/closed/bug_9741.v
new file mode 100644
index 0000000000..247155d8b3
--- /dev/null
+++ b/test-suite/bugs/closed/bug_9741.v
@@ -0,0 +1,21 @@
+(* This was failing at parsing *)
+
+Notation "'a'" := tt (only printing).
+Goal True. let a := constr:(1+1) in idtac a. Abort.
+
+(* Idem *)
+
+Require Import Coq.Strings.String.
+Require Import Coq.ZArith.ZArith.
+Open Scope string_scope.
+
+Axiom Ox: string -> Z.
+
+Axiom isMMIOAddr: Z -> Prop.
+
+Notation "'Ox' a" := (Ox a) (only printing, at level 10, format "'Ox' a").
+
+Goal False.
+ set (f := isMMIOAddr).
+ set (x := f (Ox "0018")).
+Abort.
diff --git a/test-suite/output/Implicit.out b/test-suite/output/Implicit.out
index 28afd06fbc..ef7667936c 100644
--- a/test-suite/output/Implicit.out
+++ b/test-suite/output/Implicit.out
@@ -12,3 +12,8 @@ map id' (1 :: nil)
: list nat
map (id'' (A:=nat)) (1 :: nil)
: list nat
+fix f (x : nat) : option nat := match x with
+ | 0 => None
+ | S _ => x
+ end
+ : nat -> option nat
diff --git a/test-suite/output/Implicit.v b/test-suite/output/Implicit.v
index 306532c0df..a7c4399e38 100644
--- a/test-suite/output/Implicit.v
+++ b/test-suite/output/Implicit.v
@@ -51,3 +51,13 @@ Definition id'' (A:Type) (x:A) := x.
Check map (@id'' nat) (1::nil).
+Module MatchBranchesInContext.
+
+Set Implicit Arguments.
+Set Contextual Implicit.
+
+Inductive option A := None | Some (a:A).
+Coercion some_nat := @Some nat.
+Check fix f x := match x with 0 => None | n => some_nat n end.
+
+End MatchBranchesInContext.
diff --git a/test-suite/output/ImplicitTypes.out b/test-suite/output/ImplicitTypes.out
new file mode 100644
index 0000000000..824c260e92
--- /dev/null
+++ b/test-suite/output/ImplicitTypes.out
@@ -0,0 +1,26 @@
+forall b, b = b
+ : Prop
+forall b : nat, b = b
+ : Prop
+forall b : bool, @eq bool b b
+ : Prop
+forall b : bool, b = b
+ : Prop
+forall b c : bool, b = c
+ : Prop
+forall c b : bool, b = c
+ : Prop
+forall b1 b2, b1 = b2
+ : Prop
+fun b => b = b
+ : bool -> Prop
+fix f b (n : nat) {struct n} : bool :=
+ match n with
+ | 0 => b
+ | S p => f b p
+ end
+ : bool -> nat -> bool
+∀ b c : bool, b = c
+ : Prop
+∀ b1 b2, b1 = b2
+ : Prop
diff --git a/test-suite/output/ImplicitTypes.v b/test-suite/output/ImplicitTypes.v
new file mode 100644
index 0000000000..dbc83f9229
--- /dev/null
+++ b/test-suite/output/ImplicitTypes.v
@@ -0,0 +1,37 @@
+Implicit Types b : bool.
+Check forall b, b = b.
+
+(* Check the type is not used if not the reserved one *)
+Check forall b:nat, b = b.
+
+(* Check full printing *)
+Set Printing All.
+Check forall b, b = b.
+Unset Printing All.
+
+(* Check printing of type *)
+Unset Printing Use Implicit Types.
+Check forall b, b = b.
+Set Printing Use Implicit Types.
+
+(* Check factorization: we give priority on factorization over implicit type *)
+Check forall b c, b = c.
+Check forall c b, b = c.
+
+(* Check factorization of implicit types *)
+Check forall b1 b2, b1 = b2.
+
+(* Check in "fun" *)
+Check fun b => b = b.
+
+(* Check in binders *)
+Check fix f b n := match n with 0 => b | S p => f b p end.
+
+(* Check in notations *)
+Module Notation.
+ Notation "∀ x .. y , P" := (forall x, .. (forall y, P) ..)
+ (at level 200, x binder, y binder, right associativity,
+ format "'[ ' '[ ' ∀ x .. y ']' , '/' P ']'") : type_scope.
+ Check forall b c, b = c.
+ Check forall b1 b2, b1 = b2.
+End Notation.
diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index dfc4631572..f6f6c4f1eb 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -324,11 +324,8 @@ let explain_unification_error env sigma p1 p2 = function
strbrk ": cannot ensure that " ++
t ++ strbrk " is a subtype of " ++ u]
| UnifUnivInconsistency p ->
- if !Constrextern.print_universes then
- [str "universe inconsistency: " ++
- Univ.explain_universe_inconsistency (Termops.pr_evd_level sigma) p]
- else
- [str "universe inconsistency"]
+ [str "universe inconsistency: " ++
+ Univ.explain_universe_inconsistency (Termops.pr_evd_level sigma) p]
| CannotSolveConstraint ((pb,env,t,u),e) ->
let env = make_all_name_different env sigma in
(strbrk "cannot satisfy constraint " ++ pr_leconstr_env env sigma t ++
@@ -1375,13 +1372,8 @@ let _ = CErrors.register_handler explain_exn_default
let rec vernac_interp_error_handler = function
| Univ.UniverseInconsistency i ->
- let msg =
- if !Constrextern.print_universes then
- str "." ++ spc() ++
- Univ.explain_universe_inconsistency UnivNames.pr_with_global_universes i
- else
- mt() in
- str "Universe inconsistency" ++ msg ++ str "."
+ str "Universe inconsistency." ++ spc() ++
+ Univ.explain_universe_inconsistency UnivNames.pr_with_global_universes i ++ str "."
| TypeError(ctx,te) ->
let te = map_ptype_error EConstr.of_constr te in
explain_type_error ctx Evd.empty te
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index 3644fa4507..afff0347f5 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -782,7 +782,7 @@ let warn_incompatible_format =
type syntax_parsing_extension = {
synext_level : Notation_gram.level;
synext_notation : notation;
- synext_notgram : notation_grammar;
+ synext_notgram : notation_grammar option;
}
type syntax_printing_extension = {
@@ -827,29 +827,30 @@ let check_and_extend_constr_grammar ntn rule =
let ntn_for_grammar = rule.notgram_notation in
if notation_eq ntn ntn_for_grammar then raise Not_found;
let prec = rule.notgram_level in
- let oldonlyprint,_,oldprec = Notgram_ops.level_of_notation ntn_for_grammar in
- if not (Notgram_ops.level_eq prec oldprec) && not oldonlyprint then error_parsing_incompatible_level ntn ntn_for_grammar oldprec prec;
- if oldonlyprint then raise Not_found
+ let oldparsing,oldprec = Notgram_ops.level_of_notation ntn_for_grammar in
+ if not (Notgram_ops.level_eq prec oldprec) && oldparsing <> None then error_parsing_incompatible_level ntn ntn_for_grammar oldprec prec;
+ if oldparsing = None then raise Not_found
with Not_found ->
Egramcoq.extend_constr_grammar rule
let cache_one_syntax_extension (pa_se,pp_se) =
let ntn = pa_se.synext_notation in
let prec = pa_se.synext_level in
- let onlyprint = pa_se.synext_notgram.notgram_onlyprinting in
(* Check and ensure that the level and the precomputed parsing rule is declared *)
- let parsing_to_activate =
+ let oldparsing =
try
- let oldonlyprint,_,oldprec = Notgram_ops.level_of_notation ntn in
- if not (Notgram_ops.level_eq prec oldprec) && (not oldonlyprint || onlyprint) then error_incompatible_level ntn oldprec prec;
- oldonlyprint && not onlyprint
+ let oldparsing,oldprec = Notgram_ops.level_of_notation ntn in
+ if not (Notgram_ops.level_eq prec oldprec) && (oldparsing <> None || pa_se.synext_notgram = None) then error_incompatible_level ntn oldprec prec;
+ oldparsing
with Not_found ->
(* Declare the level and the precomputed parsing rule *)
- let _ = Notgram_ops.declare_notation_level ntn ~onlyprint pa_se.synext_notgram prec in
- not onlyprint in
+ let _ = Notgram_ops.declare_notation_level ntn pa_se.synext_notgram prec in
+ None in
(* Declare the parsing rule *)
- if parsing_to_activate then
- List.iter (check_and_extend_constr_grammar ntn) pa_se.synext_notgram.notgram_rules;
+ begin match oldparsing, pa_se.synext_notgram with
+ | None, Some grams -> List.iter (check_and_extend_constr_grammar ntn) grams
+ | _ -> (* The grammars rules are canonically derived from the string and the precedence*) ()
+ end;
(* Printing *)
match pp_se with
| None -> ()
@@ -869,7 +870,7 @@ let subst_printing_rule subst x = x
let subst_syntax_extension (subst, (local, (pa_sy,pp_sy))) =
(local, ({ pa_sy with
- synext_notgram = { pa_sy.synext_notgram with notgram_rules = List.map (subst_parsing_rule subst) pa_sy.synext_notgram.notgram_rules }},
+ synext_notgram = Option.map (List.map (subst_parsing_rule subst)) pa_sy.synext_notgram },
Option.map (fun pp_sy -> {pp_sy with synext_unparsing = subst_printing_rule subst pp_sy.synext_unparsing}) pp_sy)
)
@@ -1482,7 +1483,7 @@ exception NoSyntaxRule
let recover_notation_syntax ntn =
let pa =
try
- let _,pa_rule,prec = Notgram_ops.level_of_notation ntn in
+ let pa_rule,prec = Notgram_ops.level_of_notation ntn in
{ synext_level = prec;
synext_notation = ntn;
synext_notgram = pa_rule }
@@ -1501,7 +1502,9 @@ let recover_notation_syntax ntn =
let recover_squash_syntax sy =
let sq,_ = recover_notation_syntax (InConstrEntrySomeLevel,"{ _ }") in
- sy :: sq.synext_notgram.notgram_rules
+ match sq.synext_notgram with
+ | Some gram -> sy :: gram
+ | None -> raise NoSyntaxRule
(**********************************************************************)
(* Main entry point for building parsing and printing rules *)
@@ -1534,10 +1537,13 @@ let make_pp_rule level (typs,symbols) fmt =
let make_parsing_rules (sd : SynData.syn_data) = let open SynData in
let ntn_for_grammar, prec_for_grammar, need_squash = sd.not_data in
- let pa_rule = make_pa_rule prec_for_grammar sd.pa_syntax_data ntn_for_grammar need_squash in {
+ let pa_rule =
+ if sd.only_printing then None
+ else Some (make_pa_rule prec_for_grammar sd.pa_syntax_data ntn_for_grammar need_squash)
+ in {
synext_level = sd.level;
synext_notation = fst sd.info;
- synext_notgram = { notgram_onlyprinting = sd.only_printing; notgram_rules = pa_rule };
+ synext_notgram = pa_rule;
}
let warn_irrelevant_format =
@@ -1606,7 +1612,7 @@ let add_notation_interpretation_core ~local df env ?(impls=empty_internalization
let (pa_sy,pp_sy as sy) = recover_notation_syntax (make_notation_key InConstrEntrySomeLevel symbs) in
let () = Lib.add_anonymous_leaf (inSyntaxExtension (local,sy)) in
(* If the only printing flag has been explicitly requested, put it back *)
- let onlyprint = onlyprint || pa_sy.synext_notgram.notgram_onlyprinting in
+ let onlyprint = onlyprint || pa_sy.synext_notgram = None in
let _,_,_,typs = pa_sy.synext_level in
Some pa_sy.synext_level, typs, onlyprint, pp_sy
end else None, [], false, None in
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 01:59:29 +0000