Data structure telling implicits of local variables is a map in the

intern_env

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

9 files changed, 74 insertions, 70 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 6db69807e..d380e9af6 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -44,7 +44,7 @@ type var_internalization_data =
     scope_name option list
 
 type internalization_env =
-    (identifier * var_internalization_data) list
+    (var_internalization_data) Idmap.t
 
 type glob_binder = (name * binding_kind * glob_constr option * glob_constr)
 
@@ -165,7 +165,7 @@ let error_inductive_parameter_not_implicit loc =
 (* Pre-computing the implicit arguments and arguments scopes needed   *)
 (* for interpretation *)
 
-let empty_internalization_env = []
+let empty_internalization_env = Idmap.empty
 
 let compute_explicitable_implicit imps = function
   | Inductive params ->
@@ -183,8 +183,9 @@ let compute_internalization_data env ty typ impl =
   (ty, expls_impl, impl, compute_arguments_scope typ)
 
 let compute_internalization_env env ty =
-  list_map3
-    (fun id typ impl -> (id,compute_internalization_data env ty typ impl))
+  list_fold_left3
+    (fun map id typ impl -> Idmap.add id (compute_internalization_data env ty typ impl) map)
+    empty_internalization_env
 
 (**********************************************************************)
 (* Contracting "{ _ }" in notations *)
@@ -233,10 +234,11 @@ let contract_pat_notation ntn (l,ll) =
   !ntn',(l,ll)
 
 type intern_env = {
-  ids : Names.Idset.t ;
-  unb : bool ;
-  tmp_scope : Topconstr.tmp_scope_name option ;
-  scopes : Topconstr.scope_name list }
+  ids: Names.Idset.t;
+  unb: bool;
+  tmp_scope: Topconstr.tmp_scope_name option;
+  scopes: Topconstr.scope_name list;
+  impls: internalization_env }
 
 (**********************************************************************)
 (* Remembering the parsing scope of variables in notations            *)
@@ -324,26 +326,26 @@ let locate_if_isevar loc na = function
       with Not_found -> GHole (loc, Evd.BinderType na))
   | x -> x
 
-let check_hidden_implicit_parameters id (_,_,_,impls) =
-  if List.exists (function
-    | (_,(Inductive indparams,_,_,_)) -> List.mem id indparams
+let check_hidden_implicit_parameters id impls =
+  if Idmap.exists (fun _ -> function
+    | (Inductive indparams,_,_,_) -> List.mem id indparams
     | _ -> false) impls
   then
     errorlabstrm "" (strbrk "A parameter of an inductive type " ++
     pr_id id ++ strbrk " is not allowed to be used as a bound variable in the type of its constructor.")
 
-let push_name_env ?(global_level=false) lvar env =
+let push_name_env ?(global_level=false) lvar implargs env =
   function
   | loc,Anonymous ->
       if global_level then
 	user_err_loc (loc,"", str "Anonymous variables not allowed");
       env
   | loc,Name id ->
-      check_hidden_implicit_parameters id lvar;
-      set_var_scope loc id false env (let (_,_,ntnvars,_) = lvar in ntnvars);
+      check_hidden_implicit_parameters id env.impls ;
+      set_var_scope loc id false env (let (_,ntnvars) = lvar in ntnvars);
       if global_level then Dumpglob.dump_definition (loc,id) true "var"
       else Dumpglob.dump_binding loc id;
-      {env with ids = Idset.add id env.ids}
+      {env with ids = Idset.add id env.ids; impls = Idmap.add id implargs env.impls}
 
 let intern_generalized_binder ?(global_level=false) intern_type lvar
     env bl (loc, na) b b' t ty =
@@ -554,11 +556,11 @@ let string_of_ty = function
   | Recursive -> "def"
   | Method -> "meth"
 
-let intern_var genv (ltacvars,namedctxvars,ntnvars,impls) loc id =
+let intern_var genv (ltacvars,ntnvars) namedctx loc id =
   let (ltacvars,unbndltacvars) = ltacvars in
   (* Is [id] an inductive type potentially with implicit *)
   try
-    let ty,expl_impls,impls,argsc = List.assoc id impls in
+    let ty,expl_impls,impls,argsc = Idmap.find id genv.impls in
     let expl_impls = List.map
       (fun id -> CRef (Ident (loc,id)), Some (loc,ExplByName id)) expl_impls in
     let tys = string_of_ty ty in
@@ -570,6 +572,7 @@ let intern_var genv (ltacvars,namedctxvars,ntnvars,impls) loc id =
   then
     GVar (loc,id), [], [], []
   (* Is [id] a notation variable *)
+
   else if List.mem_assoc id ntnvars
   then
     (set_var_scope loc id true genv ntnvars; GVar (loc,id), [], [], [])
@@ -586,7 +589,7 @@ let intern_var genv (ltacvars,namedctxvars,ntnvars,impls) loc id =
       | Some id0 -> Pretype_errors.error_var_not_found_loc loc id0
   with Not_found ->
     (* Is [id] a goal or section variable *)
-    let _ = Sign.lookup_named id namedctxvars in
+    let _ = Sign.lookup_named id namedctx in
       try
 	(* [id] a section variable *)
 	(* Redundant: could be done in intern_qualid *)
@@ -650,12 +653,12 @@ let intern_non_secvar_qualid loc qid intern env lvar args =
     | GRef (loc, VarRef id),_ -> error_global_not_found_loc loc qid
     | r -> r
 
-let intern_applied_reference intern env lvar args = function
+let intern_applied_reference intern env namedctx lvar args = function
   | Qualid (loc, qid) ->
       let r,args2 = intern_qualid loc qid intern env lvar args in
       find_appl_head_data r, args2
   | Ident (loc, id) ->
-      try intern_var env lvar loc id, args
+      try intern_var env lvar namedctx loc id, args
       with Not_found ->
       let qid = qualid_of_ident id in
       try
@@ -671,8 +674,8 @@ let interp_reference vars r =
   let (r,_,_,_),_ =
     intern_applied_reference (fun _ -> error_not_enough_arguments dummy_loc)
       {ids = Idset.empty; unb = false ;
-       tmp_scope = None; scopes = []}
-      (vars,[],[],[]) [] r
+       tmp_scope = None; scopes = []; impls = empty_internalization_env} []
+      (vars,[]) [] r
   in r
 
 let apply_scope_env env = function
@@ -1116,7 +1119,7 @@ let internalize sigma globalenv env allow_patvar lvar c =
   let rec intern env = function
     | CRef ref as x ->
 	let (c,imp,subscopes,l),_ =
-	  intern_applied_reference intern env lvar [] ref in
+	  intern_applied_reference intern env (Environ.named_context globalenv) lvar [] ref in
 	(match intern_impargs c env imp subscopes l with
           | [] -> c
           | l -> GApp (constr_loc x, c, l))
@@ -1207,7 +1210,7 @@ let internalize sigma globalenv env allow_patvar lvar c =
     | CAppExpl (loc, (isproj,ref), args) ->
         let (f,_,args_scopes,_),args =
 	  let args = List.map (fun a -> (a,None)) args in
-	  intern_applied_reference intern env lvar args ref in
+	  intern_applied_reference intern env (Environ.named_context globalenv) lvar args ref in
 	check_projection isproj (List.length args) f;
 	(* Rem: GApp(_,f,[]) stands for @f *)
 	GApp (loc, f, intern_args env args_scopes (List.map fst args))
@@ -1219,7 +1222,7 @@ let internalize sigma globalenv env allow_patvar lvar c =
           | _ -> isproj,f,args in
 	let (c,impargs,args_scopes,l),args =
           match f with
-            | CRef ref -> intern_applied_reference intern env lvar args ref
+            | CRef ref -> intern_applied_reference intern env (Environ.named_context globalenv) lvar args ref
             | CNotation (loc,ntn,([],[],[])) ->
                 let c = intern_notation intern env lvar loc ntn ([],[],[]) in
                 find_appl_head_data c, args
@@ -1431,7 +1434,7 @@ let internalize sigma globalenv env allow_patvar lvar c =
 	  explain_internalization_error e)
 
 (**************************************************************************)
-(* Functions to translate constr_expr into glob_constr                       *)
+(* Functions to translate constr_expr into glob_constr                    *)
 (**************************************************************************)
 
 let extract_ids env =
@@ -1440,13 +1443,14 @@ let extract_ids env =
     Idset.empty
 
 let intern_gen isarity sigma env
-               ?(impls=[]) ?(allow_patvar=false) ?(ltacvars=([],[]))
+               ?(impls=empty_internalization_env) ?(allow_patvar=false) ?(ltacvars=([],[]))
                c =
   let tmp_scope =
     if isarity then Some Notation.type_scope else None in
     internalize sigma env {ids = extract_ids env; unb = false;
-			   tmp_scope = tmp_scope; scopes = []}
-      allow_patvar (ltacvars,Environ.named_context env, [], impls) c
+			   tmp_scope = tmp_scope; scopes = [];
+			  impls = impls}
+      allow_patvar (ltacvars, []) c
 
 let intern_constr sigma env c = intern_gen false sigma env c
 
@@ -1464,7 +1468,7 @@ let intern_pattern env patt =
 (* Functions to parse and interpret constructions *)
 
 let interp_gen kind sigma env
-               ?(impls=[]) ?(allow_patvar=false) ?(ltacvars=([],[]))
+               ?(impls=empty_internalization_env) ?(allow_patvar=false) ?(ltacvars=([],[]))
                c =
   let c = intern_gen (kind=IsType) ~impls ~allow_patvar ~ltacvars sigma env c in
     Default.understand_gen kind sigma env c
@@ -1472,10 +1476,10 @@ let interp_gen kind sigma env
 let interp_constr sigma env c =
   interp_gen (OfType None) sigma env c
 
-let interp_type sigma env ?(impls=[]) c =
+let interp_type sigma env ?(impls=empty_internalization_env) c =
   interp_gen IsType sigma env ~impls c
 
-let interp_casted_constr sigma env ?(impls=[]) c typ =
+let interp_casted_constr sigma env ?(impls=empty_internalization_env) c typ =
   interp_gen (OfType (Some typ)) sigma env ~impls c
 
 let interp_open_constr sigma env c =
@@ -1503,7 +1507,7 @@ let interp_constr_judgment sigma env c =
   Default.understand_judgment sigma env (intern_constr sigma env c)
 
 let interp_constr_evars_gen_impls ?evdref ?(fail_evar=true)
-    env ?(impls=[]) kind c =
+    env ?(impls=empty_internalization_env) kind c =
   let evdref =
     match evdref with
     | None -> ref Evd.empty
@@ -1515,23 +1519,23 @@ let interp_constr_evars_gen_impls ?evdref ?(fail_evar=true)
     Default.understand_tcc_evars ~fail_evar evdref env kind c, imps
 
 let interp_casted_constr_evars_impls ?evdref ?(fail_evar=true)
-    env ?(impls=[]) c typ =
+    env ?(impls=empty_internalization_env) c typ =
   interp_constr_evars_gen_impls ?evdref ~fail_evar env ~impls (OfType (Some typ)) c
 
-let interp_type_evars_impls ?evdref ?(fail_evar=true) env ?(impls=[]) c =
+let interp_type_evars_impls ?evdref ?(fail_evar=true) env ?(impls=empty_internalization_env) c =
   interp_constr_evars_gen_impls ?evdref ~fail_evar env IsType ~impls c
 
-let interp_constr_evars_impls ?evdref ?(fail_evar=true) env ?(impls=[]) c =
+let interp_constr_evars_impls ?evdref ?(fail_evar=true) env ?(impls=empty_internalization_env) c =
   interp_constr_evars_gen_impls ?evdref ~fail_evar env (OfType None) ~impls c
 
-let interp_constr_evars_gen evdref env ?(impls=[]) kind c =
+let interp_constr_evars_gen evdref env ?(impls=empty_internalization_env) kind c =
   let c = intern_gen (kind=IsType) ~impls !evdref env c in
     Default.understand_tcc_evars evdref env kind c
 
-let interp_casted_constr_evars evdref env ?(impls=[]) c typ =
+let interp_casted_constr_evars evdref env ?(impls=empty_internalization_env) c typ =
   interp_constr_evars_gen evdref env ~impls (OfType (Some typ)) c
 
-let interp_type_evars evdref env ?(impls=[]) c =
+let interp_type_evars evdref env ?(impls=empty_internalization_env) c =
   interp_constr_evars_gen evdref env IsType ~impls c
 
 type ltac_sign = identifier list * unbound_ltac_var_map
@@ -1540,13 +1544,13 @@ let intern_constr_pattern sigma env ?(as_type=false) ?(ltacvars=([],[])) c =
   let c = intern_gen as_type ~allow_patvar:true ~ltacvars sigma env c in
   pattern_of_glob_constr c
 
-let interp_aconstr ?(impls=[]) vars recvars a =
+let interp_aconstr ?(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 c = internalize Evd.empty (Global.env()) {ids = extract_ids env; unb = false;
-						tmp_scope = None; scopes = []}
-    false (([],[]),Environ.named_context env,vl,impls) a in
+						tmp_scope = None; scopes = []; impls = impls}
+    false (([],[]),vl) a in
   (* Translate and check that [c] has all its free variables bound in [vars] *)
   let a = aconstr_of_glob_constr vars recvars c in
   (* Splits variables into those that are binding, bound, or both *)
@@ -1577,11 +1581,11 @@ let my_intern_constr sigma env lvar acc c =
 let my_intern_type sigma env lvar acc c = my_intern_constr sigma env lvar (set_type_scope acc) c
 
 let intern_context global_level sigma env params =
-  let lvar = (([],[]),Environ.named_context env, [], []) in
+  let lvar = (([],[]), []) in
     snd (List.fold_left
 	    (intern_local_binder_aux ~global_level (my_intern_constr sigma env lvar) (my_intern_type sigma env lvar) lvar)
 	    ({ids = extract_ids env; unb = false;
-	      tmp_scope = None; scopes = []}, []) params)
+	      tmp_scope = None; scopes = []; impls = empty_internalization_env}, []) params)
 
 let interp_rawcontext_gen understand_type understand_judgment env bl =
   let (env, par, _, impls) =
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index 12dc6be16..2cb706589 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -40,6 +40,7 @@ type var_internalization_type =
   | Inductive of identifier list (* list of params *)
   | Recursive
   | Method
+  | Definition
 
 type var_internalization_data =
     var_internalization_type *
@@ -52,8 +53,7 @@ type var_internalization_data =
     scope_name option list (** subscopes of the args of the variable *)
 
 (** A map of free variables to their implicit arguments and scopes *)
-type internalization_env =
-    (identifier * var_internalization_data) list
+type internalization_env = var_internalization_data Idmap.t
 
 val empty_internalization_env : internalization_env
 
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index e57180327..38492f88b 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -152,8 +152,8 @@ let build_newrecursive
         let arityc = Topconstr.prod_constr_expr arityc bl in
         let arity = Constrintern.interp_type sigma env0 arityc in
 	let impl = Constrintern.compute_internalization_data env0 Constrintern.Recursive arity [] in
-        (Environ.push_named (recname,None,arity) env, (recname, impl) :: impls))
-      (env0,[]) lnameargsardef in
+        (Environ.push_named (recname,None,arity) env, Idmap.add recname impl impls))
+      (env0,Constrintern.empty_internalization_env) lnameargsardef in
   let recdef =
     (* Declare local notations *)
     let fs = States.freeze() in
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index feff5d67c..4217b83fa 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -1410,7 +1410,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
   let equation_id = add_suffix function_name "_equation" in
   let functional_id =  add_suffix function_name "_F" in
   let term_id = add_suffix function_name "_terminate" in
-  let functional_ref = declare_fun functional_id (IsDefinition Definition) res in
+  let functional_ref = declare_fun functional_id (IsDefinition Decl_kinds.Definition) res in
   let env_with_pre_rec_args = push_rel_context(List.map (function (x,t) -> (x,None,t)) pre_rec_args) env in  
   let relation =
     interp_constr
diff --git a/plugins/subtac/subtac_classes.ml b/plugins/subtac/subtac_classes.ml
index aae538389..640d3e60d 100644
--- a/plugins/subtac/subtac_classes.ml
+++ b/plugins/subtac/subtac_classes.ml
@@ -26,11 +26,11 @@ open Util
 
 module SPretyping = Subtac_pretyping.Pretyping
 
-let interp_constr_evars_gen evdref env ?(impls=[]) kind c =
+let interp_constr_evars_gen evdref env ?(impls=Constrintern.empty_internalization_env) kind c =
   SPretyping.understand_tcc_evars evdref env kind
     (intern_gen (kind=IsType) ~impls !evdref env c)
 
-let interp_casted_constr_evars evdref env ?(impls=[]) c typ =
+let interp_casted_constr_evars evdref env ?(impls=Constrintern.empty_internalization_env) c typ =
   interp_constr_evars_gen evdref env ~impls (OfType (Some typ)) c
 
 let interp_context_evars evdref env params =
diff --git a/plugins/subtac/subtac_command.ml b/plugins/subtac/subtac_command.ml
index 9098922e3..6fe31646b 100644
--- a/plugins/subtac/subtac_command.ml
+++ b/plugins/subtac/subtac_command.ml
@@ -52,7 +52,7 @@ let evar_nf isevars c =
   Evarutil.nf_evar !isevars c
 
 let interp_gen kind isevars env
-               ?(impls=[]) ?(allow_patvar=false) ?(ltacvars=([],[]))
+               ?(impls=Constrintern.empty_internalization_env) ?(allow_patvar=false) ?(ltacvars=([],[]))
                c =
   let c' = Constrintern.intern_gen (kind=IsType) ~impls ~allow_patvar ~ltacvars ( !isevars) env c in
   let c' = SPretyping.understand_tcc_evars isevars env kind c' in
@@ -61,13 +61,13 @@ let interp_gen kind isevars env
 let interp_constr isevars env c =
   interp_gen (OfType None) isevars env c
 
-let interp_type_evars isevars env ?(impls=[]) c =
+let interp_type_evars isevars env ?(impls=Constrintern.empty_internalization_env) c =
   interp_gen IsType isevars env ~impls c
 
-let interp_casted_constr isevars env ?(impls=[]) c typ =
+let interp_casted_constr isevars env ?(impls=Constrintern.empty_internalization_env) c typ =
   interp_gen (OfType (Some typ)) isevars env ~impls c
 
-let interp_casted_constr_evars isevars env ?(impls=[]) c typ =
+let interp_casted_constr_evars isevars env ?(impls=Constrintern.empty_internalization_env) c typ =
   interp_gen (OfType (Some typ)) isevars env ~impls c
 
 let interp_open_constr isevars env c =
@@ -300,11 +300,11 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation =
       Constrintern.compute_internalization_data env
 	Constrintern.Recursive full_arity impls 
     in
-    let newimpls = [(recname, (r, l, impls @ 
-      [Some (id_of_string "recproof", Impargs.Manual, (true, false))], 
-			      scopes @ [None]))] in
-    interp_casted_constr isevars ~impls:newimpls
-      (push_rel_context ctx env) body (lift 1 top_arity)
+    let newimpls = Idmap.singleton recname
+      (r, l, impls @ [(Some (id_of_string "recproof", Impargs.Manual, (true, false)))],
+       scopes @ [None]) in
+      interp_casted_constr isevars ~impls:newimpls
+	(push_rel_context ctx env) body (lift 1 top_arity)
   in
   let intern_body_lam = it_mkLambda_or_LetIn intern_body (curry_fun :: lift_lets @ fun_bl) in
   let prop = mkLambda (Name argname, argtyp, top_arity_let) in
diff --git a/theories/Vectors/Fin.v b/theories/Vectors/Fin.v
index b90937a40..97ae56e16 100644
--- a/theories/Vectors/Fin.v
+++ b/theories/Vectors/Fin.v
@@ -53,10 +53,10 @@ fix rectS_fix n (p: t (S n)): P n p:=
   end.
 
 Definition rect2 (P: forall {n} (a b: t n), Type)
-  (H0: forall n, P (S n) F1 F1)
-  (H1: forall n (f: t n), P (S n) F1 (FS f))
-  (H2: forall n (f: t n), P (S n) (FS f) F1)
-  (HS: forall n (f g : t n), P n f g -> P (S n) (FS f) (FS g)):
+  (H0: forall n, P F1 F1)
+  (H1: forall n (f: t n), P F1 (FS f))
+  (H2: forall n (f: t n), P (FS f) F1)
+  (HS: forall n (f g : t n), P f g -> P (FS f) (FS g)):
     forall n (a b: t n), P n a b :=
 fix rect2_fix n (a: t n): forall (b: t n), P n a b :=
 match a with
@@ -64,7 +64,7 @@ match a with
                    return match n' as n0
                           return t n0 -> Type with
                             |0 => fun _ => @ID
-                            |S n0 => fun b0 => P (S n0) F1 b0
+                            |S n0 => fun b0 => P _ F1 b0
                           end b' with
                      |F1 m' => H0 m'
                      |FS m' b' => H1 m' b'
@@ -74,7 +74,7 @@ match a with
                              return t n0 -> Type with
                                |0 => fun _ => @ID
                                |S n0 => fun b0 =>
-                                 forall (a0: t n0), P (S n0) (FS a0) b0
+                                 forall (a0: t n0), P _ (FS a0) b0
                              end b' with
                          |F1 m' => fun aa => H2 m' aa
                          |FS m' b' => fun aa => HS m' aa b' (rect2_fix m' aa b')
diff --git a/theories/Vectors/VectorDef.v b/theories/Vectors/VectorDef.v
index e5bb66a20..150342ee8 100644
--- a/theories/Vectors/VectorDef.v
+++ b/theories/Vectors/VectorDef.v
@@ -34,8 +34,8 @@ Section SCHEMES.
 
 (** An induction scheme for non-empty vectors *)
 Definition rectS {A} (P:forall {n}, t A (S n) -> Type)
- (bas: forall a: A, P 0 (a :: []))
- (rect: forall a {n} (v: t A (S n)), P n v -> P (S n) (a :: v)) :=
+ (bas: forall a: A, P (a :: []))
+ (rect: forall a {n} (v: t A (S n)), P v -> P (a :: v)) :=
  fix rectS_fix {n} (v: t A (S n)) : P n v :=
  match v with
  |nil => @id
diff --git a/toplevel/record.ml b/toplevel/record.ml
index 27b6ffabe..74a33f6f9 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -41,12 +41,12 @@ let interp_fields_evars evars env nots l =
       let impls =
 	match i with
 	| Anonymous -> impls
-	| Name id -> (id, compute_internalization_data env Constrintern.Method t' impl) :: impls
+	| Name id -> Idmap.add id (compute_internalization_data env Constrintern.Method t' impl) impls
       in
       let d = (i,b',t') in
       List.iter (Metasyntax.set_notation_for_interpretation impls) no;
       (push_rel d env, impl :: uimpls, d::params, impls))
-    (env, [], [], []) nots l
+    (env, [], [], empty_internalization_env) nots l
 
 let binder_of_decl = function
   | Vernacexpr.AssumExpr(n,t) -> (n,None,t)