CoRN CProp detection improved: products of "sort" CProp are now recognized

(they used to be exported as products of sort Type).


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

3 files changed, 62 insertions, 44 deletions

diff --git a/contrib/xml/cic2acic.ml b/contrib/xml/cic2acic.ml
index 4a7c0c8ad..9cd8681b9 100644
--- a/contrib/xml/cic2acic.ml
+++ b/contrib/xml/cic2acic.ml
@@ -165,44 +165,8 @@ type sort =
  | CProp
 ;;
 
-let cprop =
- let module N = Names in
-  N.make_kn
-   (N.MPfile
-     (Libnames.dirpath_of_string "CoRN.algebra.CLogic"))
-   (N.make_dirpath [])
-   (N.mk_label "CProp")
-;;
-
 let prerr_endline _ = ();;
 
-let whd_betadeltaiotacprop env evar_map ty =
- let module R = Rawterm in
-  let red_exp =
-   R.Hnf  (*** Instead CProp is made Opaque ***)
-(*
-   R.Cbv
-    {R.rBeta = true ; R.rIota = true ; R.rDelta = true; R.rZeta=true ;
-     R.rConst = [Names.EvalConstRef cprop]
-    }
-*)
-  in
-Conv_oracle.set_opaque_const cprop;
-prerr_endline "###whd_betadeltaiotacprop:" ;
-let xxx =
-(*Pp.msgerr (Printer.prterm_env env ty);*)
-prerr_endline "";
-   Tacred.reduction_of_redexp red_exp env evar_map ty
-in
-prerr_endline "###FINE" ;
-(*
-Pp.msgerr (Printer.prterm_env env xxx);
-*)
-prerr_endline "";
-Conv_oracle.set_transparent_const cprop;
-xxx
-;;
-
 let family_of_term ty =
  match Term.kind_of_term ty with
     Term.Sort s -> Coq_sort (Term.family_of_sort s)
@@ -215,19 +179,19 @@ module CPropRetyping =
   module T = Term
 
   let outsort env sigma t =
-   family_of_term (whd_betadeltaiotacprop env sigma t)
+   family_of_term (DoubleTypeInference.whd_betadeltaiotacprop env sigma t)
 
   let rec subst_type env sigma typ = function
   | [] -> typ
   | h::rest ->
-      match T.kind_of_term (whd_betadeltaiotacprop env sigma typ) with
+      match T.kind_of_term (DoubleTypeInference.whd_betadeltaiotacprop env sigma typ) with
         | T.Prod (na,c1,c2) -> subst_type env sigma (T.subst1 h c2) rest
         | _ -> Util.anomaly "Non-functional construction"
 
                                                                                 
   let sort_of_atomic_type env sigma ft args =
   let rec concl_of_arity env ar =
-    match T.kind_of_term (whd_betadeltaiotacprop env sigma ar) with
+    match T.kind_of_term (DoubleTypeInference.whd_betadeltaiotacprop env sigma ar) with
       | T.Prod (na, t, b) -> concl_of_arity (Environ.push_rel (na,None,t) env) b
       | T.Sort s -> Coq_sort (T.family_of_sort s)
       | _ -> outsort env sigma (subst_type env sigma ft (Array.to_list args))
@@ -260,7 +224,7 @@ let typeur sigma metamap =
           try Inductiveops.find_rectype env sigma (type_of env c)
           with Not_found -> Util.anomaly "type_of: Bad recursive type" in
         let t = Reductionops.whd_beta (T.applist (p, realargs)) in
-        (match Term.kind_of_term (whd_betadeltaiotacprop env sigma (type_of env t)) with
+        (match Term.kind_of_term (DoubleTypeInference.whd_betadeltaiotacprop env sigma (type_of env t)) with
           | T.Prod _ -> Reductionops.whd_beta (T.applist (t, [c]))
           | _ -> t)
     | T.Lambda (name,c1,c2) ->
@@ -278,7 +242,7 @@ let typeur sigma metamap =
           Coq_sort T.InProp -> T.mkProp
         | Coq_sort T.InSet -> T.mkSet
         | Coq_sort T.InType -> T.mkType Univ.prop_univ (* ERROR HERE *)
-        | CProp -> T.mkConst cprop
+        | CProp -> T.mkConst DoubleTypeInference.cprop
                                                                                 
   and sort_of env t =
     match Term.kind_of_term t with
@@ -317,7 +281,7 @@ let get_sort_family_of env evar_map ty =
 
 let type_as_sort env evar_map ty =
 (* CCorn code *)
- family_of_term (whd_betadeltaiotacprop env evar_map ty)
+ family_of_term (DoubleTypeInference.whd_betadeltaiotacprop env evar_map ty)
 ;;
 
 let is_a_Prop =
diff --git a/contrib/xml/doubleTypeInference.ml b/contrib/xml/doubleTypeInference.ml
index d0ea156e7..b0a5dc702 100644
--- a/contrib/xml/doubleTypeInference.ml
+++ b/contrib/xml/doubleTypeInference.ml
@@ -19,6 +19,45 @@
 (*CSC: tutto da rifare!!! Basarsi su Retyping che e' meno costoso! *)
 type types = {synthesized : Term.types ; expected : Term.types option};;
 
+let prerr_endline _ = ();;
+
+let cprop =
+ let module N = Names in
+  N.make_kn
+   (N.MPfile
+     (Libnames.dirpath_of_string "CoRN.algebra.CLogic"))
+   (N.make_dirpath [])
+   (N.mk_label "CProp")
+;;
+
+let whd_betadeltaiotacprop env evar_map ty =
+ let module R = Rawterm in
+  let red_exp =
+   R.Hnf  (*** Instead CProp is made Opaque ***)
+(*
+   R.Cbv
+    {R.rBeta = true ; R.rIota = true ; R.rDelta = true; R.rZeta=true ;
+     R.rConst = [Names.EvalConstRef cprop]
+    }
+*)
+  in
+Conv_oracle.set_opaque_const cprop;
+prerr_endline "###whd_betadeltaiotacprop:" ;
+let xxx =
+(*Pp.msgerr (Printer.prterm_env env ty);*)
+prerr_endline "";
+   Tacred.reduction_of_redexp red_exp env evar_map ty
+in
+prerr_endline "###FINE" ;
+(*
+Pp.msgerr (Printer.prterm_env env xxx);
+*)
+prerr_endline "";
+Conv_oracle.set_transparent_const cprop;
+xxx
+;;
+
+
 (* Code similar to the code in the Typing module, but:   *)
 (*  - the term is already assumed to be well typed       *)
 (*  - some checks have been removed                      *)
@@ -33,6 +72,12 @@ let type_judgment env sigma j =
   Typeops.type_judgment env (Evarutil.j_nf_evar sigma j)
 ;;
 
+let type_judgment_cprop env sigma j =
+  match Term.kind_of_term(whd_betadeltaiotacprop env sigma (Term.body_of_type j.Environ.uj_type)) with
+    | Term.Sort s -> Some {Environ.utj_val = j.Environ.uj_val; Environ.utj_type = s }
+    | _ -> None  (* None means the CProp constant *)
+;;
+
 let double_type_of env sigma cstr expectedty subterms_to_types =
  (*CSC: the code is inefficient because judgments are created just to be   *)
  (*CSC: destroyed using Environ.j_type. Moreover I am pretty sure that the *)
@@ -170,8 +215,12 @@ let double_type_of env sigma cstr expectedty subterms_to_types =
         let varj = type_judgment env sigma j in
         let env1 = E.push_rel (name,None,varj.E.utj_val) env in
         let j' = execute env1 sigma c2 None in
-        let varj' = type_judgment env1 sigma j' in
-         Typeops.judge_of_product env name varj varj'
+        (match type_judgment_cprop env1 sigma j' with
+            Some varj' -> Typeops.judge_of_product env name varj varj'
+          | None ->
+             (* CProp found *)
+             { Environ.uj_val = T.mkProd (name, j.Environ.uj_val, j'.Environ.uj_val);
+               Environ.uj_type = T.mkConst cprop })
 
      | T.LetIn (name,c1,c2,c3) ->
 (*CSC: What are the right expected types for the source and *)
diff --git a/contrib/xml/doubleTypeInference.mli b/contrib/xml/doubleTypeInference.mli
index 2e0badbfb..a934eaa7e 100644
--- a/contrib/xml/doubleTypeInference.mli
+++ b/contrib/xml/doubleTypeInference.mli
@@ -1,5 +1,10 @@
 type types = { synthesized : Term.types; expected : Term.types option; } 
 
+val cprop : Names.kernel_name
+
+val whd_betadeltaiotacprop :
+  Environ.env -> Evd.evar_map -> Term.constr -> Term.constr
+
 val double_type_of :
   Environ.env -> Evd.evar_map -> Term.constr -> Term.constr option ->
    types Acic.CicHash.t -> unit