aboutsummaryrefslogtreecommitdiff
path: root/vernac
diff options
context:
space:
mode:
Diffstat (limited to 'vernac')
-rw-r--r--vernac/comInductive.ml19
-rw-r--r--vernac/g_vernac.mlg2
-rw-r--r--vernac/himsg.ml16
-rw-r--r--vernac/metasyntax.ml166
4 files changed, 94 insertions, 109 deletions
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index 85f2bf3708..edb03a5c89 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -433,26 +433,17 @@ let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) not
then user_err (str "Inductives with uniform parameters may not have attached notations.");
let indnames = List.map (fun ind -> ind.ind_name) indl in
- let sigma, env_params, infos =
+
+ (* In case of template polymorphism, we need to compute more constraints *)
+ let env0 = if poly then env0 else Environ.set_universes_lbound env0 Univ.Level.prop in
+
+ let sigma, env_params, (ctx_params, env_uparams, ctx_uparams, params, userimpls, useruimpls, impls, udecl) =
interp_params env0 udecl uparamsl paramsl
in
(* Interpret the arities *)
let arities = List.map (intern_ind_arity env_params sigma) indl in
- let sigma, env_params, (ctx_params, env_uparams, ctx_uparams, params, userimpls, useruimpls, impls, udecl), arities, is_template =
- let is_template = List.exists (fun (_,_,_,pseudo_poly) -> not (Option.is_empty pseudo_poly)) arities in
- if not poly && is_template then
- (* In case of template polymorphism, we need to compute more constraints *)
- let env0 = Environ.set_universes_lbound env0 Univ.Level.prop in
- let sigma, env_params, infos =
- interp_params env0 udecl uparamsl paramsl
- in
- let arities = List.map (intern_ind_arity env_params sigma) indl in
- sigma, env_params, infos, arities, is_template
- else sigma, env_params, infos, arities, is_template
- in
-
let sigma, arities = List.fold_left_map (pretype_ind_arity env_params) sigma arities in
let arities, relevances, arityconcl, indimpls = List.split4 arities in
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index d597707d12..def4ed942a 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -402,7 +402,7 @@ GRAMMAR EXTEND Gram
;
constructor_list_or_record_decl:
[ [ "|"; l = LIST1 constructor SEP "|" -> { Constructors l }
- | id = identref ; c = constructor_type; "|"; l = LIST0 constructor SEP "|" ->
+ | id = identref ; c = constructor_type; "|"; l = LIST1 constructor SEP "|" ->
{ Constructors ((c id)::l) }
| id = identref ; c = constructor_type -> { Constructors [ c id ] }
| cstr = identref; "{"; fs = record_fields; "}" ->
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 69d9bd4c41..afff0347f5 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -286,32 +286,30 @@ let pr_notation_entry = function
| InConstrEntry -> str "constr"
| InCustomEntry s -> str "custom " ++ str s
-let prec_assoc = let open Gramlib.Gramext in function
- | RightA -> (L,E)
- | LeftA -> (E,L)
- | NonA -> (L,L)
-
let precedence_of_position_and_level from_level = function
- | NumLevel n, BorderProd (_,None) -> n, Prec n
| NumLevel n, BorderProd (b,Some a) ->
- n, let (lp,rp) = prec_assoc a in if b == Left then lp else rp
- | NumLevel n, InternalProd -> n, Prec n
- | NextLevel, _ -> from_level, L
- | DefaultLevel, _ ->
- (* Fake value, waiting for PR#5 at herbelin's fork *) 200,
- Any
+ (let open Gramlib.Gramext in
+ match a, b with
+ | RightA, Left -> LevelLt n
+ | RightA, Right -> LevelLe n
+ | LeftA, Left -> LevelLe n
+ | LeftA, Right -> LevelLt n
+ | NonA, _ -> LevelLt n)
+ | NumLevel n, _ -> LevelLe n
+ | NextLevel, _ -> LevelLt from_level
+ | DefaultLevel, _ -> LevelSome
(** Computing precedences of subentries for parsing *)
let precedence_of_entry_type (from_custom,from_level) = function
| ETConstr (custom,_,x) when notation_entry_eq custom from_custom ->
precedence_of_position_and_level from_level x
- | ETConstr (custom,_,(NumLevel n,_)) -> n, Prec n
+ | ETConstr (custom,_,(NumLevel n,_)) -> LevelLe n
| ETConstr (custom,_,(NextLevel,_)) ->
user_err (strbrk "\"next level\" is only for sub-expressions in the same entry as where the notation is (" ++
quote (pr_notation_entry custom) ++ strbrk " is different from " ++
quote (pr_notation_entry from_custom) ++ str ").")
- | ETPattern (_,n) -> let n = match n with None -> 0 | Some n -> n in n, Prec n
- | _ -> 0, E (* should not matter *)
+ | ETPattern (_,n) -> let n = match n with None -> 0 | Some n -> n in LevelLe n
+ | _ -> LevelSome (* should not matter *)
(** Computing precedences for future insertion of parentheses at
the time of printing using hard-wired constr levels *)
@@ -320,14 +318,14 @@ let unparsing_precedence_of_entry_type from_level = function
(* Possible insertion of parentheses at printing time to deal
with precedence in a constr entry is managed using [prec_less]
in [ppconstr.ml] *)
- snd (precedence_of_position_and_level from_level x)
+ precedence_of_position_and_level from_level x
| ETConstr (custom,_,_) ->
(* Precedence of printing for a custom entry is managed using
explicit insertion of entry coercions at the time of building
a [constr_expr] *)
- Any
- | ETPattern (_,n) -> (* in constr *) Prec (match n with Some n -> n | None -> 0)
- | _ -> Any (* should not matter *)
+ LevelSome
+ | ETPattern (_,n) -> (* in constr *) LevelLe (match n with Some n -> n | None -> 0)
+ | _ -> LevelSome (* should not matter *)
(* Some breaking examples *)
(* "x = y" : "x /1 = y" (breaks before any symbol) *)
@@ -397,11 +395,11 @@ let unparsing_metavar i from typs =
let prec = unparsing_precedence_of_entry_type from x in
match x with
| ETConstr _ | ETGlobal | ETBigint ->
- UnpMetaVar (i,prec)
+ UnpMetaVar prec
| ETPattern _ ->
- UnpBinderMetaVar (i,prec)
+ UnpBinderMetaVar prec
| ETIdent ->
- UnpBinderMetaVar (i,prec)
+ UnpBinderMetaVar prec
| ETBinder isopen ->
assert false
@@ -455,10 +453,10 @@ let make_hunks etyps symbols from_level =
(* We add NonTerminal for simulation but remove it afterwards *)
else make true sl in
let hunk = match typ with
- | ETConstr _ -> UnpListMetaVar (i,prec,List.map snd sl')
+ | ETConstr _ -> UnpListMetaVar (prec,List.map snd sl')
| ETBinder isopen ->
check_open_binder isopen sl m;
- UnpBinderListMetaVar (i,isopen,List.map snd sl')
+ UnpBinderListMetaVar (isopen,List.map snd sl')
| _ -> assert false in
(None, hunk) :: make_with_space b prods
@@ -597,10 +595,10 @@ let hunks_of_format (from_level,(vars,typs)) symfmt =
if not (List.is_empty sl) then error_format ?loc:(find_prod_list_loc loc_slfmt fmt) ();
let symbs, l = aux (symbs,rfmt) in
let hunk = match typ with
- | ETConstr _ -> UnpListMetaVar (i,prec,slfmt)
+ | ETConstr _ -> UnpListMetaVar (prec,slfmt)
| ETBinder isopen ->
check_open_binder isopen sl m;
- UnpBinderListMetaVar (i,isopen,slfmt)
+ UnpBinderListMetaVar (isopen,slfmt)
| _ -> assert false in
symbs, hunk :: l
| symbs, (_,UnpBox (a,b)) :: fmt ->
@@ -745,15 +743,11 @@ let recompute_assoc typs = let open Gramlib.Gramext in
let pr_arg_level from (lev,typ) =
let pplev = function
- | (n,L) when Int.equal n from -> str "at next level"
- | (n,E) -> str "at level " ++ int n
- | (n,L) -> str "at level below " ++ int n
- | (n,Prec m) when Int.equal m n -> str "at level " ++ int n
- | (n,_) -> str "Unknown level" in
- Ppvernac.pr_set_entry_type (fun _ -> (*TO CHECK*) mt()) typ ++
- (match typ with
- | ETConstr _ | ETPattern _ -> spc () ++ pplev lev
- | _ -> mt ())
+ | LevelLt n when Int.equal n from -> spc () ++ str "at next level"
+ | LevelLe n -> spc () ++ str "at level " ++ int n
+ | LevelLt n -> spc () ++ str "at level below " ++ int n
+ | LevelSome -> mt () in
+ Ppvernac.pr_set_entry_type (fun _ -> (*TO CHECK*) mt()) typ ++ pplev lev
let pr_level ntn (from,fromlevel,args,typs) =
(match from with InConstrEntry -> mt () | InCustomEntry s -> str "in " ++ str s ++ spc()) ++
@@ -788,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 = {
@@ -833,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 -> ()
@@ -875,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)
)
@@ -1416,34 +1411,36 @@ let load_notation =
load_notation_common true
let open_notation i (_, nobj) =
- let scope = nobj.notobj_scope in
- let (ntn, df) = nobj.notobj_notation in
- let pat = nobj.notobj_interp in
- let onlyprint = nobj.notobj_onlyprint in
- let deprecation = nobj.notobj_deprecation in
- let specific = match scope with None -> LastLonelyNotation | Some sc -> NotationInScope sc in
- let specific_ntn = (specific,ntn) in
- let fresh = not (Notation.exists_notation_in_scope scope ntn onlyprint pat) in
- if Int.equal i 1 && fresh then begin
- (* Declare the interpretation *)
- let () = Notation.declare_notation_interpretation ntn scope pat df ~onlyprint deprecation in
- (* Declare the uninterpretation *)
- if not nobj.notobj_onlyparse then
- Notation.declare_uninterpretation (NotationRule specific_ntn) pat;
- (* Declare a possible coercion *)
- (match nobj.notobj_coercion with
- | Some (IsEntryCoercion entry) -> Notation.declare_entry_coercion specific_ntn entry
- | Some (IsEntryGlobal (entry,n)) -> Notation.declare_custom_entry_has_global entry n
- | Some (IsEntryIdent (entry,n)) -> Notation.declare_custom_entry_has_ident entry n
- | None -> ())
- end;
- (* Declare specific format if any *)
- match nobj.notobj_specific_pp_rules with
- | Some pp_sy ->
- if specific_format_to_declare specific_ntn pp_sy then
- Ppextend.declare_specific_notation_printing_rules
- specific_ntn ~extra:pp_sy.synext_extra pp_sy.synext_unparsing
- | None -> ()
+ if Int.equal i 1 then begin
+ let scope = nobj.notobj_scope in
+ let (ntn, df) = nobj.notobj_notation in
+ let pat = nobj.notobj_interp in
+ let onlyprint = nobj.notobj_onlyprint in
+ let deprecation = nobj.notobj_deprecation in
+ let specific = match scope with None -> LastLonelyNotation | Some sc -> NotationInScope sc in
+ let specific_ntn = (specific,ntn) in
+ let fresh = not (Notation.exists_notation_in_scope scope ntn onlyprint pat) in
+ if fresh then begin
+ (* Declare the interpretation *)
+ let () = Notation.declare_notation_interpretation ntn scope pat df ~onlyprint deprecation in
+ (* Declare the uninterpretation *)
+ if not nobj.notobj_onlyparse then
+ Notation.declare_uninterpretation (NotationRule specific_ntn) pat;
+ (* Declare a possible coercion *)
+ (match nobj.notobj_coercion with
+ | Some (IsEntryCoercion entry) -> Notation.declare_entry_coercion specific_ntn entry
+ | Some (IsEntryGlobal (entry,n)) -> Notation.declare_custom_entry_has_global entry n
+ | Some (IsEntryIdent (entry,n)) -> Notation.declare_custom_entry_has_ident entry n
+ | None -> ())
+ end;
+ (* Declare specific format if any *)
+ match nobj.notobj_specific_pp_rules with
+ | Some pp_sy ->
+ if specific_format_to_declare specific_ntn pp_sy then
+ Ppextend.declare_specific_notation_printing_rules
+ specific_ntn ~extra:pp_sy.synext_extra pp_sy.synext_unparsing
+ | None -> ()
+ end
let cache_notation o =
load_notation_common false 1 o;
@@ -1486,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 }
@@ -1505,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 *)
@@ -1538,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 =
@@ -1610,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-05-04 23:32:47 +0000