aboutsummaryrefslogtreecommitdiff
path: root/checker
diff options
context:
space:
mode:
Diffstat (limited to 'checker')
-rw-r--r--checker/check_stat.ml18
-rw-r--r--checker/checker.ml14
-rw-r--r--checker/cic.mli7
-rw-r--r--checker/environ.ml25
-rw-r--r--checker/environ.mli4
-rw-r--r--checker/indtypes.ml4
-rw-r--r--checker/reduction.ml7
-rw-r--r--checker/safe_typing.ml22
-rw-r--r--checker/typeops.ml2
-rw-r--r--checker/values.ml6
10 files changed, 71 insertions, 38 deletions
diff --git a/checker/check_stat.ml b/checker/check_stat.ml
index 05a2a1b992..d041f1b7e1 100644
--- a/checker/check_stat.ml
+++ b/checker/check_stat.ml
@@ -23,11 +23,17 @@ let print_memory_stat () =
let output_context = ref false
-let pr_engt = function
- Some ImpredicativeSet ->
- str "Theory: Set is impredicative"
- | None ->
- str "Theory: Set is predicative"
+let pr_engagement (impr_set,type_in_type) =
+ begin
+ match impr_set with
+ | ImpredicativeSet -> str "Theory: Set is impredicative"
+ | PredicativeSet -> str "Theory: Set is predicative"
+ end ++
+ begin
+ match type_in_type with
+ | StratifiedType -> str "Theory: Stratified type hierarchy"
+ | TypeInType -> str "Theory: Type is of type Type"
+ end
let cst_filter f csts =
Cmap_env.fold
@@ -54,7 +60,7 @@ let print_context env =
ppnl(hov 0
(fnl() ++ str"CONTEXT SUMMARY" ++ fnl() ++
str"===============" ++ fnl() ++ fnl() ++
- str "* " ++ hov 0 (pr_engt engt ++ fnl()) ++ fnl() ++
+ str "* " ++ hov 0 (pr_engagement engt ++ fnl()) ++ fnl() ++
str "* " ++ hov 0 (pr_ax csts) ++
fnl())); pp_flush()
end
diff --git a/checker/checker.ml b/checker/checker.ml
index 0f7ed8df51..d5d9b9e3b8 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -138,10 +138,11 @@ let init_load_path () =
let set_debug () = Flags.debug := true
-let engagement = ref None
-let set_engagement c = engagement := Some c
-let engage () =
- match !engagement with Some c -> Safe_typing.set_engagement c | None -> ()
+let impredicative_set = ref Cic.PredicativeSet
+let set_impredicative_set () = impredicative_set := Cic.ImpredicativeSet
+let type_in_type = ref Cic.StratifiedType
+let set_type_in_type () = type_in_type := Cic.TypeInType
+let engage () = Safe_typing.set_engagement (!impredicative_set,!type_in_type)
let admit_list = ref ([] : section_path list)
@@ -194,6 +195,7 @@ let print_usage_channel co command =
\n -silent disable trace of constants being checked\
\n\
\n -impredicative-set set sort Set impredicative\
+\n -type-in-type collapse type hierarchy\
\n\
\n -h, --help print this list of options\
\n"
@@ -319,7 +321,9 @@ let parse_args argv =
let rec parse = function
| [] -> ()
| "-impredicative-set" :: rem ->
- set_engagement Cic.ImpredicativeSet; parse rem
+ set_impredicative_set (); parse rem
+ | "-type-in-type" :: rem ->
+ set_type_in_type (); parse rem
| "-coqlib" :: s :: rem ->
if not (exists_dir s) then
diff --git a/checker/cic.mli b/checker/cic.mli
index d75af76547..881d3ca797 100644
--- a/checker/cic.mli
+++ b/checker/cic.mli
@@ -165,7 +165,10 @@ type action
(** Engagements *)
-type engagement = ImpredicativeSet
+type set_predicativity = ImpredicativeSet | PredicativeSet
+type type_hierarchy = TypeInType | StratifiedType
+
+type engagement = set_predicativity * type_hierarchy
(** {6 Representation of constants (Definition/Axiom) } *)
@@ -407,7 +410,7 @@ type compiled_library = {
comp_name : compilation_unit_name;
comp_mod : module_body;
comp_deps : library_deps;
- comp_enga : engagement option;
+ comp_enga : engagement;
comp_natsymbs : nativecode_symb_array
}
diff --git a/checker/environ.ml b/checker/environ.ml
index c0f366000a..6dbc44d6b8 100644
--- a/checker/environ.ml
+++ b/checker/environ.ml
@@ -14,7 +14,7 @@ type globals = {
type stratification = {
env_universes : Univ.universes;
- env_engagement : engagement option
+ env_engagement : engagement
}
type env = {
@@ -33,19 +33,28 @@ let empty_env = {
env_rel_context = [];
env_stratification =
{ env_universes = Univ.initial_universes;
- env_engagement = None};
+ env_engagement = (PredicativeSet,StratifiedType)};
env_imports = MPmap.empty }
let engagement env = env.env_stratification.env_engagement
let universes env = env.env_stratification.env_universes
let rel_context env = env.env_rel_context
-let set_engagement c env =
- match env.env_stratification.env_engagement with
- | Some c' -> if c=c' then env else error "Incompatible engagement"
- | None ->
- { env with env_stratification =
- { env.env_stratification with env_engagement = Some c } }
+let set_engagement (impr_set,type_in_type as c) env =
+ let expected_impr_set,expected_type_in_type =
+ env.env_stratification.env_engagement in
+ begin
+ match impr_set,expected_impr_set with
+ | PredicativeSet, ImpredicativeSet -> error "Incompatible engagement"
+ | _ -> ()
+ end;
+ begin
+ match type_in_type,expected_type_in_type with
+ | StratifiedType, TypeInType -> error "Incompatible engagement"
+ | _ -> ()
+ end;
+ { env with env_stratification =
+ { env.env_stratification with env_engagement = c } }
(* Digests *)
diff --git a/checker/environ.mli b/checker/environ.mli
index 22fe7d8f17..f3b2dd839a 100644
--- a/checker/environ.mli
+++ b/checker/environ.mli
@@ -11,7 +11,7 @@ type globals = {
env_modtypes : module_type_body MPmap.t}
type stratification = {
env_universes : Univ.universes;
- env_engagement : engagement option;
+ env_engagement : engagement;
}
type env = {
env_globals : globals;
@@ -22,7 +22,7 @@ type env = {
val empty_env : env
(* Engagement *)
-val engagement : env -> Cic.engagement option
+val engagement : env -> Cic.engagement
val set_engagement : Cic.engagement -> env -> env
(* Digests *)
diff --git a/checker/indtypes.ml b/checker/indtypes.ml
index 050c33e603..e1a6bc7c1d 100644
--- a/checker/indtypes.ml
+++ b/checker/indtypes.ml
@@ -176,7 +176,7 @@ let typecheck_arity env params inds =
(* Allowed eliminations *)
let check_predicativity env s small level =
- match s, engagement env with
+ match s, fst (engagement env) with
Type u, _ ->
(* let u' = fresh_local_univ () in *)
(* let cst = *)
@@ -184,7 +184,7 @@ let check_predicativity env s small level =
(* (universes env) in *)
if not (Univ.check_leq (universes env) level u) then
failwith "impredicative Type inductive type"
- | Prop Pos, Some ImpredicativeSet -> ()
+ | Prop Pos, ImpredicativeSet -> ()
| Prop Pos, _ ->
if not small then failwith "impredicative Set inductive type"
| Prop Null,_ -> ()
diff --git a/checker/reduction.ml b/checker/reduction.ml
index 58f0f894ff..8ddeea2a20 100644
--- a/checker/reduction.ml
+++ b/checker/reduction.ml
@@ -158,7 +158,7 @@ type conv_pb =
| CONV
| CUMUL
-let sort_cmp univ pb s0 s1 =
+let sort_cmp env univ pb s0 s1 =
match (s0,s1) with
| (Prop c1, Prop c2) when pb = CUMUL -> if c1 = Pos && c2 = Null then raise NotConvertible
| (Prop c1, Prop c2) -> if c1 <> c2 then raise NotConvertible
@@ -167,7 +167,8 @@ let sort_cmp univ pb s0 s1 =
CUMUL -> ()
| _ -> raise NotConvertible)
| (Type u1, Type u2) ->
- if not
+ if snd (engagement env) == StratifiedType
+ && not
(match pb with
| CONV -> Univ.check_eq univ u1 u2
| CUMUL -> Univ.check_leq univ u1 u2)
@@ -261,7 +262,7 @@ and eqappr univ cv_pb infos (lft1,st1) (lft2,st2) =
(match a1, a2 with
| (Sort s1, Sort s2) ->
assert (is_empty_stack v1 && is_empty_stack v2);
- sort_cmp univ cv_pb s1 s2
+ sort_cmp (infos_env infos) univ cv_pb s1 s2
| (Meta n, Meta m) ->
if n=m
then convert_stacks univ infos lft1 lft2 v1 v2
diff --git a/checker/safe_typing.ml b/checker/safe_typing.ml
index 810d6e0b65..dd94823135 100644
--- a/checker/safe_typing.ml
+++ b/checker/safe_typing.ml
@@ -32,13 +32,21 @@ let full_add_module dp mb univs digest =
let env = Modops.add_module mb env in
genv := add_digest env dp digest
-(* Check that the engagement expected by a library matches the initial one *)
-let check_engagement env c =
- match engagement env, c with
- | Some ImpredicativeSet, Some ImpredicativeSet -> ()
- | _, None -> ()
- | _, Some ImpredicativeSet ->
- error "Needs option -impredicative-set"
+(* Check that the engagement expected by a library extends the initial one *)
+let check_engagement env (expected_impredicative_set,expected_type_in_type) =
+ let impredicative_set,type_in_type = Environ.engagement env in
+ begin
+ match impredicative_set, expected_impredicative_set with
+ | PredicativeSet, ImpredicativeSet ->
+ Errors.error "Needs option -impredicative-set."
+ | _ -> ()
+ end;
+ begin
+ match type_in_type, expected_type_in_type with
+ | StratifiedType, TypeInType ->
+ Errors.error "Needs option -type-in-type."
+ | _ -> ()
+ end
(* Libraries = Compiled modules *)
diff --git a/checker/typeops.ml b/checker/typeops.ml
index 9bc4b269b8..21819992a9 100644
--- a/checker/typeops.ml
+++ b/checker/typeops.ml
@@ -128,7 +128,7 @@ let sort_of_product env domsort rangsort =
| (Prop _, Prop Pos) -> rangsort
(* Product rule (Type,Set,?) *)
| (Type u1, Prop Pos) ->
- if engagement env = Some ImpredicativeSet then
+ if fst (engagement env) = ImpredicativeSet then
(* Rule is (Type,Set,Set) in the Set-impredicative calculus *)
rangsort
else
diff --git a/checker/values.ml b/checker/values.ml
index 46b66adc4a..e82ba10327 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -193,7 +193,9 @@ let v_lazy_constr =
(** kernel/declarations *)
-let v_engagement = v_enum "eng" 1
+let v_impredicative_set = v_enum "impr-set" 2
+let v_type_in_type = v_enum "type-in-type" 2
+let v_engagement = v_tuple "eng" [|v_impredicative_set; v_type_in_type|]
let v_pol_arity =
v_tuple "polymorphic_arity" [|List(Opt v_level);v_univ|]
@@ -315,7 +317,7 @@ and v_modtype =
let v_vodigest = Sum ("module_impl",0, [| [|String|]; [|String;String|] |])
let v_deps = Array (v_tuple "dep" [|v_dp;v_vodigest|])
let v_compiled_lib =
- v_tuple "compiled" [|v_dp;v_module;v_deps;Opt v_engagement;Any|]
+ v_tuple "compiled" [|v_dp;v_module;v_deps;v_engagement;Any|]
(** Library objects *)
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-27 06:42:59 +0000