diff options
| -rw-r--r-- | interp/implicit_quantifiers.ml | 36 | ||||
| -rw-r--r-- | plugins/ltac/rewrite.ml | 66 | ||||
| -rw-r--r-- | pretyping/classops.ml | 42 | ||||
| -rw-r--r-- | pretyping/classops.mli | 2 | ||||
| -rw-r--r-- | pretyping/typeclasses.ml | 253 | ||||
| -rw-r--r-- | pretyping/typeclasses.mli | 36 | ||||
| -rw-r--r-- | printing/prettyp.ml | 3 | ||||
| -rw-r--r-- | tactics/class_tactics.ml | 4 | ||||
| -rw-r--r-- | vernac/class.ml | 4 | ||||
| -rw-r--r-- | vernac/classes.ml | 328 | ||||
| -rw-r--r-- | vernac/classes.mli | 22 | ||||
| -rw-r--r-- | vernac/comAssumption.ml | 102 | ||||
| -rw-r--r-- | vernac/comAssumption.mli | 20 | ||||
| -rw-r--r-- | vernac/himsg.ml | 4 | ||||
| -rw-r--r-- | vernac/record.ml | 25 | ||||
| -rw-r--r-- | vernac/vernac.mllib | 2 | ||||
| -rw-r--r-- | vernac/vernacentries.ml | 2 |
17 files changed, 476 insertions, 475 deletions
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml index 854651e7b7..dffccf02fc 100644 --- a/interp/implicit_quantifiers.ml +++ b/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" diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 75565c1a34..2d40ba6562 100644 --- a/plugins/ltac/rewrite.ml +++ b/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 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. *) diff --git a/printing/prettyp.ml b/printing/prettyp.ml index 8bf86e9ef6..9541ea5882 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -952,5 +952,6 @@ let print_all_instances () = let print_instances r = let env = Global.env () in - let inst = instances r in + let sigma = Evd.from_env env in + let inst = instances env sigma r in prlist_with_sep fnl (pr_instance env) inst diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index a28f4597cf..c1ac7d201a 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -362,7 +362,7 @@ and e_my_find_search db_list local_db secvars hdc complete only_classes env sigm try match hdc with | Some (hd,_) when only_classes -> - let cl = Typeclasses.class_info hd in + let cl = Typeclasses.class_info env sigma hd in if cl.cl_strict then Evarutil.undefined_evars_of_term sigma concl else Evar.Set.empty @@ -1052,7 +1052,7 @@ let error_unresolvable env comp evd = | Some s -> Evar.Set.mem ev s in let fold ev evi (found, accu) = - let ev_class = class_of_constr evd evi.evar_concl in + let ev_class = class_of_constr env evd evi.evar_concl in if not (Option.is_empty ev_class) && is_part ev then (* focus on one instance if only one was searched for *) if not found then (true, Some ev) diff --git a/vernac/class.ml b/vernac/class.ml index eb01e82b83..f3a279eab1 100644 --- a/vernac/class.ml +++ b/vernac/class.ml @@ -232,7 +232,9 @@ let check_source = function | _ -> () let cache_coercion (_,c) = - Classops.declare_coercion c + let env = Global.env () in + let sigma = Evd.from_env env in + Classops.declare_coercion env sigma c let open_coercion i o = if Int.equal i 1 then diff --git a/vernac/classes.ml b/vernac/classes.ml index d61d324941..9f233a2551 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -22,8 +22,10 @@ open Constrintern open Constrexpr open Context.Rel.Declaration open Class_tactics +open Libobject module RelDecl = Context.Rel.Declaration +module NamedDecl = Context.Named.Declaration (*i*) open Decl_kinds @@ -49,17 +51,224 @@ let classes_transparent_state () = with Not_found -> TransparentState.empty let () = - Hook.set Typeclasses.add_instance_hint_hook - (fun inst path local info poly -> + Hook.set Typeclasses.set_typeclass_transparency_hook set_typeclass_transparency; + Hook.set Typeclasses.classes_transparent_state_hook classes_transparent_state + +let add_instance_hint inst path local info poly = let inst' = match inst with IsConstr c -> Hints.IsConstr (EConstr.of_constr c, Univ.ContextSet.empty) | IsGlobal gr -> Hints.IsGlobRef gr in Flags.silently (fun () -> Hints.add_hints ~local [typeclasses_db] (Hints.HintsResolveEntry - [info, poly, false, Hints.PathHints path, inst'])) ()); - Hook.set Typeclasses.set_typeclass_transparency_hook set_typeclass_transparency; - Hook.set Typeclasses.classes_transparent_state_hook classes_transparent_state + [info, poly, false, Hints.PathHints path, inst'])) () + +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 mk_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 } + +(* + * instances persistent object + *) +let cache_instance (_, i) = + load_instance i + +let subst_instance (subst, inst) = + { inst with + is_class = fst (subst_global subst inst.is_class); + is_impl = fst (subst_global subst inst.is_impl) } + +let discharge_instance (_, inst) = + match inst.is_global with + | None -> None + | Some n -> + assert (not (isVarRef inst.is_impl)); + Some + { 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 rebuild_instance inst = + add_instance true inst; + inst + +let classify_instance inst = + if is_local inst then Dispose + else Substitute inst + +let instance_input : 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 i); + add_instance true i + +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) env sigma info local glob = + let ty, _ = Typeops.type_of_global_in_context env glob in + let info = Option.default {hint_priority = None; hint_pattern = None} info in + match class_of_constr env sigma (EConstr.of_constr ty) with + | Some (rels, ((tc,_), args) as _cl) -> + assert (not (isVarRef glob) || local); + add_instance (mk_instance tc info (not local) glob) + | None -> if warn then warning_not_a_class (glob, ty) + +(* + * classes persistent object + *) + +let cache_class (_,c) = load_class c + +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 open CVars in + 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 env = Global.env () in + let sigma = Evd.from_env env in + let grs' = + let newgrs = List.map (fun decl -> + match decl |> RelDecl.get_type |> EConstr.of_constr |> class_of_constr env sigma 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 _ -> cache_class); + open_function = (fun _ -> cache_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) + +let add_class env sigma 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 env sigma (Some info) false (ConstRef b)) + | _ -> ()) + cl.cl_projs let intern_info {hint_priority;hint_pattern} = let env = Global.env() in @@ -72,10 +281,12 @@ let existing_instance glob g info = let c = Nametab.global g in let info = Option.default Hints.empty_hint_info info in let info = intern_info info in - let instance, _ = Typeops.type_of_global_in_context (Global.env ()) c in + let env = Global.env() in + let sigma = Evd.from_env env in + let instance, _ = Typeops.type_of_global_in_context env c in let _, r = Term.decompose_prod_assum instance in - match class_of_constr Evd.empty (EConstr.of_constr r) with - | Some (_, ((tc,u), _)) -> add_instance (new_instance tc info glob c) + match class_of_constr env sigma (EConstr.of_constr r) with + | Some (_, ((tc,u), _)) -> add_instance (mk_instance tc info glob c) | None -> user_err ?loc:g.CAst.loc ~hdr:"declare_instance" (Pp.str "Constant does not build instances of a declared type class.") @@ -111,7 +322,9 @@ let id_of_class cl = let instance_hook k info global imps ?hook cst = Impargs.maybe_declare_manual_implicits false cst imps; let info = intern_info info in - Typeclasses.declare_instance (Some info) (not global) cst; + let env = Global.env () in + let sigma = Evd.from_env env in + declare_instance env sigma (Some info) (not global) cst; (match hook with Some h -> h cst | None -> ()) let declare_instance_constant k info global imps ?hook id decl poly sigma term termtype = @@ -154,7 +367,9 @@ let declare_instance_open ~pstate env sigma ?hook ~tac ~program_mode ~global ~po let cst = match gr with ConstRef kn -> kn | _ -> assert false in Impargs.declare_manual_implicits false gr imps; let pri = intern_info pri in - Typeclasses.declare_instance (Some pri) (not global) (ConstRef cst) + let env = Global.env () in + let sigma = Evd.from_env env in + declare_instance env sigma (Some pri) (not global) (ConstRef cst) in let obls, constr, typ = match term with @@ -360,96 +575,3 @@ let declare_new_instance ?(global=false) ~program_mode poly ctx (instid, bk, cl) interp_instance_context ~program_mode env ctx pl bk cl in do_declare_instance env sigma ~global ~poly k u ctx ctx' pri decl imps subst instid - -let named_of_rel_context l = - let open Vars in - let acc, ctx = - List.fold_right - (fun decl (subst, ctx) -> - let id = match RelDecl.get_name decl with Anonymous -> invalid_arg "named_of_rel_context" | Name id -> id in - let d = match decl with - | LocalAssum (_,t) -> id, None, substl subst t - | LocalDef (_,b,t) -> id, Some (substl subst b), substl subst t in - (mkVar id :: subst, d :: ctx)) - l ([], []) - in ctx - -let context ~pstate poly l = - let env = Global.env() in - let sigma = Evd.from_env env in - let sigma, (_, ((env', fullctx), impls)) = interp_context_evars ~program_mode:false env sigma l in - (* Note, we must use the normalized evar from now on! *) - let sigma = Evd.minimize_universes sigma in - let ce t = Pretyping.check_evars env (Evd.from_env env) sigma t in - let () = List.iter (fun decl -> Context.Rel.Declaration.iter_constr ce decl) fullctx in - let ctx = - try named_of_rel_context fullctx - with e when CErrors.noncritical e -> - user_err Pp.(str "Anonymous variables not allowed in contexts.") - in - let univs = - match ctx with - | [] -> assert false - | [_] -> Evd.univ_entry ~poly sigma - | _::_::_ -> - if Lib.sections_are_opened () - then - (* More than 1 variable in a section: we can't associate - universes to any specific variable so we declare them - separately. *) - begin - let uctx = Evd.universe_context_set sigma in - Declare.declare_universe_context poly uctx; - if poly then Polymorphic_entry ([||], Univ.UContext.empty) - else Monomorphic_entry Univ.ContextSet.empty - end - else if poly then - (* Multiple polymorphic axioms: they are all polymorphic the same way. *) - Evd.univ_entry ~poly sigma - else - (* Multiple monomorphic axioms: declare universes separately - to avoid redeclaring them. *) - begin - let uctx = Evd.universe_context_set sigma in - Declare.declare_universe_context poly uctx; - Monomorphic_entry Univ.ContextSet.empty - end - in - let fn status (id, b, t) = - let b, t = Option.map (to_constr sigma) b, to_constr sigma t in - if Lib.is_modtype () && not (Lib.sections_are_opened ()) then - (* Declare the universe context once *) - let decl = match b with - | None -> - (ParameterEntry (None,(t,univs),None), IsAssumption Logical) - | Some b -> - let entry = Declare.definition_entry ~univs ~types:t b in - (DefinitionEntry entry, IsAssumption Logical) - in - let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest id decl in - match class_of_constr sigma (of_constr t) with - | Some (rels, ((tc,_), args) as _cl) -> - add_instance (Typeclasses.new_instance tc Hints.empty_hint_info false (ConstRef cst)); - status - (* declare_subclasses (ConstRef cst) cl *) - | None -> status - else - let test (x, _) = match x with - | ExplByPos (_, Some id') -> Id.equal id id' - | _ -> false - in - let impl = List.exists test impls in - let decl = (Discharge, poly, Definitional) in - let nstatus = match b with - | None -> - pi3 (ComAssumption.declare_assumption ~pstate false decl (t, univs) UnivNames.empty_binders [] impl - Declaremods.NoInline (CAst.make id)) - | Some b -> - let decl = (Discharge, poly, Definition) in - let entry = Declare.definition_entry ~univs ~types:t b in - let _gr = DeclareDef.declare_definition ~ontop:pstate id decl entry UnivNames.empty_binders [] in - Lib.sections_are_opened () || Lib.is_modtype_strict () - in - status && nstatus - in - List.fold_left fn true (List.rev ctx) diff --git a/vernac/classes.mli b/vernac/classes.mli index 73e4b024ef..e7f90ff306 100644 --- a/vernac/classes.mli +++ b/vernac/classes.mli @@ -22,6 +22,12 @@ val mismatched_props : env -> constr_expr list -> Constr.rel_context -> 'a (** Instance declaration *) +val declare_instance : ?warn:bool -> env -> Evd.evar_map -> + hint_info option -> bool -> GlobRef.t -> unit +(** 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 existing_instance : bool -> qualid -> Hints.hint_info_expr option -> unit (** globality, reference, optional priority and pattern information *) @@ -64,6 +70,12 @@ val declare_new_instance : Hints.hint_info_expr -> unit +(** {6 Low level interface used by Add Morphism, do not use } *) +val mk_instance : typeclass -> hint_info -> bool -> GlobRef.t -> instance +val add_instance : instance -> unit + +val add_class : env -> Evd.evar_map -> typeclass -> unit + (** Setting opacity *) val set_typeclass_transparency : evaluable_global_reference -> bool -> bool -> unit @@ -71,13 +83,3 @@ val set_typeclass_transparency : evaluable_global_reference -> bool -> bool -> u (** For generation on names based on classes only *) val id_of_class : typeclass -> Id.t - -(** Context command *) - -(** returns [false] if, for lack of section, it declares an assumption - (unless in a module type). *) -val context - : pstate:Proof_global.t option - -> Decl_kinds.polymorphic - -> local_binder_expr list - -> bool diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml index d7bd64067b..3406b6276f 100644 --- a/vernac/comAssumption.ml +++ b/vernac/comAssumption.ml @@ -22,6 +22,7 @@ open Decl_kinds open Pretyping open Entries +module RelDecl = Context.Rel.Declaration (* 2| Variable/Hypothesis/Parameter/Axiom declarations *) let axiom_into_instance = ref false @@ -59,7 +60,9 @@ match local with in let r = VarRef ident in let () = maybe_declare_manual_implicits true r imps in - let () = Typeclasses.declare_instance None true r in + let env = Global.env () in + let sigma = Evd.from_env env in + let () = Classes.declare_instance env sigma None true r in let () = if is_coe then Class.try_add_new_coercion r ~local:true false in (r,Univ.Instance.empty,true) @@ -77,7 +80,9 @@ match local with let () = maybe_declare_manual_implicits false gr imps in let () = Declare.declare_univ_binders gr pl in let () = assumption_message ident in - let () = if do_instance then Typeclasses.declare_instance None false gr in + let env = Global.env () in + let sigma = Evd.from_env env in + let () = if do_instance then Classes.declare_instance env sigma None false gr in let () = if is_coe then Class.try_add_new_coercion gr ~local p in let inst = match ctx with | Polymorphic_entry (_, ctx) -> Univ.UContext.instance ctx @@ -173,7 +178,7 @@ let do_assumptions ~pstate ~program_mode kind nl l = let ubinders = Evd.universe_binders sigma in pi2 (List.fold_left (fun (subst,status,uctx) ((is_coe,idl),t,imps) -> let t = replace_vars subst t in - let refs, status' = declare_assumptions ~pstate idl is_coe kind (t,uctx) ubinders imps nl in + let refs, status' = declare_assumptions ~pstate idl is_coe kind (t,uctx) ubinders imps nl in let subst' = List.map2 (fun {CAst.v=id} (c,u) -> (id, Constr.mkRef (c,u))) idl refs @@ -206,3 +211,94 @@ let do_primitive id prim typopt = in let _kn = declare_constant id.CAst.v (PrimitiveEntry entry,IsPrimitive) in Flags.if_verbose Feedback.msg_info Pp.(Id.print id.CAst.v ++ str " is declared") + +let named_of_rel_context l = + let open EConstr.Vars in + let open RelDecl in + let acc, ctx = + List.fold_right + (fun decl (subst, ctx) -> + let id = match get_name decl with Anonymous -> invalid_arg "named_of_rel_context" | Name id -> id in + let d = match decl with + | LocalAssum (_,t) -> id, None, substl subst t + | LocalDef (_,b,t) -> id, Some (substl subst b), substl subst t in + (EConstr.mkVar id :: subst, d :: ctx)) + l ([], []) + in ctx + +let context ~pstate poly l = + let env = Global.env() in + let sigma = Evd.from_env env in + let sigma, (_, ((env', fullctx), impls)) = interp_context_evars ~program_mode:false env sigma l in + (* Note, we must use the normalized evar from now on! *) + let sigma = Evd.minimize_universes sigma in + let ce t = Pretyping.check_evars env (Evd.from_env env) sigma t in + let () = List.iter (fun decl -> Context.Rel.Declaration.iter_constr ce decl) fullctx in + let ctx = + try named_of_rel_context fullctx + with e when CErrors.noncritical e -> + user_err Pp.(str "Anonymous variables not allowed in contexts.") + in + let univs = + match ctx with + | [] -> assert false + | [_] -> Evd.univ_entry ~poly sigma + | _::_::_ -> + if Lib.sections_are_opened () + then + (* More than 1 variable in a section: we can't associate + universes to any specific variable so we declare them + separately. *) + begin + let uctx = Evd.universe_context_set sigma in + Declare.declare_universe_context poly uctx; + if poly then Polymorphic_entry ([||], Univ.UContext.empty) + else Monomorphic_entry Univ.ContextSet.empty + end + else if poly then + (* Multiple polymorphic axioms: they are all polymorphic the same way. *) + Evd.univ_entry ~poly sigma + else + (* Multiple monomorphic axioms: declare universes separately + to avoid redeclaring them. *) + begin + let uctx = Evd.universe_context_set sigma in + Declare.declare_universe_context poly uctx; + Monomorphic_entry Univ.ContextSet.empty + end + in + let fn status (id, b, t) = + let b, t = Option.map (EConstr.to_constr sigma) b, EConstr.to_constr sigma t in + if Lib.is_modtype () && not (Lib.sections_are_opened ()) then + (* Declare the universe context once *) + let decl = match b with + | None -> + (ParameterEntry (None,(t,univs),None), IsAssumption Logical) + | Some b -> + let entry = Declare.definition_entry ~univs ~types:t b in + (DefinitionEntry entry, IsAssumption Logical) + in + let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest id decl in + let env = Global.env () in + Classes.declare_instance env sigma (Some Hints.empty_hint_info) true (ConstRef cst); + status + else + let test (x, _) = match x with + | Constrexpr.ExplByPos (_, Some id') -> Id.equal id id' + | _ -> false + in + let impl = List.exists test impls in + let decl = (Discharge, poly, Definitional) in + let nstatus = match b with + | None -> + pi3 (declare_assumption ~pstate false decl (t, univs) UnivNames.empty_binders [] impl + Declaremods.NoInline (CAst.make id)) + | Some b -> + let decl = (Discharge, poly, Definition) in + let entry = Declare.definition_entry ~univs ~types:t b in + let _gr = DeclareDef.declare_definition ~ontop:pstate id decl entry UnivNames.empty_binders [] in + Lib.sections_are_opened () || Lib.is_modtype_strict () + in + status && nstatus + in + List.fold_left fn true (List.rev ctx) diff --git a/vernac/comAssumption.mli b/vernac/comAssumption.mli index 32914cc11b..7c64317b70 100644 --- a/vernac/comAssumption.mli +++ b/vernac/comAssumption.mli @@ -9,8 +9,6 @@ (************************************************************************) open Names -open Constr -open Entries open Vernacexpr open Constrexpr open Decl_kinds @@ -25,19 +23,13 @@ val do_assumptions -> (ident_decl list * constr_expr) with_coercion list -> bool -(************************************************************************) -(** Internal API *) -(************************************************************************) - -(** Exported for Classes *) - (** returns [false] if the assumption is neither local to a section, nor in a module type and meant to be instantiated. *) val declare_assumption : pstate:Proof_global.t option -> coercion_flag -> assumption_kind - -> types in_universes_entry + -> Constr.types Entries.in_universes_entry -> UnivNames.universe_binders -> Impargs.manual_implicits -> bool (** implicit *) @@ -45,4 +37,14 @@ val declare_assumption -> variable CAst.t -> GlobRef.t * Univ.Instance.t * bool +(** Context command *) + +(** returns [false] if, for lack of section, it declares an assumption + (unless in a module type). *) +val context + : pstate:Proof_global.t option + -> Decl_kinds.polymorphic + -> local_binder_expr list + -> bool + val do_primitive : lident -> CPrimitives.op_or_type -> constr_expr option -> unit diff --git a/vernac/himsg.ml b/vernac/himsg.ml index d329b81341..082b22b373 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -601,7 +601,7 @@ let rec explain_evar_kind env sigma evk ty = (pr_leconstr_env env sigma ty') src let explain_typeclass_resolution env sigma evi k = - match Typeclasses.class_of_constr sigma evi.evar_concl with + match Typeclasses.class_of_constr env sigma evi.evar_concl with | Some _ -> let env = Evd.evar_filtered_env evi in fnl () ++ str "Could not find an instance for " ++ @@ -614,7 +614,7 @@ let explain_placeholder_kind env sigma c e = | Some (SeveralInstancesFound n) -> strbrk " (several distinct possible type class instances found)" | None -> - match Typeclasses.class_of_constr sigma c with + match Typeclasses.class_of_constr env sigma c with | Some _ -> strbrk " (no type class instance found)" | _ -> mt () diff --git a/vernac/record.ml b/vernac/record.ml index cb67548667..a7c5318f11 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -520,8 +520,10 @@ let declare_class def cum ubinders univs id idbuild paramimpls params arity List.map map inds in let ctx_context = + let env = Global.env () in + let sigma = Evd.from_env env in List.map (fun decl -> - match Typeclasses.class_of_constr Evd.empty (EConstr.of_constr (RelDecl.get_type decl)) with + match Typeclasses.class_of_constr env sigma (EConstr.of_constr (RelDecl.get_type decl)) with | Some (_, ((cl,_), _)) -> Some cl.cl_impl | None -> None) params, params @@ -548,12 +550,14 @@ let declare_class def cum ubinders univs id idbuild paramimpls params arity cl_props = fields; cl_projs = projs } in - add_class k; impl + let env = Global.env () in + let sigma = Evd.from_env env in + Classes.add_class env sigma k; impl in List.map map data -let add_constant_class env cst = +let add_constant_class env sigma cst = let ty, univs = Typeops.type_of_global_in_context env (ConstRef cst) in let r = (Environ.lookup_constant cst env).const_relevance in let ctx, arity = decompose_prod_assum ty in @@ -566,10 +570,11 @@ let add_constant_class env cst = cl_strict = !typeclasses_strict; cl_unique = !typeclasses_unique } - in add_class tc; + in + Classes.add_class env sigma tc; set_typeclass_transparency (EvalConstRef cst) false false - -let add_inductive_class env ind = + +let add_inductive_class env sigma ind = let mind, oneind = Inductive.lookup_mind_specif env ind in let k = let ctx = oneind.mind_arity_ctxt in @@ -586,7 +591,8 @@ let add_inductive_class env ind = cl_projs = []; cl_strict = !typeclasses_strict; cl_unique = !typeclasses_unique } - in add_class k + in + Classes.add_class env sigma k let warn_already_existing_class = CWarnings.create ~name:"already-existing-class" ~category:"automation" Pp.(fun g -> @@ -594,11 +600,12 @@ let warn_already_existing_class = let declare_existing_class g = let env = Global.env () in + let sigma = Evd.from_env env in if Typeclasses.is_class g then warn_already_existing_class g else match g with - | ConstRef x -> add_constant_class env x - | IndRef x -> add_inductive_class env x + | ConstRef x -> add_constant_class env sigma x + | IndRef x -> add_inductive_class env sigma x | _ -> user_err ~hdr:"declare_existing_class" (Pp.str"Unsupported class type, only constants and inductives are allowed") diff --git a/vernac/vernac.mllib b/vernac/vernac.mllib index ce93a8baaf..3ee785413c 100644 --- a/vernac/vernac.mllib +++ b/vernac/vernac.mllib @@ -21,11 +21,11 @@ Indschemes DeclareDef Obligations ComDefinition +Classes ComAssumption ComInductive ComFixpoint ComProgramFixpoint -Classes Record Assumptions Vernacstate diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 02db75c0f9..7ef3777445 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1075,7 +1075,7 @@ let vernac_declare_instance ~atts sup inst pri = Classes.declare_new_instance ~program_mode:atts.program ~global atts.polymorphic sup inst pri let vernac_context ~pstate ~poly l = - if not (Classes.context ~pstate poly l) then Feedback.feedback Feedback.AddedAxiom + if not (ComAssumption.context ~pstate poly l) then Feedback.feedback Feedback.AddedAxiom let vernac_existing_instance ~section_local insts = let glob = not section_local in |