1 files changed, 91 insertions, 68 deletions

diff --git a/toplevel/class.ml b/toplevel/class.ml
index 214fbf5b..6a485d52 100644
--- a/toplevel/class.ml
+++ b/toplevel/class.ml
@@ -1,31 +1,29 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Errors
 open Util
 open Pp
 open Names
-open Nameops
 open Term
+open Vars
 open Termops
-open Inductive
-open Declarations
 open Entries
 open Environ
-open Inductive
-open Lib
 open Classops
 open Declare
-open Libnames
+open Globnames
 open Nametab
 open Decl_kinds
-open Safe_typing
 
-let strength_min l = if List.mem Local l then Local else Global
+let strength_min l = if List.mem `LOCAL l then `LOCAL else `GLOBAL
+
+let loc_of_bool b = if b then `LOCAL else `GLOBAL
 
 (* Errors *)
 
@@ -38,7 +36,6 @@ type coercion_error_kind =
   | NoTarget
   | WrongTarget of cl_typ * cl_typ
   | NotAClass of global_reference
-  | NotEnoughClassArgs of cl_typ
 
 exception CoercionError of coercion_error_kind
 
@@ -65,18 +62,17 @@ let explain_coercion_error g = function
   | NotAClass ref ->
       (str "Type of " ++ Printer.pr_global ref ++
          str " does not end with a sort")
-  | NotEnoughClassArgs cl ->
-      (str"Wrong number of parameters for " ++ pr_class cl)
 
 (* Verifications pour l'ajout d'une classe *)
 
 let check_reference_arity ref =
-  if not (Reductionops.is_arity (Global.env()) Evd.empty (Global.type_of_global ref)) then
+  if not (Reductionops.is_arity (Global.env()) Evd.empty (Global.type_of_global_unsafe ref)) then
     raise (CoercionError (NotAClass ref))
 
 let check_arity = function
   | CL_FUN | CL_SORT -> ()
   | CL_CONST cst -> check_reference_arity (ConstRef cst)
+  | CL_PROJ cst -> check_reference_arity (ConstRef cst)
   | CL_SECVAR id -> check_reference_arity (VarRef id)
   | CL_IND kn -> check_reference_arity (IndRef kn)
 
@@ -84,7 +80,7 @@ let check_arity = function
 
 (* check that the computed target is the provided one *)
 let check_target clt = function
-  | Some cl when cl <> clt -> raise (CoercionError (WrongTarget(clt,cl)))
+  | Some cl when not (cl_typ_eq cl clt) -> raise (CoercionError (WrongTarget(clt,cl)))
   | _ -> ()
 
 (* condition d'heritage uniforme *)
@@ -94,13 +90,15 @@ let uniform_cond nargs lt =
     | (0,[]) -> true
     | (n,t::l) ->
       let t = strip_outer_cast t in
-      isRel t && destRel t = n && aux ((n-1),l)
+      isRel t && Int.equal (destRel t) n && aux ((n-1),l)
     | _ -> false
   in
   aux (nargs,lt)
 
 let class_of_global = function
-  | ConstRef sp -> CL_CONST sp
+  | ConstRef sp -> 
+    if Environ.is_projection sp (Global.env ()) 
+    then CL_PROJ sp else CL_CONST sp
   | IndRef sp -> CL_IND sp
   | VarRef id -> CL_SECVAR id
   | ConstructRef _ as c ->
@@ -123,19 +121,19 @@ l'indice de la classe source dans la liste lp
 let get_source lp source =
   match source with
     | None ->
-	let (cl1,lv1) =
+	let (cl1,u1,lv1) =
           match lp with
 	    | [] -> raise Not_found
             | t1::_ -> find_class_type Evd.empty t1
         in
-	(cl1,lv1,1)
+	(cl1,u1,lv1,1)
     | Some cl ->
 	let rec aux = function
 	  | [] -> raise Not_found
 	  | t1::lt ->
 	      try
-		let cl1,lv1 = find_class_type Evd.empty t1 in
-		if cl = cl1 then cl1,lv1,(List.length lt+1)
+		let cl1,u1,lv1 = find_class_type Evd.empty t1 in
+		if cl_typ_eq cl cl1 then cl1,u1,lv1,(List.length lt+1)
 		else raise Not_found
               with Not_found -> aux lt
 	in aux (List.rev lp)
@@ -144,7 +142,11 @@ let get_target t ind =
   if (ind > 1) then
     CL_FUN
   else
-    fst (find_class_type Evd.empty t)
+    match pi1 (find_class_type Evd.empty t) with
+    | CL_CONST p when Environ.is_projection p (Global.env ()) -> 
+      CL_PROJ p
+    | x -> x
+      
 
 let prods_of t =
   let rec aux acc d = match kind_of_term d with
@@ -155,9 +157,13 @@ let prods_of t =
   aux [] t
 
 let strength_of_cl = function
-  | CL_CONST kn -> Global
-  | CL_SECVAR id -> Local
-  | _ -> Global
+  | CL_CONST kn -> `GLOBAL
+  | CL_SECVAR id -> `LOCAL
+  | _ -> `GLOBAL
+
+let strength_of_global = function
+  | VarRef _ -> `LOCAL
+  | _ -> `GLOBAL
 
 let get_strength stre ref cls clt =
   let stres = strength_of_cl cls in
@@ -168,28 +174,28 @@ let get_strength stre ref cls clt =
 let ident_key_of_class = function
   | CL_FUN -> "Funclass"
   | CL_SORT -> "Sortclass"
-  | CL_CONST sp -> string_of_label (con_label sp)
-  | CL_IND (sp,_) -> string_of_label (mind_label sp)
-  | CL_SECVAR id -> string_of_id id
+  | CL_CONST sp | CL_PROJ sp -> Label.to_string (con_label sp)
+  | CL_IND (sp,_) -> Label.to_string (mind_label sp)
+  | CL_SECVAR id -> Id.to_string id
 
-(* coercion identité *)
+(* Identity coercion *)
 
 let error_not_transparent source =
   errorlabstrm "build_id_coercion"
     (pr_class source ++ str " must be a transparent constant.")
 
-let build_id_coercion idf_opt source =
+let build_id_coercion idf_opt source poly =
   let env = Global.env () in
-  let vs = match source with
-    | CL_CONST sp -> mkConst sp
+  let vs, ctx = match source with
+    | CL_CONST sp -> Universes.fresh_global_instance env (ConstRef sp)
     | _ -> error_not_transparent source in
-  let c = match constant_opt_value env (destConst vs) with
+  let c = match constant_opt_value_in env (destConst vs) with
     | Some c -> c
     | None -> error_not_transparent source in
   let lams,t = decompose_lam_assum c in
   let val_f =
     it_mkLambda_or_LetIn
-      (mkLambda (Name (id_of_string "x"),
+      (mkLambda (Name Namegen.default_dependent_ident,
 		 applistc vs (extended_rel_list 0 lams),
 		 mkRel 1))
        lams
@@ -212,17 +218,17 @@ let build_id_coercion idf_opt source =
     match idf_opt with
       | Some idf -> idf
       | None ->
-	  let cl,_ = find_class_type Evd.empty t in
-	  id_of_string ("Id_"^(ident_key_of_class source)^"_"^
+	  let cl,u,_ = find_class_type Evd.empty t in
+	  Id.of_string ("Id_"^(ident_key_of_class source)^"_"^
                         (ident_key_of_class cl))
   in
   let constr_entry = (* Cast is necessary to express [val_f] is identity *)
     DefinitionEntry
-      { const_entry_body = mkCast (val_f, DEFAULTcast, typ_f);
-        const_entry_secctx = None;
-	const_entry_type = Some typ_f;
-        const_entry_opaque = false } in
-  let kn = declare_constant idf (constr_entry,IsDefinition IdentityCoercion) in
+      (definition_entry ~types:typ_f ~poly ~univs:(Univ.ContextSet.to_context ctx)
+	 ~inline:true (mkCast (val_f, DEFAULTcast, typ_f)))
+  in
+  let decl = (constr_entry, IsDefinition IdentityCoercion) in
+  let kn = declare_constant idf decl in
   ConstRef kn
 
 let check_source = function
@@ -240,14 +246,14 @@ booleen "coercion identite'?"
 lorque source est None alors target est None aussi.
 *)
 
-let add_new_coercion_core coef stre source target isid =
+let add_new_coercion_core coef stre poly source target isid =
   check_source source;
-  let t = Global.type_of_global coef in
+  let t = Global.type_of_global_unsafe coef in
   if coercion_exists coef then raise (CoercionError AlreadyExists);
   let tg,lp = prods_of t in
   let llp = List.length lp in
-  if llp = 0 then raise (CoercionError NotAFunction);
-  let (cls,lvs,ind) =
+  if Int.equal llp 0 then raise (CoercionError NotAFunction);
+  let (cls,us,lvs,ind) =
     try
       get_source lp source
     with Not_found ->
@@ -255,7 +261,7 @@ let add_new_coercion_core coef stre source target isid =
   in
   check_source (Some cls);
   if not (uniform_cond (llp-ind) lvs) then
-    msg_warn (Pp.string_of_ppcmds (explain_coercion_error coef NotUniform));
+    msg_warning (explain_coercion_error coef NotUniform);
   let clt =
     try
       get_target tg ind
@@ -265,38 +271,55 @@ let add_new_coercion_core coef stre source target isid =
   check_target clt target;
   check_arity cls;
   check_arity clt;
-  let stre' = get_strength stre coef cls clt in
-  declare_coercion coef stre' ~isid ~src:cls ~target:clt ~params:(List.length lvs)
+  let local = match get_strength stre coef cls clt with
+  | `LOCAL -> true
+  | `GLOBAL -> false
+  in
+  declare_coercion coef ~local ~isid ~src:cls ~target:clt ~params:(List.length lvs)
+
 
-let try_add_new_coercion_core ref b c d e =
-  try add_new_coercion_core ref b c d e
+let try_add_new_coercion_core ref ~local c d e f =
+  try add_new_coercion_core ref (loc_of_bool local) c d e f
   with CoercionError e ->
       errorlabstrm "try_add_new_coercion_core"
         (explain_coercion_error ref e ++ str ".")
 
-let try_add_new_coercion ref stre =
-  try_add_new_coercion_core ref stre None None false
+let try_add_new_coercion ref ~local poly =
+  try_add_new_coercion_core ref ~local poly None None false
 
-let try_add_new_coercion_subclass cl stre =
-  let coe_ref = build_id_coercion None cl in
-  try_add_new_coercion_core coe_ref stre (Some cl) None true
+let try_add_new_coercion_subclass cl ~local poly =
+  let coe_ref = build_id_coercion None cl poly in
+  try_add_new_coercion_core coe_ref ~local poly (Some cl) None true
 
-let try_add_new_coercion_with_target ref stre ~source ~target =
-  try_add_new_coercion_core ref stre (Some source) (Some target) false
+let try_add_new_coercion_with_target ref ~local poly ~source ~target =
+  try_add_new_coercion_core ref ~local poly (Some source) (Some target) false
 
-let try_add_new_identity_coercion id stre ~source ~target =
-  let ref = build_id_coercion (Some id) source in
-  try_add_new_coercion_core ref stre (Some source) (Some target) true
+let try_add_new_identity_coercion id ~local poly ~source ~target =
+  let ref = build_id_coercion (Some id) source poly in
+  try_add_new_coercion_core ref ~local poly (Some source) (Some target) true
 
-let try_add_new_coercion_with_source ref stre ~source =
-  try_add_new_coercion_core ref stre (Some source) None false
+let try_add_new_coercion_with_source ref ~local poly ~source =
+  try_add_new_coercion_core ref ~local poly (Some source) None false
 
-let add_coercion_hook stre ref =
-  try_add_new_coercion ref stre;
-  Flags.if_verbose message
-    (string_of_qualid (shortest_qualid_of_global Idset.empty ref)
-    ^ " is now a coercion")
+let add_coercion_hook poly local ref =
+  let stre = match local with
+  | Local -> true
+  | Global -> false
+  | Discharge -> assert false
+  in
+  let () = try_add_new_coercion ref stre poly in
+  let msg = pr_global_env Id.Set.empty ref ++ str " is now a coercion" in
+  Flags.if_verbose msg_info msg
+
+let add_coercion_hook poly = Lemmas.mk_hook (add_coercion_hook poly)
 
-let add_subclass_hook stre ref =
+let add_subclass_hook poly local ref =
+  let stre = match local with
+  | Local -> true
+  | Global -> false
+  | Discharge -> assert false
+  in
   let cl = class_of_global ref in
-  try_add_new_coercion_subclass cl stre
+  try_add_new_coercion_subclass cl stre poly
+
+let add_subclass_hook poly = Lemmas.mk_hook (add_subclass_hook poly)