From 0b15dfdee3357a626c77d30599e87a83ab34e471 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 15 Jul 2008 12:00:24 +0000 Subject: [PATCH] CProp_i <= Type_i , Type_i <= CProp_i --- .../cic_proof_checking/cicReduction.ml | 26 ++++++------------- .../cic_proof_checking/cicTypeChecker.ml | 25 +++--------------- .../components/cic_unification/cicRefine.ml | 2 +- helm/software/components/ng_kernel/check.ml | 9 ++++--- 4 files changed, 19 insertions(+), 43 deletions(-) diff --git a/helm/software/components/cic_proof_checking/cicReduction.ml b/helm/software/components/cic_proof_checking/cicReduction.ml index 1499712c9..ff19dff19 100644 --- a/helm/software/components/cic_proof_checking/cicReduction.ml +++ b/helm/software/components/cic_proof_checking/cicReduction.ml @@ -869,24 +869,14 @@ prerr_endline ("%%%%%%: " ^ CicPp.ppterm term' ^ " <==> " ^ CicPp.ppterm t1); *) aux test_equality_only context t1 term' ugraph with CicUtil.Subst_not_found _ -> false,ugraph) - | (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) - | (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) - | (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 (C.CProp t1|C.Type t1), C.Sort (C.CProp t2|C.Type t2)) + when test_equality_only -> + (try true,(CicUniv.add_eq t2 t1 ugraph) + with CicUniv.UniverseInconsistency _ -> false,ugraph) + | (C.Sort (C.CProp t1|C.Type t1), C.Sort (C.CProp t2|C.Type 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 diff --git a/helm/software/components/cic_proof_checking/cicTypeChecker.ml b/helm/software/components/cic_proof_checking/cicTypeChecker.ml index cf3a3c49c..289ef4b76 100644 --- a/helm/software/components/cic_proof_checking/cicTypeChecker.ml +++ b/helm/software/components/cic_proof_checking/cicTypeChecker.ml @@ -574,10 +574,9 @@ and typecheck_mutual_inductive_defs ~logger uri (itl,_,indparamsno) ugraph = with 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.Type u1), Cic.Sort (Cic.CProp u2) | Cic.Sort (Cic.CProp u1), Cic.Sort (Cic.Type u2) -> - CicUniv.add_gt u2 u1 ugraph + CicUniv.add_ge u2 u1 ugraph | Cic.Sort _, Cic.Sort Cic.Prop | Cic.Sort _, Cic.Sort Cic.CProp _ | Cic.Sort _, Cic.Sort Cic.Set @@ -1846,7 +1845,7 @@ end; | (C.Sort s1, C.Sort (C.Prop | C.Set)) -> (* different from Coq manual!!! *) t2',ugraph - | (C.Sort (C.Type t1), C.Sort (C.Type t2)) -> + | (C.Sort (C.Type t1 | C.CProp t1), C.Sort (C.Type t2)) -> let t' = CicUniv.fresh() in (try let ugraph1 = CicUniv.add_ge t' t1 ugraph in @@ -1854,7 +1853,7 @@ end; C.Sort (C.Type t'),ugraph2 with CicUniv.UniverseInconsistency msg -> raise (TypeCheckerFailure msg)) - | (C.Sort (C.CProp t1), C.Sort (C.CProp t2)) -> + | (C.Sort (C.CProp t1 | C.Type t1), C.Sort (C.CProp t2)) -> let t' = CicUniv.fresh() in (try let ugraph1 = CicUniv.add_ge t' t1 ugraph in @@ -1862,22 +1861,6 @@ end; 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 diff --git a/helm/software/components/cic_unification/cicRefine.ml b/helm/software/components/cic_unification/cicRefine.ml index bde5d63e4..956372d60 100644 --- a/helm/software/components/cic_unification/cicRefine.ml +++ b/helm/software/components/cic_unification/cicRefine.ml @@ -1104,7 +1104,7 @@ and type_of_aux' ?(clean_dummy_dependent_types=true) ?(localization_tbl = Cic.Ci | (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 ugraph1 = CicUniv.add_ge t' t1 ugraph in let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in C.Sort (C.Type t'),subst,metasenv,ugraph2 with diff --git a/helm/software/components/ng_kernel/check.ml b/helm/software/components/ng_kernel/check.ml index d6165d9db..a51d97722 100644 --- a/helm/software/components/ng_kernel/check.ml +++ b/helm/software/components/ng_kernel/check.ml @@ -149,11 +149,14 @@ let _ = | a::(b::_ as tl) -> NCicEnvironment.add_constraint true (mk_type a) (mk_type b); NCicEnvironment.add_constraint true (mk_cprop a) (mk_cprop b); - NCicEnvironment.add_constraint true (mk_type a) (mk_cprop a); NCicEnvironment.add_constraint true (mk_cprop a) (mk_type b); + NCicEnvironment.add_constraint true (mk_type a) (mk_cprop b); + NCicEnvironment.add_constraint false (mk_cprop a) (mk_type a); + NCicEnvironment.add_constraint false (mk_type a) (mk_cprop a); aux tl | [a] -> - NCicEnvironment.add_constraint true (mk_type a) (mk_cprop a); + NCicEnvironment.add_constraint false (mk_type a) (mk_cprop a); + NCicEnvironment.add_constraint false (mk_cprop a) (mk_type a); | _ -> () in aux lll @@ -167,7 +170,7 @@ let _ = let uu= OCic2NCic.nuri_of_ouri uu in indent := 0; let o = NCicLibrary.get_obj uu in -(* prerr_endline (NCicPp.ppobj o); *) + prerr_endline (NCicPp.ppobj o); try NCicTypeChecker.typecheck_obj o with -- 2.39.2