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.

interp/implicit_quantifiers.ml

@@ -231,23 +231,25 @@ let implicit_application env ?(allow_partial=true) f ty =
     | Some ({CAst.loc;v=(id, par, inst)}, gr) ->
 	let avoid = Id.Set.union env (ids_of_list (free_vars_of_constr_expr ty ~bound:env [])) in
 	let c, avoid =
-	  let c = class_info gr in
-	  let (ci, rd) = c.cl_context in
-	  if not allow_partial then
-	    begin
-              let opt_succ x n = match x with
-              | None -> succ n
-              | Some _ -> n
-              in
-	      let applen = List.fold_left (fun acc (x, y) -> opt_succ y acc) 0 par in
-	      let needlen = List.fold_left (fun acc x -> opt_succ x acc) 0 ci in
-		if not (Int.equal needlen applen) then
-                  mismatched_ctx_inst_err (Global.env ()) Typeclasses_errors.Parameters (List.map fst par) rd
-	    end;
-	  let pars = List.rev (List.combine ci rd) in
-	  let args, avoid = combine_params avoid f par pars in
-	    CAst.make ?loc @@ CAppExpl ((None, id, inst), args), avoid
-	in c, avoid
+   let env = Global.env () in
+   let sigma = Evd.from_env env in
+   let c = class_info env sigma gr in
+   let (ci, rd) = c.cl_context in
+   if not allow_partial then
+     begin
+       let opt_succ x n = match x with
+         | None -> succ n
+         | Some _ -> n
+       in
+       let applen = List.fold_left (fun acc (x, y) -> opt_succ y acc) 0 par in
+       let needlen = List.fold_left (fun acc x -> opt_succ x acc) 0 ci in
+       if not (Int.equal needlen applen) then
+         mismatched_ctx_inst_err (Global.env ()) Typeclasses_errors.Parameters (List.map fst par) rd
+     end;
+   let pars = List.rev (List.combine ci rd) in
+   let args, avoid = combine_params avoid f par pars in
+   CAst.make ?loc @@ CAppExpl ((None, id, inst), args), avoid
+ in c, avoid
 
 let warn_ignoring_implicit_status =
   CWarnings.create ~name:"ignoring_implicit_status" ~category:"implicits"

plugins/ltac/rewrite.ml

@@ -119,7 +119,7 @@ let app_poly_check env evars f args =
   (evars, cstrs), t
 
 let app_poly_nocheck env evars f args =
-  let evars, fc = f evars in 
+  let evars, fc = f evars in
     evars, mkApp (fc, args)
 
 let app_poly_sort b =
@@ -175,25 +175,29 @@ end) = struct
 
   let rewrite_relation_class = find_global relation_classes "RewriteRelation"
 
-  let proper_class = lazy (class_info (find_reference morphisms "Proper"))
-  let proper_proxy_class = lazy (class_info (find_reference morphisms "ProperProxy"))
-
-  let proper_proj = lazy (mkConst (Option.get (pi3 (List.hd (Lazy.force proper_class).cl_projs))))
-
-  let proper_type = 
-    let l = lazy (Lazy.force proper_class).cl_impl in
-      fun (evd,cstrs) -> 
-        let (evd, c) = Evarutil.new_global evd (Lazy.force l) in
-	  (evd, cstrs), c
-
-  let proper_proxy_type = 
-    let l = lazy (Lazy.force proper_proxy_class).cl_impl in
-      fun (evd,cstrs) -> 
-        let (evd, c) = Evarutil.new_global evd (Lazy.force l) in
-	  (evd, cstrs), c
+  let proper_class =
+    let r = lazy (find_reference morphisms "Proper") in
+    fun env sigma -> class_info env sigma (Lazy.force r)
+
+  let proper_proxy_class =
+    let r = lazy (find_reference morphisms "ProperProxy") in
+    fun env sigma -> class_info env sigma (Lazy.force r)
+
+  let proper_proj env sigma =
+    mkConst (Option.get (pi3 (List.hd (proper_class env sigma).cl_projs)))
+
+  let proper_type env (sigma,cstrs) =
+    let l = (proper_class env sigma).cl_impl in
+    let (sigma, c) = Evarutil.new_global sigma l in
+    (sigma, cstrs), c
+
+  let proper_proxy_type env (sigma,cstrs) =
+    let l = (proper_proxy_class env sigma).cl_impl in
+    let (sigma, c) = Evarutil.new_global sigma l in
+    (sigma, cstrs), c
 
   let proper_proof env evars carrier relation x =
-    let evars, goal = app_poly env evars proper_proxy_type [| carrier ; relation; x |] in
+    let evars, goal = app_poly env evars (proper_proxy_type env) [| carrier ; relation; x |] in
       new_cstr_evar evars env goal
 
   let get_reflexive_proof env = find_class_proof reflexive_type reflexive_proof env
@@ -800,7 +804,7 @@ let resolve_morphism env avoid oldt m ?(fnewt=fun x -> x) args args' (b,cstr) ev
     in
       (* Actual signature found *)
     let cl_args = [| appmtype' ; signature ; appm |] in
-    let evars, app = app_poly_sort b env evars (if b then PropGlobal.proper_type else TypeGlobal.proper_type)
+    let evars, app = app_poly_sort b env evars (if b then PropGlobal.proper_type env else TypeGlobal.proper_type env)
       cl_args in
     let env' = 
       let dosub, appsub = 
@@ -1310,8 +1314,8 @@ module Strategies =
 	in
 	let evars, proof =
 	  let proxy = 
-	    if prop then PropGlobal.proper_proxy_type 
-	    else TypeGlobal.proper_proxy_type
+            if prop then PropGlobal.proper_proxy_type env
+            else TypeGlobal.proper_proxy_type env
 	  in
 	  let evars, mty = app_poly_sort prop env evars proxy [| ty ; rel; t |] in
 	    new_cstr_evar evars env mty
@@ -1854,12 +1858,12 @@ let declare_relation ~pstate atts ?(binders=[]) a aeq n refl symm trans =
 
 let cHole = CAst.make @@ CHole (None, Namegen.IntroAnonymous, None)
 
-let proper_projection sigma r ty =
+let proper_projection env sigma r ty =
   let rel_vect n m = Array.init m (fun i -> mkRel(n+m-i)) in
   let ctx, inst = decompose_prod_assum sigma ty in
   let mor, args = destApp sigma inst in
   let instarg = mkApp (r, rel_vect 0 (List.length ctx)) in
-  let app = mkApp (Lazy.force PropGlobal.proper_proj,
+  let app = mkApp (PropGlobal.proper_proj env sigma,
 		  Array.append args [| instarg |]) in
     it_mkLambda_or_LetIn app ctx
 
@@ -1869,7 +1873,7 @@ let declare_projection n instance_id r =
   let sigma = Evd.from_env env in
   let sigma,c = Evd.fresh_global env sigma r in
   let ty = Retyping.get_type_of env sigma c in
-  let term = proper_projection sigma c ty in
+  let term = proper_projection env sigma c ty in
   let sigma, typ = Typing.type_of env sigma term in
   let ctx, typ = decompose_prod_assum sigma typ in
   let typ =
@@ -1924,7 +1928,7 @@ let build_morphism_signature env sigma m =
 	rel)
     cstrs
   in
-  let morph = e_app_poly env evd PropGlobal.proper_type [| t; sig_; m |] in
+  let morph = e_app_poly env evd (PropGlobal.proper_type env) [| t; sig_; m |] in
   let evd = solve_constraints env !evd in
   let evd = Evd.minimize_universes evd in
   let m = Evarutil.nf_evars_universes evd (EConstr.Unsafe.to_constr morph) in
@@ -1938,9 +1942,9 @@ let default_morphism sign m =
   let evars, _, sign, cstrs =
     PropGlobal.build_signature (sigma, Evar.Set.empty) env t (fst sign) (snd sign)
   in
-  let evars, morph = app_poly_check env evars PropGlobal.proper_type [| t; sign; m |] in
+  let evars, morph = app_poly_check env evars (PropGlobal.proper_type env) [| t; sign; m |] in
   let evars, mor = resolve_one_typeclass env (goalevars evars) morph in
-    mor, proper_projection sigma mor morph
+    mor, proper_projection env sigma mor morph
 
 let warn_add_setoid_deprecated =
   CWarnings.create ~name:"add-setoid" ~category:"deprecated" (fun () ->
@@ -1984,8 +1988,8 @@ let add_morphism_infer ~pstate atts m n : Proof_global.t option =
              (None,(instance,uctx),None),
            Decl_kinds.IsAssumption Decl_kinds.Logical)
       in
-      add_instance (Typeclasses.new_instance
-                      (Lazy.force PropGlobal.proper_class) Hints.empty_hint_info atts.global (ConstRef cst));
+      add_instance (Classes.mk_instance
+                      (PropGlobal.proper_class env evd) Hints.empty_hint_info atts.global (ConstRef cst));
       declare_projection n instance_id (ConstRef cst);
       pstate
     else
@@ -1995,8 +1999,8 @@ let add_morphism_infer ~pstate atts m n : Proof_global.t option =
       let tac = make_tactic "Coq.Classes.SetoidTactics.add_morphism_tactic" in
       let hook _ _ _ = function
         | Globnames.ConstRef cst ->
-          add_instance (Typeclasses.new_instance
-                          (Lazy.force PropGlobal.proper_class) Hints.empty_hint_info
+          add_instance (Classes.mk_instance
+                          (PropGlobal.proper_class env evd) Hints.empty_hint_info
                           atts.global (ConstRef cst));
           declare_projection n instance_id (ConstRef cst)
         | _ -> assert false

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

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