From 6719c0e318b312b51b089fea3d69d1b7103245ea Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 30 May 2008 19:28:41 +0000 Subject: [PATCH] CProp hierarchy is there! Implications: - more universes, XML file format changed, please rebuild your stuff - CProp conclusions are eliminated with _rect and not _rec - CProp and Types are interleaved, but still comparable, this may (or not) what you expect: Type_i < CProp_i < Type_i+1 < CProp_i+1 Caveats: - are_convertible sort CProp may turn to be wrong, since Type_i is convertible (<=) to CProp_i+0.5 and there is no way to set test_equality_only, an additional parameter may be useful - CProp goals will be tackled by auto even if they could be cumulated into Type that is not (by default) take into consideration --- .../components/acic_content/cicNotationPp.ml | 2 +- .../components/acic_content/cicNotationPt.ml | 2 +- .../acic_content/termAcicContent.ml | 4 +- .../acic_procedural/proceduralHelpers.ml | 2 +- helm/software/components/cic/cic.ml | 2 +- helm/software/components/cic/cicParser.ml | 15 +++--- helm/software/components/cic_acic/cic2acic.ml | 9 ++-- .../software/components/cic_acic/cic2acic.mli | 2 +- .../cic_acic/doubleTypeInference.ml | 13 ++--- .../cic_disambiguation/disambiguate.ml | 2 +- .../cic_exportation/cicExportation.ml | 2 +- .../components/cic_proof_checking/cicPp.ml | 4 +- .../cic_proof_checking/cicReduction.ml | 21 +++++--- .../cic_proof_checking/cicTypeChecker.ml | 50 +++++++++++++------ .../cic_proof_checking/freshNamesGenerator.ml | 4 +- .../components/cic_unification/cicRefine.ml | 29 ++++++++++- .../content_pres/cicNotationParser.ml | 2 +- .../content_pres/termContentPres.ml | 2 +- helm/software/components/tactics/auto.ml | 27 +++++----- .../components/tactics/eliminationTactics.ml | 2 +- .../components/tactics/primitiveTactics.ml | 2 +- helm/software/matita/dist/ChangeLog | 1 + helm/software/matita/matitaScript.ml | 2 +- 23 files changed, 126 insertions(+), 75 deletions(-) diff --git a/helm/software/components/acic_content/cicNotationPp.ml b/helm/software/components/acic_content/cicNotationPp.ml index 50312ff12..6ea839ce3 100644 --- a/helm/software/components/acic_content/cicNotationPp.ml +++ b/helm/software/components/acic_content/cicNotationPp.ml @@ -158,7 +158,7 @@ let rec pp_term ?(pp_parens = true) t = | Ast.Sort `Set -> "Set" | Ast.Sort `Prop -> "Prop" | Ast.Sort (`Type _) -> "Type" - | Ast.Sort `CProp -> "CProp" + | Ast.Sort (`CProp _)-> "CProp" | Ast.Symbol (name, _) -> "'" ^ name | Ast.UserInput -> "" diff --git a/helm/software/components/acic_content/cicNotationPt.ml b/helm/software/components/acic_content/cicNotationPt.ml index d9d92ad6f..cc481ff0a 100644 --- a/helm/software/components/acic_content/cicNotationPt.ml +++ b/helm/software/components/acic_content/cicNotationPt.ml @@ -29,7 +29,7 @@ type binder_kind = [ `Lambda | `Pi | `Exists | `Forall ] type induction_kind = [ `Inductive | `CoInductive ] -type sort_kind = [ `Prop | `Set | `Type of CicUniv.universe | `CProp ] +type sort_kind = [ `Prop | `Set | `Type of CicUniv.universe | `CProp of CicUniv.universe] type fold_kind = [ `Left | `Right ] type location = Stdpp.location diff --git a/helm/software/components/acic_content/termAcicContent.ml b/helm/software/components/acic_content/termAcicContent.ml index 2ce47bb67..7a4590849 100644 --- a/helm/software/components/acic_content/termAcicContent.ml +++ b/helm/software/components/acic_content/termAcicContent.ml @@ -103,14 +103,14 @@ let ast_of_acic0 ~output_type term_info acic k = | Cic.ASort (id,Cic.Prop) -> idref id (Ast.Sort `Prop) | Cic.ASort (id,Cic.Set) -> idref id (Ast.Sort `Set) | Cic.ASort (id,Cic.Type u) -> idref id (Ast.Sort (`Type u)) - | Cic.ASort (id,Cic.CProp) -> idref id (Ast.Sort `CProp) + | Cic.ASort (id,Cic.CProp u) -> idref id (Ast.Sort (`CProp u)) | Cic.AImplicit (id, Some `Hole) -> idref id Ast.UserInput | Cic.AImplicit (id, _) -> idref id Ast.Implicit | Cic.AProd (id,n,s,t) -> let binder_kind = match sort_of_id id with | `Set | `Type _ -> `Pi - | `Prop | `CProp -> `Forall + | `Prop | `CProp _ -> `Forall in idref id (Ast.Binder (binder_kind, (CicNotationUtil.name_of_cic_name n, Some (k s)), k t)) diff --git a/helm/software/components/acic_procedural/proceduralHelpers.ml b/helm/software/components/acic_procedural/proceduralHelpers.ml index d599bdeb2..4d8652107 100644 --- a/helm/software/components/acic_procedural/proceduralHelpers.ml +++ b/helm/software/components/acic_procedural/proceduralHelpers.ml @@ -133,7 +133,7 @@ let get_default_eliminator context uri tyno ty = let ext = match get_tail context (get_type context ty) with | C.Sort C.Prop -> "_ind" | C.Sort C.Set -> "_rec" - | C.Sort C.CProp -> "_rec" + | C.Sort (C.CProp _) -> "_rect" | C.Sort (C.Type _) -> "_rect" | t -> Printf.eprintf "CicPPP get_default_eliminator: %s\n" (Pp.ppterm t); diff --git a/helm/software/components/cic/cic.ml b/helm/software/components/cic/cic.ml index 5dd8455ea..53b4ef62b 100644 --- a/helm/software/components/cic/cic.ml +++ b/helm/software/components/cic/cic.ml @@ -49,7 +49,7 @@ type sort = Prop | Set | Type of CicUniv.universe - | CProp + | CProp of CicUniv.universe type name = | Name of string diff --git a/helm/software/components/cic/cicParser.ml b/helm/software/components/cic/cicParser.ml index e61ee78ea..30e7a0b38 100644 --- a/helm/software/components/cic/cicParser.ml +++ b/helm/software/components/cic/cicParser.ml @@ -300,23 +300,26 @@ let impredicative_set = ref true;; let sort_of_string ctxt = function | "Prop" -> Cic.Prop - | "CProp" -> Cic.CProp (* THIS CASE IS HERE ONLY TO ALLOW THE PARSING OF COQ LIBRARY * THIS SHOULD BE REMOVED AS SOON AS univ_maker OR COQ'S EXPORTATION * IS FIXED *) + | "CProp" -> Cic.CProp (CicUniv.fresh ~uri:ctxt.uri ()) | "Type" -> Cic.Type (CicUniv.fresh ~uri:ctxt.uri ()) | "Set" when !impredicative_set -> Cic.Set | "Set" -> Cic.Type (CicUniv.fresh ~uri:ctxt.uri ()) | s -> let len = String.length s in - if not(len > 5) then parse_error ctxt "sort expected"; - if not(String.sub s 0 5 = "Type:") then parse_error ctxt "sort expected"; - let s = String.sub s 5 (len - 5) in + let sort_len, mk_sort = + if len > 5 && String.sub s 0 5 = "Type:" then 5,fun x -> Cic.Type x + else if len > 6 && String.sub s 0 6 = "CProp:" then 6,fun x->Cic.CProp x + else parse_error ctxt "sort expected" + in + let s = String.sub s sort_len (len - sort_len) in let i = String.index s ':' in let id = int_of_string (String.sub s 0 i) in - let suri = String.sub s (i+1) (len - 5 - i - 1) in + let suri = String.sub s (i+1) (len - sort_len - i - 1) in let uri = UriManager.uri_of_string suri in - try Cic.Type (CicUniv.fresh ~uri ~id ()) + try mk_sort (CicUniv.fresh ~uri ~id ()) with | Failure "int_of_string" | Invalid_argument _ -> parse_error ctxt "sort expected" diff --git a/helm/software/components/cic_acic/cic2acic.ml b/helm/software/components/cic_acic/cic2acic.ml index b039b7e5b..01a4bb144 100644 --- a/helm/software/components/cic_acic/cic2acic.ml +++ b/helm/software/components/cic_acic/cic2acic.ml @@ -25,19 +25,20 @@ (* $Id$ *) -type sort_kind = [ `Prop | `Set | `Type of CicUniv.universe | `CProp ] +type sort_kind = [ `Prop | `Set | `Type of CicUniv.universe | `CProp of CicUniv.universe ] let string_of_sort = function | `Prop -> "Prop" | `Set -> "Set" | `Type u -> "Type:" ^ string_of_int (CicUniv.univno u) ^ ":" ^ UriManager.string_of_uri (CicUniv.univuri u) - | `CProp -> "CProp" + | `CProp u -> "CProp:" ^ string_of_int (CicUniv.univno u) ^ ":" ^ UriManager.string_of_uri (CicUniv.univuri u) + let sort_of_sort = function | Cic.Prop -> `Prop | Cic.Set -> `Set | Cic.Type u -> `Type u - | Cic.CProp -> `CProp + | Cic.CProp u -> `CProp u (* let hashtbl_add_time = ref 0.0;; *) @@ -149,7 +150,7 @@ let acic_of_cic_context' ~computeinnertypes:global_computeinnertypes | C.Sort C.Set -> `Set | C.Sort (C.Type u) -> `Type u | C.Meta _ -> `Type (CicUniv.fresh()) - | C.Sort C.CProp -> `CProp + | C.Sort (C.CProp u) -> `CProp u | t -> prerr_endline ("Cic2acic.sort_of applied to: " ^ CicPp.ppterm t) ; assert false diff --git a/helm/software/components/cic_acic/cic2acic.mli b/helm/software/components/cic_acic/cic2acic.mli index b63a585e6..c3cf56e88 100644 --- a/helm/software/components/cic_acic/cic2acic.mli +++ b/helm/software/components/cic_acic/cic2acic.mli @@ -31,7 +31,7 @@ type anntypes = {annsynthesized : Cic.annterm ; annexpected : Cic.annterm option} ;; -type sort_kind = [ `Prop | `Set | `Type of CicUniv.universe | `CProp ] +type sort_kind = [ `Prop | `Set | `Type of CicUniv.universe | `CProp of CicUniv.universe] val string_of_sort: sort_kind -> string (*val sort_of_string: string -> sort_kind*) diff --git a/helm/software/components/cic_acic/doubleTypeInference.ml b/helm/software/components/cic_acic/doubleTypeInference.ml index 6fa7cce5a..1671b98d2 100644 --- a/helm/software/components/cic_acic/doubleTypeInference.ml +++ b/helm/software/components/cic_acic/doubleTypeInference.ml @@ -608,15 +608,10 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty = let t1' = CicReduction.whd context t1 in let t2' = CicReduction.whd ((Some (name,C.Decl s))::context) t2 in match (t1', t2') with - (C.Sort _, C.Sort s2) - when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) -> - (* different from Coq manual!!! *) - C.Sort s2 - | (C.Sort (C.Type t1), C.Sort (C.Type t2)) -> - C.Sort (C.Type (CicUniv.fresh())) - | (C.Sort _,C.Sort (C.Type t1)) -> - (* TASSI: CONSRTAINTS: the same in cictypechecker,cicrefine *) - C.Sort (C.Type t1) (* c'e' bisogno di un fresh? *) + | (C.Sort _, C.Sort s2) when (s2 = C.Prop || s2 = C.Set) -> C.Sort s2 + | (C.Sort (C.Type t1), C.Sort (C.Type t2)) ->C.Sort(C.Type(CicUniv.fresh())) + | (C.Sort _,C.Sort (C.Type t1)) -> C.Sort (C.Type t1) + | (C.Sort _,C.Sort (C.CProp t1)) -> C.Sort (C.CProp t1) | (C.Meta _, C.Sort _) -> t2' | (C.Meta _, (C.Meta (_,_) as t)) | (C.Sort _, (C.Meta (_,_) as t)) when CicUtil.is_closed t -> diff --git a/helm/software/components/cic_disambiguation/disambiguate.ml b/helm/software/components/cic_disambiguation/disambiguate.ml index 41c24c9ae..68afd810b 100644 --- a/helm/software/components/cic_disambiguation/disambiguate.ml +++ b/helm/software/components/cic_disambiguation/disambiguate.ml @@ -542,7 +542,7 @@ let interpretate_term ?(create_dummy_ids=false) ~(context: Cic.name list) ~env ~ | CicNotationPt.Sort `Prop -> Cic.Sort Cic.Prop | CicNotationPt.Sort `Set -> Cic.Sort Cic.Set | CicNotationPt.Sort (`Type u) -> Cic.Sort (Cic.Type u) - | CicNotationPt.Sort `CProp -> Cic.Sort Cic.CProp + | CicNotationPt.Sort (`CProp u) -> Cic.Sort (Cic.CProp u) | CicNotationPt.Symbol (symbol, instance) -> resolve env (Symbol (symbol, instance)) () | _ -> assert false (* god bless Bologna *) diff --git a/helm/software/components/cic_exportation/cicExportation.ml b/helm/software/components/cic_exportation/cicExportation.ml index cd5ab3ace..c595c6d7d 100644 --- a/helm/software/components/cic_exportation/cicExportation.ml +++ b/helm/software/components/cic_exportation/cicExportation.ml @@ -182,7 +182,7 @@ let rec pp ~in_type t context = | C.Set -> "Set" | C.Type _ -> "Type" (*| C.Type u -> ("Type" ^ CicUniv.string_of_universe u)*) - | C.CProp -> "CProp" + | C.CProp _ -> "CProp" ) | C.Implicit (Some `Hole) -> "%" | C.Implicit _ -> "?" diff --git a/helm/software/components/cic_proof_checking/cicPp.ml b/helm/software/components/cic_proof_checking/cicPp.ml index 1686cd357..58f319f4a 100644 --- a/helm/software/components/cic_proof_checking/cicPp.ml +++ b/helm/software/components/cic_proof_checking/cicPp.ml @@ -114,7 +114,7 @@ let rec pp t l = | C.Set -> "Set" | C.Type _ -> "Type" (*| C.Type u -> ("Type" ^ CicUniv.string_of_universe u)*) - | C.CProp -> "CProp" + | C.CProp _ -> "CProp" ) | C.Implicit (Some `Hole) -> "%" | C.Implicit _ -> "?" @@ -347,7 +347,7 @@ let ppsort = function | Cic.Prop -> "Prop" | Cic.Set -> "Set" | Cic.Type _ -> "Type" - | Cic.CProp -> "CProp" + | Cic.CProp _ -> "CProp" (* MATITA NAMING CONVENTION *) diff --git a/helm/software/components/cic_proof_checking/cicReduction.ml b/helm/software/components/cic_proof_checking/cicReduction.ml index 5e02fdbaa..1499712c9 100644 --- a/helm/software/components/cic_proof_checking/cicReduction.ml +++ b/helm/software/components/cic_proof_checking/cicReduction.ml @@ -869,19 +869,26 @@ prerr_endline ("%%%%%%: " ^ CicPp.ppterm term' ^ " <==> " ^ CicPp.ppterm t1); *) aux test_equality_only context t1 term' ugraph with CicUtil.Subst_not_found _ -> false,ugraph) - (* TASSI: CONSTRAINTS *) - | (C.Sort (C.Type t1), C.Sort (C.Type t2)) when test_equality_only -> + | (C.Sort (C.Type t1), C.Sort (C.Type t2)) + | (C.Sort (C.CProp t1), C.Sort (C.CProp t2)) when test_equality_only -> (try true,(CicUniv.add_eq t2 t1 ugraph) with CicUniv.UniverseInconsistency _ -> false,ugraph) - (* TASSI: CONSTRAINTS *) - | (C.Sort (C.Type t1), C.Sort (C.Type t2)) -> + | (C.Sort (C.Type t1), C.Sort (C.Type t2)) + | (C.Sort (C.CProp t1), C.Sort (C.CProp t2)) -> (try true,(CicUniv.add_ge t2 t1 ugraph) with CicUniv.UniverseInconsistency _ -> false,ugraph) - (* TASSI: CONSTRAINTS *) - | (C.Sort s1, C.Sort (C.Type _)) -> (not test_equality_only),ugraph - (* TASSI: CONSTRAINTS *) + | (C.Sort (C.CProp t1), C.Sort (C.Type t2)) when not test_equality_only -> + (try + true,(CicUniv.add_gt t2 t1 ugraph) + with CicUniv.UniverseInconsistency _ -> false,ugraph) + | (C.Sort (C.Type t1), C.Sort (C.CProp t2)) when not test_equality_only -> + (try + true,(CicUniv.add_ge t2 t1 ugraph) + with CicUniv.UniverseInconsistency _ -> false,ugraph) + | (C.Sort s1, C.Sort (C.Type _)) + | (C.Sort s1, C.Sort (C.CProp _)) -> (not test_equality_only),ugraph | (C.Sort s1, C.Sort s2) -> (s1 = s2),ugraph | (C.Prod (name1,s1,t1), C.Prod(_,s2,t2)) -> let b',ugraph' = aux true context s1 s2 ugraph in diff --git a/helm/software/components/cic_proof_checking/cicTypeChecker.ml b/helm/software/components/cic_proof_checking/cicTypeChecker.ml index 4dfe78301..1756497c0 100644 --- a/helm/software/components/cic_proof_checking/cicTypeChecker.ml +++ b/helm/software/components/cic_proof_checking/cicTypeChecker.ml @@ -572,11 +572,15 @@ and typecheck_mutual_inductive_defs ~logger uri (itl,_,indparamsno) ugraph = match CicReduction.whd context con_sort, CicReduction.whd [] ty_sort with - Cic.Sort (Cic.Type u1), Cic.Sort (Cic.Type u2) -> + Cic.Sort (Cic.Type u1), Cic.Sort (Cic.Type u2) + | Cic.Sort (Cic.CProp u1), Cic.Sort (Cic.CProp u2) + | Cic.Sort (Cic.Type u1), Cic.Sort (Cic.CProp u2) -> CicUniv.add_ge u2 u1 ugraph + | Cic.Sort (Cic.CProp u1), Cic.Sort (Cic.Type u2) -> + CicUniv.add_gt u2 u1 ugraph | Cic.Sort _, Cic.Sort Cic.Prop + | Cic.Sort _, Cic.Sort Cic.CProp _ | Cic.Sort _, Cic.Sort Cic.Set - | Cic.Sort Cic.CProp, Cic.Sort Cic.CProp | Cic.Sort _, Cic.Sort Cic.Type _ -> ugraph | a,b -> raise @@ -1156,7 +1160,7 @@ and check_allowed_sort_elimination ~subst ~metasenv ~logger context uri i ((Some (name,C.Decl so))::context) ta true | (C.Sort C.Prop, C.Sort C.Prop) when need_dummy -> true,ugraph | (C.Sort C.Prop, C.Sort C.Set) - | (C.Sort C.Prop, C.Sort C.CProp) + | (C.Sort C.Prop, C.Sort (C.CProp _)) | (C.Sort C.Prop, C.Sort (C.Type _) ) when need_dummy -> (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in match o with @@ -1182,12 +1186,9 @@ and check_allowed_sort_elimination ~subst ~metasenv ~logger context uri i UriManager.string_of_uri uri))) ) | (C.Sort C.Set, C.Sort C.Prop) when need_dummy -> true , ugraph - | (C.Sort C.CProp, C.Sort C.Prop) when need_dummy -> true , ugraph | (C.Sort C.Set, C.Sort C.Set) when need_dummy -> true , ugraph - | (C.Sort C.Set, C.Sort C.CProp) when need_dummy -> true , ugraph - | (C.Sort C.CProp, C.Sort C.Set) when need_dummy -> true , ugraph - | (C.Sort C.CProp, C.Sort C.CProp) when need_dummy -> true , ugraph - | ((C.Sort C.Set, C.Sort (C.Type _)) | (C.Sort C.CProp, C.Sort (C.Type _))) + | (C.Sort C.Set, C.Sort (C.Type _)) + | (C.Sort C.Set, C.Sort (C.CProp _)) when need_dummy -> (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in match o with @@ -1209,6 +1210,7 @@ and check_allowed_sort_elimination ~subst ~metasenv ~logger context uri i UriManager.string_of_uri uri))) ) | (C.Sort (C.Type _), C.Sort _) when need_dummy -> true , ugraph + | (C.Sort (C.CProp _), C.Sort _) when need_dummy -> true , ugraph | (_,_) -> false,ugraph in check_allowed_sort_elimination_aux ugraph context arity2 need_dummy @@ -1837,9 +1839,7 @@ end; | (C.Sort s1, C.Sort (C.Prop | C.Set)) -> (* different from Coq manual!!! *) t2',ugraph - | (C.Sort (C.Prop | C.Set | C.CProp), C.Sort C.CProp ) -> t2', ugraph | (C.Sort (C.Type t1), C.Sort (C.Type t2)) -> - (* TASSI: CONSRTAINTS: the same in doubletypeinference, cicrefine *) let t' = CicUniv.fresh() in (try let ugraph1 = CicUniv.add_ge t' t1 ugraph in @@ -1847,10 +1847,32 @@ end; C.Sort (C.Type t'),ugraph2 with CicUniv.UniverseInconsistency msg -> raise (TypeCheckerFailure msg)) - | (C.Sort _,C.Sort (C.Type t1)) - | (C.Sort (C.Type t1), C.Sort C.CProp) -> - (* TASSI: CONSRTAINTS: the same in doubletypeinference, cicrefine *) - C.Sort (C.Type t1),ugraph (* c'e' bisogno di un fresh? *) + | (C.Sort (C.CProp t1), C.Sort (C.CProp t2)) -> + let t' = CicUniv.fresh() in + (try + let ugraph1 = CicUniv.add_ge t' t1 ugraph in + let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in + C.Sort (C.CProp t'),ugraph2 + with + CicUniv.UniverseInconsistency msg -> raise (TypeCheckerFailure msg)) + | (C.Sort (C.Type t1), C.Sort (C.CProp t2)) -> + let t' = CicUniv.fresh() in + (try + let ugraph1 = CicUniv.add_ge t' t1 ugraph in + let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in + C.Sort (C.CProp t'),ugraph2 + with + CicUniv.UniverseInconsistency msg -> raise (TypeCheckerFailure msg)) + | (C.Sort (C.CProp t1), C.Sort (C.Type t2)) -> + let t' = CicUniv.fresh() in + (try + let ugraph1 = CicUniv.add_gt t' t1 ugraph in + let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in + C.Sort (C.Type t'),ugraph2 + with + CicUniv.UniverseInconsistency msg -> raise (TypeCheckerFailure msg)) + | (C.Sort _,C.Sort (C.Type t1)) -> C.Sort (C.Type t1),ugraph + | (C.Sort _,C.Sort (C.CProp t1)) -> C.Sort (C.CProp t1),ugraph | (C.Meta _, C.Sort _) -> t2',ugraph | (C.Meta _, (C.Meta (_,_) as t)) | (C.Sort _, (C.Meta (_,_) as t)) when CicUtil.is_closed t -> diff --git a/helm/software/components/cic_proof_checking/freshNamesGenerator.ml b/helm/software/components/cic_proof_checking/freshNamesGenerator.ml index 1cb86b35a..daa0e5432 100755 --- a/helm/software/components/cic_proof_checking/freshNamesGenerator.ml +++ b/helm/software/components/cic_proof_checking/freshNamesGenerator.ml @@ -30,7 +30,7 @@ let debug_print = fun _ -> () let rec higher_name arity = function Cic.Sort Cic.Prop - | Cic.Sort Cic.CProp -> + | Cic.Sort (Cic.CProp _) -> if arity = 0 then "A" (* propositions *) else if arity = 1 then "P" (* predicates *) else "R" (*relations *) @@ -87,7 +87,7 @@ let mk_fresh_name ~subst metasenv context name ~typ = in (match ty with C.Sort C.Prop - | C.Sort C.CProp -> "H" + | C.Sort (C.CProp _) -> "H" | _ -> guess_a_name context typ ) with CicTypeChecker.TypeCheckerFailure _ -> "H" diff --git a/helm/software/components/cic_unification/cicRefine.ml b/helm/software/components/cic_unification/cicRefine.ml index a1a7bdea8..b5204de02 100644 --- a/helm/software/components/cic_unification/cicRefine.ml +++ b/helm/software/components/cic_unification/cicRefine.ml @@ -1065,8 +1065,7 @@ and type_of_aux' ?(clean_dummy_dependent_types=true) ?(localization_tbl = Cic.Ci let t1'' = CicReduction.whd ~subst context t1 in let t2'' = CicReduction.whd ~subst context_for_t2 t2 in match (t1'', t2'') with - (C.Sort s1, C.Sort s2) - when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) -> + | (C.Sort s1, C.Sort s2) when (s2 = C.Prop || s2 = C.Set) -> (* different than Coq manual!!! *) C.Sort s2,subst,metasenv,ugraph | (C.Sort (C.Type t1), C.Sort (C.Type t2)) -> @@ -1077,8 +1076,34 @@ and type_of_aux' ?(clean_dummy_dependent_types=true) ?(localization_tbl = Cic.Ci C.Sort (C.Type t'),subst,metasenv,ugraph2 with CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg)) + | (C.Sort (C.CProp t1), C.Sort (C.CProp t2)) -> + let t' = CicUniv.fresh() in + (try + let ugraph1 = CicUniv.add_ge t' t1 ugraph in + let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in + C.Sort (C.CProp t'),subst,metasenv,ugraph2 + with + CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg)) + | (C.Sort (C.Type t1), C.Sort (C.CProp t2)) -> + let t' = CicUniv.fresh() in + (try + let ugraph1 = CicUniv.add_ge t' t1 ugraph in + let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in + C.Sort (C.CProp t'),subst,metasenv,ugraph2 + with + CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg)) + | (C.Sort (C.CProp t1), C.Sort (C.Type t2)) -> + let t' = CicUniv.fresh() in + (try + let ugraph1 = CicUniv.add_gt t' t1 ugraph in + let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in + C.Sort (C.Type t'),subst,metasenv,ugraph2 + with + CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg)) | (C.Sort _,C.Sort (C.Type t1)) -> C.Sort (C.Type t1),subst,metasenv,ugraph + | (C.Sort _,C.Sort (C.CProp t1)) -> + C.Sort (C.CProp t1),subst,metasenv,ugraph | (C.Meta _, C.Sort _) -> t2'',subst,metasenv,ugraph | (C.Sort _,C.Meta _) | (C.Meta _,C.Meta _) -> (* TODO how can we force the meta to become a sort? If we don't we diff --git a/helm/software/components/content_pres/cicNotationParser.ml b/helm/software/components/content_pres/cicNotationParser.ml index 5aac1ef7d..bae4a8f59 100644 --- a/helm/software/components/content_pres/cicNotationParser.ml +++ b/helm/software/components/content_pres/cicNotationParser.ml @@ -427,7 +427,7 @@ EXTEND [ "Prop" -> `Prop | "Set" -> `Set | "Type" -> `Type (CicUniv.fresh ()) - | "CProp" -> `CProp + | "CProp" -> `CProp (CicUniv.fresh ()) ] ]; explicit_subst: [ diff --git a/helm/software/components/content_pres/termContentPres.ml b/helm/software/components/content_pres/termContentPres.ml index 0f51e36a9..1ee406623 100644 --- a/helm/software/components/content_pres/termContentPres.ml +++ b/helm/software/components/content_pres/termContentPres.ml @@ -100,7 +100,7 @@ let binder_symbol s = let string_of_sort_kind = function | `Prop -> "Prop" | `Set -> "Set" - | `CProp -> "CProp" + | `CProp _ -> "CProp" | `Type _ -> "Type" let pp_ast0 t k = diff --git a/helm/software/components/tactics/auto.ml b/helm/software/components/tactics/auto.ml index 37f0939bd..c3e2b6b48 100644 --- a/helm/software/components/tactics/auto.ml +++ b/helm/software/components/tactics/auto.ml @@ -30,6 +30,14 @@ let debug = false;; let debug_print s = if debug then prerr_endline (Lazy.force s);; +let is_propositional context sort = + match CicReduction.whd context sort with + | Cic.Sort Cic.Prop + | Cic.Sort (Cic.CProp _) -> true + | _-> false +;; + + type auto_params = Cic.term list * (string * string) list let elems = ref [] ;; @@ -133,11 +141,7 @@ let is_unit_equation context metasenv oldnewmeta term = CicTypeChecker.type_of_aux' metasenv context mt CicUniv.oblivion_ugraph in - let b, _ = - CicReduction.are_convertible ~metasenv context - sort (Cic.Sort Cic.Prop) u - in - if b then Some i else None + if is_propositional context sort then Some i else None | _ -> assert false) args in @@ -314,11 +318,7 @@ let fill_hypothesis context metasenv oldnewmeta term tables (universe:Universe.u CicTypeChecker.type_of_aux' metasenv context mt CicUniv.oblivion_ugraph in - let b, _ = - CicReduction.are_convertible ~metasenv context - sort (Cic.Sort Cic.Prop) u - in - if b then Some i else None + if is_propositional context sort then Some i else None | _ -> assert false) args in @@ -686,7 +686,7 @@ let ppterm ctx t = ;; let is_in_prop context subst metasenv ty = let sort,u = typeof ~subst metasenv context ty CicUniv.oblivion_ugraph in - fst (CicReduction.are_convertible context sort (Cic.Sort Cic.Prop) u) + is_propositional context sort ;; let assert_proof_is_valid proof metasenv context goalty = @@ -723,10 +723,7 @@ let split_goals_in_prop metasenv subst gl = let _,context,ty = CicUtil.lookup_meta g metasenv in try let sort,u = typeof ~subst metasenv context ty ugraph in - let b,_ = - CicReduction.are_convertible - ~subst ~metasenv context sort (Cic.Sort Cic.Prop) u in - b + is_propositional context sort with | CicTypeChecker.AssertFailure s | CicTypeChecker.TypeCheckerFailure s -> diff --git a/helm/software/components/tactics/eliminationTactics.ml b/helm/software/components/tactics/eliminationTactics.ml index 6e0c223d2..5a293bcaf 100644 --- a/helm/software/components/tactics/eliminationTactics.ml +++ b/helm/software/components/tactics/eliminationTactics.ml @@ -155,7 +155,7 @@ let warn s = debug_print (lazy ("DECOMPOSE: " ^ (Lazy.force s))) (* roba seria ------------------------------------------------------------- *) -let decompose_tac ?(sorts=[CicPp.ppsort C.Prop; CicPp.ppsort C.CProp]) +let decompose_tac ?(sorts=[CicPp.ppsort C.Prop; CicPp.ppsort (C.CProp (CicUniv.fresh ()))]) ?(mk_fresh_name_callback = F.mk_fresh_name ~subst:[]) () = let decompose_tac status = let (proof, goal) = status in diff --git a/helm/software/components/tactics/primitiveTactics.ml b/helm/software/components/tactics/primitiveTactics.ml index 53bfc39a9..3822b7eac 100644 --- a/helm/software/components/tactics/primitiveTactics.ml +++ b/helm/software/components/tactics/primitiveTactics.ml @@ -646,7 +646,7 @@ let elim_tac ?using ?(pattern = PET.conclusion_pattern None) term = match ty_ty with C.Sort C.Prop -> "_ind" | C.Sort C.Set -> "_rec" - | C.Sort C.CProp -> "_rec" + | C.Sort (C.CProp _) -> "_rect" | C.Sort (C.Type _)-> "_rect" | C.Meta (_,_) -> raise TheTypeOfTheCurrentGoalIsAMetaICannotChooseTheRightElimiantionPrinciple | _ -> assert false diff --git a/helm/software/matita/dist/ChangeLog b/helm/software/matita/dist/ChangeLog index e171b8386..a7a7e0ce1 100644 --- a/helm/software/matita/dist/ChangeLog +++ b/helm/software/matita/dist/ChangeLog @@ -1,6 +1,7 @@ 0.5.? - ?/?/? - ? * refinement of match fixed to prevent useless unfolding, head_beta_reduce is used instead of whd ~delta:true + * CProp hierarchy, interleaved with type (used to be a single universe) 0.5.1 - 29/5/2008 - minor bug fix release * visualization of inductive types reports the number of fixed parameters diff --git a/helm/software/matita/matitaScript.ml b/helm/software/matita/matitaScript.ml index a27b01831..9e0f85b58 100644 --- a/helm/software/matita/matitaScript.ml +++ b/helm/software/matita/matitaScript.ml @@ -247,7 +247,7 @@ let cic2grafite context menv t = | Cic.Meta _ -> PT.Implicit | Cic.Sort (Cic.Type u) -> PT.Sort (`Type u) | Cic.Sort Cic.Set -> PT.Sort `Set - | Cic.Sort Cic.CProp -> PT.Sort `CProp + | Cic.Sort (Cic.CProp u) -> PT.Sort (`CProp u) | Cic.Sort Cic.Prop -> PT.Sort `Prop | _ as t -> PT.Ident ("ERROR: "^CicPp.ppterm t, None) in -- 2.39.2