Imported Upstream version 8.0pl3+8.1alphaupstream/8.0pl3+8.1alpha

1 files changed, 92 insertions, 136 deletions

diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index d69efe3a..a6aa2a8e 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: cooking.ml,v 1.17.8.1 2004/07/16 19:30:24 herbelin Exp $ i*)
+(*i $Id: cooking.ml 6748 2005-02-18 22:17:50Z herbelin $ i*)
 
 open Pp
 open Util
@@ -19,154 +19,110 @@ open Reduction
 
 (*s Cooking the constants. *)
 
-type 'a modification =
-  | NOT_OCCUR
-  | DO_ABSTRACT of 'a * constr array
-  | DO_REPLACE of constant_body
+type work_list = identifier array Cmap.t * identifier array KNmap.t
 
-type work_list =
-    (constant * constant modification) list
-    * (inductive * inductive modification) list
-    * (constructor * constructor modification) list
+let dirpath_prefix p = match repr_dirpath p with
+  | [] -> anomaly "dirpath_prefix: empty dirpath"
+  | _::l -> make_dirpath l
 
-type recipe = {
-  d_from : constant_body;
-  d_abstract : identifier list;
-  d_modlist : work_list }
+let pop_kn kn =
+  let (mp,dir,l) = Names.repr_kn kn in
+  Names.make_kn mp (dirpath_prefix dir) l
+
+let pop_con con = 
+  let (mp,dir,l) = Names.repr_con con in
+  Names.make_con mp (dirpath_prefix dir) l
+
+type my_global_reference =
+  | ConstRef of constant
+  | IndRef of inductive
+  | ConstructRef of constructor
+
+let cache = (Hashtbl.create 13 : (my_global_reference, constr) Hashtbl.t)
+
+let clear_cooking_sharing () = Hashtbl.clear cache
+
+let share r (cstl,knl) =
+  try Hashtbl.find cache r
+  with Not_found ->
+  let f,l =
+    match r with
+    | IndRef (kn,i) -> 
+	mkInd (pop_kn kn,i), KNmap.find kn knl
+    | ConstructRef ((kn,i),j) -> 
+	mkConstruct ((pop_kn kn,i),j), KNmap.find kn knl
+    | ConstRef cst ->
+	mkConst (pop_con cst), Cmap.find cst cstl in
+  let c = mkApp (f, Array.map mkVar l) in
+  Hashtbl.add cache r c;
+  (* has raised Not_found if not in work_list *)
+  c
 
-let failure () =
-  anomalylabstrm "generic__modify_opers"
-    (str"An oper which was never supposed to appear has just appeared" ++
-     spc () ++ str"Either this is in system code, and you need to" ++ spc () ++
-     str"report this error," ++ spc () ++
-     str"Or you are using a user-written tactic which calls" ++ spc () ++
-     str"generic__modify_opers, in which case the user-written code" ++
-     spc () ++ str"is broken - this function is an internal system" ++
-     spc () ++ str"for internal system use only")
-
-let modify_opers replfun (constl,indl,cstrl) =
+let update_case_info ci modlist =
+  try
+    let ind, n = 
+      match kind_of_term (share (IndRef ci.ci_ind) modlist) with
+      | App (f,l) -> (destInd f, Array.length l)
+      | Ind ind -> ind, 0
+      | _ -> assert false in
+    { ci with ci_ind = ind; ci_npar = ci.ci_npar + n }
+  with Not_found ->
+    ci
+
+let empty_modlist = (Cmap.empty, KNmap.empty)
+
+let expmod_constr modlist c =
   let rec substrec c =
-    let c' = map_constr substrec c in
-    match kind_of_term c' with
+    match kind_of_term c with
       | Case (ci,p,t,br) ->
+	  map_constr substrec (mkCase (update_case_info ci modlist,p,t,br))
+
+      | Ind ind ->
 	  (try
-	     match List.assoc ci.ci_ind indl with
-	       | DO_ABSTRACT (ind,abs_vars) ->
-		   let n' = Array.length abs_vars + ci.ci_npar in
-                   let ci' = { ci with
-                               ci_ind = ind;
-                               ci_npar = n' } in
-		   mkCase (ci',p,t,br)
-	       | _ -> raise Not_found
-	   with
-	     | Not_found -> c')
-
-      | Ind spi ->
-	  (try
-	     (match List.assoc spi indl with
-		| NOT_OCCUR -> failure ()
-		| DO_ABSTRACT (oper',abs_vars) ->
-                    mkApp (mkInd oper', abs_vars)
-		| DO_REPLACE _ -> assert false)
+	    share (IndRef ind) modlist
 	   with 
-	     | Not_found -> c')
-
-      | Construct spi ->
+	    | Not_found -> map_constr substrec c)
+	  
+      | Construct cstr ->
 	  (try
-	     (match List.assoc spi cstrl with
-		| NOT_OCCUR -> failure ()
-		| DO_ABSTRACT (oper',abs_vars) ->
-		    mkApp (mkConstruct oper', abs_vars)
-		| DO_REPLACE _ -> assert false)
+	    share (ConstructRef cstr) modlist
 	   with 
-	     | Not_found -> c')
-
-      | Const kn ->
+	    | Not_found -> map_constr substrec c)
+	  
+      | Const cst ->
 	  (try
-	     (match List.assoc kn constl with
-		| NOT_OCCUR -> failure ()
-		| DO_ABSTRACT (oper',abs_vars) ->
-		    mkApp (mkConst oper', abs_vars)
-		| DO_REPLACE cb -> substrec (replfun (kn,cb)))
+	    share (ConstRef cst) modlist
 	   with 
-	     | Not_found -> c')
-  
-    | _ -> c'
-  in 
-  if (constl,indl,cstrl) = ([],[],[]) then fun x -> x else substrec
+	    | Not_found -> map_constr substrec c)
+
+  | _ -> map_constr substrec c
 
-let expmod_constr modlist c =
-  let simpfun = 
-    if modlist = ([],[],[]) then fun x -> x else nf_betaiota in
-  let expfun (kn,cb) = 
-    if cb.const_opaque then
-      errorlabstrm "expmod_constr"
-	(str"Cannot unfold the value of " ++
-        str(string_of_kn kn) ++ spc () ++
-        str"You cannot declare local lemmas as being opaque" ++ spc () ++
-        str"and then require that theorems which use them" ++ spc () ++
-        str"be transparent");
-    match cb.const_body with
-      | Some body -> Declarations.force body
-      | None -> assert false
-  in
-  let c' = modify_opers expfun modlist c in
-  match kind_of_term c' with
-    | Cast (value,typ) -> mkCast (simpfun value,simpfun typ)
-    | _ -> simpfun c'
-
-let expmod_type modlist c =
-  type_app (expmod_constr modlist) c
-
-let abstract_constant ids_to_abs hyps (body,typ) =
-  let abstract_once_typ ((hyps,typ) as sofar) id =
-    match hyps with
-      | (hyp,c,t as decl)::rest when hyp = id ->
-	  let typ' = mkNamedProd_wo_LetIn decl typ in
-	  (rest, typ')
-      | _ -> 
-	  sofar
-  in
-  let abstract_once_body ((hyps,body) as sofar) id =
-    match hyps with
-      | (hyp,c,t as decl)::rest when hyp = id ->
-	  let body' = mkNamedLambda_or_LetIn decl body in
-	  (rest, body')
-      | _ -> 
-	  sofar
-  in
-  let (_,typ') =
-    List.fold_left abstract_once_typ (hyps,typ) ids_to_abs 
-  in
-  let body' = match body with
-      None -> None
-    | Some l_body -> 
-	Some (Declarations.from_val
-		(let body = Declarations.force l_body in
-		 let (_,body') = 
-		   List.fold_left abstract_once_body (hyps,body) ids_to_abs
-		 in
-		   body'))
   in
-    (body',typ')
+  if modlist = empty_modlist then c
+  else under_outer_cast nf_betaiota (substrec c)
+
+let abstract_constant_type =
+   List.fold_left (fun c d -> mkNamedProd_wo_LetIn d c)
+
+let abstract_constant_body =
+  List.fold_left (fun c d -> mkNamedLambda_or_LetIn d c)
+
+type recipe = {
+  d_from : constant_body;
+  d_abstract : named_context;
+  d_modlist : work_list }
+
+let on_body f = 
+  option_app (fun c -> Declarations.from_val (f (Declarations.force c)))
 
 let cook_constant env r =
   let cb = r.d_from in
-  let typ = expmod_type r.d_modlist cb.const_type in
-  let body = 
-    option_app 
-      (fun lconstr -> 
-	 Declarations.from_val 
-	   (expmod_constr r.d_modlist (Declarations.force lconstr))) 
-      cb.const_body
-  in
-  let hyps =
-    Sign.fold_named_context
-      (fun d ctxt ->
-        Sign.add_named_decl
-          (map_named_declaration (expmod_constr r.d_modlist) d)
-          ctxt)
-      cb.const_hyps
-      ~init:empty_named_context in
-  let body,typ = abstract_constant r.d_abstract hyps (body,typ) in
-  (body, typ, cb.const_constraints, cb.const_opaque)
+  let hyps = Sign.map_named_context (expmod_constr r.d_modlist) r.d_abstract in
+  let body =
+    on_body (fun c ->
+      abstract_constant_body (expmod_constr r.d_modlist c) hyps) 
+      cb.const_body in
+  let typ =
+    abstract_constant_type (expmod_constr r.d_modlist cb.const_type) hyps in
+  let boxed = Cemitcodes.is_boxed cb.const_body_code in
+  (body, typ, cb.const_constraints, cb.const_opaque, boxed)