From 9c732a5c878bac2592cb397aca3d17cfefdcd023 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 10 Jul 2015 01:13:59 +0200
Subject: Option -type-in-type: added support in checker and making it
 contaminating in vo files (this was not done yet in 24d0027f0 and
 090fffa57b).

Reused field "engagement" to carry information about both
impredicativity of set and type in type.

For the record: maybe some further checks to do around the sort of the
inductive types in coqchk?
---
 kernel/declarations.mli |  5 ++++-
 kernel/environ.ml       | 17 ++++++++---------
 kernel/environ.mli      |  7 ++-----
 kernel/fast_typeops.ml  |  6 ++----
 kernel/indtypes.ml      |  2 +-
 kernel/pre_env.ml       |  6 ++----
 kernel/pre_env.mli      |  3 +--
 kernel/safe_typing.ml   | 26 +++++++++++++++-----------
 kernel/safe_typing.mli  |  5 +----
 kernel/typeops.ml       |  6 ++----
 10 files changed, 38 insertions(+), 45 deletions(-)

(limited to 'kernel')

diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index c1c19a757c..561c66b422 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -14,7 +14,10 @@ open Context
    declarations. This includes global constants/axioms, mutual
    inductive definitions, modules and module types *)
 
-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) } *)
 
diff --git a/kernel/environ.ml b/kernel/environ.ml
index a79abbb7e8..30b28177c9 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -46,11 +46,14 @@ let empty_env = empty_env
 
 let engagement env = env.env_stratification.env_engagement
 
-let type_in_type env = env.env_stratification.env_type_in_type
-
 let is_impredicative_set env = 
-  match engagement env with
-  | Some ImpredicativeSet -> true
+  match fst (engagement env) with
+  | ImpredicativeSet -> true
+  | _ -> false
+
+let type_in_type env =
+  match snd (engagement env) with
+  | TypeInType -> true
   | _ -> false
 
 let universes env = env.env_stratification.env_universes
@@ -191,11 +194,7 @@ let check_constraints c env =
 
 let set_engagement c env = (* Unsafe *)
   { env with env_stratification =
-    { env.env_stratification with env_engagement = Some c } }
-
-let set_type_in_type env =
-  { env with env_stratification =
-    { env.env_stratification with env_type_in_type = true } }
+    { env.env_stratification with env_engagement = c } }
 
 let push_constraints_to_env (_,univs) env =
   add_constraints univs env
diff --git a/kernel/environ.mli b/kernel/environ.mli
index ede356e699..4ad0327fc7 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -50,10 +50,9 @@ val opaque_tables : env -> Opaqueproof.opaquetab
 val set_opaque_tables : env -> Opaqueproof.opaquetab -> env
 
 
-val engagement    : env -> engagement option
+val engagement    : env -> engagement
 val is_impredicative_set : env -> bool
-
-val type_in_type  : env -> bool
+val type_in_type : env -> bool
 
 (** is the local context empty *)
 val empty_context : env -> bool
@@ -215,8 +214,6 @@ val push_constraints_to_env : 'a Univ.constrained -> env -> env
 
 val set_engagement : engagement -> env -> env
 
-val set_type_in_type : env -> env
-
 (** {6 Sets of referred section variables }
    [global_vars_set env c] returns the list of [id]'s occurring either
    directly as [Var id] in [c] or indirectly as a section variable
diff --git a/kernel/fast_typeops.ml b/kernel/fast_typeops.ml
index 86fb1b64c6..d22abff10c 100644
--- a/kernel/fast_typeops.ml
+++ b/kernel/fast_typeops.ml
@@ -182,14 +182,12 @@ let sort_of_product env domsort rangsort =
     | (Prop _,  Prop Pos) -> rangsort
     (* Product rule (Type,Set,?) *)
     | (Type u1, Prop Pos) ->
-        begin match engagement env with
-        | Some ImpredicativeSet ->
+        if is_impredicative_set env then
           (* Rule is (Type,Set,Set) in the Set-impredicative calculus *)
           rangsort
-        | _ ->
+        else
           (* Rule is (Type_i,Set,Type_i) in the Set-predicative calculus *)
           Type (Universe.sup Universe.type0 u1)
-        end
     (* Product rule (Prop,Type_i,Type_i) *)
     | (Prop Pos,  Type u2)  -> Type (Universe.sup Universe.type0 u2)
     (* Product rule (Prop,Type_i,Type_i) *)
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 31c0e83c84..9c79009dba 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -173,7 +173,7 @@ let cumulate_arity_large_levels env sign =
     sign (Universe.type0m,env))
 
 let is_impredicative env u =
-  is_type0m_univ u || (is_type0_univ u && engagement env = Some ImpredicativeSet)
+  is_type0m_univ u || (is_type0_univ u && is_impredicative_set env)
 
 (* Returns the list [x_1, ..., x_n] of levels contributing to template
    polymorphism. The elements x_k is None if the k-th parameter (starting
diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml
index 557ed3d7da..5f3f559a2c 100644
--- a/kernel/pre_env.ml
+++ b/kernel/pre_env.ml
@@ -46,8 +46,7 @@ type globals = {
 
 type stratification = {
   env_universes : universes;
-  env_engagement : engagement option;
-  env_type_in_type : bool
+  env_engagement : engagement
 }
 
 type val_kind =
@@ -95,8 +94,7 @@ let empty_env = {
   env_nb_rel = 0;
   env_stratification = {
     env_universes = initial_universes;
-    env_engagement = None;
-    env_type_in_type = false};
+    env_engagement = (PredicativeSet,StratifiedType) };
   env_conv_oracle = Conv_oracle.empty;
   retroknowledge = Retroknowledge.initial_retroknowledge;
   indirect_pterms = Opaqueproof.empty_opaquetab }
diff --git a/kernel/pre_env.mli b/kernel/pre_env.mli
index 03ac41b45e..0ce0bed235 100644
--- a/kernel/pre_env.mli
+++ b/kernel/pre_env.mli
@@ -33,8 +33,7 @@ type globals = {
 
 type stratification = {
   env_universes : universes;
-  env_engagement : engagement option;
-  env_type_in_type : bool
+  env_engagement : engagement
 }
 
 type lazy_val
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index d8473183ab..907ad2a1d4 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -184,16 +184,20 @@ let set_engagement c senv =
 
 (** Check that the engagement [c] expected by a library matches
     the current (initial) one *)
-let check_engagement env c =
-  match Environ.engagement env, c with
-  | None, Some ImpredicativeSet ->
-    Errors.error "Needs option -impredicative-set."
-  | _ -> ()
-
-let set_type_in_type senv = 
-  { senv with
-    env = Environ.set_type_in_type senv.env;
-    type_in_type = true }
+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
 
 (** {6 Stm machinery } *)
 
@@ -734,7 +738,7 @@ type compiled_library = {
   comp_name : DirPath.t;
   comp_mod : module_body;
   comp_deps : library_info array;
-  comp_enga : engagement option;
+  comp_enga : engagement;
   comp_natsymbs : Nativecode.symbols
 }
 
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 1e9cdbda0e..2b4324b96f 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -99,12 +99,9 @@ val add_constraints :
 (* (\** Generator of universes *\) *)
 (* val next_universe : int safe_transformer *)
 
-(** Setting the strongly constructive or classical logical engagement *)
+(** Setting the type theory flavor *)
 val set_engagement : Declarations.engagement -> safe_transformer0
 
-(** Collapsing the type hierarchy *)
-val set_type_in_type : safe_transformer0
-
 (** {6 Interactive module functions } *)
 
 val start_module : Label.t -> module_path safe_transformer
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 48dbacf1a4..fe82d85d5d 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -252,14 +252,12 @@ let sort_of_product env domsort rangsort =
     | (Prop _,  Prop Pos) -> rangsort
     (* Product rule (Type,Set,?) *)
     | (Type u1, Prop Pos) ->
-        begin match engagement env with
-        | Some ImpredicativeSet ->
+        if is_impredicative_set env then
           (* Rule is (Type,Set,Set) in the Set-impredicative calculus *)
           rangsort
-        | _ ->
+        else
           (* Rule is (Type_i,Set,Type_i) in the Set-predicative calculus *)
           Type (Universe.sup Universe.type0 u1)
-        end
     (* Product rule (Prop,Type_i,Type_i) *)
     | (Prop Pos,  Type u2)  -> Type (Universe.sup Universe.type0 u2)
     (* Product rule (Prop,Type_i,Type_i) *)
-- 
cgit v1.2.3