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

10 files changed, 71 insertions, 55 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 2adeb27cc..4e8732c7a 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 2a8085682..5535b6c84 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 87e39aba2..b571d0344 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 d46657b5c..9c4ac8d7e 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 0ab7ec6c7..12c3dcbba 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)
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 6c75e8415..91badbfd7 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -132,7 +132,7 @@ let rec abstract_glob_constr c = function
 
 let interp_casted_constr_with_implicits sigma env impls c  =
   Constrintern.intern_gen Pretyping.WithoutTypeConstraint sigma env ~impls
-    ~allow_patvar:false  ~ltacvars:([],Id.Set.empty) c
+    ~allow_patvar:false  ~ltacvars:(Id.Set.empty, Id.Set.empty) c
 
 (*
    Construct a fixpoint as a Glob_term
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index eca9c7716..b397bcaa3 100644
--- a/tactics/tacintern.ml
+++ b/tactics/tacintern.ml
@@ -305,7 +305,7 @@ let intern_binding_name ist x =
 let intern_constr_gen allow_patvar isarity {ltacvars=lfun; gsigma=sigma; genv=env} c =
   let warn = if !strict_check then fun x -> x else Constrintern.for_grammar in
   let scope = if isarity then Pretyping.IsType else Pretyping.WithoutTypeConstraint in
-  let ltacvars = (Id.Set.elements lfun, Id.Set.empty) in
+  let ltacvars = (lfun, Id.Set.empty) in
   let c' =
     warn (Constrintern.intern_gen scope ~allow_patvar ~ltacvars sigma env) c
   in
@@ -378,7 +378,7 @@ let intern_flag ist red =
 let intern_constr_with_occurrences ist (l,c) = (l,intern_constr ist c)
 
 let intern_constr_pattern ist ~as_type ~ltacvars pc =
-  let ltacvars = Id.Set.elements ltacvars, Id.Set.empty in
+  let ltacvars = ltacvars, Id.Set.empty in
   let metas,pat = Constrintern.intern_constr_pattern
     ist.gsigma ist.genv ~as_type ~ltacvars pc
   in
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 14c8c8f66..30813d530 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -478,9 +478,9 @@ let interp_gen kind ist allow_patvar flags env sigma (c,ce) =
        context at globalization time: we retype with the now known
        intros/lettac/inversion hypothesis names *)
   | Some c ->
-      let fold id _ accu = id :: accu in
-      let ltacvars = Id.Map.fold fold constrvars [] in
-      let bndvars = Id.Map.fold (fun x _ accu -> Id.Set.add x accu) ist.lfun Id.Set.empty in
+      let fold id _ accu = Id.Set.add id accu in
+      let ltacvars = Id.Map.fold fold constrvars Id.Set.empty in
+      let bndvars = Id.Map.fold fold ist.lfun Id.Set.empty in
       let ltacdata = (ltacvars, bndvars) in
       intern_gen kind ~allow_patvar ~ltacvars:ltacdata sigma env c
   in
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 8ec699c71..46037bcbc 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -888,7 +888,7 @@ let set_internalization_type typs =
 let make_internalization_vars recvars mainvars typs =
   let maintyps = List.combine mainvars typs in
   let extratyps = List.map (fun (x,y) -> (y,List.assoc x maintyps)) recvars in
-  maintyps@extratyps
+  maintyps @ extratyps
 
 let make_interpretation_type isrec = function
   | NtnInternTypeConstr when isrec -> NtnTypeConstrList
@@ -901,14 +901,17 @@ let make_interpretation_vars recvars allvars =
     Option.equal String.equal sc1 sc2 &&
     List.equal String.equal l1 l2
   in
-  List.iter (fun (x,y) ->
-    if not (eq_subscope (fst (List.assoc x allvars)) (fst (List.assoc y allvars))) then
-      error_not_same_scope x y) recvars;
+  let check (x, y) =
+    let (scope1, _) = Id.Map.find x allvars in
+    let (scope2, _) = Id.Map.find y allvars in
+    if not (eq_subscope scope1 scope2) then error_not_same_scope x y
+  in
+  let () = List.iter check recvars in
   let useless_recvars = List.map snd recvars in
   let mainvars =
-    List.filter (fun (x,_) -> not (List.mem x useless_recvars)) allvars in
-  List.map (fun (x,(sc,typ)) ->
-    (x,(sc,make_interpretation_type (List.mem_assoc x recvars) typ))) mainvars
+    Id.Map.filter (fun x _ -> not (List.mem x useless_recvars)) allvars in
+  Id.Map.mapi (fun x (sc, typ) ->
+    (sc, make_interpretation_type (List.mem_assoc x recvars) typ)) mainvars
 
 let check_rule_productivity l =
   if List.for_all (function NonTerminal _ -> true | _ -> false) l then
@@ -1160,6 +1163,10 @@ let make_syntax_rules (i_typs,ntn,prec,need_squash,sy_data) =
 (**********************************************************************)
 (* Main functions about notations                                     *)
 
+let to_map l =
+  let fold accu (x, v) = Id.Map.add x v accu in
+  List.fold_left fold Id.Map.empty l
+
 let add_notation_in_scope local df c mods scope =
   let (msgs,i_data,i_typs,sy_data) = compute_syntax_data df mods in
   (* Prepare the parsing and printing rules *)
@@ -1167,13 +1174,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 i_vars recvars c in
+  let (acvars, ac) = interp_notation_constr (to_map i_vars) (to_map recvars) 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 notation = {
     notobj_local = local;
     notobj_scope = scope;
-    notobj_interp = (interp, ac);
+    notobj_interp = (List.map_filter map i_vars, ac);
+    (** Order is important here! *)
     notobj_onlyparse = onlyparse;
     notobj_notation = df';
   } in
@@ -1195,13 +1204,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 i_vars recvars c in
+  let (acvars, ac) = interp_notation_constr ~impls (to_map i_vars) (to_map recvars) 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 notation = {
     notobj_local = local;
     notobj_scope = scope;
-    notobj_interp = (interp, ac);
+    notobj_interp = (List.map_filter map i_vars, ac);
+    (** Order is important here! *)
     notobj_onlyparse = onlyparse;
     notobj_notation = df';
   } in
@@ -1309,9 +1320,11 @@ let add_syntactic_definition ident (vars,c) local onlyparse =
   let vars,pat =
     try [], NRef (try_interp_name_alias (vars,c))
     with Not_found ->
-      let i_vars = List.map (fun id -> (id,NtnInternTypeConstr)) vars in
-      let vars,pat = interp_notation_constr i_vars [] c in
-      List.map (fun (id,(sc,kind)) -> (id,sc)) vars, pat
+      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 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
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 3981d17a9..88da26e83 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1061,7 +1061,7 @@ 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 [] [] t in
+    let t = Notation_ops.notation_constr_of_glob_constr Id.Map.empty Id.Map.empty t in
     Reserve.declare_reserved_type idl t)
   in List.iter sb_decl bl