CProp dropped in favour of a cprop universe exported from NCicEnvironment,

which is just an URI recognized by the pretty printer.

diff --git a/helm/software/components/ng_kernel/.depend b/helm/software/components/ng_kernel/.depend
index 22002034a9259268d4a964fd161e1e319b143096..0e324483a6f2fd943db46ad3b74ca18ef3c2c02c 100644 (file)
--- a/helm/software/components/ng_kernel/.depend
+++ b/helm/software/components/ng_kernel/.depend
@@ -14,16 +14,20 @@ nUri.cmo: nUri.cmi
 nUri.cmx: nUri.cmi 
 nReference.cmo: nUri.cmi nReference.cmi 
 nReference.cmx: nUri.cmx nReference.cmi 
-nCicUtils.cmo: nCic.cmo nCicUtils.cmi 
-nCicUtils.cmx: nCic.cmx nCicUtils.cmi 
-nCicSubstitution.cmo: nCicUtils.cmi nCic.cmo nCicSubstitution.cmi 
-nCicSubstitution.cmx: nCicUtils.cmx nCic.cmx nCicSubstitution.cmi 
+nCicUtils.cmo: nReference.cmi nCic.cmo nCicUtils.cmi 
+nCicUtils.cmx: nReference.cmx nCic.cmx nCicUtils.cmi 
+nCicSubstitution.cmo: nReference.cmi nCicUtils.cmi nCic.cmo \
+    nCicSubstitution.cmi 
+nCicSubstitution.cmx: nReference.cmx nCicUtils.cmx nCic.cmx \
+    nCicSubstitution.cmi 
 oCic2NCic.cmo: nUri.cmi nReference.cmi nCicSubstitution.cmi nCic.cmo \
     oCic2NCic.cmi 
 oCic2NCic.cmx: nUri.cmx nReference.cmx nCicSubstitution.cmx nCic.cmx \
     oCic2NCic.cmi 
-nCic2OCic.cmo: nUri.cmi nReference.cmi nCic.cmo nCic2OCic.cmi 
-nCic2OCic.cmx: nUri.cmx nReference.cmx nCic.cmx nCic2OCic.cmi 
+nCic2OCic.cmo: nUri.cmi nReference.cmi nCicEnvironment.cmi nCic.cmo \
+    nCic2OCic.cmi 
+nCic2OCic.cmx: nUri.cmx nReference.cmx nCicEnvironment.cmx nCic.cmx \
+    nCic2OCic.cmi 
 nCicLibrary.cmo: oCic2NCic.cmi nUri.cmi nCic2OCic.cmi nCicLibrary.cmi 
 nCicLibrary.cmx: oCic2NCic.cmx nUri.cmx nCic2OCic.cmx nCicLibrary.cmi 
 nCicEnvironment.cmo: nUri.cmi nReference.cmi nCicLibrary.cmi nCic.cmo \

diff --git a/helm/software/components/ng_kernel/TEST b/helm/software/components/ng_kernel/TEST
index bf33415d3b1a5408f665e63d22c480e745fc45ac..3479aed5bd9e386dee0b2e0f902fa7bf9e92488f 100644 (file)
--- a/helm/software/components/ng_kernel/TEST
+++ b/helm/software/components/ng_kernel/TEST
@@ -43,10 +43,11 @@ Sophia-Antipolis/Float: vecchio nucleo troppo lento
 Sophia-Antipolis/geometry: vecchio nucleo troppo lento
 Rocq/ALGEBRA/CATEGORY_THEORY: vecchio nucleo troppo lento
 
-Sophia-Antipolis/Algebra: nuovo nucleo diverge
-   cic:/Sophia-Antipolis/Algebra/Sub_module/submodule_op.con
-Sophia-Antipolis/Buchberger: nuovo nucleo diverge
-   cic:/Sophia-Antipolis/Buchberger/BuchRed/redbuch_stable.con
+## = diventato addirittura velocissimo dopo universi + proof irrelevance + altezze
+##Sophia-Antipolis/Algebra: nuovo nucleo diverge
+##   cic:/Sophia-Antipolis/Algebra/Sub_module/submodule_op.con
+##Sophia-Antipolis/Buchberger: nuovo nucleo diverge
+##   cic:/Sophia-Antipolis/Buchberger/BuchRed/redbuch_stable.con
 matita/freescale: nuovo nucleo molto piu' lento del vecchio?
 
 lannion: nuovo nucleo impredicative set

diff --git a/helm/software/components/ng_kernel/check.ml b/helm/software/components/ng_kernel/check.ml
index ab012367ace8d4159b77175d7f92eb5feda5ac70..fb9d553b8e40b7bc3f38f0f9c914b3b5eef98bfb 100644 (file)
--- a/helm/software/components/ng_kernel/check.ml
+++ b/helm/software/components/ng_kernel/check.ml
@@ -12,7 +12,7 @@
 (* $Id$ *)
 
 let debug = true
-let ignore_exc = false
+let ignore_exc = true
 let rank_all_dependencies = false
 let trust_environment = false
 

diff --git a/helm/software/components/ng_kernel/nCic.ml b/helm/software/components/ng_kernel/nCic.ml
index afd73e53ef231a30a987b854e6eface05cddf5ea..d3bc8d793730e7cf8c6b1dc471b254beb98063f4 100644 (file)
--- a/helm/software/components/ng_kernel/nCic.ml
+++ b/helm/software/components/ng_kernel/nCic.ml
@@ -16,7 +16,7 @@
 type universe = (bool * NUri.uri) list 
   (* Max of non-empty list of named universes, or their successor (when true) *)
 
-type sort = Prop | Type of universe | CProp
+type sort = Prop | Type of universe
 
 type implicit_annotation = [ `Closed | `Type | `Hole | `Term ]
 

diff --git a/helm/software/components/ng_kernel/nCic2OCic.ml b/helm/software/components/ng_kernel/nCic2OCic.ml
index 20482ec7136e8d0490d1e8bf575949033bf191f4..d9edb1100c7d45340f97a907353decc2fc345c6d 100644 (file)
--- a/helm/software/components/ng_kernel/nCic2OCic.ml
+++ b/helm/software/components/ng_kernel/nCic2OCic.ml
@@ -15,6 +15,8 @@ let ouri_of_nuri u = UriManager.uri_of_string (NUri.string_of_uri u);;
 
 let ouri_of_reference (NReference.Ref (u,_)) = ouri_of_nuri u;;
 
+let cprop = [false, NUri.uri_of_string ("cic:/matita/pts/CProp.univ")];;
+
 let nn_2_on = function
   | "_" -> Cic.Anonymous
   | s -> Cic.Name s
@@ -32,7 +34,10 @@ let convert_term uri n_fl t =
  | NCic.LetIn (n,ty_s,s,t) -> 
      Cic.LetIn (nn_2_on n,convert_term k s,convert_term k ty_s, convert_term (k+1) t)
  | NCic.Sort NCic.Prop -> Cic.Sort Cic.Prop 
- | NCic.Sort NCic.CProp -> Cic.Sort Cic.CProp 
+ | NCic.Sort (NCic.Type u) when
+    (* BUG HERE: I should use NCicEnvironment.universe_eq, but I do not
+       want to add this recursion between the modules *)
+    (*NCicEnvironment.universe_eq*) u=cprop -> Cic.Sort Cic.CProp 
  | NCic.Sort (NCic.Type _) -> Cic.Sort (Cic.Type (CicUniv.fresh ()))
  | NCic.Implicit _ -> assert false
  | NCic.Const (NReference.Ref (u,NReference.Ind (_,i,_))) -> 

diff --git a/helm/software/components/ng_kernel/nCicEnvironment.ml b/helm/software/components/ng_kernel/nCicEnvironment.ml
index bd0587a43a53f3fd6afb5f8dda9954167c9716f1..46552d5aa690e649354315ead787b6014da77716 100644 (file)
--- a/helm/software/components/ng_kernel/nCicEnvironment.ml
+++ b/helm/software/components/ng_kernel/nCicEnvironment.ml
@@ -19,7 +19,8 @@ exception ObjectNotFound of string Lazy.t;;
 exception BadDependency of string Lazy.t;;
 exception BadConstraint of string Lazy.t;;
 
-let type0 = [false, NUri.uri_of_string ("cic:/matita/pts/Type.univ")]
+let type0 = []
+let cprop = [false, NUri.uri_of_string ("cic:/matita/pts/CProp.univ")]
 
 let le_constraints = ref [] (* strict,a,b *)
 

diff --git a/helm/software/components/ng_kernel/nCicEnvironment.mli b/helm/software/components/ng_kernel/nCicEnvironment.mli
index 67b3857d1703f71ea1cb0abe191247fc3c974090..d3c60a3c2e417dfe4df428c6e21d40fc85c308b0 100644 (file)
--- a/helm/software/components/ng_kernel/nCicEnvironment.mli
+++ b/helm/software/components/ng_kernel/nCicEnvironment.mli
@@ -21,6 +21,7 @@ val get_checked_obj: NUri.uri -> NCic.obj
 val get_relevance: NReference.reference -> bool list
 
 val type0: NCic.universe
+val cprop: NCic.universe
 (* universe_* raise BadConstraints if the second arg. is an inferred universe *)
 val universe_eq: NCic.universe -> NCic.universe -> bool
 val universe_leq: NCic.universe -> NCic.universe -> bool

diff --git a/helm/software/components/ng_kernel/nCicPp.ml b/helm/software/components/ng_kernel/nCicPp.ml
index 449c4313bb2673781be828c83a797f76779a75ac..9f609c85042e166f6c62729255709c58161ab660 100644 (file)
--- a/helm/software/components/ng_kernel/nCicPp.ml
+++ b/helm/software/components/ng_kernel/nCicPp.ml
@@ -133,7 +133,6 @@ let trivial_pp_term ~context ~subst ~metasenv ?(inside_fix=false) t =
    | C.Implicit _ -> F.fprintf f "?"
    | C.Meta (n,_) -> F.fprintf f "?%d" n
    | C.Sort C.Prop -> F.fprintf f "Prop"
-   | C.Sort C.CProp -> F.fprintf f "CProp"
    | C.Sort (C.Type []) -> F.fprintf f "IllFormedUniverse"
    | C.Sort (C.Type [false, u]) -> F.fprintf f "%s" (NUri.name_of_uri u)
    | C.Sort (C.Type [true, u]) -> F.fprintf f "S(%s)" (NUri.name_of_uri u)

diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml
index ae145a9c6acaa1de15fc2afa14e00ddf26232c26..c028b916f24d6e9d39ac53c93782ed840d0b2c31 100644 (file)
--- a/helm/software/components/ng_kernel/nCicTypeChecker.ml
+++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml
@@ -128,8 +128,6 @@ let sort_of_prod ~metasenv ~subst context (name,s) (t1, t2) =
    | C.Sort s1, C.Sort C.Prop -> t2
    | C.Sort (C.Type u1), C.Sort (C.Type u2) -> C.Sort (C.Type (u1@u2)) 
    | C.Sort _,C.Sort (C.Type _) -> t2
-   | C.Sort (C.Type _) , C.Sort C.CProp -> t1
-   | C.Sort _, C.Sort C.CProp
    | C.Meta (_,(_,(C.Irl 0 | C.Ctx []))), C.Sort _
    | C.Meta (_,(_,(C.Irl 0 | C.Ctx []))), C.Meta (_,(_,(C.Irl 0 | C.Ctx [])))
    | C.Sort _, C.Meta  (_,(_,(C.Irl 0 | C.Ctx []))) -> t2
@@ -678,9 +676,9 @@ let rec typeof ~subst ~metasenv context term =
             (PP.ppterm ~subst ~metasenv ~context so)
             )));
           (match arity1, R.whd ~subst ((name,C.Decl so)::context) ta with
-            | (C.Sort (C.CProp | C.Type _), C.Sort _)
+            | (C.Sort C.Type _, C.Sort _)
             | (C.Sort C.Prop, C.Sort C.Prop) -> ()
-            | (C.Sort C.Prop, C.Sort (C.CProp | C.Type _)) ->
+            | (C.Sort C.Prop, C.Sort C.Type _) ->
         (* TODO: we should pass all these parameters since we
          * have them already *)
                 let inductive,leftno,itl,_,i = E.get_checked_indtys r in
@@ -755,7 +753,6 @@ and check_mutual_inductive_defs uri ~metasenv ~subst is_ind leftno tyl =
                       " of the constructor is not included in the inductive" ^
                       " type sort " ^ PP.ppterm ~metasenv ~subst ~context s2)))
              | C.Sort _, C.Sort C.Prop
-             | C.Sort C.CProp, C.Sort C.CProp
              | C.Sort _, C.Sort C.Type _ -> ()
              | _, _ ->
                 raise

diff --git a/helm/software/components/ng_kernel/oCic2NCic.ml b/helm/software/components/ng_kernel/oCic2NCic.ml
index aa546d773ca7821f43aada14e2562831ce9e66fa..0e9ff4831c4f2469818a4a722b696800174a7154 100644 (file)
--- a/helm/software/components/ng_kernel/oCic2NCic.ml
+++ b/helm/software/components/ng_kernel/oCic2NCic.ml
@@ -22,6 +22,8 @@ let mk_type n =
      [false, NUri.uri_of_string ("cic:/matita/pts/Type"^string_of_int n^".univ")]
 ;;
 
+let cprop = [false, NUri.uri_of_string ("cic:/matita/pts/CProp.univ")];;
+
 (* porcatissima *)
 type reference = Ref of NUri.uri * NReference.spec
 let reference_of_ouri u indinfo =
@@ -621,7 +623,7 @@ let convert_term uri t =
         let ty, fixpoints_ty = aux k octx ctx n_fix uri ty in
         NCic.LetIn ("cast", ty, t, NCic.Rel 1), fixpoints_t @ fixpoints_ty
     | Cic.Sort Cic.Prop -> NCic.Sort NCic.Prop,[]
-    | Cic.Sort Cic.CProp -> NCic.Sort NCic.CProp,[]
+    | Cic.Sort Cic.CProp -> NCic.Sort (NCic.Type cprop),[]
     | Cic.Sort (Cic.Type u) -> 
           NCic.Sort (NCic.Type (mk_type (CicUniv.get_rank u))),[] 
     | Cic.Sort Cic.Set -> NCic.Sort (NCic.Type (mk_type 0)),[]