Discharge (encore bugge)

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

6 files changed, 156 insertions, 14 deletions

diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 46dd750781..5c2aa643b2 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -382,6 +382,14 @@ let sort_of_product domsort rangsort g =
            (* Product rule (Type_i,Type_i,Type_i) *) 
            | Type u1 -> let (u12,cst) = sup u1 u2 g in Type u12, cst)
 
+let sort_of_product_without_univ domsort rangsort =
+  match rangsort with
+    | Prop _ -> rangsort
+    | Type u2 ->
+        (match domsort with
+           | Prop _ -> rangsort
+           | Type u1 -> Type dummy_univ)
+
 let abs_rel env sigma name var j =
   let rngtyp = whd_betadeltaiota env sigma j.uj_kind in
   let cvar = incast_type var in
diff --git a/kernel/typeops.mli b/kernel/typeops.mli
index 9542dba9f8..20cec7273a 100644
--- a/kernel/typeops.mli
+++ b/kernel/typeops.mli
@@ -55,6 +55,8 @@ val gen_rel :
   env -> 'a evar_map -> name -> typed_type -> unsafe_judgment 
     -> unsafe_judgment * constraints
 
+val sort_of_product_without_univ : sorts -> sorts -> sorts
+
 val cast_rel : 
   env -> 'a evar_map -> unsafe_judgment -> unsafe_judgment 
     -> unsafe_judgment
diff --git a/lib/options.ml b/lib/options.ml
index c0f14ee30b..26869e7adc 100644
--- a/lib/options.ml
+++ b/lib/options.ml
@@ -11,10 +11,11 @@ let print_emacs = ref false
 
 let emacs_str s = if !print_emacs then s else "" 
 
-(* Silent *)
+(* Silent / Verbose *)
 let silent = ref false
 let make_silent flag = silent := flag; ()
 let is_silent () = !silent
+let verbose () = not !silent
 
 let silently f x =
   let oldsilent = !silent in
diff --git a/lib/options.mli b/lib/options.mli
index 9137883523..dc6b5b9824 100644
--- a/lib/options.mli
+++ b/lib/options.mli
@@ -12,6 +12,7 @@ val emacs_str : string -> string
 
 val make_silent : bool -> unit
 val is_silent : unit -> bool
+val verbose : unit -> bool
 val silently : ('a -> 'b) -> 'a -> 'b
 
 val set_print_hyps_limit : int -> unit
diff --git a/parsing/termast.ml b/parsing/termast.ml
index cdaa2a2686..0ddee900fb 100644
--- a/parsing/termast.ml
+++ b/parsing/termast.ml
@@ -27,7 +27,7 @@ let ids_of_ctxt cl =
        | Rel n ->
 	   warning "ids_of_ctxt: rel";
 	   id_of_string ("REL "^(string_of_int n))
-       | _-> anomaly"ids_of_ctxt")
+       | _-> anomaly "ids_of_ctxt")
     (Array.to_list cl)
 
 let ast_of_ident id = nvar (string_of_id id)
diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml
index bd605b53eb..84b357c5d1 100644
--- a/toplevel/discharge.ml
+++ b/toplevel/discharge.ml
@@ -4,12 +4,14 @@
 open Pp
 open Util
 open Names
+open Sign
 open Generic
 open Term
 open Constant
 open Inductive
 open Instantiate
 open Reduction
+open Typeops
 open Libobject
 open Lib
 open Declare
@@ -20,6 +22,72 @@ open Recordops
 let recalc_sp sp =
   let (_,spid,k) = repr_path sp in Lib.make_path spid k
 
+(* Abstractions. *)
+
+let whd_all c = whd_betadeltaiota (Global.env()) Evd.empty c
+
+let generalize_type id var c =
+  let c' = mkProd (Name id) var.body (subst_var id c.body) in
+  let c'ty = sort_of_product_without_univ var.typ c.typ in 
+  { body = c'; typ = c'ty }
+
+let casted_generalize id var c =
+  let c' = mkProd (Name id) var.body (subst_var id (cast_term c)) in
+  let s = destSort (whd_all (cast_type c)) in
+  let c'ty = sort_of_product_without_univ var.typ s in 
+  mkCast c' (DOP0 (Sort c'ty))
+
+let abstract_inductive ids_to_abs hyps inds =
+  let abstract_one_var id ty inds =
+    let ntyp = List.length inds in 
+    let new_refs = list_tabulate (fun k -> applist(Rel (k+2),[Rel 1])) ntyp in 
+    let inds' =
+      List.map
+      	(function (tname,arity,cnames,lc) -> 
+	   let arity' = generalize_type id ty arity in
+	   let lc' =
+	     under_dlams 
+               (fun b -> casted_generalize id ty (substl new_refs b)) lc
+	   in
+           (tname,arity',cnames,lc'))
+      	inds
+    in 
+    (inds',ABSTRACT)
+  in
+  let abstract_once ((hyps,inds,modl) as sofar) id =
+    if isnull_sign hyps or id <> fst (hd_sign hyps) then 
+      sofar
+  else
+    let (inds',modif) = abstract_one_var id (snd (hd_sign hyps)) inds in 
+    (tl_sign hyps,inds',modif::modl)
+  in
+  let (_,inds',revmodl) =
+    List.fold_left abstract_once (hyps,inds,[]) ids_to_abs in
+  let inds'' = List.map (fun (a,b,c,d) -> (a,b.body,c,d)) inds' in
+  (inds'', List.rev revmodl)
+
+let abstract_constant ids_to_abs hyps (body,typ) =
+  let abstract_once ((hyps,body,typ,modl) as sofar) id =
+    if isnull_sign hyps or id <> fst(hd_sign hyps) then 
+      sofar
+    else
+      let name = Name id in
+      let var = snd (hd_sign hyps) in
+      let cvar = incast_type var in
+      let body' = mkLambda name cvar (subst_var id body) in
+      let typ' =
+    	{ body = mkProd name cvar (subst_var id typ.body);
+	  typ  = sort_of_product_without_univ var.typ typ.typ } 
+      in
+      (tl_sign hyps,body',typ',ABSTRACT::modl)
+  in
+  let (_,body',typ',revmodl) =
+    List.fold_left abstract_once (hyps,body,typ,[]) ids_to_abs in
+  (body',typ', List.rev revmodl)
+
+
+(* Substitutions. *)
+
 let expmod_constr modlist c =
   let env = Global.env() in
   let sigma = Evd.empty in
@@ -58,11 +126,68 @@ let expmod_constr modlist c =
 
 let expmod_type modlist {body=c;typ=s} = {body=expmod_constr modlist c;typ=s}
 
-let process_constant (ids_to_discard,work_alist) cb =
-  failwith "todo"
 
-let process_inductive (ids_to_discard,work_alist) mib =
-  failwith "todo"
+(* Discharge of inductive types. *)
+
+let process_inductive osecsp nsecsp (ids_to_discard,modlist) mib =
+  assert (Array.length mib.mind_packets > 0);
+  let finite = mib.mind_packets.(0).mind_finite in
+  let inds = 
+    array_map_to_list
+      (fun mip ->
+	 (mip.mind_typename,
+	  expmod_type modlist mip.mind_arity,
+	  Array.to_list mip.mind_consnames,
+	  under_dlams (expmod_constr modlist) mip.mind_lc))
+      mib.mind_packets
+  in
+  let (inds',modl) = abstract_inductive ids_to_discard mib.mind_hyps inds in
+  let lmodif_one_mind i = 
+    let nbc = Array.length (mind_nth_type_packet mib i).mind_consnames in 
+    (MutInd(osecsp,i),DO_ABSTRACT(MutInd(nsecsp,i),modl))::
+    (MutCase(Some (osecsp,i)),DO_ABSTRACT(MutCase(Some (nsecsp,i)),[]))::
+    (list_tabulate
+       (function j -> 
+	  let j' = j + 1 in
+	  (MutConstruct((osecsp,i),j'),
+	   DO_ABSTRACT(MutConstruct((nsecsp,i),j'),modl)))
+       nbc) 
+  in
+  let modifs = List.flatten (list_tabulate lmodif_one_mind mib.mind_ntypes) in 
+  ({ mind_entry_nparams = mib.mind_nparams + (List.length modl);
+     mind_entry_finite = finite;
+     mind_entry_inds = inds' },
+   modifs)
+
+
+(* Discharge of constants. *)
+
+let process_constant osecsp nsecsp (ids_to_discard,modlist) cb =
+  let body = global_reference CCI (basename osecsp) in
+  let typ = expmod_type modlist cb.const_type in
+  let (body',typ',modl) = 
+    abstract_constant ids_to_discard cb.const_hyps (body,typ)
+  in
+  let mods = (Const osecsp, DO_ABSTRACT(Const nsecsp,modl)) :: modlist in
+  ({ const_entry_body = body'; const_entry_type = Some typ'.body },
+   mods)
+
+
+(* Discharge of the various objects of the environment. *)
+
+let constant_message sp =
+  if Options.verbose() then 
+    pPNL [< print_id (basename sp); 'sTR " is discharged." >]
+
+let inductive_message inds =
+  if Options.verbose() then 
+    pPNL (hOV 0 
+	    (match inds with
+	       | [] -> assert false
+	       | [(i,_,_,_)] -> [< print_id i; 'sTR " is discharged." >]
+	       | l -> [< prlist_with_sep pr_coma 
+			   (fun (id,_,_,_) -> print_id id) l;
+			 'sPC; 'sTR "are discharged.">]))
 
 let process_object sec_sp (ids_to_discard,work_alist) (sp,lobj) =
   let tag = object_tag lobj in 
@@ -76,25 +201,30 @@ let process_object sec_sp (ids_to_discard,work_alist) (sp,lobj) =
 	  declare_variable id (expmod_a,stre,sticky);
           (ids_to_discard,work_alist)
 	end
-	  
+
     | "CONSTANT" ->
 	let stre = constant_strength sp in
 	if stre = (DischargeAt sec_sp) then
 	  (ids_to_discard, (Const sp, DO_REPLACE) :: work_alist)
 	else begin
 	  let cb = Global.lookup_constant sp in
-	  let ((_,spid,spk)) = repr_path sp in
-	  let ce = process_constant (ids_to_discard,work_alist) cb in
+	  let spid = basename sp in
+	  let newsp = recalc_sp sp in
+	  let (ce,mods) = 
+	    process_constant sp newsp (ids_to_discard,work_alist) cb in
 	  declare_constant spid (ce,stre);
-          (ids_to_discard,work_alist)
+	  constant_message sp;
+          (ids_to_discard,mods@work_alist)
 	end
-	  
+  
     | "INDUCTIVE" ->
 	let mib = Global.lookup_mind sp in
-	let ((_,spid,spk)) = repr_path sp in
-	let mie = process_inductive (ids_to_discard,work_alist) mib in
+	let newsp = recalc_sp sp in
+	let (mie,mods) = 
+	  process_inductive sp newsp (ids_to_discard,work_alist) mib in
 	let _ = declare_mind mie in
-        (ids_to_discard,work_alist)
+	inductive_message mie.mind_entry_inds;
+        (ids_to_discard,mods@work_alist)
 
     | "CLASS" -> 
 	let ((cl,clinfo) as x) = outClass lobj in