Découpage des différentes fonctionnalités de build_mutual et definition_structure + export des sous-fonctions

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

4 files changed, 60 insertions, 32 deletions

diff --git a/toplevel/command.ml b/toplevel/command.ml
index 30d293ba98..68d0455128 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -134,7 +134,7 @@ let corecursive_message = function
   | l   -> hOV 0 [< prlist_with_sep pr_coma pr_id l;
                     'sPC; 'sTR "are corecursively defined">]
 
-let build_mutual lparams lnamearconstrs finite =
+let interp_mutual lparams lnamearconstrs finite = 
   let allnames = 
     List.fold_left 
       (fun acc (id,_,l) -> id::(List.map fst l)@acc) [] lnamearconstrs in
@@ -182,14 +182,24 @@ let build_mutual lparams lnamearconstrs finite =
 	   mind_entry_lc = constrs })
       (List.rev arityl) lnamearconstrs
   in
-  let mie = { mind_entry_finite = finite; mind_entry_inds = mispecvec }
-  in
+  { mind_entry_finite = finite; mind_entry_inds = mispecvec },
+  lrecnames
+
+let declare_mutual_with_eliminations mie lrecnames finite =
   let sp = declare_mind mie in
   if is_verbose() then pPNL(minductive_message lrecnames);
   if finite then
-    for i = 0 to List.length mispecvec - 1 do
+    for i = 0 to List.length lrecnames - 1 do
       declare_eliminations sp i
-    done
+    done;
+  sp
+
+let build_mutual_give_path lparams lnamearconstrs finite =
+  let mie, lrecnames = interp_mutual lparams lnamearconstrs finite in
+  declare_mutual_with_eliminations mie lrecnames finite
+
+let build_mutual lparams lnamearconstrs finite =
+  let _ = build_mutual_give_path lparams lnamearconstrs finite in ()
 
 (* try to find non recursive definitions *)
 
diff --git a/toplevel/command.mli b/toplevel/command.mli
index ec43a2efb9..abd42a87ea 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -30,6 +30,11 @@ val build_mutual :
   (identifier * Coqast.t) list -> 
     (identifier * Coqast.t * (identifier * Coqast.t) list) list -> bool -> unit
 
+val build_mutual_give_path : 
+  (identifier * Coqast.t) list -> 
+    (identifier * Coqast.t * (identifier * Coqast.t) list) list -> bool
+      -> section_path
+
 val build_recursive :
   (identifier * ((identifier * Coqast.t) list) * Coqast.t * Coqast.t) list 
   -> unit
diff --git a/toplevel/record.ml b/toplevel/record.ml
index f08c7dcfd9..19e399bab7 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -90,29 +90,15 @@ let warning_or_error coe st =
   if coe then errorlabstrm "structure" st;
   pPNL (hOV 0 [< 'sTR"Warning: "; st >])
 
-(* Fields have names [idfs] and types [tyfs]; [coers] is a boolean list 
-   telling if the corresponding field must me a coercion *)
-
-let definition_structure (is_coe,idstruc,ps,cfs,idbuild,s) =
-  let coers,fs = List.split cfs in     
-  let idps,typs = List.split ps in      
-  let idfs,tyfs = List.split fs in
-  if not (free_in_asts idstruc tyfs) then error "A record cannot be recursive";
-  let newps,newfs = typecheck_params_and_field ps fs in
-  let app_constructor = 
-    ope("APPLISTEXPL",
-        (nvar (string_of_id idstruc))::
-        List.map (fun id -> nvar(string_of_id id)) idps) in
-  let type_constructor = make_constructor fs app_constructor in 
-  let _ = build_mutual ps [(idstruc,s,[(idbuild,type_constructor)])] true in
+(* We build projections *)
+let declare_projections idstruc coers params constr_types =
   let r = global_reference CCI idstruc in
-  let rsp = op_of_mind r in
-  let x = Environ.named_hd (Global.env()) r Anonymous in
-  let lp = List.length idps in
+  let lp = List.length constr_types in
   let rp1 = applist (r,(rel_list 0 lp)) in
   let rp2 = applist (r,(rel_list 1 lp)) in
-
-  (* We build projections *)
+  let x = Environ.named_hd (Global.env()) r Anonymous in
+  let args =  (* Rel 1 refers to "x" *)
+    (List.map (fun (id,_) -> mkVar id) constr_types)@[mkRel 1] in
   let (sp_projs,_,_) =
     List.fold_left2
       (fun (sp_projs,ids_not_ok,subst) coe (fi,ti) -> 
@@ -129,11 +115,11 @@ let definition_structure (is_coe,idstruc,ps,cfs,idbuild,s) =
            (None::sp_projs,fi::ids_not_ok,subst)
          end else 
 	   let p = mkLambda (x, rp2, replace_vars subst ti) in
-	   let branch = mk_LambdaCit newfs (mkVar fi) in
+	   let branch = mk_LambdaCit constr_types (mkVar fi) in
 	   let ci = Inductive.make_case_info
 		      (Global.lookup_mind_specif (destMutInd r))
 		      (Some PrintLet) [| RegularPat |] in
-	   let proj = mk_LambdaCit newps 
+	   let proj = mk_LambdaCit params 
 			(mkLambda (x, rp1,
 				   mkMutCase (ci, p, mkRel 1, [|branch|]))) in
 	   let ok = 
@@ -156,12 +142,30 @@ let definition_structure (is_coe,idstruc,ps,cfs,idbuild,s) =
              if coe then
 	       Class.try_add_new_coercion_record fi NeverDischarge idstruc;
              let constr_fi = global_reference CCI fi in
-             let constr_fip = (* Rel 1 refers to "x" *)
-               applist (constr_fi,(List.map mkVar idps)@[mkRel 1])
+             let constr_fip = applist (constr_fi,args)
              in (Some(path_of_const constr_fi)::sp_projs,
 		 ids_not_ok, (fi,constr_fip)::subst)
 	   end)
-      ([],[],[]) coers newfs
-  in 
+      ([],[],[]) coers constr_types
+  in sp_projs
+
+(* Fields have names [idfs] and types [tyfs]; [coers] is a boolean list 
+   telling if the corresponding field must me a coercion *)
+let definition_structure (is_coe,idstruc,ps,cfs,idbuild,s) =
+  let coers,fs = List.split cfs in     
+  let idps,typs = List.split ps in      
+  let idfs,tyfs = List.split fs in
+  if not (free_in_asts idstruc tyfs) then error "A record cannot be recursive";
+  let newps,newfs = typecheck_params_and_field ps fs in
+  let app_constructor = 
+    ope("APPLISTEXPL",
+        (nvar (string_of_id idstruc))::
+        List.map (fun id -> nvar(string_of_id id)) idps) in
+  let type_constructor = make_constructor fs app_constructor in 
+  let sp = build_mutual_give_path
+	     ps [(idstruc,s,[(idbuild,type_constructor)])] true in
+  let sp_projs = declare_projections idstruc coers newps newfs in
+
+  let rsp = (sp,0) in
   if is_coe then Class.try_add_new_coercion idbuild NeverDischarge;
-  Recordops.add_new_struc (rsp,idbuild,lp,List.rev sp_projs)
+  Recordops.add_new_struc (rsp,idbuild,List.length idps,List.rev sp_projs)
diff --git a/toplevel/record.mli b/toplevel/record.mli
index c3fbb70f23..88a3e120fb 100644
--- a/toplevel/record.mli
+++ b/toplevel/record.mli
@@ -6,6 +6,15 @@ open Names
 open Term
 (*i*)
 
+(* [declare_projections id coers params fields] declare projections of
+   record [id] (if allowed), and put them as coercions accordingly to
+   [coers] *)
+
+val declare_projections :
+  identifier -> bool list -> 
+   (identifier * types) list -> (identifier * types) list -> 
+      constant_path option list
+
 val definition_structure :
    bool * identifier * (identifier * Coqast.t) list *
   (bool * (identifier * Coqast.t)) list * identifier *