Commit to perform double type inference also on inner types.

 * Motivation: the inner sorts computed for the inner types were computed
   by Coq itself. Thus Nijmegen's CProp was exported as Type. To export CProp
   as CProp I have to implement a CProp-aware single type inference.
   To avoid the reimplementation I use double type inference.
 * Known problems: the double type inference algorithm is slower than the
   usual type inference algorithm. Moreover too many types and sorts are
   computed in this way. As a consequence the exportation module is now
   much slower (the exportation time seems to be doubled in the average
   case).

In the future I will try to restore the original performances.


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

2 files changed, 19 insertions, 5 deletions

diff --git a/contrib/xml/cic2acic.ml b/contrib/xml/cic2acic.ml
index a6b2eaf00..767790b87 100644
--- a/contrib/xml/cic2acic.ml
+++ b/contrib/xml/cic2acic.ml
@@ -359,7 +359,9 @@ let acic_of_cic_context' computeinnertypes seed ids_to_terms constr_to_ids
       in
        let ainnertypes,innertype,innersort,expected_available =
         let {D.synthesized = synthesized; D.expected = expected} =
-         if computeinnertypes then
+         if computeinnertypes
+          || (match Term.kind_of_term tt with Term.Sort _ -> false | _ -> true)
+         then
 try
           Acic.CicHash.find terms_to_types tt
 with _ ->
diff --git a/contrib/xml/doubleTypeInference.ml b/contrib/xml/doubleTypeInference.ml
index 3c5362509..6337506e7 100644
--- a/contrib/xml/doubleTypeInference.ml
+++ b/contrib/xml/doubleTypeInference.ml
@@ -165,7 +165,7 @@ let double_type_of env sigma cstr expectedty subterms_to_types =
 (try
         Typeops.judge_of_type u
  with _ -> (* Successor of a non universe-variable universe anomaly *)
- (Pp.ppnl (Pp.str "Warning: universe refresh performed!!!") ; flush stdout ) ;
+ (*(Pp.ppnl (Pp.str "Warning: universe refresh performed!!!") ; flush stdout ) ;*)
   Typeops.judge_of_type (Termops.new_univ ())
 )
 
@@ -238,7 +238,7 @@ let double_type_of env sigma cstr expectedty subterms_to_types =
 	 j
     in
      let synthesized = E.j_type judgement in
-     let synthesized' = Reductionops.nf_beta synthesized in
+     let synthesized' = Unshare.unshare (Reductionops.nf_beta synthesized) in
       let types,res =
        match expectedty with
           None ->
@@ -251,14 +251,26 @@ let double_type_of env sigma cstr expectedty subterms_to_types =
            (* the synthesized type. Let's forget it.       *)
            {synthesized = synthesized' ; expected = None}, synthesized
         | Some expectedty' ->
-           {synthesized = synthesized' ; expected = Some expectedty'},
+           {synthesized = synthesized' ; expected = Some (Unshare.unshare expectedty')},
            expectedty'
       in
 (*CSC: debugging stuff to be removed *)
 if Acic.CicHash.mem subterms_to_types cstr then
  (Pp.ppnl (Pp.(++) (Pp.str "DUPLICATE INSERTION: ") (Printer.prterm cstr)) ; flush stdout ) ;
        Acic.CicHash.add subterms_to_types cstr types ;
-       E.make_judge cstr res
+       let recur_on_type ty =
+        match Term.kind_of_term ty with
+           Term.Sort _ -> ()
+         | _ ->
+           ignore (execute env sigma ty None)
+       in
+        recur_on_type types.synthesized ;
+        begin
+         match types.expected with
+            None -> ()
+          | Some ty -> recur_on_type ty
+        end ;
+        E.make_judge cstr res
 
 
  and execute_recdef env sigma (names,lar,vdef) =