aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2017-08-12 14:23:11 +0200
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2018-02-20 10:03:03 +0100
commit6e1f26a075a48fb32bce32e07d6b58e2f38b97a5 (patch)
tree38babec4eba2840b916402c85df00971804918bd /interp
parent65505b835d6a77b8702d11d09e8cf6b84c529c65 (diff)
More precise explanation when a notation is not reversible for printing.
Diffstat (limited to 'interp')
-rw-r--r--interp/constrintern.mli2
-rw-r--r--interp/notation_ops.ml11
-rw-r--r--interp/notation_ops.mli2
3 files changed, 9 insertions, 6 deletions
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index 632b423b0..87b587b71 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -185,7 +185,7 @@ val global_reference_in_absolute_module : DirPath.t -> Id.t -> Globnames.global_
val interp_notation_constr : env -> ?impls:internalization_env ->
notation_interp_env -> constr_expr ->
(bool * subscopes * notation_var_internalization_type) Id.Map.t *
- notation_constr * reversibility_flag
+ notation_constr * reversibility_status
(** Globalization options *)
val parsing_explicit : bool ref
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 2e3f19a37..472b9de59 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -396,7 +396,7 @@ let notation_constr_and_vars_of_glob_constr a =
t, !found, !has_ltac
let check_variables_and_reversibility nenv (found,foundrec,foundrecbinding) =
- let injective = ref true in
+ let injective = ref [] in
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
@@ -419,7 +419,7 @@ let check_variables_and_reversibility nenv (found,foundrec,foundrecbinding) =
user_err Pp.(str
(Id.to_string x ^
" should not be bound in a recursive pattern of the right-hand side."))
- else injective := false
+ else injective := x :: !injective
in
let check_pair s x y where =
if not (List.mem_f (pair_equal Id.equal Id.equal) (x,y) where) then
@@ -440,12 +440,15 @@ let check_variables_and_reversibility nenv (found,foundrec,foundrecbinding) =
end
| NtnInternTypeIdent -> check_bound x in
Id.Map.iter check_type vars;
- !injective
+ List.rev !injective
let notation_constr_of_glob_constr nenv a =
let a, found, has_ltac = notation_constr_and_vars_of_glob_constr a in
let injective = check_variables_and_reversibility nenv found in
- a, not has_ltac && injective
+ let status = if has_ltac then HasLtac else match injective with
+ | [] -> APrioriReversible
+ | l -> NonInjective l in
+ a, status
(**********************************************************************)
(* Substitution of kernel names, avoiding a list of bound identifiers *)
diff --git a/interp/notation_ops.mli b/interp/notation_ops.mli
index 0904a4ea3..80348c78e 100644
--- a/interp/notation_ops.mli
+++ b/interp/notation_ops.mli
@@ -29,7 +29,7 @@ val ldots_var : Id.t
bound by the notation; also interpret recursive patterns *)
val notation_constr_of_glob_constr : notation_interp_env ->
- glob_constr -> notation_constr * reversibility_flag
+ glob_constr -> notation_constr * reversibility_status
(** Re-interpret a notation as a [glob_constr], taking care of binders *)