From 57e708bca8555d6146c4e3d07c0a9b6a546373ce Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 19 May 2008 23:00:11 +0000 Subject: [PATCH] CProp dropped in favour of a cprop universe exported from NCicEnvironment, which is just an URI recognized by the pretty printer. --- helm/software/components/ng_kernel/.depend | 16 ++++++++++------ helm/software/components/ng_kernel/TEST | 9 +++++---- helm/software/components/ng_kernel/check.ml | 2 +- helm/software/components/ng_kernel/nCic.ml | 2 +- helm/software/components/ng_kernel/nCic2OCic.ml | 7 ++++++- .../components/ng_kernel/nCicEnvironment.ml | 3 ++- .../components/ng_kernel/nCicEnvironment.mli | 1 + helm/software/components/ng_kernel/nCicPp.ml | 1 - .../components/ng_kernel/nCicTypeChecker.ml | 7 ++----- helm/software/components/ng_kernel/oCic2NCic.ml | 4 +++- 10 files changed, 31 insertions(+), 21 deletions(-) diff --git a/helm/software/components/ng_kernel/.depend b/helm/software/components/ng_kernel/.depend index 22002034a..0e324483a 100644 --- 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 bf33415d3..3479aed5b 100644 --- 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 ab012367a..fb9d553b8 100644 --- 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 afd73e53e..d3bc8d793 100644 --- 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 20482ec71..d9edb1100 100644 --- 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 bd0587a43..46552d5aa 100644 --- 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 67b3857d1..d3c60a3c2 100644 --- 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 449c4313b..9f609c850 100644 --- 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 ae145a9c6..c028b916f 100644 --- 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 aa546d773..0e9ff4831 100644 --- 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)),[] -- 2.39.2