1 files changed, 113 insertions, 102 deletions

diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index b8da6b68..08051fd3 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -1,9 +1,11 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
 (*i*)
@@ -11,12 +13,16 @@ open Names
 open Globnames
 open Decl_kinds
 open Term
+open Constr
 open Vars
 open Evd
 open Util
 open Typeclasses_errors
 open Libobject
 open Context.Rel.Declaration
+
+module RelDecl = Context.Rel.Declaration
+module NamedDecl = Context.Named.Declaration
 (*i*)
 
 let typeclasses_unique_solutions = ref false
@@ -27,8 +33,7 @@ open Goptions
 
 let _ =
   declare_bool_option
-    { optsync  = true;
-      optdepr  = false;
+    { optdepr  = false;
       optname  = "check that typeclasses proof search returns unique solutions";
       optkey   = ["Typeclasses";"Unique";"Solutions"];
       optread  = get_typeclasses_unique_solutions;
@@ -55,18 +60,21 @@ type direction = Forward | Backward
 
 (* This module defines type-classes *)
 type typeclass = {
+  (* Universe quantification *)
+  cl_univs : Univ.AUContext.t;
+
   (* The class implementation *)
   cl_impl : global_reference;
 
   (* Context in which the definitions are typed. Includes both typeclass parameters and superclasses. *)
-  cl_context : (global_reference * bool) option list * Context.Rel.t;
+  cl_context : global_reference option list * Context.Rel.t;
 
   (* Context of definitions and properties on defs, will not be shared *)
   cl_props : Context.Rel.t;
 
   (* The method implementaions as projections. *)
   cl_projs : (Name.t * (direction * Vernacexpr.hint_info_expr) option
-	      * constant option) list;
+	      * Constant.t option) list;
   
   cl_strict : bool;
 
@@ -79,9 +87,8 @@ type instance = {
   is_class: global_reference;
   is_info: Vernacexpr.hint_info_expr;
   (* Sections where the instance should be redeclared,
-     -1 for discard, 0 for none. *)
-  is_global: int;
-  is_poly: bool;
+     None for discard, Some 0 for none. *)
+  is_global: int option;
   is_impl: global_reference;
 }
 
@@ -91,15 +98,16 @@ let instance_impl is = is.is_impl
 
 let hint_priority is = is.is_info.Vernacexpr.hint_priority
 
-let new_instance cl info glob poly impl =
+let new_instance cl info glob impl =
   let global =
-    if glob then Lib.sections_depth ()
-    else -1
+    if glob then Some (Lib.sections_depth ())
+    else None
   in
+  if match global with Some n -> n>0 && isVarRef impl | _ -> false then
+    CErrors.user_err (Pp.str "Cannot set Global an instance referring to a section variable.");
     { is_class = cl.cl_impl;
       is_info = info ;
       is_global = global ;
-      is_poly = poly;
       is_impl = impl }
 
 (*
@@ -109,64 +117,48 @@ let new_instance cl info glob poly impl =
 let classes : typeclasses ref = Summary.ref Refmap.empty ~name:"classes"
 let instances : instances ref = Summary.ref Refmap.empty ~name:"instances"
 
-open Declarations
-
-let typeclass_univ_instance (cl,u') =
-  let subst = 
-    let u = 
-      match cl.cl_impl with
-      | ConstRef c -> 
-        let cb = Global.lookup_constant c in
-	  if cb.const_polymorphic then Univ.UContext.instance cb.const_universes
-	  else Univ.Instance.empty
-      | IndRef c ->
-         let mib,oib = Global.lookup_inductive c in
-	  if mib.mind_polymorphic then Univ.UContext.instance mib.mind_universes
-	  else Univ.Instance.empty
-      | _ -> Univ.Instance.empty
-    in Array.fold_left2 (fun subst u u' -> Univ.LMap.add u u' subst) 
-      Univ.LMap.empty (Univ.Instance.to_array u) (Univ.Instance.to_array u')
-  in
-  let subst_ctx = Context.Rel.map (subst_univs_level_constr subst) in
-    { cl with cl_context = fst cl.cl_context, subst_ctx (snd cl.cl_context);
-      cl_props = subst_ctx cl.cl_props}, u'
+let typeclass_univ_instance (cl, u) =
+  assert (Univ.AUContext.size cl.cl_univs == Univ.Instance.length u);
+  let subst_ctx c = Context.Rel.map (subst_instance_constr u) c in
+    { cl with cl_context = on_snd subst_ctx cl.cl_context;
+      cl_props = subst_ctx cl.cl_props}
 
 let class_info c =
   try Refmap.find c !classes
-  with Not_found -> not_a_class (Global.env()) (printable_constr_of_global c)
+  with Not_found -> not_a_class (Global.env()) (EConstr.of_constr (printable_constr_of_global c))
 
-let global_class_of_constr env c =
-  try let gr, u = Universes.global_of_constr c in
+let global_class_of_constr env sigma c =
+  try let gr, u = Termops.global_of_constr sigma c in
 	class_info gr, u
   with Not_found -> not_a_class env c
 
-let dest_class_app env c =
-  let cl, args = decompose_app c in
-    global_class_of_constr env cl, args
+let dest_class_app env sigma c =
+  let cl, args = EConstr.decompose_app sigma c in
+    global_class_of_constr env sigma cl, (List.map EConstr.Unsafe.to_constr args)
 
-let dest_class_arity env c =
-  let rels, c = decompose_prod_assum c in
-    rels, dest_class_app env c
+let dest_class_arity env sigma c =
+  let open EConstr in
+  let rels, c = decompose_prod_assum sigma c in
+    rels, dest_class_app env sigma c
 
-let class_of_constr c =
-  try Some (dest_class_arity (Global.env ()) c)
+let class_of_constr sigma c =
+  try Some (dest_class_arity (Global.env ()) sigma c)
   with e when CErrors.noncritical e -> None
 
-let is_class_constr c = 
-  try let gr, u = Universes.global_of_constr c in
+let is_class_constr sigma c = 
+  try let gr, u = Termops.global_of_constr sigma c in
 	Refmap.mem gr !classes
   with Not_found -> false
 
 let rec is_class_type evd c =
-  let c, args = decompose_app c in
-    match kind_of_term c with
+  let c, _ = Termops.decompose_app_vect evd c in
+    match EConstr.kind evd c with
     | Prod (_, _, t) -> is_class_type evd t
-    | Evar (e, _) when Evd.is_defined evd e ->
-      is_class_type evd (Evarutil.whd_head_evar evd c)
-    | _ -> is_class_constr c
+    | Cast (t, _, _) -> is_class_type evd t
+    | _ -> is_class_constr evd c
       
 let is_class_evar evd evi =
-  is_class_type evd evi.Evd.evar_concl
+  is_class_type evd (EConstr.of_constr evi.Evd.evar_concl)
 
 (*
  * classes persistent object
@@ -181,13 +173,14 @@ let subst_class (subst,cl) =
   let do_subst_con c = Mod_subst.subst_constant subst c
   and do_subst c = Mod_subst.subst_mps subst c
   and do_subst_gr gr = fst (subst_global subst gr) in
-  let do_subst_ctx = List.smartmap (map_constr do_subst) in
+  let do_subst_ctx = List.smartmap (RelDecl.map_constr do_subst) in
   let do_subst_context (grs,ctx) =
-    List.smartmap (Option.smartmap (fun (gr,b) -> do_subst_gr gr, b)) grs,
+    List.smartmap (Option.smartmap do_subst_gr) grs,
     do_subst_ctx ctx in
   let do_subst_projs projs = List.smartmap (fun (x, y, z) -> 
     (x, y, Option.smartmap do_subst_con z)) projs in
-  { cl_impl = do_subst_gr cl.cl_impl;
+  { cl_univs = cl.cl_univs;
+    cl_impl = do_subst_gr cl.cl_impl;
     cl_context = do_subst_context cl.cl_context;
     cl_props = do_subst_ctx cl.cl_props;
     cl_projs = do_subst_projs cl.cl_projs;
@@ -197,22 +190,18 @@ let subst_class (subst,cl) =
 let discharge_class (_,cl) =
   let repl = Lib.replacement_context () in
   let rel_of_variable_context ctx = List.fold_right
-    ( fun (n,_,b,t) (ctx', subst) ->
-        let decl = match b with
-                   | None -> LocalAssum (Name n, substn_vars 1 subst t)
-		   | Some b -> LocalDef (Name n, substn_vars 1 subst b, substn_vars 1 subst t)
-	in
-	(decl :: ctx', n :: subst)
+    ( fun (decl,_) (ctx', subst) ->
+        let decl' = decl |> NamedDecl.map_constr (substn_vars 1 subst) |> NamedDecl.to_rel_decl in
+	(decl' :: ctx', NamedDecl.get_id decl :: subst)
     ) ctx ([], []) in
-  let discharge_rel_context subst n rel =
+  let discharge_rel_context (subst, usubst) n rel =
     let rel = Context.Rel.map (Cooking.expmod_constr repl) rel in
-    let ctx, _ =
-      List.fold_right
-	(fun decl (ctx, k) ->
-	   map_constr (substn_vars k subst) decl :: ctx, succ k
-	)
-	rel ([], n)
-    in ctx
+    let fold decl (ctx, k) =
+      let map c = subst_univs_level_constr usubst (substn_vars k subst c) in
+      RelDecl.map_constr map decl :: ctx, succ k
+    in
+    let ctx, _ = List.fold_right fold rel ([], n) in
+    ctx
   in
   let abs_context cl =
     match cl.cl_impl with
@@ -222,22 +211,25 @@ let discharge_class (_,cl) =
   let discharge_context ctx' subst (grs, ctx) =
     let grs' =
       let newgrs = List.map (fun decl ->
-			     match decl |> get_type |> class_of_constr with
+			     match decl |> RelDecl.get_type |> EConstr.of_constr |> class_of_constr Evd.empty with
 			     | None -> None
-			     | Some (_, ((tc,_), _)) -> Some (tc.cl_impl, true))
+                             | Some (_, ((tc,_), _)) -> Some tc.cl_impl)
 			    ctx'
       in
-      List.smartmap (Option.smartmap (fun (gr, b) -> Lib.discharge_global gr, b)) grs
+      List.smartmap (Option.smartmap Lib.discharge_global) grs
       @ newgrs
     in grs', discharge_rel_context subst 1 ctx @ ctx' in
   let cl_impl' = Lib.discharge_global cl.cl_impl in
   if cl_impl' == cl.cl_impl then cl else
-    let ctx, usubst, uctx = abs_context cl in
+    let info = abs_context cl in
+    let ctx = info.Lib.abstr_ctx in
     let ctx, subst = rel_of_variable_context ctx in
-    let context = discharge_context ctx subst cl.cl_context in
-    let props = discharge_rel_context subst (succ (List.length (fst cl.cl_context))) cl.cl_props in
+    let usubst, cl_univs' = Lib.discharge_abstract_universe_context info cl.cl_univs in
+    let context = discharge_context ctx (subst, usubst) cl.cl_context in
+    let props = discharge_rel_context (subst, usubst) (succ (List.length (fst cl.cl_context))) cl.cl_props in
     let discharge_proj (x, y, z) = x, y, Option.smartmap Lib.discharge_con z in
-      { cl_impl = cl_impl';
+      { cl_univs = cl_univs';
+        cl_impl = cl_impl';
 	cl_context = context;
 	cl_props = props;
 	cl_projs = List.smartmap discharge_proj cl.cl_projs;
@@ -284,15 +276,18 @@ let build_subclasses ~check env sigma glob { hint_priority = pri } =
         Nameops.add_suffix _id ("_subinstance_" ^ string_of_int !i))
   in
   let ty, ctx = Global.type_of_global_in_context env glob in
-  let sigma = Evd.merge_context_set Evd.univ_rigid sigma (Univ.ContextSet.of_context ctx) in
+  let inst, ctx = Universes.fresh_instance_from ctx None in
+  let ty = Vars.subst_instance_constr inst ty in
+  let ty = EConstr.of_constr ty in
+  let sigma = Evd.merge_context_set Evd.univ_rigid sigma ctx in
   let rec aux pri c ty path =
-    let ty = Evarutil.nf_evar sigma ty in
-      match class_of_constr ty with
+      match class_of_constr sigma ty with
       | None -> []
       | Some (rels, ((tc,u), args)) ->
 	let instapp = 
-	  Reductionops.whd_beta sigma (appvectc c (Context.Rel.to_extended_vect 0 rels))
+	  Reductionops.whd_beta sigma (EConstr.of_constr (appvectc c (Context.Rel.to_extended_vect mkRel 0 rels)))
 	in
+	let instapp = EConstr.Unsafe.to_constr instapp in
 	let projargs = Array.of_list (args @ [instapp]) in
 	let projs = List.map_filter 
 	  (fun (n, b, proj) ->
@@ -301,8 +296,10 @@ let build_subclasses ~check env sigma glob { hint_priority = pri } =
 	   | Some (Backward, _) -> None
 	   | Some (Forward, info) ->
 	     let proj = Option.get proj in
+	     let rels = List.map (fun d -> Termops.map_rel_decl EConstr.Unsafe.to_constr d) rels in
+	     let u = EConstr.EInstance.kind sigma u in
 	     let body = it_mkLambda_or_LetIn (mkApp (mkConstU (proj,u), projargs)) rels in
-	       if check && check_instance env sigma body then None
+	       if check && check_instance env sigma (EConstr.of_constr body) then None
 	       else 
 		 let newpri =
 		   match pri, info.hint_priority with
@@ -314,12 +311,12 @@ let build_subclasses ~check env sigma glob { hint_priority = pri } =
 	in
 	let declare_proj hints (cref, info, body) =
 	  let path' = cref :: path in
-	  let ty = Retyping.get_type_of env sigma body in
+	  let ty = Retyping.get_type_of env sigma (EConstr.of_constr body) in
 	  let rest = aux pri body ty path' in
 	    hints @ (path', info, body) :: rest
 	in List.fold_left declare_proj [] projs 
   in
-  let term = Universes.constr_of_global_univ (glob,Univ.UContext.instance ctx) in
+  let term = Universes.constr_of_global_univ (glob, inst) in
     (*FIXME subclasses should now get substituted for each particular instance of
       the polymorphic superclass *)
     aux pri term ty [glob]
@@ -357,22 +354,34 @@ let subst_instance (subst, (action, inst)) = action,
       is_impl = fst (subst_global subst inst.is_impl) }
 
 let discharge_instance (_, (action, inst)) =
-  if inst.is_global <= 0 then None
-  else Some (action,
+  match inst.is_global with
+  | None -> None
+  | Some n ->
+    assert (not (isVarRef inst.is_impl));
+    Some (action,
     { inst with 
-      is_global = pred inst.is_global;
+      is_global = Some (pred n);
       is_class = Lib.discharge_global inst.is_class;
       is_impl = Lib.discharge_global inst.is_impl })
     
 
-let is_local i = Int.equal i.is_global (-1)
+let is_local i = (i.is_global == None)
+
+let is_local_for_hint i =
+  match i.is_global with
+  | None -> true  (* i.e. either no Global keyword not in section, or in section *)
+  | Some n -> n <> 0 (* i.e. in a section, declare the hint as local
+     since discharge is managed by rebuild_instance which calls again
+     add_instance_hint; don't ask hints to take discharge into account
+     itself *)
 
 let add_instance check inst =
   let poly = Global.is_polymorphic inst.is_impl in
-  add_instance_hint (IsGlobal inst.is_impl) [inst.is_impl] (is_local inst) 
+  let local = is_local_for_hint inst in
+  add_instance_hint (IsGlobal inst.is_impl) [inst.is_impl] local
     inst.is_info poly;
   List.iter (fun (path, pri, c) -> add_instance_hint (IsConstr c) path
-    (is_local inst) pri poly)
+    local pri poly)
     (build_subclasses ~check:(check && not (isVarRef inst.is_impl))
        (Global.env ()) (Evd.from_env (Global.env ())) inst.is_impl inst.is_info)
 
@@ -407,11 +416,12 @@ let remove_instance i =
   remove_instance_hint i.is_impl
 
 let declare_instance info local glob =
-  let ty = Global.type_of_global_unsafe glob in
+  let ty, _ = Global.type_of_global_in_context (Global.env ()) glob in
   let info = Option.default {hint_priority = None; hint_pattern = None} info in
-    match class_of_constr ty with
+    match class_of_constr Evd.empty (EConstr.of_constr ty) with
     | Some (rels, ((tc,_), args) as _cl) ->
-      add_instance (new_instance tc info (not local) (Flags.use_polymorphic_flag ()) glob)
+      assert (not (isVarRef glob) || local);
+      add_instance (new_instance tc info (not local) glob)
     | None -> ()
 
 let add_class cl =
@@ -420,7 +430,7 @@ let add_class cl =
 	     match inst with
 	     | Some (Backward, info) ->
 	       (match body with
-	       | None -> CErrors.error "Non-definable projection can not be declared as a subinstance"
+	       | None -> CErrors.user_err Pp.(str "Non-definable projection can not be declared as a subinstance")
 	       | Some b -> declare_instance (Some info) false (ConstRef b))
 	     | _ -> ())
   cl.cl_projs
@@ -433,19 +443,20 @@ let add_class cl =
 
 let instance_constructor (cl,u) args =
   let lenpars = List.count is_local_assum (snd cl.cl_context) in
+  let open EConstr in
   let pars = fst (List.chop lenpars args) in
     match cl.cl_impl with
       | IndRef ind -> 
         let ind = ind, u in
-          (Some (applistc (mkConstructUi (ind, 1)) args),
-	   applistc (mkIndU ind) pars)
+          (Some (applist (mkConstructUi (ind, 1), args)),
+           applist (mkIndU ind, pars))
       | ConstRef cst -> 
         let cst = cst, u in
 	let term = match args with
 	  | [] -> None
 	  | _ -> Some (List.last args)
 	in
-	  (term, applistc (mkConstU cst) pars)
+          (term, applist (mkConstU cst, pars))
       | _ -> assert false
 
 let typeclasses () = Refmap.fold (fun _ l c -> l :: c) !classes []
@@ -512,7 +523,7 @@ let mark_unresolvable evi = mark_resolvability false evi
 let mark_resolvable evi = mark_resolvability true evi
 
 open Evar_kinds
-type evar_filter = existential_key -> Evar_kinds.t -> bool
+type evar_filter = Evar.t -> Evar_kinds.t -> bool
 
 let all_evars _ _ = true
 let all_goals _ = function VarInstance _ | GoalEvar -> true | _ -> false
@@ -543,8 +554,8 @@ let solve_all_instances env evd filter unique split fail =
   Hook.get get_solve_all_instances env evd filter unique split fail
 
 (** Profiling resolution of typeclasses *)
-(* let solve_classeskey = Profile.declare_profile "solve_typeclasses" *)
-(* let solve_problem = Profile.profile5 solve_classeskey solve_problem *)
+(* let solve_classeskey = CProfile.declare_profile "solve_typeclasses" *)
+(* let solve_problem = CProfile.profile5 solve_classeskey solve_problem *)
 
 let resolve_typeclasses ?(fast_path = true) ?(filter=no_goals) ?(unique=get_typeclasses_unique_solutions ())
     ?(split=true) ?(fail=true) env evd =