aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--interp/constrintern.ml6
-rw-r--r--interp/constrintern.mli3
-rw-r--r--interp/notation_ops.ml22
-rw-r--r--interp/notation_ops.mli5
-rw-r--r--interp/reserve.ml8
-rw-r--r--intf/notation_term.mli6
-rw-r--r--toplevel/metasyntax.ml43
-rw-r--r--toplevel/vernacentries.ml8
8 files changed, 74 insertions, 27 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index e9ebcf39f..cc4655315 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1799,15 +1799,15 @@ let intern_constr_pattern env ?(as_type=false) ?(ltacvars=empty_ltac_sign) c =
~allow_patvar:true ~ltacvars env c in
pattern_of_glob_constr c
-let interp_notation_constr ?(impls=empty_internalization_env) vars recvars a =
+let interp_notation_constr ?(impls=empty_internalization_env) nenv a =
let env = Global.env () in
(* [vl] is intended to remember the scope of the free variables of [a] *)
- let vl = Id.Map.map (fun typ -> (ref None, typ)) vars in
+ let vl = Id.Map.map (fun typ -> (ref None, typ)) nenv.ninterp_var_type in
let c = internalize (Global.env()) {ids = extract_ids env; unb = false;
tmp_scope = None; scopes = []; impls = impls}
false (empty_ltac_sign, vl) a in
(* Translate and check that [c] has all its free variables bound in [vars] *)
- let a = notation_constr_of_glob_constr vars recvars c in
+ let a = notation_constr_of_glob_constr nenv c in
(* Splits variables into those that are binding, bound, or both *)
(* binding and bound *)
let out_scope = function None -> None,[] | Some (a,l) -> a,l in
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index bbee24957..90c3779fc 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -165,8 +165,7 @@ val global_reference_in_absolute_module : DirPath.t -> Id.t -> constr
(** Interprets a term as the left-hand side of a notation. The returned map is
guaranteed to have the same domain as the input one. *)
val interp_notation_constr : ?impls:internalization_env ->
- notation_var_internalization_type Id.Map.t ->
- Id.t Id.Map.t -> constr_expr ->
+ notation_interp_env -> constr_expr ->
(subscopes * notation_var_internalization_type) Id.Map.t *
notation_constr
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 10b088481..ce9deb0db 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -300,10 +300,12 @@ let notation_constr_and_vars_of_glob_constr a =
let pair_equal eq1 eq2 (a,b) (a',b') = eq1 a a' && eq2 b b'
-let check_variables vars recvars (found,foundrec,foundrecbinding) =
+let check_variables nenv (found,foundrec,foundrecbinding) =
+ let recvars = nenv.ninterp_rec_vars in
let fold _ y accu = Id.Set.add y accu in
let useless_vars = Id.Map.fold fold recvars Id.Set.empty in
- let vars = Id.Map.filter (fun y _ -> not (Id.Set.mem y useless_vars)) vars in
+ let filter y _ = not (Id.Set.mem y useless_vars) in
+ let vars = Id.Map.filter filter nenv.ninterp_var_type in
let check_recvar x =
if Id.List.mem x found then
errorlabstrm "" (pr_id x ++
@@ -321,8 +323,7 @@ let check_variables vars recvars (found,foundrec,foundrecbinding) =
error
(Id.to_string x ^
" should not be bound in a recursive pattern of the right-hand side.")
- else
- error (Id.to_string x ^ " is unbound in the right-hand side.")
+ else nenv.ninterp_only_parse <- true
in
let check_pair s x y where =
if not (List.mem_f (pair_equal Id.equal Id.equal) (x,y) where) then
@@ -344,16 +345,21 @@ let check_variables vars recvars (found,foundrec,foundrecbinding) =
| NtnInternTypeIdent -> check_bound x in
Id.Map.iter check_type vars
-let notation_constr_of_glob_constr vars recvars a =
- let a,found = notation_constr_and_vars_of_glob_constr a in
- check_variables vars recvars found;
+let notation_constr_of_glob_constr nenv a =
+ let a, found = notation_constr_and_vars_of_glob_constr a in
+ let () = check_variables nenv found in
a
(* Substitution of kernel names, avoiding a list of bound identifiers *)
let notation_constr_of_constr avoiding t =
let t = Detyping.detype false avoiding [] t in
- notation_constr_of_glob_constr Id.Map.empty Id.Map.empty t
+ let nenv = {
+ ninterp_var_type = Id.Map.empty;
+ ninterp_rec_vars = Id.Map.empty;
+ ninterp_only_parse = false;
+ } in
+ notation_constr_of_glob_constr nenv t
let rec subst_pat subst pat =
match pat with
diff --git a/interp/notation_ops.mli b/interp/notation_ops.mli
index 9c4ac8d7e..4f84af5fe 100644
--- a/interp/notation_ops.mli
+++ b/interp/notation_ops.mli
@@ -16,9 +16,8 @@ open Glob_term
(** Translate a [glob_constr] into a notation given the list of variables
bound by the notation; also interpret recursive patterns *)
-val notation_constr_of_glob_constr :
- notation_var_internalization_type Id.Map.t ->
- Id.t Id.Map.t -> glob_constr -> notation_constr
+val notation_constr_of_glob_constr : notation_interp_env ->
+ glob_constr -> notation_constr
(** Name of the special identifier used to encode recursive notations *)
val ldots_var : Id.t
diff --git a/interp/reserve.ml b/interp/reserve.ml
index 77ca9e267..4328be7d8 100644
--- a/interp/reserve.ml
+++ b/interp/reserve.ml
@@ -107,12 +107,18 @@ let _ = Namegen.set_reserved_typed_name revert_reserved_type
open Glob_term
+let default_env () = {
+ ninterp_var_type = Id.Map.empty;
+ ninterp_rec_vars = Id.Map.empty;
+ ninterp_only_parse = false;
+}
+
let anonymize_if_reserved na t = match na with
| Name id as na ->
(try
if not !Flags.raw_print &&
(try
- let ntn = notation_constr_of_glob_constr Id.Map.empty Id.Map.empty t in
+ let ntn = notation_constr_of_glob_constr (default_env ()) t in
Pervasives.(=) ntn (find_reserved_type id) (** FIXME *)
with UserError _ -> false)
then GHole (Loc.ghost,Evar_kinds.BinderType na,None)
diff --git a/intf/notation_term.mli b/intf/notation_term.mli
index 411b14f1f..ac5e0f5f9 100644
--- a/intf/notation_term.mli
+++ b/intf/notation_term.mli
@@ -73,3 +73,9 @@ type notation_var_internalization_type =
type interpretation =
(Id.t * (subscopes * notation_var_instance_type)) list *
notation_constr
+
+type notation_interp_env = {
+ ninterp_var_type : notation_var_internalization_type Id.Map.t;
+ ninterp_rec_vars : Id.t Id.Map.t;
+ mutable ninterp_only_parse : bool;
+}
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index b2493a2a1..0aec4a7b7 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -924,9 +924,17 @@ let check_rule_productivity l =
if (match l with SProdList _ :: _ -> true | _ -> false) then
error "A recursive notation must start with at least one symbol."
-let is_not_printable = function
- | NVar _ -> msg_warning (strbrk "This notation will not be used for printing as it is bound to a single variable."); true
- | _ -> false
+let is_not_printable onlyparse noninjective = function
+| NVar _ ->
+ let () = if not onlyparse then
+ msg_warning (strbrk "This notation will not be used for printing as it is bound to a single variable.")
+ in
+ true
+| _ ->
+ if not onlyparse && noninjective then
+ let () = msg_warning (strbrk "This notation will not be used for printing as it is not reversible.") in
+ true
+ else false
let find_precedence lev etyps symbols =
match symbols with
@@ -1178,10 +1186,15 @@ let add_notation_in_scope local df c mods scope =
(* Prepare the interpretation *)
let (onlyparse, recvars,mainvars, df') = i_data in
let i_vars = make_internalization_vars recvars mainvars i_typs in
- let (acvars, ac) = interp_notation_constr (to_map i_vars) (to_map recvars) c in
+ let nenv = {
+ ninterp_var_type = to_map i_vars;
+ ninterp_rec_vars = to_map recvars;
+ ninterp_only_parse = false;
+ } in
+ let (acvars, ac) = interp_notation_constr nenv c in
let interp = make_interpretation_vars recvars acvars in
let map (x, _) = try Some (x, Id.Map.find x interp) with Not_found -> None in
- let onlyparse = onlyparse || is_not_printable ac in
+ let onlyparse = is_not_printable onlyparse nenv.ninterp_only_parse ac in
let notation = {
notobj_local = local;
notobj_scope = scope;
@@ -1208,10 +1221,15 @@ let add_notation_interpretation_core local df ?(impls=empty_internalization_env)
let path = (Lib.library_dp(),Lib.current_dirpath true) in
let df' = (make_notation_key symbs,(path,df)) in
let i_vars = make_internalization_vars recvars mainvars i_typs in
- let (acvars, ac) = interp_notation_constr ~impls (to_map i_vars) (to_map recvars) c in
+ let nenv = {
+ ninterp_var_type = to_map i_vars;
+ ninterp_rec_vars = to_map recvars;
+ ninterp_only_parse = false;
+ } in
+ let (acvars, ac) = interp_notation_constr ~impls nenv c in
let interp = make_interpretation_vars recvars acvars in
let map (x, _) = try Some (x, Id.Map.find x interp) with Not_found -> None in
- let onlyparse = onlyparse || is_not_printable ac in
+ let onlyparse = is_not_printable onlyparse nenv.ninterp_only_parse ac in
let notation = {
notobj_local = local;
notobj_scope = scope;
@@ -1321,17 +1339,24 @@ let try_interp_name_alias = function
| _ -> raise Not_found
let add_syntactic_definition ident (vars,c) local onlyparse =
+ let nonprintable = ref false in
let vars,pat =
try [], NRef (try_interp_name_alias (vars,c))
with Not_found ->
let fold accu id = Id.Map.add id NtnInternTypeConstr accu in
let i_vars = List.fold_left fold Id.Map.empty vars in
- let nvars, pat = interp_notation_constr i_vars Id.Map.empty c in
+ let nenv = {
+ ninterp_var_type = i_vars;
+ ninterp_rec_vars = Id.Map.empty;
+ ninterp_only_parse = false;
+ } in
+ let nvars, pat = interp_notation_constr nenv c in
+ let () = nonprintable := nenv.ninterp_only_parse in
let map id = let (sc, _) = Id.Map.find id nvars in (id, sc) in
List.map map vars, pat
in
let onlyparse = match onlyparse with
- | None when (is_not_printable pat) -> Some Flags.Current
+ | None when (is_not_printable false !nonprintable pat) -> Some Flags.Current
| p -> p
in
Syntax_def.declare_syntactic_definition local ident onlyparse (vars,pat)
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 399471b74..b8a368c82 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1006,11 +1006,17 @@ let vernac_declare_arguments locality r l nargs flags =
(make_section_locality locality) c (rargs, nargs, flags)
| _ -> errorlabstrm "" (strbrk "Modifiers of the behavior of the simpl tactic are relevant for constants only.")
+let default_env () = {
+ Notation_term.ninterp_var_type = Id.Map.empty;
+ ninterp_rec_vars = Id.Map.empty;
+ ninterp_only_parse = false;
+}
+
let vernac_reserve bl =
let sb_decl = (fun (idl,c) ->
let t = Constrintern.interp_type Evd.empty (Global.env()) c in
let t = Detyping.detype false [] [] t in
- let t = Notation_ops.notation_constr_of_glob_constr Id.Map.empty Id.Map.empty t in
+ let t = Notation_ops.notation_constr_of_glob_constr (default_env ()) t in
Reserve.declare_reserved_type idl t)
in List.iter sb_decl bl
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-09 19:43:23 +0000