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.

5 files changed, 27 insertions, 17 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)