Set devient predicatif par defaut

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4726 85f007b7-540e-0410-9357-904b9bb8a0f7

6 files changed, 85 insertions, 27 deletions

diff --git a/kernel/environ.ml b/kernel/environ.ml
index 4e930a09ef..7b1eff341a 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -23,18 +23,25 @@ type compilation_unit_name = dir_path * checksum
 
 type global = Constant | Inductive
 
+type engagement = StronglyConstructive | StronglyClassical
+
 type globals = {
   env_constants : constant_body KNmap.t;
   env_inductives : mutual_inductive_body KNmap.t;
   env_modules : module_body MPmap.t;
   env_modtypes : module_type_body KNmap.t }
 
+type stratification = {
+  env_universes : universes;
+  env_engagement : engagement option
+}
+
 type env = {
-  env_globals       : globals;
-  env_named_context : named_context;
-  env_rel_context   : rel_context;
-  env_universes     : universes }
-  
+  env_globals        : globals;
+  env_named_context  : named_context;
+  env_rel_context    : rel_context;
+  env_stratification : stratification }
+
 let empty_env = { 
   env_globals = {
     env_constants = KNmap.empty;
@@ -43,9 +50,12 @@ let empty_env = {
     env_modtypes = KNmap.empty };
   env_named_context = empty_named_context;
   env_rel_context = empty_rel_context;
-  env_universes = initial_universes }
+  env_stratification = {
+    env_universes = initial_universes;
+    env_engagement = None } }
 
-let universes env = env.env_universes
+let engagement env = env.env_stratification.env_engagement
+let universes env = env.env_stratification.env_universes
 let named_context env = env.env_named_context
 let rel_context env = env.env_rel_context
 
@@ -170,13 +180,22 @@ let add_mind kn mib env =
 
 (* Universe constraints *)
 let set_universes g env =
-  if env.env_universes == g then env else { env with env_universes = g }
+  if env.env_stratification.env_universes == g then env
+  else
+    { env with env_stratification = 
+      { env.env_stratification with env_universes = g } }
 
 let add_constraints c env =
   if c == Constraint.empty then 
     env 
-  else 
-    { env with env_universes = merge_constraints c env.env_universes }
+  else
+    let s = env.env_stratification in
+    { env with env_stratification = 
+      { s with env_universes = merge_constraints c s.env_universes } }
+
+let set_engagement c env = (* Unsafe *)
+  { env with env_stratification =
+    { env.env_stratification with env_engagement = Some c } }
 
 (* Lookup of section variables *)
 let lookup_constant_variables c env =
diff --git a/kernel/environ.mli b/kernel/environ.mli
index baf1a71e14..4a18224a0e 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -25,7 +25,8 @@ open Sign
    - a context for section variables and goal assumptions
    - a context for global constants and axioms
    - a context for inductive definitions
-   - a set of universe constraints *)
+   - a set of universe constraints
+   - a flag telling if Set is, can be, or cannot be set impredicative *)
 
 type env
 
@@ -35,6 +36,10 @@ val universes     : env -> Univ.universes
 val rel_context   : env -> rel_context
 val named_context : env -> named_context
 
+type engagement = StronglyConstructive | StronglyClassical
+
+val engagement    : env -> engagement option
+
 (* is the local context empty *)
 val empty_context : env -> bool
 
@@ -118,6 +123,8 @@ val lookup_modtype : kernel_name -> env -> module_type_body
 val set_universes   :   Univ.universes -> env -> env
 val add_constraints : Univ.constraints -> env -> env
 
+val set_engagement : engagement -> env -> env
+
 (***********************************************************************)
 (* Sets of referred section variables *)
 (* [global_vars_set env c] returns the list of [id]'s occurring as
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 5a18643164..d009a668f8 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -148,9 +148,11 @@ let small_unit constrsinfos =
 
 (* [smax] is the max of the sorts of the products of the constructor type *)
 
-let enforce_type_constructor arsort smax cst =
+let enforce_type_constructor env arsort smax cst =
   match smax, arsort with
     | Type uc, Type ua -> enforce_geq ua uc cst
+    | Type uc, Prop Pos when engagement env <> Some StronglyConstructive ->
+        error "Large inductive types in Set need option -strongly-constructive"
     | _,_ -> cst
 
 let type_one_constructor env_ar_par params arsort c =
@@ -163,7 +165,7 @@ let type_one_constructor env_ar_par params arsort c =
   (* If the arity is at some level Type arsort, then the sort of the
      constructor must be below arsort; here we consider constructors with the
      global parameters (which add a priori more constraints on their sort) *)
-  let cst2 = enforce_type_constructor arsort j.utj_type cst in
+  let cst2 = enforce_type_constructor env_ar_par arsort j.utj_type cst in
 
   (infos, full_cstr_type, cst2)
 
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index fb54c16c8f..5dc9883285 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -406,12 +406,35 @@ let current_msid senv = senv.modinfo.msid
 let add_constraints cst senv = 
   {senv with env = Environ.add_constraints cst senv.env}
 
+(* Check that the engagement expected by a library matches the initial one *)
+let check_engagement env c =
+  match Environ.engagement env, c with
+    | Some StronglyClassical, Some StronglyClassical -> ()
+    | Some StronglyConstructive, Some StronglyConstructive -> ()
+    | _, None -> ()
+    | _, Some StronglyClassical ->
+        error "Needs option -strongly-classical"
+    | _, Some StronglyConstructive ->
+        error "Needs option -strongly-classical"
+
+(* Check the initial engagement (possibly after a state input) *)
+let check_initial_engagement env c =
+  match Environ.engagement env, c with
+    | Some StronglyConstructive, StronglyClassical ->
+        error "Already engaged for a strongly constructive logic"
+    | Some StronglyClassical, StronglyConstructive ->
+        error "Already engaged for a strongly classical logic"
+    | _ -> ()
+
+let set_engagement c senv =
+  check_initial_engagement senv.env c;
+  {senv with env = Environ.set_engagement c senv.env}
 
 
 (* Libraries = Compiled modules *)
 
 type compiled_library = 
-    dir_path * module_body * library_info list
+    dir_path * module_body * library_info list * engagement option
 
 
 (* We check that only initial state Require's were performed before 
@@ -466,7 +489,7 @@ let export senv dir =
       mod_equiv = None;
       mod_constraints = Constraint.empty }
   in
-    modinfo.msid, (dir,mb,senv.imports)
+    modinfo.msid, (dir,mb,senv.imports,engagement senv.env)
 
 
 let check_imports senv needed =
@@ -494,8 +517,9 @@ loaded by side-effect once and for all (like it is done in OCaml).
 Would this be correct with respect to undo's and stuff ?
 *)
  
-let import (dp,mb,depends) digest senv = 
+let import (dp,mb,depends,engmt) digest senv = 
   check_imports senv depends;
+  check_engagement senv.env engmt;
   let mp = MPfile dp in
   let env = senv.env in
   mp, { senv with 
@@ -548,7 +572,7 @@ and lighten_modexpr = function
   | MEBapply (mexpr,marg,u) ->
       MEBapply (lighten_modexpr mexpr,lighten_modexpr marg,u)
 
-let lighten_library (dp,mb,depends) = (dp,lighten_module mb,depends)
+let lighten_library (dp,mb,depends,s) = (dp,lighten_module mb,depends,s)
 
 
 type judgment = unsafe_judgment
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index a5d8dc4d10..86e423dd83 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -65,6 +65,9 @@ val add_modtype :
 val add_constraints : 
   Univ.constraints -> safe_environment -> safe_environment
 
+(* Settin the strongly constructive or classical logical engagement *)
+val set_engagement : Environ.engagement -> safe_environment -> safe_environment
+
 
 (*s Interactive module functions *)
 val start_module : 
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 7b72de6092..96e3cabd42 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -188,19 +188,22 @@ let judge_of_apply env funj argjv =
     Constraint.empty
     (Array.to_list argjv)
 
-(*
-let applykey = Profile.declare_profile "judge_of_apply";;
-let judge_of_apply env nocheck funj argjl
-  = Profile.profile5 applykey judge_of_apply env nocheck funj argjl;;
-*)
-
-
 (* Type of product *)
 
-let sort_of_product domsort rangsort =
+let sort_of_product env domsort rangsort =
   match (domsort, rangsort) with
     (* Product rule (s,Prop,Prop) *) 
-    | (_,       Prop _)  -> rangsort
+    | (_,       Prop Null)  -> rangsort
+    (* Product rule (Prop/Set,Set,Set) *)
+    | (Prop _,  Prop Pos) -> rangsort
+    (* Product rule (Type,Set,?) *)
+    | (Type u1, Prop Pos) ->
+        if engagement env = Some StronglyConstructive 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 *)
+          domsort
     (* Product rule (Prop,Type_i,Type_i) *)
     | (Prop _,  Type _)  -> rangsort
     (* Product rule (Type_i,Type_i,Type_i) *) 
@@ -215,7 +218,7 @@ let sort_of_product domsort rangsort =
   where j.uj_type is convertible to a sort s2
 *)
 let judge_of_product env name t1 t2 =
-  let s = sort_of_product t1.utj_type t2.utj_type in
+  let s = sort_of_product env t1.utj_type t2.utj_type in
   { uj_val = mkProd (name, t1.utj_val, t2.utj_val);
     uj_type = mkSort s }