Replacing uses of association lists by maps in notations.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16655 85f007b7-540e-0410-9357-904b9bb8a0f7

5 files changed, 37 insertions, 34 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 2adeb27cc5..4e8732c7aa 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -271,7 +271,7 @@ let error_expect_binder_notation_type loc id =
 
 let set_var_scope loc id istermvar env ntnvars =
   try
-    let idscopes,typ = List.assoc id ntnvars in
+    let idscopes,typ = Id.Map.find id ntnvars in
     let () = if istermvar then
       (* scopes have no effect on the interpretation of identifiers *)
       begin match !idscopes with
@@ -381,7 +381,8 @@ let push_name_env ?(global_level=false) lvar implargs env =
   | loc,Name id ->
       check_hidden_implicit_parameters id env.impls ;
       let (_,ntnvars) = lvar in
-      if ntnvars = [] && Id.equal id ldots_var then error_ldots_var loc;
+      if Id.Map.is_empty ntnvars && Id.equal id ldots_var
+        then error_ldots_var loc;
       set_var_scope loc id false env ntnvars;
       if global_level then Dumpglob.dump_definition (loc,id) true "var"
       else Dumpglob.dump_binding loc id;
@@ -621,17 +622,18 @@ let intern_var genv (ltacvars,ntnvars) namedctx loc id =
     GVar (loc,id), make_implicits_list impls, argsc, expl_impls
   with Not_found ->
   (* Is [id] bound in current term or is an ltac var bound to constr *)
-  if Id.Set.mem id genv.ids or List.mem id ltacvars
+  if Id.Set.mem id genv.ids or Id.Set.mem id ltacvars
   then
     GVar (loc,id), [], [], []
   (* Is [id] a notation variable *)
-  else if List.mem_assoc id ntnvars
+  else if Id.Map.mem id ntnvars
   then
     (set_var_scope loc id true genv ntnvars; GVar (loc,id), [], [], [])
   (* Is [id] the special variable for recursive notations *)
   else if Id.equal id ldots_var
-  then
-    if ntnvars != [] then GVar (loc,id), [], [], [] else error_ldots_var loc
+  then if Id.Map.is_empty ntnvars
+    then error_ldots_var loc
+    else GVar (loc,id), [], [], []
   else if Id.Set.mem id unbndltacvars then
     (* Is [id] bound to a free name in ltac (this is an ltac error message) *)
     user_err_loc (loc,"intern_var",
@@ -751,7 +753,7 @@ let interp_reference vars r =
     intern_applied_reference (fun _ -> error_not_enough_arguments Loc.ghost)
       {ids = Id.Set.empty; unb = false ;
        tmp_scope = None; scopes = []; impls = empty_internalization_env} []
-      (vars,[]) [] r
+      (vars, Id.Map.empty) [] r
   in r
 
 (**********************************************************************)
@@ -1536,7 +1538,7 @@ let internalize sigma globalenv env allow_patvar lvar c =
     let tm' = intern env tm in
     (* the "as" part *)
     let extra_id,na = match tm', na with
-      | GVar (loc,id), None when not (List.mem_assoc id (snd lvar)) -> Some id,(loc,Name id)
+      | GVar (loc,id), None when not (Id.Map.mem id (snd lvar)) -> Some id,(loc,Name id)
       | GRef (loc, VarRef id), None -> Some id,(loc,Name id)
       | _, None -> None,(Loc.ghost,Anonymous)
       | _, Some (loc,na) -> None,(loc,na) in
@@ -1659,9 +1661,9 @@ let scope_of_type_kind = function
   | OfType typ -> compute_type_scope typ
   | WithoutTypeConstraint -> None
 
-type ltac_sign = Id.t list * Id.Set.t
+type ltac_sign = Id.Set.t * Id.Set.t
 
-let empty_ltac_sign = ([], Id.Set.empty)
+let empty_ltac_sign = (Id.Set.empty, Id.Set.empty)
 
 let intern_gen kind sigma env
                ?(impls=empty_internalization_env) ?(allow_patvar=false) ?(ltacvars=empty_ltac_sign)
@@ -1670,7 +1672,7 @@ let intern_gen kind sigma env
   internalize sigma env {ids = extract_ids env; unb = false;
 		         tmp_scope = tmp_scope; scopes = [];
 			 impls = impls}
-    allow_patvar (ltacvars, []) c
+    allow_patvar (ltacvars, Id.Map.empty) c
 
 let intern_constr sigma env c = intern_gen WithoutTypeConstraint sigma env c
 
@@ -1751,7 +1753,7 @@ let intern_constr_pattern sigma env ?(as_type=false) ?(ltacvars=empty_ltac_sign)
 let interp_notation_constr ?(impls=empty_internalization_env) vars recvars a =
   let env = Global.env () in
   (* [vl] is intended to remember the scope of the free variables of [a] *)
-  let vl = List.map (fun (id,typ) -> (id,(ref None,typ))) vars in
+  let vl = Id.Map.map (fun typ -> (ref None, typ)) vars in
   let c = internalize Evd.empty (Global.env()) {ids = extract_ids env; unb = false;
 						tmp_scope = None; scopes = []; impls = impls}
     false (empty_ltac_sign, vl) a in
@@ -1760,7 +1762,7 @@ let interp_notation_constr ?(impls=empty_internalization_env) vars recvars a =
   (* 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
-  let vars = List.map (fun (id,(sc,typ)) -> (id,(out_scope !sc,typ))) vl in
+  let vars = Id.Map.map (fun (sc, typ) -> (out_scope !sc, typ)) vl in
   (* Returns [a] and the ordered list of variables with their scopes *)
   vars, a
 
@@ -1783,7 +1785,7 @@ let my_intern_constr sigma env lvar acc c =
 
 let intern_context global_level sigma env impl_env binders =
   try
-  let lvar = (empty_ltac_sign, []) in
+  let lvar = (empty_ltac_sign, Id.Map.empty) in
   let lenv, bl = List.fold_left
 	    (intern_local_binder_aux ~global_level (my_intern_constr sigma env lvar) lvar)
 	    ({ids = extract_ids env; unb = false;
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index 2a80856827..5535b6c84e 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -68,7 +68,7 @@ val compute_internalization_env : env -> var_internalization_type ->
   Id.t list -> types list -> Impargs.manual_explicitation list list ->
   internalization_env
 
-type ltac_sign = Id.t list * Id.Set.t
+type ltac_sign = Id.Set.t * Id.Set.t
 
 type glob_binder = (Name.t * binding_kind * glob_constr option * glob_constr)
 
@@ -163,14 +163,12 @@ val construct_reference : named_context -> Id.t -> constr
 val global_reference : Id.t -> constr
 val global_reference_in_absolute_module : DirPath.t -> Id.t -> constr
 
-(** Interprets a term as the left-hand side of a notation; the boolean
-    list is a set and this set is [true] for a variable occurring in
-    term position, [false] for a variable occurring in binding
-    position; [true;false] if in both kinds of position *)
+(** 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 ->
-  (Id.t * notation_var_internalization_type) list ->
-  (Id.t * Id.t) list -> constr_expr ->
-  (Id.t * (subscopes * notation_var_internalization_type)) list *
+  notation_var_internalization_type Id.Map.t ->
+  Id.t Id.Map.t -> constr_expr ->
+  (subscopes * notation_var_internalization_type) Id.Map.t *
   notation_constr
 
 (** Globalization options *)
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 87e39aba2b..b571d03442 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -303,14 +303,16 @@ let rec list_rev_mem_assoc x = function
   | (_,x')::l -> Id.equal x x' || list_rev_mem_assoc x l
 
 let check_variables vars recvars (found,foundrec,foundrecbinding) =
-  let useless_vars = List.map snd recvars in
-  let vars = List.filter (fun (y,_) -> not (List.mem y useless_vars)) 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 check_recvar x =
     if List.mem x found then
       errorlabstrm "" (pr_id x ++
 	strbrk " should only be used in the recursive part of a pattern.") in
-  List.iter (fun (x,y) -> check_recvar x; check_recvar y)
-    (foundrec@foundrecbinding);
+  let check (x, y) = check_recvar x; check_recvar y in
+  let () = List.iter check foundrec in
+  let () = List.iter check foundrecbinding in
   let check_bound x =
     if not (List.mem x found) then
       if List.mem_assoc x foundrec or List.mem_assoc x foundrecbinding
@@ -324,20 +326,20 @@ let check_variables vars recvars (found,foundrec,foundrecbinding) =
       errorlabstrm "" (strbrk "in the right-hand side, " ++ pr_id x ++
 	str " and " ++ pr_id y ++ strbrk " should appear in " ++ str s ++
 	str " position as part of a recursive pattern.") in
-  let check_type (x,typ) =
+  let check_type x typ =
     match typ with
     | NtnInternTypeConstr ->
 	begin
-	  try check_pair "term" x (List.assoc x recvars) foundrec
+	  try check_pair "term" x (Id.Map.find x recvars) foundrec
 	  with Not_found -> check_bound x
 	end
     | NtnInternTypeBinder ->
 	begin
-	  try check_pair "binding" x (List.assoc x recvars) foundrecbinding
+	  try check_pair "binding" x (Id.Map.find x recvars) foundrecbinding
 	  with Not_found -> check_bound x
 	end
     | NtnInternTypeIdent -> check_bound x in
-  List.iter check_type vars
+  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
@@ -347,7 +349,8 @@ let notation_constr_of_glob_constr vars recvars a =
 (* Substitution of kernel names, avoiding a list of bound identifiers *)
 
 let notation_constr_of_constr avoiding t =
- notation_constr_of_glob_constr [] [] (Detyping.detype false avoiding [] t)
+  let t = Detyping.detype false avoiding [] t in
+  notation_constr_of_glob_constr Id.Map.empty Id.Map.empty t
 
 let rec subst_pat subst pat =
   match pat with
diff --git a/interp/notation_ops.mli b/interp/notation_ops.mli
index d46657b5c7..9c4ac8d7ec 100644
--- a/interp/notation_ops.mli
+++ b/interp/notation_ops.mli
@@ -17,8 +17,8 @@ open Glob_term
     bound by the notation; also interpret recursive patterns           *)
 
 val notation_constr_of_glob_constr :
-  (Id.t * notation_var_internalization_type) list ->
-  (Id.t * Id.t) list -> glob_constr -> notation_constr
+  notation_var_internalization_type Id.Map.t ->
+  Id.t Id.Map.t -> 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 0ab7ec6c7d..12c3dcbba3 100644
--- a/interp/reserve.ml
+++ b/interp/reserve.ml
@@ -112,7 +112,7 @@ let anonymize_if_reserved na t = match na with
       (try
 	if not !Flags.raw_print &&
 	   (try
-            let ntn = notation_constr_of_glob_constr [] [] t in
+            let ntn = notation_constr_of_glob_constr Id.Map.empty Id.Map.empty t in
             Pervasives.(=) ntn (find_reserved_type id) (** FIXME *)
             with UserError _ -> false)
 	then GHole (Loc.ghost,Evar_kinds.BinderType na)