Mise en place d'un système optionnel de discharge immédiat; prise en compte des défs locales dans les arguments des inductifs; nettoyage divers

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

6 files changed, 157 insertions, 80 deletions

diff --git a/library/declare.ml b/library/declare.ml
index 82966022b..57e58256e 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -48,12 +48,17 @@ type sticky = bool
 
 type variable_declaration = section_variable_entry * strength * sticky
 
-let vartab = ref (Spmap.empty : (identifier * variable_declaration) Spmap.t)
+let vartab =
+  ref ((Spmap.empty, []) :
+       (identifier * variable_declaration) Spmap.t * section_path list)
+
+let current_section_context () =
+  List.map (fun sp -> (basename sp, sp)) (snd !vartab)
 
 let _ = Summary.declare_summary "VARIABLE"
 	  { Summary.freeze_function = (fun () -> !vartab);
 	    Summary.unfreeze_function = (fun ft -> vartab := ft);
-	    Summary.init_function = (fun () -> vartab := Spmap.empty);
+	    Summary.init_function = (fun () -> vartab := (Spmap.empty, []));
 	    Summary.survive_section = false }
 
 let cache_variable (sp,(id,(d,_,_) as vd)) =
@@ -65,7 +70,7 @@ let cache_variable (sp,(id,(d,_,_) as vd)) =
     | SectionLocalDef c -> Global.push_named_def (id,c)
   end;
   Nametab.push_local sp (VarRef sp);
-  vartab := Spmap.add sp vd !vartab
+  vartab := let (m,l) = !vartab in (Spmap.add sp vd m, sp::l)
 
 let (in_variable, out_variable) =
   let od = {
@@ -87,7 +92,7 @@ let cache_parameter (sp,c) =
   if Nametab.exists_cci sp then
     errorlabstrm "cache_parameter"
       [< pr_id (basename sp); 'sTR " already exists" >];
-  Global.add_parameter sp c;
+  Global.add_parameter sp c (current_section_context ());
   Nametab.push sp (ConstRef sp)
 
 let load_parameter _ = ()
@@ -132,9 +137,10 @@ let cache_constant (sp,(cdt,stre,op)) =
   if Nametab.exists_cci sp then
     errorlabstrm "cache_constant"
       [< pr_id (basename sp); 'sTR " already exists" >] ;
+  let sc = current_section_context() in
   begin match cdt with 
-    | ConstantEntry ce -> Global.add_constant sp ce
-    | ConstantRecipe r -> Global.add_discharged_constant sp r
+    | ConstantEntry ce -> Global.add_constant sp ce sc
+    | ConstantRecipe r -> Global.add_discharged_constant sp r sc
   end;
   Nametab.push sp (ConstRef sp);
   if op then Global.set_opaque sp;
@@ -197,7 +203,7 @@ let check_exists_inductive (sp,_) =
 let cache_inductive (sp,mie) =
   let names = inductive_names sp mie in
   List.iter check_exists_inductive names;
-  Global.add_mind sp mie;
+  Global.add_mind sp mie (current_section_context ());
   List.iter (fun (sp, ref) -> Nametab.push sp ref) names
 
 let load_inductive _ = ()
@@ -236,12 +242,12 @@ let constant_or_parameter_strength sp =
   try constant_strength sp with Not_found -> NeverDischarge
 
 let get_variable sp = 
-  let (id,(_,str,sticky)) = Spmap.find sp !vartab in
+  let (id,(_,str,sticky)) = Spmap.find sp (fst !vartab) in
   let (c,ty) = Global.lookup_named id in
   ((id,c,ty),str,sticky)
 
 let variable_strength sp =
-  let _,(_,str,_) = Spmap.find sp !vartab in str
+  let _,(_,str,_) = Spmap.find sp (fst !vartab) in str
 
 (* Global references. *)
 
@@ -267,11 +273,11 @@ let mind_oper_of_id sp id mib =
 	   mip.mind_consnames)
     mib.mind_packets
 
-let context_of_global_reference env = function
-  | VarRef sp -> [] (* Hum !, pas correct *)
-  | ConstRef sp -> (Environ.lookup_constant sp env).const_hyps
-  | IndRef (sp,_) -> (Environ.lookup_mind sp env).mind_hyps
-  | ConstructRef ((sp,_),_) -> (Environ.lookup_mind sp env).mind_hyps
+let context_of_global_reference = function
+  | VarRef sp -> []
+  | ConstRef sp -> (Global.lookup_constant sp).const_hyps
+  | IndRef (sp,_) -> (Global.lookup_mind sp).mind_hyps
+  | ConstructRef ((sp,_),_) -> (Global.lookup_mind sp).mind_hyps
 
 (*
 let global_sp_operator env sp id =
@@ -282,87 +288,102 @@ let global_sp_operator env sp id =
     mind_oper_of_id sp id mib, mib.mind_hyps
 *)
 
-let occur_decl env (id,c,t) hyps =
-  try
-    let (c',t') = Sign.lookup_id id hyps in
-    let matching_bodies = match c,c' with
-      | None, _ -> true
-      | Some c, None -> false
-      | Some c, Some c' -> is_conv env Evd.empty c c' in
-    let matching_types = 
-      is_conv env Evd.empty (body_of_type t) (body_of_type t') in
-    matching_types & matching_bodies
-  with Not_found -> false
-
-(*
-let find_common_hyps_then_abstract c env hyps' hyps = 
-  snd (fold_named_context_both_sides
-	 (fun
-	    (env,c) (id,_,_ as d) hyps ->
-	      if occur_decl env d hyps' then 
-		(Environ.push_named_decl d env,c)
-	      else
-		let hyps'' = List.rev (d :: hyps) in
-		(env, Environ.it_mkNamedLambda_or_LetIn c hyps''))
-	 hyps
-	 (env,c))
-*)
+let rec occur_section_variable sp = function
+  | (_,sp')::_ when sp = sp' -> true
+  | _::l -> occur_section_variable sp l
+  | [] -> false
 
 let rec quantify_extra_hyps c = function
-  | (id,None,t)::hyps -> mkNamedLambda id t (quantify_extra_hyps c hyps)
+  | (sp,None,t)::hyps ->
+      mkNamedLambda (basename sp) t (quantify_extra_hyps c hyps)
   (* Buggé car id n'apparaît pas dans les instances des constantes dans c *)
   (* et id n'est donc pas substitué dans ces constantes *)
-  | (id,Some b,t)::hyps -> mkNamedLetIn id b t (quantify_extra_hyps c hyps)
+  | (sp,Some b,t)::hyps ->
+      mkNamedLetIn (basename sp) b t (quantify_extra_hyps c hyps)
   | [] -> c
 
-let rec find_common_hyps_then_abstract c env hyps' = function
-  | (id,_,_ as d) :: hyps when occur_decl env d hyps' ->
-      find_common_hyps_then_abstract c (Environ.push_named_decl d env) hyps' hyps
-  | hyps -> quantify_extra_hyps c hyps
+let find_common_hyps_then_abstract c hyps' hyps =
+  let rec find = function
+    | (sp,_,_) :: hyps when occur_section_variable sp hyps' -> find hyps
+    | hyps -> quantify_extra_hyps c hyps in
+  find (List.rev hyps)
 
-let find_common_hyps_then_abstract c env hyps' hyps =
-  find_common_hyps_then_abstract c env hyps' (List.rev hyps)
-
-let current_section_context () =
-  let current = Spmap.fold (fun _ (id,_) hyps -> id::hyps) !vartab [] in
-  List.fold_right
-    (fun (id,_,_ as d) hyps -> if List.mem id current then d::hyps else hyps)
-    (Global.named_context ()) []
+let section_variable_paths () = snd !vartab
 
 let find_section_variable id =
   let l =
     Spmap.fold
       (fun sp (id',_) hyps -> if id=id' then sp::hyps else hyps)
-      !vartab [] in
+      (fst !vartab) [] in
   match l with
     | [] -> raise Not_found
     | [sp] -> sp
     | _ -> error "Arghh, you blasted me with several variables of same name"
 
+let last_section_hyps dir =
+  List.fold_right
+    (fun sp hyps -> if dirpath sp = dir then basename sp :: hyps else hyps)
+    (snd !vartab) []
+
+let rec find_var id = function
+  | [] -> raise Not_found
+  | sp::l -> if basename sp = id then sp else find_var id l
+
+let implicit_section_args ref =
+  if Options.immediate_discharge then
+    let hyps = context_of_global_reference ref in
+    let hyps0 = section_variable_paths () in
+    let rec keep acc = function
+      | (sp,None,_)::hyps ->
+	  let acc = if List.mem sp hyps0 then sp::acc else acc in
+	  keep acc hyps
+      | (_,Some _,_)::hyps -> keep acc hyps
+      | [] -> acc
+    in keep [] hyps
+  else []
+
+let section_hyps ref =
+  let hyps = context_of_global_reference ref in
+  let hyps0 = section_variable_paths () in
+  let rec keep acc = function
+    | (sp,b,_ as d)::hyps ->
+	let acc = if List.mem sp hyps0 then (sp,b=None)::acc else acc in
+	keep acc hyps
+    | [] -> acc
+  in keep [] hyps
+
 let extract_instance ref args =
-  let hyps = context_of_global_reference (Global.env ()) ref in
+  if Options.immediate_discharge then args
+  else
+  let hyps = context_of_global_reference ref in
   let hyps0 = current_section_context () in
   let na = Array.length args in
   let rec peel n acc = function
-    | (_,None,_ as d)::hyps ->
-	if List.mem d hyps0 then peel (n-1) acc hyps
+    | (sp,None,_ as d)::hyps ->
+	if List.mem_assoc (basename sp) hyps0 then peel (n-1) acc hyps
 	else peel (n-1) (args.(n)::acc) hyps
     | (_,Some _,_)::hyps -> peel n acc hyps
     | [] -> Array.of_list acc
   in peel (na-1) [] hyps
 
-let constr_of_reference _ env ref =
-  let hyps = context_of_global_reference env ref in
+let constr_of_reference _ _ ref =
+if Options.immediate_discharge then
+  match ref with
+    | VarRef sp -> mkVar (basename sp)
+    | ConstRef sp -> mkConst (sp,[||])
+    | ConstructRef sp -> mkMutConstruct (sp,[||])
+    | IndRef sp -> mkMutInd (sp,[||])
+else
+  let hyps = context_of_global_reference ref in
   let hyps0 = current_section_context () in
-  let env0 = Environ.reset_context env in
-  let args = instance_from_named_context hyps in
+  let args = instance_from_section_context hyps in
   let body = match ref with
     | VarRef sp -> mkVar (basename sp)
     | ConstRef sp -> mkConst (sp,Array.of_list args)
     | ConstructRef sp -> mkMutConstruct (sp,Array.of_list args)
     | IndRef sp -> mkMutInd (sp,Array.of_list args)
   in
-  find_common_hyps_then_abstract body env0 hyps0 hyps
+  find_common_hyps_then_abstract body hyps0 hyps
 
 let construct_absolute_reference env sp =
   constr_of_reference Evd.empty env (Nametab.absolute_reference sp)
@@ -384,6 +405,10 @@ let global_qualified_reference qid =
 let global_absolute_reference sp = 
   construct_absolute_reference (Global.env()) sp
 
+let global_reference_in_absolute_module dir id = 
+  constr_of_reference Evd.empty (Global.env())
+    (Nametab.locate_in_absolute_module dir id)
+
 let global_reference kind id = 
   construct_reference (Global.env()) kind id
 
@@ -414,6 +439,21 @@ let path_of_inductive_path (sp,tyi) =
     let (pa,_,k) = repr_path sp in 
     Names.make_path pa (mip.mind_typename) k 
 
+(* Util *)
+let instantiate_inductive_section_params t ind =
+  if Options.immediate_discharge then 
+  let sign = section_hyps (IndRef ind) in
+  let rec inst s ctxt t =
+    let k = kind_of_term t in
+    match (ctxt,k) with
+    | (sp,true)::ctxt, IsLambda(_,_,t) ->
+	inst ((mkVar (basename sp))::s) ctxt t
+    | (sp,false)::ctxt, IsLetIn(_,_,_,t) -> 
+	inst ((mkVar (basename sp))::s) ctxt t
+    | [], _ -> substl s t
+    | _ -> anomaly"instantiate_params: term and ctxt mismatch"
+  in inst [] sign t
+  else t
 (* Eliminations. *)
 
 let eliminations = [ (prop,"_ind") ; (spec,"_rec") ; (types,"_rect") ]
@@ -426,6 +466,9 @@ let elimination_suffix = function
 let declare_one_elimination mispec =
   let mindstr = string_of_id (mis_typename mispec) in
   let declare na c =
+    (* Hack to get const_hyps right in the declaration *)
+    let c = instantiate_inductive_section_params c (fst (mis_inductive mispec))
+    in
     let _ = declare_constant (id_of_string na)
       (ConstantEntry { const_entry_body = c; const_entry_type = None }, 
        NeverDischarge,false) in
@@ -444,10 +487,12 @@ let declare_one_elimination mispec =
 
 let declare_eliminations sp =
   let mib = Global.lookup_mind sp in
+(*
   let ids = ids_of_named_context mib.mind_hyps in
   if not (list_subset ids (ids_of_named_context (Global.named_context ()))) then    error ("Declarations of elimination scheme outside the section "^
     "of the inductive definition is not implemented");
-  let ctxt = instance_from_named_context mib.mind_hyps in
+*)
+  let ctxt = instance_from_section_context mib.mind_hyps in
   for i = 0 to Array.length mib.mind_packets - 1 do
     if mind_type_finite mib i then
       let mispec = Global.lookup_mind_specif ((sp,i), Array.of_list ctxt) in 
diff --git a/library/declare.mli b/library/declare.mli
index 894cebd0d..07dc96914 100644
--- a/library/declare.mli
+++ b/library/declare.mli
@@ -72,6 +72,7 @@ val out_variable : Libobject.obj -> identifier * variable_declaration
 val get_variable : variable_path -> named_declaration * strength * sticky
 val variable_strength : variable_path -> strength
 val find_section_variable : identifier -> variable_path
+val last_section_hyps : dir_path -> identifier list
 
 (*s [global_reference k id] returns the object corresponding to
     the name [id] in the global environment. It may be a constant, 
@@ -81,6 +82,9 @@ val find_section_variable : identifier -> variable_path
     [construct_reference] is a version which looks for variables in a 
     given environment instead of looking in the current global environment. *)
 
+val context_of_global_reference : global_reference -> section_context
+val instantiate_inductive_section_params : constr -> inductive_path -> constr
+val implicit_section_args : global_reference -> section_path list
 val extract_instance : global_reference -> constr array -> constr array
 
 val constr_of_reference :
@@ -88,6 +92,7 @@ val constr_of_reference :
 
 val global_qualified_reference : qualid -> constr
 val global_absolute_reference : section_path -> constr
+val global_reference_in_absolute_module : dir_path -> identifier -> constr
 
 val construct_qualified_reference : Environ.env -> qualid -> constr
 val construct_absolute_reference : Environ.env -> section_path -> constr
diff --git a/library/global.ml b/library/global.ml
index e5f0d07fd..c07452988 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -35,11 +35,11 @@ let named_context () = named_context !global_env
 let push_named_def idc = global_env := push_named_def idc !global_env
 let push_named_assum idc = global_env := push_named_assum idc !global_env
 
-let add_parameter sp c = global_env := add_parameter sp c !global_env
-let add_constant sp ce = global_env := add_constant sp ce !global_env
-let add_discharged_constant sp r = 
-  global_env := add_discharged_constant sp r !global_env
-let add_mind sp mie = global_env := add_mind sp mie !global_env
+let add_parameter sp c l = global_env := add_parameter sp c l !global_env
+let add_constant sp ce l = global_env := add_constant sp ce l !global_env
+let add_discharged_constant sp r l = 
+  global_env := add_discharged_constant sp r l !global_env
+let add_mind sp mie l = global_env := add_mind sp mie l !global_env
 let add_constraints c = global_env := add_constraints c !global_env
 
 let pop_named_decls ids = global_env := pop_named_decls ids !global_env
@@ -87,8 +87,6 @@ let mind_is_recursive =
 
 let mind_nconstr = Util.compose Inductive.mis_nconstr lookup_mind_specif
 let mind_nparams = Util.compose Inductive.mis_nparams lookup_mind_specif
-let mind_nf_arity x =
-  body_of_type (Inductive.mis_user_arity (lookup_mind_specif x))
 let mind_nf_lc = Util.compose Inductive.mis_nf_lc lookup_mind_specif
 
 
diff --git a/library/global.mli b/library/global.mli
index 0ad3e3713..74a7197d4 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -26,10 +26,11 @@ val named_context : unit -> named_context
 val push_named_assum : identifier * constr -> unit
 val push_named_def : identifier * constr -> unit
 
-val add_parameter : section_path -> constr -> unit
-val add_constant : section_path -> constant_entry -> unit
-val add_discharged_constant : section_path -> Cooking.recipe -> unit
-val add_mind : section_path -> mutual_inductive_entry -> unit
+val add_parameter : section_path -> constr -> local_names -> unit
+val add_constant : section_path -> constant_entry -> local_names -> unit
+val add_discharged_constant : section_path -> Cooking.recipe -> 
+  local_names -> unit
+val add_mind : section_path -> mutual_inductive_entry -> local_names -> unit
 val add_constraints : constraints -> unit
 
 val pop_named_decls : identifier list -> unit
@@ -61,6 +62,5 @@ val env_of_context : named_context -> env
 val mind_is_recursive : inductive -> bool
 val mind_nconstr : inductive -> int
 val mind_nparams : inductive -> int
-val mind_nf_arity : inductive -> constr
 val mind_nf_lc : inductive -> constr array
 
diff --git a/library/nametab.ml b/library/nametab.ml
index b62f4d867..c8e10a1ed 100755
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -148,15 +148,34 @@ let constant_sp_of_id id =
     | ConstRef sp -> sp
     | _ -> raise Not_found
 
-let check_absoluteness sp =
-  match dirpath sp with
+let check_absoluteness dir =
+  match dir with
     | a::_ when List.mem a !roots -> ()
-    | _ -> anomaly ("Not an absolute path: "^(string_of_path sp))
+    | _ -> anomaly ("Not an absolute dirpath: "^(string_of_dirpath dir))
 
 let absolute_reference sp =
-  check_absoluteness sp;
+  check_absoluteness (dirpath sp);
   locate (qualid_of_sp sp)
 
+exception Found of global_reference
+let locate_in_module dir id =
+  let rec exists_in id (Closed (ccitab,_,modtab)) =
+    try raise (Found (Stringmap.find id ccitab))
+    with Not_found -> 
+      Stringmap.iter (fun _ (sp,mc) -> exists_in id mc) modtab
+  in
+  let rec search (Closed (ccitab,_,modtab) as mc) = function
+    | modid :: dir' -> search (snd (Stringmap.find modid modtab)) dir'
+    | [] -> 
+	try exists_in id mc; raise Not_found
+	with Found ref -> ref
+  in
+  search !persistent_nametab dir
+
+let locate_in_absolute_module dir id =
+  check_absoluteness dir;
+  locate_in_module dir (string_of_id id)
+
 (* These are entry points to make the contents of a module/section visible *)
 (* in the current env (does not affect the absolute name space `coq_root') *)
 let open_module_contents qid =
@@ -165,7 +184,13 @@ let open_module_contents qid =
 (*  Stringmap.iter (fun _ -> Libobject.open_object) objtab;*)
   Stringmap.iter push_mod_current modtab
 
-let open_section_contents = open_module_contents
+let conditional_push ref = push_cci_current ref (* TODO *)
+
+let open_section_contents qid =
+  let _, (Closed (ccitab,objtab,modtab)) = locate_module qid in
+  Stringmap.iter push_cci_current ccitab;
+(*  Stringmap.iter (fun _ -> Libobject.open_object) objtab;*)
+  Stringmap.iter push_mod_current modtab
 
 let rec rec_open_module_contents qid =
   let _, (Closed (ccitab,objtab,modtab)) = locate_module qid in
diff --git a/library/nametab.mli b/library/nametab.mli
index 64cba70c2..08aea7ccc 100755
--- a/library/nametab.mli
+++ b/library/nametab.mli
@@ -59,3 +59,7 @@ val push_library_root : string -> unit
    especially, constructor/inductive names are turned into internal
    references inside a block of mutual inductive *)
 val absolute_reference : section_path -> global_reference
+
+(* [locate_in_absolute_module dir id] finds [id] in module [dir] or in
+   one of its section/subsection *)
+val locate_in_absolute_module : dir_path -> identifier -> global_reference