diff options
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/classes.ml | 9 | ||||
| -rw-r--r-- | toplevel/classes.mli | 4 | ||||
| -rw-r--r-- | toplevel/record.ml | 51 | ||||
| -rw-r--r-- | toplevel/record.mli | 2 | ||||
| -rw-r--r-- | toplevel/vernacentries.ml | 2 |
5 files changed, 55 insertions, 13 deletions
diff --git a/toplevel/classes.ml b/toplevel/classes.ml index 3c29c5fcb..ad6c4236e 100644 --- a/toplevel/classes.ml +++ b/toplevel/classes.ml @@ -44,14 +44,7 @@ let _ = Hook.set Typeclasses.set_typeclass_transparency_hook set_typeclass_transparency; Hook.set Typeclasses.classes_transparent_state_hook (fun () -> Auto.Hint_db.transparent_state (Auto.searchtable_map typeclasses_db)) - -let declare_class g = - match global g with - | ConstRef x -> Typeclasses.add_constant_class x - | IndRef x -> Typeclasses.add_inductive_class x - | _ -> user_err_loc (loc_of_reference g, "declare_class", - Pp.str"Unsupported class type, only constants and inductives are allowed") - + (** TODO: add subinstances *) let existing_instance glob g pri = let c = global g in diff --git a/toplevel/classes.mli b/toplevel/classes.mli index 489f2aa5f..f0932c826 100644 --- a/toplevel/classes.mli +++ b/toplevel/classes.mli @@ -20,10 +20,6 @@ val mismatched_params : env -> constr_expr list -> rel_context -> 'a val mismatched_props : env -> constr_expr list -> rel_context -> 'a -(** Post-hoc class declaration. *) - -val declare_class : reference -> unit - (** Instance declaration *) val existing_instance : bool -> reference -> int option -> unit diff --git a/toplevel/record.ml b/toplevel/record.ml index d23338930..177aa1cd6 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -49,6 +49,16 @@ let _ = optread = (fun () -> !typeclasses_strict); optwrite = (fun b -> typeclasses_strict := b); } +let typeclasses_unique = ref false +let _ = + declare_bool_option + { optsync = true; + optdepr = false; + optname = "unique typeclass instances"; + optkey = ["Typeclasses";"Unique";"Instances"]; + optread = (fun () -> !typeclasses_unique); + optwrite = (fun b -> typeclasses_unique := b); } + let interp_fields_evars env evars impls_env nots l = List.fold_left2 (fun (env, uimpls, params, impls) no ((loc, i), b, t) -> @@ -431,6 +441,7 @@ let declare_class finite def poly ctx id idbuild paramimpls params arity fieldim let k = { cl_impl = impl; cl_strict = !typeclasses_strict; + cl_unique = !typeclasses_unique; cl_context = ctx_context; cl_props = fields; cl_projs = projs } @@ -440,6 +451,46 @@ let declare_class finite def poly ctx id idbuild paramimpls params arity fieldim (* k.cl_projs coers priorities; *) add_class k; impl + +let add_constant_class cst = + let ty = Universes.unsafe_type_of_global (ConstRef cst) in + let ctx, arity = decompose_prod_assum ty in + let tc = + { cl_impl = ConstRef cst; + cl_context = (List.map (const None) ctx, ctx); + cl_props = [(Anonymous, None, arity)]; + cl_projs = []; + cl_strict = !typeclasses_strict; + cl_unique = !typeclasses_unique + } + in add_class tc; + set_typeclass_transparency (EvalConstRef cst) false false + +let add_inductive_class ind = + let mind, oneind = Global.lookup_inductive ind in + let k = + let ctx = oneind.mind_arity_ctxt in + let inst = Univ.UContext.instance mind.mind_universes in + let ty = Inductive.type_of_inductive_knowing_parameters + (push_rel_context ctx (Global.env ())) + ((mind,oneind),inst) + (Array.map (fun x -> lazy x) (Termops.extended_rel_vect 0 ctx)) + in + { cl_impl = IndRef ind; + cl_context = List.map (const None) ctx, ctx; + cl_props = [Anonymous, None, ty]; + cl_projs = []; + cl_strict = !typeclasses_strict; + cl_unique = !typeclasses_unique } + in add_class k + +let declare_existing_class g = + match g with + | ConstRef x -> add_constant_class x + | IndRef x -> add_inductive_class x + | _ -> user_err_loc (Loc.dummy_loc, "declare_existing_class", + Pp.str"Unsupported class type, only constants and inductives are allowed") + open Vernacexpr (* [fs] corresponds to fields and [ps] to parameters; [coers] is a diff --git a/toplevel/record.mli b/toplevel/record.mli index 873e1ff0c..befa5f72c 100644 --- a/toplevel/record.mli +++ b/toplevel/record.mli @@ -40,3 +40,5 @@ val definition_structure : inductive_kind * Decl_kinds.polymorphic * Decl_kinds.recursivity_kind * lident with_coercion * local_binder list * (local_decl_expr with_instance with_priority with_notation) list * Id.t * constr_expr option -> global_reference + +val declare_existing_class : global_reference -> unit diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 97f7ace0d..490addddb 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -792,7 +792,7 @@ let vernac_declare_instances locality ids pri = List.iter (fun id -> Classes.existing_instance glob id pri) ids let vernac_declare_class id = - Classes.declare_class id + Record.declare_existing_class (Nametab.global id) (***********) (* Solving *) |