diff options
| -rw-r--r-- | interp/constrintern.mli | 2 | ||||
| -rw-r--r-- | interp/notation_ops.ml | 11 | ||||
| -rw-r--r-- | interp/notation_ops.mli | 2 | ||||
| -rw-r--r-- | intf/notation_term.ml | 2 | ||||
| -rw-r--r-- | vernac/metasyntax.ml | 40 |
5 files changed, 33 insertions, 24 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 *) diff --git a/intf/notation_term.ml b/intf/notation_term.ml index cad6f4b82..d1cbb6a33 100644 --- a/intf/notation_term.ml +++ b/intf/notation_term.ml @@ -74,7 +74,7 @@ type interpretation = (Id.t * (subscopes * notation_var_instance_type)) list * notation_constr -type reversibility_flag = bool +type reversibility_status = APrioriReversible | HasLtac | NonInjective of Id.t list type notation_interp_env = { ninterp_var_type : notation_var_internalization_type Id.Map.t; diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index 3be357598..c295434d0 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -979,16 +979,24 @@ let warn_notation_bound_to_variable = let warn_non_reversible_notation = CWarnings.create ~name:"non-reversible-notation" ~category:"parsing" - (fun () -> - strbrk "This notation will not be used for printing as it is not reversible.") - -let is_not_printable onlyparse nonreversible = function + (function + | APrioriReversible -> assert false + | HasLtac -> + strbrk "This notation contains Ltac expressions: it will not be used for printing." + | NonInjective ids -> + let n = List.length ids in + strbrk (String.plural n "Variable") ++ spc () ++ pr_enum Id.print ids ++ spc () ++ + strbrk (if n > 1 then "do" else "does") ++ + str " not occur in the right-hand side." ++ spc() ++ + strbrk "The notation will not be used for printing as it is not reversible.") + +let is_not_printable onlyparse reversibility = function | NVar _ -> if not onlyparse then warn_notation_bound_to_variable (); true | _ -> - if not onlyparse && nonreversible then - (warn_non_reversible_notation (); true) + if not onlyparse && reversibility <> APrioriReversible then + (warn_non_reversible_notation reversibility; true) else onlyparse let find_precedence lev etyps symbols onlyprint = @@ -1329,10 +1337,10 @@ let add_notation_in_scope local df env c mods scope = ninterp_var_type = to_map i_vars; ninterp_rec_vars = to_map sd.recvars; } in - let (acvars, ac, reversible) = interp_notation_constr env nenv c in + let (acvars, ac, reversibility) = interp_notation_constr env nenv c in let interp = make_interpretation_vars sd.recvars acvars in let map (x, _) = try Some (x, Id.Map.find x interp) with Not_found -> None in - let onlyparse = is_not_printable sd.only_parsing (not reversible) ac in + let onlyparse = is_not_printable sd.only_parsing reversibility ac in let notation = { notobj_local = local; notobj_scope = scope; @@ -1368,10 +1376,10 @@ let add_notation_interpretation_core local df env ?(impls=empty_internalization_ ninterp_var_type = to_map i_vars; ninterp_rec_vars = to_map recvars; } in - let (acvars, ac, reversible) = interp_notation_constr env ~impls nenv c in + let (acvars, ac, reversibility) = interp_notation_constr env ~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 = is_not_printable onlyparse (not reversible) ac in + let onlyparse = is_not_printable onlyparse reversibility ac in let notation = { notobj_local = local; notobj_scope = scope; @@ -1499,9 +1507,8 @@ let try_interp_name_alias = function | _ -> raise Not_found let add_syntactic_definition env ident (vars,c) local onlyparse = - let nonprintable = ref false in - let vars,pat = - try [], NRef (try_interp_name_alias (vars,c)) + let vars,reversibility,pat = + try [], APrioriReversible, 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 @@ -1509,13 +1516,12 @@ let add_syntactic_definition env ident (vars,c) local onlyparse = ninterp_var_type = i_vars; ninterp_rec_vars = Id.Map.empty; } in - let nvars, pat, reversible = interp_notation_constr env nenv c in - let () = nonprintable := not reversible in + let nvars, pat, reversibility = interp_notation_constr env nenv c in let map id = let (_,sc,_) = Id.Map.find id nvars in (id, sc) in - List.map map vars, pat + List.map map vars, reversibility, pat in let onlyparse = match onlyparse with - | None when (is_not_printable false !nonprintable pat) -> Some Flags.Current + | None when (is_not_printable false reversibility pat) -> Some Flags.Current | p -> p in Syntax_def.declare_syntactic_definition local ident onlyparse (vars,pat) |