Functionalize env in type classes

I had to reorganize the code a bit. The Context command moved to
comAssumption, as it is not so related to type classes. We were able to
remove a few hooks on the way.

4 files changed, 48 insertions, 285 deletions

diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index 570c83a0da..20215029af 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -318,21 +318,21 @@ let warn_ambiguous_path =
 (* add_coercion_in_graph : coe_index * cl_index * cl_index -> unit
                          coercion,source,target *)
 
-let different_class_params i =
+let different_class_params env i =
   let ci = class_info_from_index i in
     if (snd ci).cl_param > 0 then true
     else 
       match fst ci with
-      | CL_IND i -> Global.is_polymorphic (IndRef i)
-      | CL_CONST c -> Global.is_polymorphic (ConstRef c)
+      | CL_IND i -> Environ.is_polymorphic env (IndRef i)
+      | CL_CONST c -> Environ.is_polymorphic env (ConstRef c)
       | _ -> false
 
-let add_coercion_in_graph (ic,source,target) =
+let add_coercion_in_graph env (ic,source,target) =
   let old_inheritance_graph = !inheritance_graph in
   let ambig_paths =
     (ref [] : ((cl_index * cl_index) * inheritance_path) list ref) in
   let try_add_new_path (i,j as ij) p =
-    if not (Bijint.Index.equal i j) || different_class_params i then
+    if not (Bijint.Index.equal i j) || different_class_params env i then
       match lookup_path_between_class ij with
       | q ->
         if not (compare_path p q) then
@@ -386,29 +386,29 @@ let subst_coercion subst c =
 
 (* Computation of the class arity *)
 
-let reference_arity_length ref =
-  let t, _ = Typeops.type_of_global_in_context (Global.env ()) ref in
-  List.length (fst (Reductionops.splay_arity (Global.env()) Evd.empty (EConstr.of_constr t))) (** FIXME *)
+let reference_arity_length env sigma ref =
+  let t, _ = Typeops.type_of_global_in_context env ref in
+  List.length (fst (Reductionops.splay_arity env sigma (EConstr.of_constr t)))
 
-let projection_arity_length p =
-  let len = reference_arity_length (ConstRef (Projection.Repr.constant p)) in
+let projection_arity_length env sigma p =
+  let len = reference_arity_length env sigma (ConstRef (Projection.Repr.constant p)) in
   len - Projection.Repr.npars p
 
-let class_params = function
+let class_params env sigma = function
   | CL_FUN | CL_SORT -> 0
-  | CL_CONST sp -> reference_arity_length (ConstRef sp)
-  | CL_PROJ sp -> projection_arity_length sp
-  | CL_SECVAR sp -> reference_arity_length (VarRef sp)
-  | CL_IND sp  -> reference_arity_length (IndRef sp)
+  | CL_CONST sp -> reference_arity_length env sigma (ConstRef sp)
+  | CL_PROJ sp -> projection_arity_length env sigma sp
+  | CL_SECVAR sp -> reference_arity_length env sigma (VarRef sp)
+  | CL_IND sp  -> reference_arity_length env sigma (IndRef sp)
 
 (* add_class : cl_typ -> locality_flag option -> bool -> unit *)
 
-let add_class cl =
-  add_new_class cl { cl_param = class_params cl }
+let add_class env sigma cl =
+  add_new_class cl { cl_param = class_params env sigma cl }
 
-let declare_coercion c =
-  let () = add_class c.coercion_source in
-  let () = add_class c.coercion_target in
+let declare_coercion env sigma c =
+  let () = add_class env sigma c.coercion_source in
+  let () = add_class env sigma c.coercion_target in
   let is, _ = class_info c.coercion_source in
   let it, _ = class_info c.coercion_target in
   let xf =
@@ -419,7 +419,7 @@ let declare_coercion c =
       coe_param = c.coercion_params;
     } in
   let () = add_new_coercion c.coercion_type xf in
-  add_coercion_in_graph (xf,is,it)
+  add_coercion_in_graph env (xf,is,it)
 
 (* For printing purpose *)
 let pr_cl_index = Bijint.Index.print
diff --git a/pretyping/classops.mli b/pretyping/classops.mli
index 1d381bb223..46c6d4c697 100644
--- a/pretyping/classops.mli
+++ b/pretyping/classops.mli
@@ -87,7 +87,7 @@ type coercion = {
 
 val subst_coercion : substitution -> coercion -> coercion
 
-val declare_coercion : coercion -> unit
+val declare_coercion : env -> evar_map -> coercion -> unit
 
 (** {6 Access to coercions infos } *)
 val coercion_exists : coe_typ -> bool
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 1496712bbc..ee27aea93f 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -17,11 +17,8 @@ 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*)
 
 (* Core typeclasses hints *)
@@ -38,12 +35,6 @@ let get_typeclasses_unique_solutions =
     ~key:["Typeclasses";"Unique";"Solutions"]
     ~value:false
 
-let (add_instance_hint, add_instance_hint_hook) = Hook.make ()
-let add_instance_hint id = Hook.get add_instance_hint id
-
-let (remove_instance_hint, remove_instance_hint_hook) = Hook.make ()
-let remove_instance_hint id = Hook.get remove_instance_hint id
-
 let (set_typeclass_transparency, set_typeclass_transparency_hook) = Hook.make ()
 let set_typeclass_transparency gr local c = Hook.get set_typeclass_transparency gr local c
 
@@ -97,18 +88,6 @@ let instance_impl is = is.is_impl
 
 let hint_priority is = is.is_info.hint_priority
 
-let new_instance cl info glob impl =
-  let global =
-    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_impl = impl }
-
 (*
  * states management
  *)
@@ -122,11 +101,10 @@ let typeclass_univ_instance (cl, u) =
     { cl with cl_context = on_snd subst_ctx cl.cl_context;
       cl_props = subst_ctx cl.cl_props}
 
-let class_info c =
+let class_info env sigma c =
   try GlobRef.Map.find c !classes
   with Not_found ->
-    let env = Global.env() in
-    not_a_class env (Evd.from_env env) (EConstr.of_constr (printable_constr_of_global c))
+    not_a_class env sigma (EConstr.of_constr (printable_constr_of_global c))
 
 let global_class_of_constr env sigma c =
   try let gr, u = Termops.global_of_constr sigma c in
@@ -142,8 +120,8 @@ let dest_class_arity env sigma c =
   let rels, c = decompose_prod_assum sigma c in
     rels, dest_class_app env sigma c
 
-let class_of_constr sigma c =
-  try Some (dest_class_arity (Global.env ()) sigma c)
+let class_of_constr env sigma c =
+  try Some (dest_class_arity env sigma c)
   with e when CErrors.noncritical e -> None
 
 let is_class_constr sigma c = 
@@ -176,103 +154,9 @@ let rec is_maybe_class_type evd c =
 
 let () = Hook.set Evd.is_maybe_typeclass_hook (fun evd c -> is_maybe_class_type evd (EConstr.of_constr c))
 
-(*
- * classes persistent object
- *)
-
-let load_class (_, cl) =
+let load_class cl =
   classes := GlobRef.Map.add cl.cl_impl cl !classes
 
-let cache_class = load_class
-
-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.Smart.map (RelDecl.map_constr do_subst) in
-  let do_subst_context (grs,ctx) =
-    List.Smart.map (Option.Smart.map do_subst_gr) grs,
-    do_subst_ctx ctx in
-  let do_subst_projs projs = List.Smart.map (fun (x, y, z) ->
-    (x, y, Option.Smart.map do_subst_con z)) projs in
-  { 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;
-    cl_strict = cl.cl_strict;
-    cl_unique = cl.cl_unique }
-
-let discharge_class (_,cl) =
-  let repl = Lib.replacement_context () in
-  let rel_of_variable_context ctx = List.fold_right
-    ( 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, usubst) n rel =
-    let rel = Context.Rel.map (Cooking.expmod_constr repl) rel in
-    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
-      | VarRef _ | ConstructRef _ -> assert false
-      | ConstRef cst -> Lib.section_segment_of_constant cst
-      | IndRef (ind,_) -> Lib.section_segment_of_mutual_inductive ind in
-  let discharge_context ctx' subst (grs, ctx) =
-    let grs' =
-      let newgrs = List.map (fun decl ->
-			     match decl |> RelDecl.get_type |> EConstr.of_constr |> class_of_constr Evd.empty with
-			     | None -> None
-                             | Some (_, ((tc,_), _)) -> Some tc.cl_impl)
-			    ctx'
-      in
-      grs @ newgrs
-    in grs', discharge_rel_context subst 1 ctx @ ctx' in
-  try
-    let info = abs_context cl in
-    let ctx = info.Lib.abstr_ctx in
-    let ctx, subst = rel_of_variable_context ctx 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 = x in
-    { cl_univs = cl_univs';
-      cl_impl = cl.cl_impl;
-      cl_context = context;
-      cl_props = props;
-      cl_projs = List.Smart.map discharge_proj cl.cl_projs;
-      cl_strict = cl.cl_strict;
-      cl_unique = cl.cl_unique
-    }
-  with Not_found -> (* not defined in the current section *)
-    cl
-
-let rebuild_class cl = 
-  try 
-    let cst = Tacred.evaluable_of_global_reference (Global.env ()) cl.cl_impl in
-      set_typeclass_transparency cst false false; cl
-  with e when CErrors.noncritical e -> cl
-
-let class_input : typeclass -> obj =
-  declare_object
-    { (default_object "type classes state") with
-      cache_function = cache_class;
-      load_function = (fun _ -> load_class);
-      open_function = (fun _ -> load_class);
-      classify_function = (fun x -> Substitute x);
-      discharge_function = (fun a -> Some (discharge_class a));
-      rebuild_function = rebuild_class;
-      subst_function = subst_class }
-
-let add_class cl =
-  Lib.add_anonymous_leaf (class_input cl)
-
 (** Build the subinstances hints. *)
 
 let check_instance env sigma c =
@@ -295,7 +179,7 @@ let build_subclasses ~check env sigma glob { hint_priority = pri } =
   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 =
-      match class_of_constr sigma ty with
+      match class_of_constr env sigma ty with
       | None -> []
       | Some (rels, ((tc,u), args)) ->
 	let instapp = 
@@ -336,136 +220,23 @@ let build_subclasses ~check env sigma glob { hint_priority = pri } =
     aux pri term ty [glob]
 
 (*
- * instances persistent object
+ * interface functions
  *)
 
-type instance_action = 
-  | AddInstance
-  | RemoveInstance
-
-let load_instance inst = 
-  let insts = 
+let load_instance inst =
+  let insts =
     try GlobRef.Map.find inst.is_class !instances
     with Not_found -> GlobRef.Map.empty in
   let insts = GlobRef.Map.add inst.is_impl inst insts in
   instances := GlobRef.Map.add inst.is_class insts !instances
 
 let remove_instance inst =
-  let insts = 
+  let insts =
     try GlobRef.Map.find inst.is_class !instances
     with Not_found -> assert false in
   let insts = GlobRef.Map.remove inst.is_impl insts in
   instances := GlobRef.Map.add inst.is_class insts !instances
 
-let cache_instance (_, (action, i)) =
-  match action with 
-  | AddInstance -> load_instance i
-  | RemoveInstance -> remove_instance i      
-
-let subst_instance (subst, (action, inst)) = action,
-  { inst with 
-      is_class = fst (subst_global subst inst.is_class);
-      is_impl = fst (subst_global subst inst.is_impl) }
-
-let discharge_instance (_, (action, inst)) =
-  match inst.is_global with
-  | None -> None
-  | Some n ->
-    assert (not (isVarRef inst.is_impl));
-    Some (action,
-    { inst with 
-      is_global = Some (pred n);
-      is_class = inst.is_class;
-      is_impl = inst.is_impl })
-    
-
-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
-  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
-    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)
-
-let rebuild_instance (action, inst) =
-  let () = match action with
-  | AddInstance -> add_instance true inst
-  | _ -> ()
-  in
-  (action, inst)
-
-let classify_instance (action, inst) =
-  if is_local inst then Dispose
-  else Substitute (action, inst)
-
-let instance_input : instance_action * instance -> obj =
-  declare_object
-    { (default_object "type classes instances state") with
-      cache_function = cache_instance;
-      load_function = (fun _ x -> cache_instance x);
-      open_function = (fun _ x -> cache_instance x);
-      classify_function = classify_instance;
-      discharge_function = discharge_instance;
-      rebuild_function = rebuild_instance;
-      subst_function = subst_instance }
-
-let add_instance i =
-  Lib.add_anonymous_leaf (instance_input (AddInstance, i));
-  add_instance true i
-
-let remove_instance i =
-  Lib.add_anonymous_leaf (instance_input (RemoveInstance, i));
-  remove_instance_hint i.is_impl
-
-let warning_not_a_class =
-  let name = "not-a-class" in
-  let category = "typeclasses" in
-  CWarnings.create ~name ~category (fun (n, ty) ->
-      let env = Global.env () in
-      let evd = Evd.from_env env in
-      Pp.(str "Ignored instance declaration for “"
-          ++ Nametab.pr_global_env Id.Set.empty n
-          ++ str "”: “"
-          ++ Termops.Internal.print_constr_env env evd (EConstr.of_constr ty)
-          ++ str "” is not a class")
-    )
-
-let declare_instance ?(warn = false) info local glob =
-  let ty, _ = Typeops.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 Evd.empty (EConstr.of_constr ty) with
-    | Some (rels, ((tc,_), args) as _cl) ->
-      assert (not (isVarRef glob) || local);
-      add_instance (new_instance tc info (not local) glob)
-    | None -> if warn then warning_not_a_class (glob, ty)
-
-let add_class cl =
-  add_class cl;
-  List.iter (fun (n, inst, body) ->
-      match inst with
-      | Some (Backward, info) ->
-        (match body with
-         | None -> CErrors.user_err Pp.(str "Non-definable projection can not be declared as a subinstance")
-         | Some b -> declare_instance ~warn:true (Some info) false (ConstRef b))
-      | _ -> ())
-    cl.cl_projs
-
-
-(*
- * interface functions
- *)
 
 let instance_constructor (cl,u) args =
   let lenpars = List.count is_local_assum (snd cl.cl_context) in
@@ -497,8 +268,8 @@ let all_instances () =
     GlobRef.Map.fold (fun k v acc -> v :: acc) v acc)
     !instances []
 
-let instances r = 
-  let cl = class_info r in instances_of cl    
+let instances env sigma r =
+  let cl = class_info env sigma r in instances_of cl
 
 let is_class gr = 
   GlobRef.Map.exists (fun _ v -> GlobRef.equal v.cl_impl gr) !classes
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index f8aedf88c2..e42b82c51f 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -9,7 +9,6 @@
 (************************************************************************)
 
 open Names
-open Globnames
 open Constr
 open Evd
 open Environ
@@ -54,19 +53,25 @@ type typeclass = {
       no backtracking and sharing of resolution. *)
 }
 
-type instance
+type instance = {
+  is_class: GlobRef.t;
+  is_info: hint_info;
+  (* Sections where the instance should be redeclared,
+     None for discard, Some 0 for none. *)
+  is_global: int option;
+  is_impl: GlobRef.t;
+}
 
-val instances : GlobRef.t -> instance list
+val instances : env -> evar_map -> GlobRef.t -> instance list
 val typeclasses : unit -> typeclass list
 val all_instances : unit -> instance list
 
-val add_class : typeclass -> unit
+val load_class : typeclass -> unit
 
-val new_instance : typeclass -> hint_info -> bool -> GlobRef.t -> instance
-val add_instance : instance -> unit
+val load_instance : instance -> unit
 val remove_instance : instance -> unit
 
-val class_info : GlobRef.t -> typeclass (** raises a UserError if not a class *)
+val class_info : env -> evar_map -> GlobRef.t -> typeclass (** raises a UserError if not a class *)
 
 
 (** These raise a UserError if not a class.
@@ -78,7 +83,8 @@ val dest_class_app : env -> evar_map -> EConstr.constr -> (typeclass * EConstr.E
 val typeclass_univ_instance : typeclass Univ.puniverses -> typeclass
 
 (** Just return None if not a class *)
-val class_of_constr : evar_map -> EConstr.constr -> (EConstr.rel_context * ((typeclass * EConstr.EInstance.t) * constr list)) option
+val class_of_constr : env -> evar_map -> EConstr.constr ->
+  (EConstr.rel_context * ((typeclass * EConstr.EInstance.t) * constr list)) option
 
 val instance_impl : instance -> GlobRef.t
 
@@ -122,23 +128,9 @@ val set_typeclass_transparency : evaluable_global_reference -> bool -> bool -> u
 val classes_transparent_state_hook : (unit -> TransparentState.t) Hook.t
 val classes_transparent_state : unit -> TransparentState.t
 
-val add_instance_hint_hook :
-  (global_reference_or_constr -> GlobRef.t list ->
-   bool (* local? *) -> hint_info -> Decl_kinds.polymorphic -> unit) Hook.t
-val remove_instance_hint_hook : (GlobRef.t -> unit) Hook.t
-val add_instance_hint : global_reference_or_constr -> GlobRef.t list ->
-  bool -> hint_info -> Decl_kinds.polymorphic -> unit
-val remove_instance_hint : GlobRef.t -> unit
-
 val solve_all_instances_hook : (env -> evar_map -> evar_filter -> bool -> bool -> bool -> evar_map) Hook.t
 val solve_one_instance_hook : (env -> evar_map -> EConstr.types -> bool -> evar_map * EConstr.constr) Hook.t
 
-(** Declares the given global reference as an instance of its type.
-    Does nothing — or emit a “not-a-class” warning if the [warn] argument is set —
-    when said type is not a registered type class. *)
-val declare_instance : ?warn:bool -> hint_info option -> bool -> GlobRef.t -> unit
-
-
 (** Build the subinstances hints for a given typeclass object.
     check tells if we should check for existence of the 
     subinstances and add only the missing ones. *)