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.

1 files changed, 12 insertions, 241 deletions

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