Gestion maintenant purement fonctionnelle des implicites des point-fixes; ajout de la prise en compte dynamique des arguments scope pour les inductifs

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

4 files changed, 53 insertions, 39 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 2ccd2f69c3..c46cad89be 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -22,11 +22,13 @@ open Topconstr
 open Nametab
 open Symbols
 
-type implicits_env = (* To interpret inductive type with implicits *)
-    (identifier * (identifier list * Impargs.implicits_list)) list
+(* To interpret implicits and arg scopes of recursive variables in
+   inductive types and recursive definitions *)
+type var_internalisation_data =
+    identifier list * Impargs.implicits_list * scope_name option list
 
-type full_implicits_env =
-    identifier list * implicits_env
+type implicits_env = (identifier * var_internalisation_data) list
+type full_implicits_env = identifier list * implicits_env
 
 let interning_grammar = ref false
 
@@ -233,17 +235,17 @@ let intern_var (env,_,_ as genv) (ltacvars,vars2,vars3,_,impls) loc id =
   let (vars1,unbndltacvars) = ltacvars in
   (* Is [id] an inductive type potentially with implicit *)
   try
-    let l,impl = List.assoc id impls in
+    let l,impl,argsc = List.assoc id impls in
     let l = List.map 
       (fun id -> CRef (Ident (loc,id)), Some (loc,ExplByName id)) l in
-    RVar (loc,id), impl, [],
+    RVar (loc,id), impl, argsc,
     (if !Options.v7 & !interning_grammar then [] else l)
   with Not_found ->
   (* Is [id] bound in current env or is an ltac var bound to constr *)
   if Idset.mem id env or List.mem id vars1
   then
       RVar (loc,id), [], [], []
-  (* Is [id] a notation variables *)
+  (* Is [id] a notation variable *)
   else if List.mem_assoc id vars3
   then
     (set_var_scope loc id genv vars3; RVar (loc,id), [], [], [])
@@ -256,15 +258,16 @@ let intern_var (env,_,_ as genv) (ltacvars,vars2,vars3,_,impls) loc id =
 	  pr_id id ++ str " ist not bound to a term")
       | Some id0 -> Pretype_errors.error_var_not_found_loc loc id0
   with Not_found ->
-  (* Is [id] a section variable *)
+  (* Is [id] a goal or section variable *)
   let _ = Sign.lookup_named id vars2 in
-  (* Car Fixpoint met les fns définies temporairement comme vars de sect *)
-  let imps, args_scopes =
-    try
-      let ref = VarRef id in
-      implicits_of_global ref, find_arguments_scope ref
-    with _ -> [], [] in
-  RRef (loc, VarRef id), imps, args_scopes, []
+  try
+    (* [id] a section variable *)
+    (* Redundant: could be done in intern_qualid *)
+    let ref = VarRef id in
+    RRef (loc, ref), implicits_of_global ref, find_arguments_scope ref, []
+  with _ ->
+    (* [id] a goal variable *)
+    RVar (loc,id), [], [], []
 
 let find_appl_head_data (_,_,_,_,impls) = function
   | RRef (_,ref) as x -> x,implicits_of_global ref,find_arguments_scope ref,[]
@@ -1011,8 +1014,8 @@ let interp_rawtype sigma env c =
 let interp_rawtype_with_implicits sigma env impls c =
   interp_rawconstr_gen_with_implicits true sigma env impls false ([],[]) c
 
-let interp_rawconstr_with_implicits env vars impls c =
-  interp_rawconstr_gen_with_implicits false Evd.empty env ([],impls) false
+let interp_rawconstr_with_implicits sigma env vars impls c =
+  interp_rawconstr_gen_with_implicits false sigma env ([],impls) false
     (vars,[]) c
 
 (*
@@ -1085,6 +1088,10 @@ let interp_openconstr_gen sigma env (ltacvars,unbndltacvars) c exptyp =
 let interp_casted_constr sigma env c typ = 
   understand_gen sigma env [] (Some typ) (interp_rawconstr sigma env c)
 
+let interp_casted_constr_with_implicits sigma env impls c typ =
+  understand_gen sigma env [] (Some typ) 
+    (interp_rawconstr_with_implicits sigma env [] impls c)
+
 let interp_constrpattern_gen sigma env ltacvar c =
   let c = interp_rawconstr_gen false sigma env true (ltacvar,[]) c in
   pattern_of_rawconstr c
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index 2b87d0d66d..91a3454766 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -33,11 +33,13 @@ open Termops
    - insert existential variables for implicit arguments
 *)
 
-type implicits_env = (* To interpret inductive type with implicits *)
-    (identifier * (identifier list * Impargs.implicits_list)) list
+(* To interpret implicits and arg scopes of recursive variables in
+   inductive types and recursive definitions *)
+type var_internalisation_data =
+    identifier list * Impargs.implicits_list * scope_name option list
 
-type full_implicits_env =
-    identifier list * implicits_env
+type implicits_env = (identifier * var_internalisation_data) list
+type full_implicits_env = identifier list * implicits_env
 
 type ltac_sign = 
   identifier list * (identifier * identifier option) list
@@ -66,8 +68,12 @@ val interp_casted_openconstr    :
 val interp_type_with_implicits : 
   evar_map -> env -> full_implicits_env -> constr_expr -> types
 
+val interp_casted_constr_with_implicits :
+  evar_map -> env -> implicits_env -> constr_expr -> types -> constr
+
 val interp_rawconstr_with_implicits :
-  env -> identifier list -> implicits_env -> constr_expr -> rawconstr
+  evar_map -> env -> identifier list -> implicits_env -> constr_expr -> 
+    rawconstr
 
 (*s Build a judgement from *)
 val judgment_of_rawconstr : evar_map -> env -> constr_expr -> unsafe_judgment
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 30548d74d2..4ecca992dc 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -37,6 +37,7 @@ open Indtypes
 open Vernacexpr
 open Decl_kinds
 open Pretyping
+open Symbols
 
 let mkLambdaCit = List.fold_right (fun (x,a) b -> mkLambdaC(x,a,b))
 let mkProdCit = List.fold_right (fun (x,a) b -> mkProdC(x,a,b))
@@ -298,6 +299,7 @@ let interp_mutual lparams lnamearconstrs finite =
          let arity = interp_type sigma env_params arityc in
 	 let fullarity = it_mkProd_or_LetIn arity params in
 	 let env' = Termops.push_rel_assum (Name recname,fullarity) env in
+	 let argsc = compute_arguments_scope fullarity in
 	 let ind_impls' = 
 	   if Impargs.is_implicit_args() then
 	     let impl = Impargs.compute_implicits false env_params fullarity in
@@ -305,9 +307,9 @@ let interp_mutual lparams lnamearconstrs finite =
 	     let l = List.fold_right
 	       (fun imp l -> if Impargs.is_status_implicit imp then
 		 Impargs.name_of_implicit imp::l else l) paramimpl [] in
-	     (recname,(l,impl))::ind_impls
+	     (recname,(l,impl,argsc))::ind_impls
 	   else
-	     (recname,([],[]))::ind_impls in
+	     (recname,([],[],argsc))::ind_impls in
 	 (env', ind_impls', (arity::arl)))
       (env0, [], []) lnamearconstrs
   in
@@ -452,15 +454,19 @@ let build_recursive (lnameargsardef:(fixpoint_expr *decl_notation) list)  =
   and sigma = Evd.empty
   and env0 = Global.env()
   and nv = Array.of_list (List.map (fun ((_,n,_,_,_),_) -> n) lnameargsardef) in
-  let fs = States.freeze() in
-  (* Declare the notations for the recursive types pushed in local context*)
-  let (rec_sign,arityl) = 
+  (* Build the recursive context and notations for the recursive types *)
+  let (rec_sign,rec_impls,arityl) = 
     List.fold_left 
-      (fun (env,arl) ((recname,_,bl,arityc,_),_) -> 
+      (fun (env,impls,arl) ((recname,_,bl,arityc,_),_) -> 
         let arityc = prod_rawconstr arityc bl in
         let arity = interp_type sigma env0 arityc in
-        (Environ.push_named (recname,None,arity) env, (arity::arl)))
-      (env0,[]) lnameargsardef in
+	let impl = 
+	  if Impargs.is_implicit_args()
+	  then Impargs.compute_implicits false env0 arity
+	  else [] in
+	let impls' =(recname,([],impl,compute_arguments_scope arity))::impls in
+        (Environ.push_named (recname,None,arity) env, impls', arity::arl))
+      (env0,[],[]) lnameargsardef in
   let arityl = List.rev arityl in
   let notations = 
     List.fold_right (fun (_,ntnopt) l -> option_cons ntnopt l) 
@@ -468,21 +474,17 @@ let build_recursive (lnameargsardef:(fixpoint_expr *decl_notation) list)  =
 
   let recdef =
 
-    (* Declare local context and local notations *)
+    (* Declare local notations *)
     let fs = States.freeze() in
     let def = 
       try
 	List.iter (fun (df,c,scope) -> (* No scope for tmp notation *)
 	  Metasyntax.add_notation_interpretation df [] c None) notations;
-	List.iter2
-	  (fun recname arity -> 
-            let _ = declare_variable recname
-	      (Lib.cwd(),SectionLocalAssum arity, IsAssumption Definitional) in
-	    ()) lrecnames arityl;
 	List.map2
 	  (fun ((_,_,bl,_,def),_) arity ->
             let def = abstract_rawconstr def bl in
-            interp_casted_constr sigma rec_sign def arity)
+            interp_casted_constr_with_implicits 
+	      sigma rec_sign rec_impls def arity)
           lnameargsardef arityl
       with e ->
 	States.unfreeze fs; raise e in
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index c4d8bce9e2..a3415cbaa9 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -1199,8 +1199,7 @@ let add_notation_interpretation df names c sc =
   check_notation_existence (make_notation_key symbs);
   let (acvars,ac) = interp_aconstr names vars c in
   let a = (remove_vars recs acvars,ac) (* For recursive parts *) in
-  let a_for_old = interp_rawconstr_with_implicits (Global.env()) vars names c 
-  in
+  let a_for_old = interp_rawconstr_with_implicits Evd.empty (Global.env()) vars names c in
   let for_oldpp = set_data_for_v7_pp recs a_for_old vars in
   add_notation_interpretation_core false symbs for_oldpp df a sc false false