Merge branch 'beforepoly' of /Users/mat/research/coq/git into trunk

kernel/indtypes.ml

@@ -130,21 +130,6 @@ let infos_and_sort env ctx t =
     | _ -> (* don't fail if not positive, it is tested later *) max
   in aux env ctx t type0m_univ
 
-let is_small_univ u =
-  (* Compatibility with homotopy model where we interpret only Prop
-     to have proof-irrelevant equality. *)
-  is_type0m_univ u
-
-(* let small_unit constrsinfos arsign_lev = *)
-(*   let issmall = List.for_all is_small constrsinfos in *)
-(*   let issmall' = *)
-(*     if constrsinfos <> [] && !indices_matter then *)
-(*       issmall && is_small_univ arsign_lev *)
-(*     else *)
-(*       issmall in *)
-(*   let isunit = is_unit constrsinfos in *)
-(*   issmall', isunit *)
-
 (* Computing the levels of polymorphic inductive types
 
    For each inductive type of a block that is of level u_i, we have
@@ -200,7 +185,7 @@ let cumulate_arity_large_levels env sign =
     (fun (_,_,t as d) (lev,env) ->
       let tj, _ = infer_type env t in
       let u = univ_of_sort tj.utj_type in
-	((if is_small_univ u then lev else sup u lev), push_rel d env))
+	(sup u lev, push_rel d env))
     sign (type0m_univ,env))
 
 let is_impredicative env u =

kernel/inductive.ml

@@ -137,61 +137,6 @@ let cons_subst u su subst =
   try (u, sup su (List.assoc u subst)) :: List.remove_assoc u subst
   with Not_found -> (u, su) :: subst
 
-(* let actualize_decl_level env lev t = *)
-(*   let sign,s = dest_arity env t in *)
-(*   mkArity (sign,lev) *)
-
-(* let polymorphism_on_non_applied_parameters = false *)
-
-(* (\* Bind expected levels of parameters to actual levels *\) *)
-(* (\* Propagate the new levels in the signature *\) *)
-(* let rec make_subst env = function *)
-(*   | (_,Some _,_ as t)::sign, exp, args -> *)
-(*       let ctx,subst = make_subst env (sign, exp, args) in *)
-(*       t::ctx, subst *)
-(*   | d::sign, None::exp, args -> *)
-(*       let args = match args with _::args -> args | [] -> [] in *)
-(*       let ctx,subst = make_subst env (sign, exp, args) in *)
-(*       d::ctx, subst *)
-(*   | d::sign, Some u::exp, a::args -> *)
-(*       (\* We recover the level of the argument, but we don't change the *\) *)
-(*       (\* level in the corresponding type in the arity; this level in the *\) *)
-(*       (\* arity is a global level which, at typing time, will be enforce *\) *)
-(*       (\* to be greater than the level of the argument; this is probably *\) *)
-(*       (\* a useless extra constraint *\) *)
-(*       let s = sort_as_univ (snd (dest_arity env a)) in *)
-(*       let ctx,subst = make_subst env (sign, exp, args) in *)
-(*       d::ctx, cons_subst u s subst *)
-(*   | (na,None,t as d)::sign, Some u::exp, [] -> *)
-(*       (\* No more argument here: we instantiate the type with a fresh level *\) *)
-(*       (\* which is first propagated to the corresponding premise in the arity *\) *)
-(*       (\* (actualize_decl_level), then to the conclusion of the arity (via *\) *)
-(*       (\* the substitution) *\) *)
-(*       let ctx,subst = make_subst env (sign, exp, []) in *)
-(*       if polymorphism_on_non_applied_parameters then *)
-(* 	let s = fresh_local_univ () in *)
-(* 	let t = actualize_decl_level env (Type s) t in *)
-(* 	(na,None,t)::ctx, cons_subst u s subst *)
-(*       else *)
-(* 	d::ctx, subst *)
-(*   | sign, [], _ -> *)
-(*       (\* Uniform parameters are exhausted *\) *)
-(*       sign,[] *)
-(*   | [], _, _ -> *)
-(*       assert false *)
-
-(* let instantiate_universes env ctx ar argsorts = *)
-(*   let args = Array.to_list argsorts in *)
-(*   let ctx,subst = make_subst env (ctx,ar.poly_param_levels,args) in *)
-(*   let level = subst_large_constraints subst ar.poly_level in *)
-(*   ctx, *)
-(*   (\* Singleton type not containing types are interpretable in Prop *\) *)
-(*   if is_type0m_univ level then prop_sort *)
-(*   (\* Non singleton type not containing types are interpretable in Set *\) *)
-(*   else if is_type0_univ level then set_sort *)
-(*   (\* This is a Type with constraints *\) *)
-(*  else Type level *)
-
 exception SingletonInductiveBecomesProp of identifier
 
 (* Type of an inductive type *)

kernel/term.ml

@@ -77,8 +77,12 @@ let sorts_ord s1 s2 =
   | Type _, Prop _ -> 1
 
 let is_prop_sort = function
-| Prop Null -> true
-| _ -> false
+  | Prop Null -> true
+  | _ -> false
+
+let is_set_sort = function
+  | Prop Pos -> true
+  | _ -> false
 
 type sorts_family = InProp | InSet | InType
 
@@ -333,7 +337,7 @@ let rec is_Type c = match kind_of_term c with
 
 let is_small = function
   | Prop _ -> true
-  | _ -> false
+  | Type u -> is_small_univ u
 
 let iskind c = isprop c or is_Type c
 

kernel/term.mli

@@ -31,6 +31,7 @@ val type1_sort  : sorts
 
 val sorts_ord : sorts -> sorts -> int
 val is_prop_sort : sorts -> bool
+val is_set_sort : sorts -> bool
 val univ_of_sort : sorts -> Univ.universe
 val sort_of_univ : Univ.universe -> sorts
 

kernel/univ.ml

@@ -36,6 +36,12 @@ module Level = struct
     | Set
     | Level of int * Names.dir_path
 
+  let set = Set
+  let prop = Prop
+  let is_small = function
+    | Level _ -> false
+    | _ -> true
+
   (* A specialized comparison function: we compare the [int] part first.
      This way, most of the time, the [dir_path] part is not considered.
 
@@ -74,6 +80,10 @@ module Level = struct
     | Level (n,d) -> Names.string_of_dirpath d^"."^string_of_int n
 
   let pr u = str (to_string u)
+
+  let is_small = function
+    | Prop | Set -> true
+    | _ -> false
 end
 
 let pr_universe_list l = 
@@ -214,10 +224,16 @@ struct
       let gtl' = CList.uniquize gtl in
 	if gel' == gel && gtl' == gtl then x
 	else normalize (Max (gel', gtl'))
+
+  let is_small u = 
+    match normalize u with
+    | Atom l -> Level.is_small l
+    | _ -> false
 
 end
 
 let pr_uni = Universe.pr
+let is_small_univ = Universe.is_small
 
 open Universe
 

kernel/univ.mli

@@ -14,6 +14,10 @@ sig
   (** Type of universe levels. A universe level is essentially a unique name
       that will be associated to constraints later on. *)
 
+  val set : t
+  val prop : t
+  val is_small : t -> bool
+
   val compare : t -> t -> int
   (** Comparison function *)
 
@@ -114,6 +118,7 @@ val type1_univ : universe  (** the universe of the type of Prop/Set *)
 val is_type0_univ : universe -> bool
 val is_type0m_univ : universe -> bool
 val is_univ_variable : universe -> bool
+val is_small_univ : universe -> bool
 
 val universe_level : universe -> universe_level option
 val compare_levels : universe_level -> universe_level -> int

library/universes.ml

@@ -93,6 +93,14 @@ let fresh_global_or_constr_instance env = function
   | IsConstr c -> c, Univ.empty_universe_context_set
   | IsGlobal gr -> fresh_global_instance env gr
 
+let global_of_constr c =
+  match kind_of_term c with
+  | Const (c, u) -> ConstRef c, u
+  | Ind (i, u) -> IndRef i, u
+  | Construct (c, u) -> ConstructRef c, u
+  | Var id -> VarRef id, []
+  | _ -> raise Not_found
+
 open Declarations
 
 let type_of_reference env r =

library/universes.mli

@@ -48,6 +48,9 @@ val fresh_global_instance : env -> Globnames.global_reference ->
 val fresh_global_or_constr_instance : env -> Globnames.global_reference_or_constr -> 
   constr in_universe_context_set
 
+(** Raises [Not_found] if not a global reference. *)
+val global_of_constr : constr -> Globnames.global_reference puniverses
+
 val extend_context : 'a in_universe_context_set -> universe_context_set -> 
   'a in_universe_context_set
 

plugins/micromega/EnvRing.v

@@ -30,15 +30,15 @@ Section MakeRingPol.
  Variable ARth : almost_ring_theory rO rI radd rmul rsub ropp req.
 
  (* Coefficients *)
- Variable C: Set.
+ Variable C: Type.
  Variable (cO cI: C) (cadd cmul csub : C->C->C) (copp : C->C).
  Variable ceqb : C->C->bool.
  Variable phi : C -> R.
  Variable CRmorph : ring_morph rO rI radd rmul rsub ropp req
                                 cO cI cadd cmul csub copp ceqb phi.
 
  (* Power coefficients *)
- Variable Cpow : Set.
+ Variable Cpow : Type.
  Variable Cp_phi : N -> Cpow.
  Variable rpow : R -> Cpow -> R.
  Variable pow_th : power_theory rI rmul req Cp_phi rpow.
@@ -108,7 +108,7 @@ Section MakeRingPol.
     - (Pinj i (Pc c)) is (Pc c)
  *)
 
- Inductive Pol : Set :=
+ Inductive Pol : Type :=
   | Pc : C -> Pol
   | Pinj : positive -> Pol -> Pol
   | PX : Pol -> positive -> Pol -> Pol.
@@ -929,7 +929,7 @@ Qed.
 
  (** Definition of polynomial expressions *)
 
- Inductive PExpr : Set :=
+ Inductive PExpr : Type :=
   | PEc : C -> PExpr
   | PEX : positive -> PExpr
   | PEadd : PExpr -> PExpr -> PExpr

plugins/micromega/RingMicromega.v

@@ -49,15 +49,15 @@ Notation "x < y" := (rlt x y).
 
 (* Assume we have a type of coefficients C and a morphism from C to R *)
 
-Variable C : Set.
+Variable C : Type.
 Variables cO cI : C.
 Variables cplus ctimes cminus: C -> C -> C.
 Variable copp : C -> C.
 Variables ceqb cleb : C -> C -> bool.
 Variable phi : C -> R.
 
 (* Power coefficients *)
-Variable E : Set. (* the type of exponents *)
+Variable E : Type. (* the type of exponents *)
 Variable pow_phi : N -> E.
 Variable rpow : R -> E -> R.
 
@@ -139,7 +139,7 @@ Qed.
 
 (* Begin Micromega *)
 
-Definition PolC := Pol C : Set. (* polynomials in generalized Horner form, defined in Ring_polynom or EnvRing *)
+Definition PolC := Pol C. (* polynomials in generalized Horner form, defined in Ring_polynom or EnvRing *)
 Definition PolEnv := Env R. (* For interpreting PolC *)
 Definition eval_pol (env : PolEnv) (p:PolC) : R :=
    Pphi rplus rtimes phi env p.
@@ -286,7 +286,7 @@ destruct o' ; rewrite H1 ; now rewrite  (Rplus_0_l sor).
  now apply (Rplus_nonneg_nonneg sor).
 Qed.
 
-Inductive Psatz : Set :=
+Inductive Psatz : Type :=
 | PsatzIn : nat -> Psatz
 | PsatzSquare : PolC -> Psatz
 | PsatzMulC : PolC -> Psatz -> Psatz

plugins/setoid_ring/Field_theory.v

@@ -48,7 +48,7 @@ Section AlmostField.
  Let rinv_l := AFth.(AFinv_l).
 
  (* Coefficients *)
- Variable C: Set.
+ Variable C: Type.
  Variable (cO cI: C) (cadd cmul csub : C->C->C) (copp : C->C).
  Variable ceqb : C->C->bool.
  Variable phi : C -> R.
@@ -109,7 +109,7 @@ Hint Resolve lem1 lem2 lem3 lem4 lem5 lem6 lem7 lem8 lem9 lem10
      lem11 lem12 lem13 lem14 lem15 lem16 SRinv_ext.
 
  (* Power coefficients *)
- Variable Cpow : Set.
+ Variable Cpow : Type.
  Variable Cp_phi : N -> Cpow.
  Variable rpow : R -> Cpow -> R.
  Variable pow_th : power_theory rI rmul req Cp_phi rpow.
@@ -605,7 +605,7 @@ Qed.
 
 (* The input: syntax of a field expression *)
 
-Inductive FExpr : Set :=
+Inductive FExpr : Type :=
    FEc: C ->  FExpr
  | FEX: positive ->  FExpr
  | FEadd: FExpr -> FExpr ->  FExpr
@@ -633,7 +633,7 @@ Strategy expand [FEeval].
 
 (* The result of the normalisation *)
 
-Record linear : Set := mk_linear {
+Record linear : Type := mk_linear {
    num : PExpr C;
    denum : PExpr C;
    condition : list (PExpr C) }.
@@ -856,7 +856,7 @@ destruct n.
  trivial.
 Qed.
 
-Record rsplit : Set := mk_rsplit {
+Record rsplit : Type := mk_rsplit {
    rsplit_left : PExpr C;
    rsplit_common : PExpr C;
    rsplit_right : PExpr C}.

plugins/setoid_ring/Ring_polynom.v

@@ -27,15 +27,15 @@ Section MakeRingPol.
  Variable ARth : almost_ring_theory rO rI radd rmul rsub ropp req.
 
  (* Coefficients *)
- Variable C: Set.
+ Variable C: Type.
  Variable (cO cI: C) (cadd cmul csub : C->C->C) (copp : C->C).
  Variable ceqb : C->C->bool.
  Variable phi : C -> R.
  Variable CRmorph : ring_morph rO rI radd rmul rsub ropp req
                                 cO cI cadd cmul csub copp ceqb phi.
 
  (* Power coefficients *)
- Variable Cpow : Set.
+ Variable Cpow : Type.
  Variable Cp_phi : N -> Cpow.
  Variable rpow : R -> Cpow -> R.
  Variable pow_th : power_theory rI rmul req Cp_phi rpow.
@@ -110,7 +110,7 @@ Section MakeRingPol.
     - (Pinj i (Pc c)) is (Pc c)
  *)
 
- Inductive Pol : Set :=
+ Inductive Pol : Type :=
   | Pc : C -> Pol
   | Pinj : positive -> Pol -> Pol
   | PX : Pol -> positive -> Pol -> Pol.
@@ -908,7 +908,7 @@ Section MakeRingPol.
 
  (** Definition of polynomial expressions *)
 
- Inductive PExpr : Set :=
+ Inductive PExpr : Type :=
   | PEc : C -> PExpr
   | PEX : positive -> PExpr
   | PEadd : PExpr -> PExpr -> PExpr