Notations can now accept dummy arguments. If ever a bound variable is not

used, they are automatically flagged as only parsing. CAVEAT: unused
arguments are not typechecked, because they are dropped before the
interpretation phase.

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