diff options
-rw-r--r-- | contrib/subtac/subtac_classes.ml | 29 | ||||
-rw-r--r-- | interp/implicit_quantifiers.ml | 15 | ||||
-rw-r--r-- | interp/implicit_quantifiers.mli | 9 | ||||
-rw-r--r-- | parsing/prettyp.ml | 2 | ||||
-rw-r--r-- | parsing/prettyp.mli | 2 | ||||
-rw-r--r-- | pretyping/clenv.ml | 9 | ||||
-rw-r--r-- | pretyping/clenv.mli | 1 | ||||
-rw-r--r-- | pretyping/typeclasses.ml | 149 | ||||
-rw-r--r-- | pretyping/typeclasses.mli | 41 | ||||
-rw-r--r-- | pretyping/typeclasses_errors.ml | 7 | ||||
-rw-r--r-- | pretyping/typeclasses_errors.mli | 9 | ||||
-rw-r--r-- | tactics/class_tactics.ml4 | 96 | ||||
-rw-r--r-- | theories/Classes/Equivalence.v | 6 | ||||
-rw-r--r-- | theories/Classes/Functions.v | 4 | ||||
-rw-r--r-- | theories/Classes/Morphisms.v | 118 | ||||
-rw-r--r-- | theories/Classes/RelationClasses.v | 173 | ||||
-rw-r--r-- | theories/Classes/SetoidClass.v | 6 | ||||
-rw-r--r-- | theories/Classes/SetoidTactics.v | 3 | ||||
-rw-r--r-- | theories/FSets/FSetFacts.v | 2 | ||||
-rw-r--r-- | toplevel/classes.ml | 124 | ||||
-rw-r--r-- | toplevel/classes.mli | 8 | ||||
-rw-r--r-- | toplevel/himsg.ml | 8 | ||||
-rw-r--r-- | toplevel/vernacentries.ml | 5 |
23 files changed, 404 insertions, 422 deletions
diff --git a/contrib/subtac/subtac_classes.ml b/contrib/subtac/subtac_classes.ml index a2184a557..39865f1f9 100644 --- a/contrib/subtac/subtac_classes.ml +++ b/contrib/subtac/subtac_classes.ml @@ -108,11 +108,8 @@ let new_instance ctx (instid, bk, cl) props pri = let tclass = match bk with | Explicit -> - let id, par = Implicit_quantifiers.destClassAppExpl cl in - let k = - try class_info (snd id) - with Not_found -> unbound_class env id - in + let loc, id, par = Implicit_quantifiers.destClassAppExpl cl in + let k = class_info (Nametab.global id) in let applen = List.fold_left (fun acc (x, y) -> if y = None then succ acc else acc) 0 par in let needlen = List.fold_left (fun acc (x, y) -> if x = None then succ acc else acc) 0 k.cl_context in if needlen <> applen then @@ -129,7 +126,7 @@ let new_instance ctx (instid, bk, cl) props pri = in t, avoid | None -> failwith ("new instance: under-applied typeclass")) par (List.rev k.cl_context) - in Topconstr.CAppExpl (Util.dummy_loc, (None, Ident id), pars) + in Topconstr.CAppExpl (loc, (None, id), pars) | Implicit -> cl in @@ -143,13 +140,8 @@ let new_instance ctx (instid, bk, cl) props pri = let c = Command.generalize_constr_expr tclass ctx in let c' = interp_type_evars isevars env c in let ctx, c = Classes.decompose_named_assum c' in - (match kind_of_term c with - App (c, args) -> - let cl = Option.get (class_of_constr c) in - cl, ctx, substitution_of_constrs (List.map snd cl.cl_context) (List.rev (Array.to_list args)) - | _ -> - let cl = Option.get (class_of_constr c) in - cl, ctx, []) + let cl, args = Typeclasses.dest_class_app c in + cl, ctx, substitution_of_constrs (List.map snd cl.cl_context) (List.rev (Array.to_list args)) in let id = match snd instid with @@ -159,7 +151,7 @@ let new_instance ctx (instid, bk, cl) props pri = errorlabstrm "new_instance" (Nameops.pr_id id ++ Pp.str " already exists"); id | Anonymous -> - let i = Nameops.add_suffix k.cl_name "_instance_0" in + let i = Nameops.add_suffix (Classes.id_of_class k) "_instance_0" in Termops.next_global_ident_away false i (Termops.ids_of_context env) in let env' = Classes.push_named_context ctx' env in @@ -187,18 +179,17 @@ let new_instance ctx (instid, bk, cl) props pri = ([], props) k.cl_props in if rest <> [] then - unbound_method env' k.cl_name (fst (List.hd rest)) + unbound_method env' k.cl_impl (fst (List.hd rest)) else type_ctx_instance isevars env' k.cl_props props substctx in - let app = - applistc (mkConstruct (k.cl_impl, 1)) (List.rev_map snd subst) - in + let inst_constr, ty_constr = instance_constructor k in + let app = inst_constr (List.rev_map snd subst) in let term = it_mkNamedLambda_or_LetIn app ctx' in isevars := Evarutil.nf_evar_defs !isevars; let term = Evarutil.nf_isevar !isevars term in let termtype = - let app = applistc (mkInd (k.cl_impl)) (List.rev_map snd substctx) in + let app = applistc ty_constr (List.rev_map snd substctx) in let t = it_mkNamedProd_or_LetIn app ctx' in Evarutil.nf_isevar !isevars t in diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml index 8a0b940b1..3b2b5d3d4 100644 --- a/interp/implicit_quantifiers.ml +++ b/interp/implicit_quantifiers.ml @@ -159,12 +159,12 @@ let compute_context_vars env l = let destClassApp cl = match cl with - | CApp (loc, (None,CRef (Ident f)), l) -> f, List.map fst l + | CApp (loc, (None,CRef ref), l) -> loc, ref, List.map fst l | _ -> raise Not_found - + let destClassAppExpl cl = match cl with - | CApp (loc, (None,CRef (Ident f)), l) -> f, l + | CApp (loc, (None,CRef ref), l) -> loc, ref, l | _ -> raise Not_found let full_class_binders env l = @@ -173,12 +173,13 @@ let full_class_binders env l = List.fold_left (fun (l', avoid) (iid, bk, cl as x) -> match bk with Explicit -> - let (id, l) = destClassAppExpl cl in + let (loc, id, l) = destClassAppExpl cl in + let gr = Nametab.global id in (try - let c = class_info (snd id) in + let c = class_info gr in let args, avoid = combine_params_freevar avoid l (List.rev c.cl_context) in - (iid, bk, CAppExpl (fst id, (None, Ident id), args)) :: l', avoid - with Not_found -> unbound_class (Global.env ()) id) + (iid, bk, CAppExpl (loc, (None, id), args)) :: l', avoid + with Not_found -> not_a_class (Global.env ()) (constr_of_global gr)) | Implicit -> (x :: l', avoid)) ([], avoid) l in List.rev l' diff --git a/interp/implicit_quantifiers.mli b/interp/implicit_quantifiers.mli index 4ea95fc43..9ecdcd6c0 100644 --- a/interp/implicit_quantifiers.mli +++ b/interp/implicit_quantifiers.mli @@ -20,12 +20,13 @@ open Mod_subst open Rawterm open Topconstr open Util +open Libnames open Typeclasses (*i*) val ids_of_list : identifier list -> Idset.t -val destClassApp : constr_expr -> identifier located * constr_expr list -val destClassAppExpl : constr_expr -> identifier located * (constr_expr * explicitation located option) list +val destClassApp : constr_expr -> loc * reference * constr_expr list +val destClassAppExpl : constr_expr -> loc * reference * (constr_expr * explicitation located option) list val free_vars_of_constr_expr : Topconstr.constr_expr -> ?bound:Idset.t -> @@ -55,10 +56,10 @@ val implicits_of_binders : local_binder list -> (Topconstr.explicitation * (bool val implicits_of_rawterm : Rawterm.rawconstr -> (Topconstr.explicitation * (bool * bool)) list val combine_params : Names.Idset.t -> - (Names.Idset.t -> (Names.identifier * bool) option * (Names.identifier * Term.constr option * Term.types) -> + (Names.Idset.t -> (global_reference * bool) option * (Names.identifier * Term.constr option * Term.types) -> Topconstr.constr_expr * Names.Idset.t) -> (Topconstr.constr_expr * Topconstr.explicitation located option) list -> - ((Names.identifier * bool) option * Term.named_declaration) list -> + ((global_reference * bool) option * Term.named_declaration) list -> Topconstr.constr_expr list * Names.Idset.t diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml index b39cdedda..767072e2b 100644 --- a/parsing/prettyp.ml +++ b/parsing/prettyp.ml @@ -763,7 +763,7 @@ let print_canonical_projections () = open Typeclasses let pr_typeclass env t = - gallina_print_inductive (fst t.cl_impl) + print_ref false t.cl_impl let print_typeclasses () = let env = Global.env () in diff --git a/parsing/prettyp.mli b/parsing/prettyp.mli index c6478376d..db1d8bb10 100644 --- a/parsing/prettyp.mli +++ b/parsing/prettyp.mli @@ -60,7 +60,7 @@ val print_canonical_projections : unit -> std_ppcmds (* Pretty-printing functions for type classes and instances *) val print_typeclasses : unit -> std_ppcmds -val print_instances : reference -> std_ppcmds +val print_instances : global_reference -> std_ppcmds val inspect : int -> std_ppcmds diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml index 3406d06aa..0d462f793 100644 --- a/pretyping/clenv.ml +++ b/pretyping/clenv.ml @@ -141,13 +141,16 @@ let clenv_conv_leq env sigma t c bound = check_evars env sigma evars (applist (c,args)); args -let mk_clenv_from_n gls n (c,cty) = - let evd = create_goal_evar_defs gls.sigma in +let mk_clenv_from_env environ sigma n (c,cty) = + let evd = create_goal_evar_defs sigma in let (env,args,concl) = clenv_environments evd n cty in { templval = mk_freelisted (match args with [] -> c | _ -> applist (c,args)); templtyp = mk_freelisted concl; evd = env; - env = Global.env_of_context gls.it.evar_hyps } + env = environ } + +let mk_clenv_from_n gls n (c,cty) = + mk_clenv_from_env (Global.env_of_context gls.it.evar_hyps) gls.sigma n (c, cty) let mk_clenv_from gls = mk_clenv_from_n gls None diff --git a/pretyping/clenv.mli b/pretyping/clenv.mli index 1697bb3c2..6a7038a07 100644 --- a/pretyping/clenv.mli +++ b/pretyping/clenv.mli @@ -54,6 +54,7 @@ val mk_clenv_from : evar_info sigma -> constr * types -> clausenv val mk_clenv_from_n : evar_info sigma -> int option -> constr * types -> clausenv val mk_clenv_type_of : evar_info sigma -> constr -> clausenv +val mk_clenv_from_env : env -> evar_map -> int option -> constr * types -> clausenv (***************************************************************) (* linking of clenvs *) diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index 47be84460..9d837df0e 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -30,22 +30,22 @@ type rels = constr list (* This module defines type-classes *) type typeclass = { - (* Name of the class. FIXME: should not necessarily be globally unique. *) - cl_name : identifier; + (* The class implementation *) + cl_impl : global_reference; (* Context in which the definitions are typed. Includes both typeclass parameters and superclasses. *) - cl_context : ((identifier * bool) option * named_declaration) list; + cl_context : ((global_reference * bool) option * named_declaration) list; cl_params: int; (* Context of definitions and properties on defs, will not be shared *) cl_props : named_context; - - (* The class implementation: a record parameterized by the context with defs in it. *) - cl_impl : inductive; + + (* The method implementaions as projections. *) + cl_projs : constant list; } -type typeclasses = (identifier, typeclass) Gmap.t +type typeclasses = (global_reference, typeclass) Gmap.t type instance = { is_class: typeclass; @@ -53,11 +53,11 @@ type instance = { is_impl: constant; } -type instances = (identifier, instance list) Gmap.t +type instances = (global_reference, instance list) Gmap.t let classes : typeclasses ref = ref Gmap.empty -let methods : (identifier, identifier) Gmap.t ref = ref Gmap.empty +let methods : (constant, global_reference) Gmap.t ref = ref Gmap.empty let instances : instances ref = ref Gmap.empty @@ -124,47 +124,64 @@ open Libobject let subst (_,subst,(cl,m,inst)) = let do_subst_con c = fst (Mod_subst.subst_con subst c) and do_subst c = Mod_subst.subst_mps subst c - and do_subst_ind (kn,i) = (Mod_subst.subst_kn subst kn,i) + and do_subst_gr gr = fst (subst_global subst gr) in let do_subst_named ctx = - List.map (fun (na, b, t) -> + list_smartmap (fun (na, b, t) -> (na, Option.smartmap do_subst b, do_subst t)) ctx in let do_subst_ctx ctx = - List.map (fun (cl, (na, b, t)) -> - (cl, (na, Option.smartmap do_subst b, do_subst t))) + list_smartmap (fun (cl, (na, b, t)) -> + (Option.smartmap (fun (gr,b) -> do_subst_gr gr, b) cl, + (na, Option.smartmap do_subst b, do_subst t))) ctx in - let subst_class cl = - let cl' = { cl with cl_impl = do_subst_ind cl.cl_impl; + let do_subst_projs projs = list_smartmap do_subst_con projs in + let subst_class k cl classes = + let k = do_subst_gr k in + let cl' = { cl with cl_impl = k; cl_context = do_subst_ctx cl.cl_context; - cl_props = do_subst_named cl.cl_props; } - in if cl' = cl then cl else cl' + cl_props = do_subst_named cl.cl_props; + cl_projs = do_subst_projs cl.cl_projs; } + in + let cl' = if cl' = cl then cl else cl' in + Gmap.add k cl' classes in - let subst_inst classes insts = - List.map (fun is -> - let is' = - { is_class = Gmap.find is.is_class.cl_name classes; - is_pri = is.is_pri; - is_impl = do_subst_con is.is_impl } - in if is' = is then is else is') insts + let classes = Gmap.fold subst_class cl Gmap.empty in + let subst_inst k insts instances = + let k = do_subst_gr k in + let cl = Gmap.find k classes in + let insts' = + list_smartmap (fun is -> + let is' = + { is_class = cl; + is_pri = is.is_pri; + is_impl = do_subst_con is.is_impl } + in if is' = is then is else is') insts + in Gmap.add k insts' instances in - let classes = Gmap.map subst_class cl in - let instances = Gmap.map (subst_inst classes) inst in + let instances = Gmap.fold subst_inst inst Gmap.empty in (classes, m, instances) let discharge (_,(cl,m,inst)) = - let subst_class cl = - { cl with cl_impl = Lib.discharge_inductive cl.cl_impl } + let discharge_named (cl, r) = + Option.smartmap (fun (gr, b) -> Lib.discharge_global gr, b) cl, r in - let subst_inst classes insts = - List.map (fun is -> { is_impl = Lib.discharge_con is.is_impl; - is_pri = is.is_pri; - is_class = Gmap.find is.is_class.cl_name classes; }) insts + let subst_class cl = + { cl with cl_impl = Lib.discharge_global cl.cl_impl; + cl_context = list_smartmap discharge_named cl.cl_context; + cl_projs = list_smartmap Lib.discharge_con cl.cl_projs } in let classes = Gmap.map subst_class cl in - let instances = Gmap.map (subst_inst classes) inst in + let subst_inst insts = + List.map (fun is -> + { is_impl = Lib.discharge_con is.is_impl; + is_pri = is.is_pri; + is_class = Gmap.find (Lib.discharge_global is.is_class.cl_impl) classes; }) + insts + in + let instances = Gmap.map subst_inst inst in Some (classes, m, instances) let (input,output) = @@ -181,24 +198,20 @@ let (input,output) = let update () = Lib.add_anonymous_leaf (input (!classes, !methods, !instances)) -let class_methods cl = - List.map (function (x, _, _) -> x) cl.cl_props - let add_class c = - classes := Gmap.add c.cl_name c !classes; - methods := List.fold_left (fun acc x -> Gmap.add x c.cl_name acc) !methods (class_methods c); + classes := Gmap.add c.cl_impl c !classes; + methods := List.fold_left (fun acc x -> Gmap.add x c.cl_impl acc) !methods c.cl_projs; update () let class_info c = - Gmap.find c !classes + try Gmap.find c !classes + with _ -> not_a_class (Global.env()) (constr_of_global c) -let class_of_inductive ind = - let res = Gmap.fold - (fun k v acc -> match acc with None -> if v.cl_impl = ind then Some v else acc | _ -> acc) - !classes None - in match res with - None -> raise Not_found - | Some cl -> cl +let instance_constructor cl = + match cl.cl_impl with + | IndRef ind -> (fun args -> applistc (mkConstruct (ind, 1)) args), mkInd ind + | ConstRef cst -> list_last, mkConst cst + | _ -> assert false let typeclasses () = Gmap.fold (fun _ l c -> l :: c) !classes [] @@ -210,25 +223,16 @@ let gmapl_add x y m = Gmap.add x [y] m let instances_of c = - try Gmap.find c.cl_name !instances with Not_found -> [] + try Gmap.find c.cl_impl !instances with Not_found -> [] let add_instance i = - try - let cl = Gmap.find i.is_class.cl_name !classes in - instances := gmapl_add cl.cl_name { i with is_class = cl } !instances; - add_instance_hint (qualid_of_con i.is_impl) i.is_pri; - update () - with Not_found -> unbound_class (Global.env ()) (dummy_loc, i.is_class.cl_name) - -open Libnames - -let id_of_reference r = - let (_, id) = repr_qualid (snd (qualid_of_reference r)) in id + let cl = Gmap.find i.is_class.cl_impl !classes in + instances := gmapl_add cl.cl_impl { i with is_class = cl } !instances; + add_instance_hint (qualid_of_con i.is_impl) i.is_pri; + update () let instances r = - let id = id_of_reference r in - try let cl = class_info id in instances_of cl - with Not_found -> unbound_class (Global.env()) (loc_of_reference r, id) + let cl = class_info r in instances_of cl let solve_instanciation_problem = ref (fun _ _ _ _ -> assert false) let solve_instanciations_problem = ref (fun _ _ _ _ -> assert false) @@ -273,12 +277,11 @@ let resolve_one_typeclass_evd env evd types = let method_typeclass ref = match ref with | ConstRef c -> - let (_, _, l) = Names.repr_con c in - class_info (Gmap.find (Names.id_of_label l) !methods) + class_info (Gmap.find c !methods) | _ -> raise Not_found -let is_class ind = - Gmap.fold (fun k v acc -> acc || v.cl_impl = ind) !classes false +let is_class gr = + Gmap.fold (fun k v acc -> acc || v.cl_impl = gr) !classes false let is_implicit_arg k = match k with @@ -332,14 +335,18 @@ let is_independent evm ev = (* in sat (Evarutil.nf_evar_defs evd) *) let class_of_constr c = - let extract_ind c = - match kind_of_term c with - Ind ind -> (try Some (class_of_inductive ind) with Not_found -> None) - | _ -> None + let extract_cl c = + try Some (class_info (global_of_constr c)) with _ -> None in match kind_of_term c with - App (c, _) -> extract_ind c - | _ -> extract_ind c + App (c, _) -> extract_cl c + | _ -> extract_cl c + +let dest_class_app c = + let cl c = class_info (global_of_constr c) in + match kind_of_term c with + App (c, args) -> cl c, args + | _ -> cl c, [||] (* To embed a boolean for resolvability status. This is essentially a hack to mark which evars correspond to diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli index dba60234b..193f3ae3c 100644 --- a/pretyping/typeclasses.mli +++ b/pretyping/typeclasses.mli @@ -24,20 +24,21 @@ open Util (* This module defines type-classes *) type typeclass = { - (* Name of the class. FIXME: should not necessarily be globally unique. *) - cl_name : identifier; + (* The class implementation: a record parameterized by the context with defs in it or a definition if + the class is a singleton. This acts as the classe's global identifier. *) + cl_impl : global_reference; (* Context in which the definitions are typed. Includes both typeclass parameters and superclasses. The boolean indicates if the typeclass argument is a direct superclass. *) - cl_context : ((identifier * bool) option * named_declaration) list; + cl_context : ((global_reference * bool) option * named_declaration) list; cl_params : int; (* This is the length of the suffix of the context which should be considered explicit parameters. *) (* Context of definitions and properties on defs, will not be shared *) cl_props : named_context; - (* The class implementation: a record parameterized by the context with defs in it. *) - cl_impl : inductive; + (* The methods implementations of the typeclass as projections. *) + cl_projs : constant list; } type instance = { @@ -46,7 +47,7 @@ type instance = { is_impl: constant; } -val instances : Libnames.reference -> instance list +val instances : global_reference -> instance list val typeclasses : unit -> typeclass list val add_class : typeclass -> unit val add_instance : instance -> unit @@ -54,16 +55,16 @@ val add_instance : instance -> unit val register_add_instance_hint : (reference -> int option -> unit) -> unit val add_instance_hint : reference -> int option -> unit -val class_info : identifier -> typeclass (* raises Not_found *) -val class_of_inductive : inductive -> typeclass (* raises Not_found *) +val class_info : global_reference -> typeclass (* raises a UserError if not a class *) +val is_class : global_reference -> bool +val class_of_constr : constr -> typeclass option +val dest_class_app : constr -> typeclass * constr array (* raises a UserError if not a class *) + +(* Returns the constructor for the given fields of the class and the type constructor. *) +val instance_constructor : typeclass -> (constr list -> constr) * types val resolve_one_typeclass : env -> types -> types (* Raises Not_found *) val resolve_one_typeclass_evd : env -> evar_defs ref -> types -> types (* Raises Not_found *) - -val is_class : inductive -> bool - -val class_of_constr : constr -> typeclass option - val resolve_typeclass : env -> evar -> evar_info -> evar_defs * bool -> evar_defs * bool (* Use evar_extra for marking resolvable evars. *) @@ -88,9 +89,15 @@ val nf_substitution : evar_map -> substitution -> substitution val is_implicit_arg : hole_kind -> bool +val qualid_of_con : Names.constant -> Libnames.reference -val subst : 'a * Mod_subst.substitution * - ((Names.identifier, typeclass) Gmap.t * 'b * ('c, instance list) Gmap.t) -> - (Names.identifier, typeclass) Gmap.t * 'b * ('c, instance list) Gmap.t -val qualid_of_con : Names.constant -> Libnames.reference +(* debug *) + +(* val subst : *) +(* 'a * Mod_subst.substitution * *) +(* ((Libnames.global_reference, typeclass) Gmap.t * 'b * *) +(* ('c, instance list) Gmap.t) -> *) +(* (Libnames.global_reference, typeclass) Gmap.t * 'b * *) +(* ('c, instance list) Gmap.t *) + diff --git a/pretyping/typeclasses_errors.ml b/pretyping/typeclasses_errors.ml index 980f327cb..1648f667a 100644 --- a/pretyping/typeclasses_errors.ml +++ b/pretyping/typeclasses_errors.ml @@ -19,13 +19,14 @@ open Nametab open Mod_subst open Topconstr open Util +open Libnames (*i*) type contexts = Parameters | Properties type typeclass_error = - | UnboundClass of identifier located - | UnboundMethod of identifier * identifier located (* Class name, method *) + | NotAClass of constr + | UnboundMethod of global_reference * identifier located (* Class name, method *) | NoInstance of identifier located * constr list | MismatchedContextInstance of contexts * constr_expr list * named_context (* found, expected *) @@ -33,7 +34,7 @@ exception TypeClassError of env * typeclass_error let typeclass_error env err = raise (TypeClassError (env, err)) -let unbound_class env id = typeclass_error env (UnboundClass id) +let not_a_class env c = typeclass_error env (NotAClass c) let unbound_method env cid id = typeclass_error env (UnboundMethod (cid, id)) diff --git a/pretyping/typeclasses_errors.mli b/pretyping/typeclasses_errors.mli index fbc2f2544..82e37f41d 100644 --- a/pretyping/typeclasses_errors.mli +++ b/pretyping/typeclasses_errors.mli @@ -19,21 +19,22 @@ open Nametab open Mod_subst open Topconstr open Util +open Libnames (*i*) type contexts = Parameters | Properties type typeclass_error = - | UnboundClass of identifier located - | UnboundMethod of identifier * identifier located (* Class name, method *) + | NotAClass of constr + | UnboundMethod of global_reference * identifier located (* Class name, method *) | NoInstance of identifier located * constr list | MismatchedContextInstance of contexts * constr_expr list * named_context (* found, expected *) exception TypeClassError of env * typeclass_error -val unbound_class : env -> identifier located -> 'a +val not_a_class : env -> constr -> 'a -val unbound_method : env -> identifier -> identifier located -> 'a +val unbound_method : env -> global_reference -> identifier located -> 'a val no_instance : env -> identifier located -> constr list -> 'a diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4 index dd552845d..4edb8191e 100644 --- a/tactics/class_tactics.ml4 +++ b/tactics/class_tactics.ml4 @@ -36,7 +36,7 @@ open Classes open Topconstr open Pfedit open Command - +open Libnames open Evd (** Typeclasses instance search tactic / eauto *) @@ -418,12 +418,10 @@ END (** Typeclass-based rewriting. *) -let morphism_class = lazy (class_info (id_of_string "Morphism")) +let morphism_class = + lazy (class_info (Nametab.global (Qualid (dummy_loc, qualid_of_string "Coq.Classes.Morphisms.Morphism")))) -let get_respect cl = - Option.get (List.hd (Recordops.lookup_projections cl.cl_impl)) - -let respect_proj = lazy (get_respect (Lazy.force morphism_class)) +let respect_proj = lazy (mkConst (List.hd (Lazy.force morphism_class).cl_projs)) let gen_constant dir s = Coqlib.gen_constant "Class_setoid" dir s let coq_proj1 = lazy(gen_constant ["Init"; "Logic"] "proj1") @@ -433,14 +431,14 @@ let impl = lazy (gen_constant ["Program"; "Basics"] "impl") let arrow = lazy (gen_constant ["Program"; "Basics"] "arrow") let coq_id = lazy (gen_constant ["Program"; "Basics"] "id") -let reflexive_type = lazy (gen_constant ["Classes"; "RelationClasses"] "Reflexive") -let reflexive_proof = lazy (gen_constant ["Classes"; "RelationClasses"] "reflexive") +let reflexive_type = lazy (gen_constant ["Classes"; "RelationClasses"] "reflexive") +let reflexive_proof = lazy (gen_constant ["Classes"; "RelationClasses"] "reflexivity") -let symmetric_type = lazy (gen_constant ["Classes"; "RelationClasses"] "Symmetric") -let symmetric_proof = lazy (gen_constant ["Classes"; "RelationClasses"] "symmetric") +let symmetric_type = lazy (gen_constant ["Classes"; "RelationClasses"] "symmetric") +let symmetric_proof = lazy (gen_constant ["Classes"; "RelationClasses"] "symmetry") -let transitive_type = lazy (gen_constant ["Classes"; "RelationClasses"] "Transitive") -let transitive_proof = lazy (gen_constant ["Classes"; "RelationClasses"] "transitive") +let transitive_type = lazy (gen_constant ["Classes"; "RelationClasses"] "transitive") +let transitive_proof = lazy (gen_constant ["Classes"; "RelationClasses"] "transitivity") let inverse = lazy (gen_constant ["Classes"; "RelationClasses"] "inverse") let complement = lazy (gen_constant ["Classes"; "RelationClasses"] "complement") @@ -474,7 +472,7 @@ let arrow_morphism a b = let setoid_refl pars x = applistc (Lazy.force setoid_refl_proj) (pars @ [x]) -let morphism_class_proj = lazy (Lazy.force morphism_class, Lazy.force respect_proj) +let morphism_type = lazy (constr_of_global (Lazy.force morphism_class).cl_impl) exception Found of (constr * constr * (types * types) list * constr * constr array * (constr * (constr * constr * constr * constr)) option array) @@ -539,7 +537,6 @@ let symmetric_proof env = find_class_proof symmetric_type symmetric_proof env let transitive_proof env = find_class_proof transitive_type transitive_proof env let resolve_morphism env sigma oldt m ?(fnewt=fun x -> x) args args' cstr evars = - let (morphism_cl, morphism_proj) = Lazy.force morphism_class_proj in let morph_instance, proj, sigargs, m', args, args' = (* if is_equiv env sigma m then *) (* let params, rest = array_chop 3 args in *) @@ -566,10 +563,10 @@ let resolve_morphism env sigma oldt m ?(fnewt=fun x -> x) args args' cstr evars let cstrs = List.map (function None -> None | Some (_, (a, r, _, _)) -> Some (a, r)) (Array.to_list morphobjs') in let signature, sigargs = build_signature evars env appmtype cstrs cstr (fun (a, r) -> r) in let cl_args = [| appmtype ; signature ; appm |] in - let app = mkApp (mkInd morphism_cl.cl_impl, cl_args) in + let app = mkApp (Lazy.force morphism_type, cl_args) in let morph = Evarutil.e_new_evar evars env app in let proj = - mkApp (mkConst morphism_proj, + mkApp (Lazy.force respect_proj, Array.append cl_args [|morph|]) in morph, proj, sigargs, appm, morphobjs, morphobjs' @@ -605,9 +602,9 @@ type hypinfo = { abs : (constr * types) option; } -let decompose_setoid_eqhyp gl c left2right = - let ctype = pf_type_of gl c in - let eqclause = Clenv.make_clenv_binding gl (c,ctype) Rawterm.NoBindings in +let decompose_setoid_eqhyp env sigma c left2right = + let ctype = Typing.type_of env sigma c in + let eqclause = Clenv.mk_clenv_from_env env sigma None (c,ctype) in let (equiv, args) = decompose_app (Clenv.clenv_type eqclause) in let rec split_last_two = function | [c1;c2] -> [],(c1, c2) @@ -652,7 +649,15 @@ let rewrite2_unif_flags = { let allowK = true -let unify_eqn gl hypinfo t = +let refresh_hypinfo env sigma hypinfo = + let {l2r=l2r; c = c} = !hypinfo in + match c with + | Some c -> + (* Refresh the clausenv to not get the same meta twice in the goal. *) + hypinfo := decompose_setoid_eqhyp env sigma c l2r; + | _ -> () + +let unify_eqn env sigma hypinfo t = try let {cl=cl; prf=prf; rel=rel; l2r=l2r; c1=c1; c2=c2; c=c; abs=abs} = !hypinfo in let env' = @@ -665,27 +670,21 @@ let unify_eqn gl hypinfo t = let c1 = Clenv.clenv_nf_meta env' c1 and c2 = Clenv.clenv_nf_meta env' c2 and rel = Clenv.clenv_nf_meta env' rel in - let car = pf_type_of gl c1 in + let car = Typing.type_of env'.env (Evd.evars_of env'.evd) c1 in let prf = if abs = None then (* let (rel, args) = destApp typ in *) (* let relargs, args = array_chop (Array.length args - 2) args in *) (* let rel = mkApp (rel, relargs) in *) let prf = Clenv.clenv_value env' in - begin - match c with - | Some c when occur_meta prf -> - (* Refresh the clausenv to not get the same meta twice in the goal. *) - hypinfo := decompose_setoid_eqhyp gl c l2r; - | _ -> () - end; + if occur_meta prf then refresh_hypinfo env sigma hypinfo; prf else prf in let res = if l2r then (prf, (car, rel, c1, c2)) else - try (mkApp (symmetric_proof (pf_env gl) car rel, [| c1 ; c2 ; prf |]), (car, rel, c2, c1)) + try (mkApp (symmetric_proof env car rel, [| c1 ; c2 ; prf |]), (car, rel, c2, c1)) with Not_found -> (prf, (car, mkApp (Lazy.force inverse, [| car ; rel |]), c2, c1)) in Some (env', res) @@ -705,7 +704,7 @@ let unfold_id t = let build_new gl env sigma occs hypinfo concl cstr evars = let is_occ occ = occs = [] || List.mem occ occs in let rec aux env t occ cstr = - match unify_eqn gl hypinfo t with + match unify_eqn env sigma hypinfo t with | Some (env', (prf, hypinfo as x)) -> if is_occ occ then ( evars := Evd.evar_merge !evars (Evd.evars_of (Evd.undefined_evars env'.evd)); @@ -755,6 +754,7 @@ let build_new gl env sigma occs hypinfo concl cstr evars = | Lambda (n, t, b) -> let env' = Environ.push_rel (n, None, t) env in + refresh_hypinfo env' sigma hypinfo; let b', occ = aux env' b occ None in let res = match b' with @@ -849,7 +849,7 @@ let cl_rewrite_clause_aux hypinfo goal_meta occs clause gl = let cl_rewrite_clause c left2right occs clause gl = let meta = Evarutil.new_meta() in - let hypinfo = ref (decompose_setoid_eqhyp gl c left2right) in + let hypinfo = ref (decompose_setoid_eqhyp (pf_env gl) (project gl) c left2right) in cl_rewrite_clause_aux hypinfo meta occs clause gl open Genarg @@ -954,7 +954,7 @@ END let mkappc s l = CAppExpl (dummy_loc,(None,(Libnames.Ident (dummy_loc,id_of_string s))),l) let declare_instance a aeq n s = ((dummy_loc,Name n),Explicit, - CApp (dummy_loc, (None, mkIdentC (id_of_string s)), + CApp (dummy_loc, (None, mkRefC (Qualid (dummy_loc, qualid_of_string s))), [(a,None);(aeq,None)])) let anew_instance instance fields = new_instance [] instance fields None (fun _ -> ()) @@ -973,19 +973,19 @@ let init_setoid () = check_required_library ["Coq";"Setoids";"Setoid"] let declare_instance_refl a aeq n lemma = - let instance = declare_instance a aeq (add_suffix n "_refl") "Reflexive" + let instance = declare_instance a aeq (add_suffix n "_refl") "Coq.Classes.RelationClasses.reflexive" in anew_instance instance - [((dummy_loc,id_of_string "reflexive"),[],lemma)] + [((dummy_loc,id_of_string "reflexivity"),[],lemma)] let declare_instance_sym a aeq n lemma = - let instance = declare_instance a aeq (add_suffix n "_sym") "Symmetric" + let instance = declare_instance a aeq (add_suffix n "_sym") "Coq.Classes.RelationClasses.symmetric" in anew_instance instance - [((dummy_loc,id_of_string "symmetric"),[],lemma)] + [((dummy_loc,id_of_string "symmetry"),[],lemma)] let declare_instance_trans a aeq n lemma = - let instance = declare_instance a aeq (add_suffix n "_trans") "Transitive" + let instance = declare_instance a aeq (add_suffix n "_trans") "Coq.Classes.RelationClasses.transitive" in anew_instance instance - [((dummy_loc,id_of_string "transitive"),[],lemma)] + [((dummy_loc,id_of_string "transitivity"),[],lemma)] let constr_tac = Tacinterp.interp (Tacexpr.TacAtom (dummy_loc, Tacexpr.TacAnyConstructor None)) @@ -993,7 +993,7 @@ let declare_relation a aeq n refl symm trans = init_setoid (); match (refl,symm,trans) with (None, None, None) -> - let instance = declare_instance a aeq n "DefaultRelation" + let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.DefaultRelation" in ignore(anew_instance instance []) | (Some lemma1, None, None) -> ignore (declare_instance_refl a aeq n lemma1) @@ -1007,7 +1007,7 @@ let declare_relation a aeq n refl symm trans = | (Some lemma1, None, Some lemma3) -> let lemma_refl = declare_instance_refl a aeq n lemma1 in let lemma_trans = declare_instance_trans a aeq n lemma3 in - let instance = declare_instance a aeq n "PreOrder" + let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.PreOrder" in ignore( anew_instance instance [((dummy_loc,id_of_string "preorder_refl"), [], mkIdentC lemma_refl); @@ -1015,7 +1015,7 @@ let declare_relation a aeq n refl symm trans = | (None, Some lemma2, Some lemma3) -> let lemma_sym = declare_instance_sym a aeq n lemma2 in let lemma_trans = declare_instance_trans a aeq n lemma3 in - let instance = declare_instance a aeq n "PER" + let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.PER" in ignore( anew_instance instance [((dummy_loc,id_of_string "per_sym"), [], mkIdentC lemma_sym); @@ -1024,7 +1024,7 @@ let declare_relation a aeq n refl symm trans = let lemma_refl = declare_instance_refl a aeq n lemma1 in let lemma_sym = declare_instance_sym a aeq n lemma2 in let lemma_trans = declare_instance_trans a aeq n lemma3 in - let instance = declare_instance a aeq n "Equivalence" + let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.Equivalence" in ignore( anew_instance instance [((dummy_loc,id_of_string "equiv_refl"), [], mkIdentC lemma_refl); @@ -1075,7 +1075,7 @@ let respect_projection r ty = let ctx, inst = Sign.decompose_prod_assum ty in let mor, args = destApp inst in let instarg = mkApp (r, rel_vect 0 (List.length ctx)) in - let app = mkApp (mkConst (Lazy.force respect_proj), + let app = mkApp (Lazy.force respect_proj, Array.append args [| instarg |]) in it_mkLambda_or_LetIn app ctx @@ -1131,7 +1131,7 @@ let build_morphism_signature m = evars in let morph = - mkApp (mkInd (Lazy.force morphism_class).cl_impl, [| t; sig_; m |]) + mkApp (Lazy.force morphism_type, [| t; sig_; m |]) in let evd = resolve_all_evars_once false (true, 15) env (fun x evi -> class_of_constr evi.Evd.evar_concl <> None) !isevars in @@ -1145,7 +1145,7 @@ let default_morphism sign m = build_signature isevars env t (fst sign) (snd sign) (fun (ty, rel) -> rel) in let morph = - mkApp (mkInd (Lazy.force morphism_class).cl_impl, [| t; sign; m |]) + mkApp (Lazy.force morphism_type, [| t; sign; m |]) in let mor = resolve_one_typeclass env morph in mor, respect_projection mor morph @@ -1156,7 +1156,7 @@ VERNAC COMMAND EXTEND AddSetoid1 let lemma_refl = declare_instance_refl a aeq n (mkappc "Seq_refl" [a;aeq;t]) in let lemma_sym = declare_instance_sym a aeq n (mkappc "Seq_sym" [a;aeq;t]) in let lemma_trans = declare_instance_trans a aeq n (mkappc "Seq_trans" [a;aeq;t]) in - let instance = declare_instance a aeq n "Equivalence" + let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.Equivalence" in ignore( anew_instance instance [((dummy_loc,id_of_string "equiv_refl"), [], mkIdentC lemma_refl); @@ -1256,10 +1256,10 @@ let unification_rewrite l2r c1 c2 cl rel but gl = let get_hyp gl c clause l2r = match kind_of_term (pf_type_of gl c) with Prod _ -> - let hi = decompose_setoid_eqhyp gl c l2r in + let hi = decompose_setoid_eqhyp (pf_env gl) (project gl) c l2r in let but = match clause with Some id -> pf_get_hyp_typ gl id | None -> pf_concl gl in unification_rewrite hi.l2r hi.c1 hi.c2 hi.cl hi.rel but gl - | _ -> decompose_setoid_eqhyp gl c l2r + | _ -> decompose_setoid_eqhyp (pf_env gl) (project gl) c l2r let general_s_rewrite l2r c ~new_goals gl = let meta = Evarutil.new_meta() in diff --git a/theories/Classes/Equivalence.v b/theories/Classes/Equivalence.v index 5543f615d..dd9cfbca5 100644 --- a/theories/Classes/Equivalence.v +++ b/theories/Classes/Equivalence.v @@ -35,16 +35,16 @@ Definition equiv [ Equivalence A R ] : relation A := R. (** Shortcuts to make proof search possible (unification won't unfold equiv). *) -Program Instance [ sa : ! Equivalence A ] => equiv_refl : Reflexive equiv. +Program Instance [ sa : ! Equivalence A ] => equiv_refl : reflexive equiv. -Program Instance [ sa : ! Equivalence A ] => equiv_sym : Symmetric equiv. +Program Instance [ sa : ! Equivalence A ] => equiv_sym : symmetric equiv. Next Obligation. Proof. symmetry ; auto. Qed. -Program Instance [ sa : ! Equivalence A ] => equiv_trans : Transitive equiv. +Program Instance [ sa : ! Equivalence A ] => equiv_trans : transitive equiv. Next Obligation. Proof. diff --git a/theories/Classes/Functions.v b/theories/Classes/Functions.v index 11c60a3aa..2795e4218 100644 --- a/theories/Classes/Functions.v +++ b/theories/Classes/Functions.v @@ -22,10 +22,10 @@ Require Export Coq.Classes.Morphisms. Set Implicit Arguments. Unset Strict Implicit. -Class [ m : ! Morphism (A -> B) (RA ++> RB) f ] => Injective := +Class [ m : ! Morphism (A -> B) (RA ++> RB) f ] => Injective : Prop := injective : forall x y : A, RB (f x) (f y) -> RA x y. -Class [ m : ! Morphism (A -> B) (RA ++> RB) f ] => Surjective := +Class [ m : ! Morphism (A -> B) (RA ++> RB) f ] => Surjective : Prop := surjective : forall y, exists x : A, RB y (f x). Definition Bijective [ m : ! Morphism (A -> B) (RA ++> RB) (f : A -> B) ] := diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v index 4fbbe2a40..c752cae86 100644 --- a/theories/Classes/Morphisms.v +++ b/theories/Classes/Morphisms.v @@ -46,7 +46,7 @@ Notation " R --> R' " := (@respectful _ _ (inverse R) R') (right associativity, The relation [R] will be instantiated by [respectful] and [A] by an arrow type for usual morphisms. *) -Class Morphism A (R : relation A) (m : A) := +Class Morphism A (R : relation A) (m : A) : Prop := respect : R m m. (** Here we build an equivalence instance for functions which relates respectful ones only. *) @@ -54,7 +54,6 @@ Class Morphism A (R : relation A) (m : A) := Definition respecting [ Equivalence A (R : relation A), Equivalence B (R' : relation B) ] : Type := { morph : A -> B | respectful R R' morph morph }. - Ltac obligations_tactic ::= program_simpl. Program Instance [ Equivalence A R, Equivalence B R' ] => @@ -63,21 +62,21 @@ Program Instance [ Equivalence A R, Equivalence B R' ] => Next Obligation. Proof. - constructor ; intros. + red ; intros. destruct x ; simpl. apply r ; auto. Qed. Next Obligation. Proof. - constructor ; intros. + red ; intros. symmetry ; apply H. symmetry ; auto. Qed. Next Obligation. Proof. - constructor ; intros. + red ; intros. transitivity (proj1_sig y y0). apply H ; auto. apply H0. reflexivity. @@ -116,51 +115,32 @@ Typeclasses unfold relation. them up to [impl] in each way. Very important instances as we need [impl] morphisms at the top level when we rewrite. *) -Class SubRelation A (R S : relation A) := +Class SubRelation A (R S : relation A) : Prop := subrelation :> Morphism (S ==> R) id. Instance iff_impl_subrelation : SubRelation Prop impl iff. -Proof. - constructor ; red ; intros. - tauto. -Qed. +Proof. reduce. tauto. Qed. Instance iff_inverse_impl_subrelation : SubRelation Prop (inverse impl) iff. Proof. - constructor ; red ; intros. - tauto. + reduce. tauto. Qed. -Instance [ SubRelation A R₁ R₂ ] => +Instance [ sub : SubRelation A R₁ R₂ ] => morphisms_subrelation : SubRelation (B -> A) (R ==> R₁) (R ==> R₂). Proof. - constructor ; repeat red. intros x y H x₁ y₁ H₁. - destruct subrelation. - red in respect0, H ; unfold id in *. - apply respect0. - apply H. - apply H₁. + reduce. apply* sub. apply H. assumption. Qed. -Instance [ SubRelation A R₂ R₁ ] => +Instance [ sub : SubRelation A R₂ R₁ ] => morphisms_subrelation_left : SubRelation (A -> B) (R₁ ==> R) (R₂ ==> R) | 3. Proof. - constructor ; repeat red ; intros x y H x₁ y₁ H₁. - destruct subrelation. - red in respect0, H ; unfold id in *. - apply H. - apply respect0. - apply H₁. + reduce. apply* H. apply* sub. assumption. Qed. Lemma subrelation_morphism [ SubRelation A R₁ R₂, Morphism R₂ m ] : Morphism R₁ m. Proof. - intros. - destruct subrelation. - red in respect0 ; intros. - constructor. - unfold id in * ; apply respect0. - apply respect. + intros. apply* H. apply H0. Qed. Inductive done : nat -> Type := @@ -183,7 +163,7 @@ Program Instance iff_iff_iff_impl_morphism : Morphism (iff ==> iff ==> iff) impl (* Typeclasses eauto := debug. *) -Program Instance [ ! Symmetric A R, Morphism (R ==> impl) m ] => reflexive_impl_iff : Morphism (R ==> iff) m. +Program Instance [ ! symmetric A R, Morphism (R ==> impl) m ] => reflexive_impl_iff : Morphism (R ==> iff) m. Next Obligation. Proof. @@ -192,12 +172,12 @@ Program Instance [ ! Symmetric A R, Morphism (R ==> impl) m ] => reflexive_impl_ (** The complement of a relation conserves its morphisms. *) -Program Instance {A} (RA : relation A) [ Morphism (RA ==> RA ==> iff) R ] => +Program Instance {A} (RA : relation A) [ mR : Morphism (RA ==> RA ==> iff) R ] => complement_morphism : Morphism (RA ==> RA ==> iff) (complement R). Next Obligation. Proof. - unfold complement ; intros. + unfold complement. pose (respect). pose (r x y H). pose (r0 x0 y0 H0). @@ -211,7 +191,6 @@ Program Instance {A} (RA : relation A) [ Morphism (RA ==> RA ==> iff) R ] => Next Obligation. Proof. - unfold inverse ; unfold flip. apply respect ; auto. Qed. @@ -226,7 +205,7 @@ Program Instance {A B C : Type} [ Morphism (RA ==> RB ==> RC) (f : A -> B -> C) (** Every transitive relation gives rise to a binary morphism on [impl], contravariant in the first argument, covariant in the second. *) -Program Instance [ ! Transitive A (R : relation A) ] => +Program Instance [ ! transitive A (R : relation A) ] => trans_contra_co_morphism : Morphism (R --> R ++> impl) R. Next Obligation. @@ -237,19 +216,15 @@ Program Instance [ ! Transitive A (R : relation A) ] => (** Dually... *) -Program Instance [ ! Transitive A (R : relation A) ] => +Program Instance [ ! transitive A (R : relation A) ] => trans_co_contra_inv_impl_morphism : Morphism (R ++> R --> inverse impl) R. Next Obligation. Proof with auto. - intros. - destruct (trans_contra_co_morphism (R:=inverse R)). - revert respect0. - unfold respectful, inverse, flip, impl in * ; intros. - eapply respect0 ; eauto. + apply* trans_contra_co_morphism ; eauto. eauto. Qed. -(* Program Instance [ Transitive A (R : relation A), Symmetric A R ] => *) +(* Program Instance [ transitive A (R : relation A), symmetric A R ] => *) (* trans_sym_contra_co_inv_impl_morphism : ? Morphism (R --> R ++> inverse impl) R. *) (* Next Obligation. *) @@ -263,7 +238,7 @@ Program Instance [ ! Transitive A (R : relation A) ] => (** Morphism declarations for partial applications. *) -Program Instance [ ! Transitive A R ] (x : A) => +Program Instance [ ! transitive A R ] (x : A) => trans_contra_inv_impl_morphism : Morphism (R --> inverse impl) (R x). Next Obligation. @@ -271,7 +246,7 @@ Program Instance [ ! Transitive A R ] (x : A) => transitivity y... Qed. -Program Instance [ ! Transitive A R ] (x : A) => +Program Instance [ ! transitive A R ] (x : A) => trans_co_impl_morphism : Morphism (R ==> impl) (R x). Next Obligation. @@ -279,22 +254,20 @@ Program Instance [ ! Transitive A R ] (x : A) => transitivity x0... Qed. -Program Instance [ ! Transitive A R, Symmetric R ] (x : A) => +Program Instance [ ! transitive A R, symmetric R ] (x : A) => trans_sym_co_inv_impl_morphism : Morphism (R ==> inverse impl) (R x). Next Obligation. Proof with auto. transitivity y... - symmetry... Qed. -Program Instance [ ! Transitive A R, Symmetric R ] (x : A) => +Program Instance [ ! transitive A R, symmetric R ] (x : A) => trans_sym_contra_impl_morphism : Morphism (R --> impl) (R x). Next Obligation. Proof with auto. transitivity x0... - symmetry... Qed. Program Instance [ Equivalence A R ] (x : A) => @@ -311,7 +284,7 @@ Program Instance [ Equivalence A R ] (x : A) => (** With symmetric relations, variance is no issue ! *) (* Program Instance (A B : Type) (R : relation A) (R' : relation B) *) -(* [ Morphism _ (R ==> R') m ] [ Symmetric A R ] => *) +(* [ Morphism _ (R ==> R') m ] [ symmetric A R ] => *) (* sym_contra_morphism : Morphism (R --> R') m. *) (* Next Obligation. *) @@ -323,48 +296,39 @@ Program Instance [ Equivalence A R ] (x : A) => (** [R] is reflexive, hence we can build the needed proof. *) Program Instance (A B : Type) (R : relation A) (R' : relation B) - [ Morphism (R ==> R') m ] [ Reflexive R ] (x : A) => + [ Morphism (R ==> R') m ] [ reflexive R ] (x : A) => reflexive_partial_app_morphism : Morphism R' (m x) | 3. - Next Obligation. - Proof with auto. - intros. - apply (respect (m:=m))... - reflexivity. - Qed. - (** Every transitive relation induces a morphism by "pushing" an [R x y] on the left of an [R x z] proof to get an [R y z] goal. *) -Program Instance [ ! Transitive A R ] => +Program Instance [ ! transitive A R ] => trans_co_eq_inv_impl_morphism : Morphism (R ==> (@eq A) ==> inverse impl) R. Next Obligation. Proof with auto. transitivity y... - subst x0... Qed. -Program Instance [ ! Transitive A R ] => +Program Instance [ ! transitive A R ] => trans_contra_eq_impl_morphism : Morphism (R --> (@eq A) ==> impl) R. Next Obligation. Proof with auto. transitivity x... - subst x0... Qed. (** Every symmetric and transitive relation gives rise to an equivariant morphism. *) -Program Instance [ ! Transitive A R, Symmetric R ] => +Program Instance [ ! transitive A R, symmetric R ] => trans_sym_morphism : Morphism (R ==> R ==> iff) R. Next Obligation. Proof with auto. split ; intros. - transitivity x0... transitivity x... symmetry... + transitivity x0... transitivity x... - transitivity y... transitivity y0... symmetry... + transitivity y... transitivity y0... Qed. Program Instance [ Equivalence A R ] => @@ -443,12 +407,12 @@ Program Instance or_iff_morphism : (* red ; intros. subst ; split; trivial. *) (* Qed. *) -Instance (A B : Type) [ ! Reflexive B R ] (m : A -> B) => +Instance (A B : Type) [ ! reflexive B R ] (m : A -> B) => eq_reflexive_morphism : Morphism (@Logic.eq A ==> R) m | 3. Proof. simpl_relation. Qed. -Instance (A B : Type) [ ! Reflexive B R' ] => - Reflexive (@Logic.eq A ==> R'). +Instance (A B : Type) [ ! reflexive B R' ] => + reflexive (@Logic.eq A ==> R'). Proof. simpl_relation. Qed. (** [respectful] is a morphism for relation equivalence. *) @@ -481,12 +445,13 @@ Proof. split ; intros ; intuition. Qed. -Class (A : Type) (R : relation A) => Normalizes (m : A) (m' : A) := +Class (A : Type) (R : relation A) => Normalizes (m : A) (m' : A) : Prop := normalizes : R m m'. Instance (A : Type) (R : relation A) (B : Type) (R' : relation B) => Normalizes relation_equivalence (inverse R ==> inverse R') (inverse (R ==> R')) . Proof. + reduce. symmetry ; apply inverse_respectful. Qed. @@ -494,6 +459,7 @@ Instance (A : Type) (R : relation A) (B : Type) (R' R'' : relation B) [ Normalizes relation_equivalence R' (inverse R'') ] => Normalizes relation_equivalence (inverse R ==> R') (inverse (R ==> R'')) . Proof. + red. pose normalizes. setoid_rewrite r. setoid_rewrite inverse_respectful. @@ -504,19 +470,13 @@ Program Instance (A : Type) (R : relation A) [ Morphism R m ] => morphism_inverse_morphism : Morphism (inverse R) m | 2. - Next Obligation. - Proof. - apply respect. - Qed. - (** Bootstrap !!! *) Instance morphism_morphism : Morphism (relation_equivalence ==> @eq _ ==> iff) (@Morphism A). Proof. - simpl_relation. - subst. + simpl_relation. unfold relation_equivalence in H. - split ; constructor ; intros. + split ; red ; intros. setoid_rewrite <- H. apply respect. setoid_rewrite H. @@ -527,7 +487,7 @@ Lemma morphism_releq_morphism (A : Type) (R : relation A) (R' : relation A) [ Normalizes relation_equivalence R R' ] [ Morphism R' m ] : Morphism R m. Proof. - intros. + intros. pose respect. assert(n:=normalizes). setoid_rewrite n. diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v index b053b27f2..53079674f 100644 --- a/theories/Classes/RelationClasses.v +++ b/theories/Classes/RelationClasses.v @@ -1,4 +1,4 @@ -(* -*- coq-prog-args: ("-emacs-U" "-nois") -*- *) +(* -*- coq-prog-args: ("-emacs-U" "-top" "Coq.Classes.RelationClasses") -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) @@ -50,133 +50,139 @@ Proof. reflexivity. Qed. (** We rebind relations in separate classes to be able to overload each proof. *) -Class Reflexive A (R : relation A) := - reflexive : forall x, R x x. +Class reflexive A (R : relation A) := + reflexivity : forall x, R x x. -Class Irreflexive A (R : relation A) := - irreflexive : forall x, R x x -> False. +Class irreflexive A (R : relation A) := + irreflexivity : forall x, R x x -> False. -Class Symmetric A (R : relation A) := - symmetric : forall x y, R x y -> R y x. +Class symmetric A (R : relation A) := + symmetry : forall x y, R x y -> R y x. -Class Asymmetric A (R : relation A) := - asymmetric : forall x y, R x y -> R y x -> False. +Class asymmetric A (R : relation A) := + asymmetry : forall x y, R x y -> R y x -> False. -Class Transitive A (R : relation A) := - transitive : forall x y z, R x y -> R y z -> R x z. +Class transitive A (R : relation A) := + transitivity : forall x y z, R x y -> R y z -> R x z. -Implicit Arguments Reflexive [A]. -Implicit Arguments Irreflexive [A]. -Implicit Arguments Symmetric [A]. -Implicit Arguments Asymmetric [A]. -Implicit Arguments Transitive [A]. +Implicit Arguments reflexive [A]. +Implicit Arguments irreflexive [A]. +Implicit Arguments symmetric [A]. +Implicit Arguments asymmetric [A]. +Implicit Arguments transitive [A]. -Hint Resolve @irreflexive : ord. +Hint Resolve @irreflexivity : ord. (** We can already dualize all these properties. *) -Program Instance [ bla : ! Reflexive A R ] => flip_reflexive : Reflexive (flip R) := - reflexive := reflexive (R:=R). +Program Instance [ ! reflexive A R ] => flip_reflexive : reflexive (flip R) := + reflexivity := reflexivity (R:=R). -Program Instance [ ! Irreflexive A R ] => flip_irreflexive : Irreflexive (flip R) := - irreflexive := irreflexive (R:=R). +Program Instance [ ! irreflexive A R ] => flip_irreflexive : irreflexive (flip R) := + irreflexivity := irreflexivity (R:=R). -Program Instance [ ! Symmetric A R ] => flip_symmetric : Symmetric (flip R). +Program Instance [ ! symmetric A R ] => flip_symmetric : symmetric (flip R). Solve Obligations using unfold flip ; program_simpl ; clapply symmetric. -Program Instance [ ! Asymmetric A R ] => flip_asymmetric : Asymmetric (flip R). +Program Instance [ ! asymmetric A R ] => flip_asymmetric : asymmetric (flip R). - Solve Obligations using program_simpl ; unfold flip in * ; intros ; clapply asymmetric. + Solve Obligations using program_simpl ; unfold flip in * ; intros ; clapply asymmetry. -Program Instance [ ! Transitive A R ] => flip_transitive : Transitive (flip R). +Program Instance [ ! transitive A R ] => flip_transitive : transitive (flip R). - Solve Obligations using unfold flip ; program_simpl ; clapply transitive. + Solve Obligations using unfold flip ; program_simpl ; clapply transitivity. (** Have to do it again for Prop. *) -Program Instance [ ! Reflexive A (R : relation A) ] => inverse_reflexive : Reflexive (inverse R) := - reflexive := reflexive (R:=R). +Program Instance [ ! reflexive A (R : relation A) ] => inverse_reflexive : reflexive (inverse R) := + reflexivity := reflexivity (R:=R). -Program Instance [ ! Irreflexive A (R : relation A) ] => inverse_irreflexive : Irreflexive (inverse R) := - irreflexive := irreflexive (R:=R). +Program Instance [ ! irreflexive A (R : relation A) ] => inverse_irreflexive : irreflexive (inverse R) := + irreflexivity := irreflexivity (R:=R). -Program Instance [ ! Symmetric A (R : relation A) ] => inverse_symmetric : Symmetric (inverse R). +Program Instance [ ! symmetric A (R : relation A) ] => inverse_symmetric : symmetric (inverse R). Solve Obligations using unfold inverse, flip ; program_simpl ; clapply symmetric. -Program Instance [ ! Asymmetric A (R : relation A) ] => inverse_asymmetric : Asymmetric (inverse R). +Program Instance [ ! asymmetric A (R : relation A) ] => inverse_asymmetric : asymmetric (inverse R). - Solve Obligations using program_simpl ; unfold inverse, flip in * ; intros ; clapply asymmetric. + Solve Obligations using program_simpl ; unfold inverse, flip in * ; intros ; clapply asymmetry. -Program Instance [ ! Transitive A (R : relation A) ] => inverse_transitive : Transitive (inverse R). +Program Instance [ ! transitive A (R : relation A) ] => inverse_transitive : transitive (inverse R). - Solve Obligations using unfold inverse, flip ; program_simpl ; clapply transitive. + Solve Obligations using unfold inverse, flip ; program_simpl ; clapply transitivity. -Program Instance [ ! Reflexive A (R : relation A) ] => - reflexive_complement_irreflexive : Irreflexive (complement R). +Program Instance [ ! reflexive A (R : relation A) ] => + reflexive_complement_irreflexive : irreflexive (complement R). - Next Obligation. - Proof. - apply H. - apply reflexive. - Qed. - -Program Instance [ ! Irreflexive A (R : relation A) ] => - irreflexive_complement_reflexive : Reflexive (complement R). +Program Instance [ ! irreflexive A (R : relation A) ] => + irreflexive_complement_reflexive : reflexive (complement R). Next Obligation. Proof. red. intros H. - apply (irreflexive H). + apply (irreflexivity H). Qed. -Program Instance [ ! Symmetric A (R : relation A) ] => complement_symmetric : Symmetric (complement R). +Program Instance [ ! symmetric A (R : relation A) ] => complement_symmetric : symmetric (complement R). Next Obligation. Proof. red ; intros H'. - apply (H (symmetric H')). + apply (H (symmetry H')). Qed. (** * Standard instances. *) +Ltac reduce_goal := + match goal with + | [ |- _ <-> _ ] => fail 1 + | _ => red ; intros ; try reduce_goal + end. + +Ltac reduce := reduce_goal. + +Tactic Notation "apply" "*" constr(t) := + first [ refine t | refine (t _) | refine (t _ _) | refine (t _ _ _) | refine (t _ _ _ _) | + refine (t _ _ _ _ _) | refine (t _ _ _ _ _ _) | refine (t _ _ _ _ _ _ _) ]. + Ltac simpl_relation := - try red ; unfold inverse, flip, impl, arrow ; program_simpl ; try tauto ; - repeat (red ; intros) ; try ( solve [ intuition ]). + unfold inverse, flip, impl, arrow ; try reduce ; program_simpl ; + try ( solve [ intuition ]). Ltac obligations_tactic ::= simpl_relation. (** Logical implication. *) -Program Instance impl_refl : Reflexive impl. -Program Instance impl_trans : Transitive impl. +Program Instance impl_refl : reflexive impl. +Program Instance impl_trans : transitive impl. (** Logical equivalence. *) -Program Instance iff_refl : Reflexive iff. -Program Instance iff_sym : Symmetric iff. -Program Instance iff_trans : Transitive iff. +Program Instance iff_refl : reflexive iff. +Program Instance iff_sym : symmetric iff. +Program Instance iff_trans : transitive iff. (** Leibniz equality. *) -Program Instance eq_refl : Reflexive (@eq A). -Program Instance eq_sym : Symmetric (@eq A). -Program Instance eq_trans : Transitive (@eq A). +Program Instance eq_refl : reflexive (@eq A). +Program Instance eq_sym : symmetric (@eq A). +Program Instance eq_trans : transitive (@eq A). (** Various combinations of reflexivity, symmetry and transitivity. *) (** A [PreOrder] is both reflexive and transitive. *) Class PreOrder A (R : relation A) := - preorder_refl :> Reflexive R ; - preorder_trans :> Transitive R. + preorder_refl :> reflexive R ; + preorder_trans :> transitive R. (** A partial equivalence relation is symmetric and transitive. *) Class PER (carrier : Type) (pequiv : relation carrier) := - per_sym :> Symmetric pequiv ; - per_trans :> Transitive pequiv. + per_sym :> symmetric pequiv ; + per_trans :> transitive pequiv. (** We can build a PER on the Coq function space if we have PERs on the domain and codomain. *) @@ -187,33 +193,28 @@ Program Instance [ PER A (R : relation A), PER B (R' : relation B) ] => Next Obligation. Proof with auto. - constructor ; intros... assert(R x0 x0). - clapply transitive. clapply symmetric. - clapply transitive. + transitivity y0... symmetry... + transitivity (y x0)... Qed. (** The [Equivalence] typeclass. *) Class Equivalence (carrier : Type) (equiv : relation carrier) := - equiv_refl :> Reflexive equiv ; - equiv_sym :> Symmetric equiv ; - equiv_trans :> Transitive equiv. + equiv_refl :> reflexive equiv ; + equiv_sym :> symmetric equiv ; + equiv_trans :> transitive equiv. (** We can now define antisymmetry w.r.t. an equivalence relation on the carrier. *) -Class [ Equivalence A eqA ] => Antisymmetric (R : relation A) := - antisymmetric : forall x y, R x y -> R y x -> eqA x y. - -Program Instance [ eq : Equivalence A eqA, Antisymmetric eq R ] => - flip_antisymmetric : Antisymmetric eq (flip R). - - Solve Obligations using unfold inverse, flip ; program_simpl ; eapply @antisymmetric ; eauto. +Class [ Equivalence A eqA ] => antisymmetric (R : relation A) := + antisymmetry : forall x y, R x y -> R y x -> eqA x y. -Program Instance [ eq : Equivalence A eqA, Antisymmetric eq (R : relation A) ] => - inverse_antisymmetric : Antisymmetric eq (inverse R). +Program Instance [ eq : Equivalence A eqA, antisymmetric eq R ] => + flip_antisymmetric : antisymmetric eq (flip R). - Solve Obligations using unfold inverse, flip ; program_simpl ; eapply @antisymmetric ; eauto. +Program Instance [ eq : Equivalence A eqA, antisymmetric eq (R : relation A) ] => + inverse_antisymmetric : antisymmetric eq (inverse R). (** Leibinz equality [eq] is an equivalence relation. *) @@ -240,18 +241,6 @@ Program Instance relation_equivalence_equivalence : Next Obligation. Proof. - constructor ; red ; intros. - apply reflexive. - Qed. - - Next Obligation. - Proof. - constructor ; red ; intros. - apply symmetric ; apply H. - Qed. - - Next Obligation. - Proof. - constructor ; red ; intros. - apply transitive with (y x0 y0) ; [ apply H | apply H0 ]. + unfold relation_equivalence in *. + apply transitivity with (y x0 y0) ; [ apply H | apply H0 ]. Qed. diff --git a/theories/Classes/SetoidClass.v b/theories/Classes/SetoidClass.v index 5cf33542c..d2ee4f443 100644 --- a/theories/Classes/SetoidClass.v +++ b/theories/Classes/SetoidClass.v @@ -40,13 +40,13 @@ Typeclasses unfold @equiv. (** Shortcuts to make proof search easier. *) -Definition setoid_refl [ sa : Setoid A ] : Reflexive equiv. +Definition setoid_refl [ sa : Setoid A ] : reflexive equiv. Proof. eauto with typeclass_instances. Qed. -Definition setoid_sym [ sa : Setoid A ] : Symmetric equiv. +Definition setoid_sym [ sa : Setoid A ] : symmetric equiv. Proof. eauto with typeclass_instances. Qed. -Definition setoid_trans [ sa : Setoid A ] : Transitive equiv. +Definition setoid_trans [ sa : Setoid A ] : transitive equiv. Proof. eauto with typeclass_instances. Qed. Existing Instance setoid_refl. diff --git a/theories/Classes/SetoidTactics.v b/theories/Classes/SetoidTactics.v index 9f6dfab42..ee8c530fa 100644 --- a/theories/Classes/SetoidTactics.v +++ b/theories/Classes/SetoidTactics.v @@ -74,7 +74,7 @@ Ltac red_subst_eq_morphism concl := Ltac destruct_morphism := match goal with - | [ |- @Morphism ?A ?R ?m ] => constructor + | [ |- @Morphism ?A ?R ?m ] => red end. Ltac reverse_arrows x := @@ -91,4 +91,3 @@ Ltac default_add_morphism_tactic := end. Ltac add_morphism_tactic := default_add_morphism_tactic. - diff --git a/theories/FSets/FSetFacts.v b/theories/FSets/FSetFacts.v index b0c8ee008..0c19176f8 100644 --- a/theories/FSets/FSetFacts.v +++ b/theories/FSets/FSetFacts.v @@ -431,7 +431,7 @@ Add Relation t Subset Instance In_s_m : Morphism (E.eq ==> Subset ++> impl) In | 1. Proof. - do 2 red ; intros. unfold Subset, impl; intros; eauto with set. + simpl_relation. eauto with set. Qed. Add Morphism Empty with signature Subset --> impl as Empty_s_m. diff --git a/toplevel/classes.ml b/toplevel/classes.ml index 3896f02dd..cff8bce1e 100644 --- a/toplevel/classes.ml +++ b/toplevel/classes.ml @@ -129,26 +129,21 @@ let declare_implicit_proj c proj imps sub = Impargs.declare_manual_implicits true (ConstRef proj) true expls let declare_implicits impls subs cl = - let projs = Recordops.lookup_projections cl.cl_impl in - Util.list_iter3 - (fun c imps sub -> - match c with - | None -> assert(false) - | Some p -> declare_implicit_proj cl p imps sub) - projs impls subs; - let len = List.length cl.cl_context in - let indimps = - list_fold_left_i - (fun i acc (is, (na, b, t)) -> - if len - i <= cl.cl_params then acc - else - match is with - None | Some (_, false) -> (ExplByPos (i, Some na), (false, true)) :: acc - | _ -> acc) - 1 [] (List.rev cl.cl_context) - in - Impargs.declare_manual_implicits true (IndRef cl.cl_impl) false indimps - + Util.list_iter3 (fun p imps sub -> declare_implicit_proj cl p imps sub) + cl.cl_projs impls subs; + let len = List.length cl.cl_context in + let indimps = + list_fold_left_i + (fun i acc (is, (na, b, t)) -> + if len - i <= cl.cl_params then acc + else + match is with + None | Some (_, false) -> (ExplByPos (i, Some na), (false, true)) :: acc + | _ -> acc) + 1 [] (List.rev cl.cl_context) + in + Impargs.declare_manual_implicits true cl.cl_impl false indimps + let rel_of_named_context subst l = List.fold_right (fun (id, _, t) (ctx, acc) -> (Name id, None, subst_vars acc t) :: ctx, id :: acc) @@ -277,26 +272,54 @@ let new_class id par ar sup props = let ctx_props = Evarutil.nf_named_context_evar sigma ctx_props in let arity = Reductionops.nf_evar sigma arity in let ce t = Evarutil.check_evars env0 Evd.empty isevars t in - let kn = - let idb = id_of_string ("Build_" ^ (string_of_id (snd id))) in + let impl, projs = let params, subst = rel_of_named_context [] ctx_params in let fields, _ = rel_of_named_context subst ctx_props in List.iter (fun (_,c,t) -> ce t; match c with Some c -> ce c | None -> ()) (params @ fields); - declare_structure env0 (snd id) idb params arity fields + match fields with + [(Name proj_name, _, field)] -> + let class_type = it_mkProd_or_LetIn arity params in + let class_body = it_mkLambda_or_LetIn field params in + let class_entry = + { const_entry_body = class_body; + const_entry_type = Some class_type; + const_entry_opaque = false; + const_entry_boxed = false } + in + let cst = Declare.declare_constant (snd id) + (DefinitionEntry class_entry, IsDefinition Definition) + in + let inst_type = appvectc (mkConst cst) (rel_vect 0 (List.length params)) in + let proj_type = it_mkProd_or_LetIn (mkProd(Name (snd id), inst_type, lift 1 field)) params in + let proj_body = it_mkLambda_or_LetIn (mkLambda (Name (snd id), inst_type, mkRel 1)) params in + let proj_entry = + { const_entry_body = proj_body; + const_entry_type = Some proj_type; + const_entry_opaque = false; + const_entry_boxed = false } + in + let proj_cst = Declare.declare_constant proj_name + (DefinitionEntry proj_entry, IsDefinition Definition) + in + ConstRef cst, [proj_cst] + | _ -> + let idb = id_of_string ("Build_" ^ (string_of_id (snd id))) in + let kn = declare_structure env0 (snd id) idb params arity fields in + IndRef kn, (List.map Option.get (Recordops.lookup_projections kn)) in let ctx_context = List.map (fun ((na, b, t) as d) -> match Typeclasses.class_of_constr t with - | Some cl -> (Some (cl.cl_name, List.exists (fun (_, n) -> n = Name na) supnames), d) + | Some cl -> (Some (cl.cl_impl, List.exists (fun (_, n) -> n = Name na) supnames), d) | None -> (None, d)) ctx_params in let k = - { cl_name = snd id; + { cl_impl = impl; cl_params = List.length par; cl_context = ctx_context; cl_props = ctx_props; - cl_impl = kn } + cl_projs = projs } in declare_implicits (List.rev prop_impls) subs k; add_class k @@ -324,15 +347,7 @@ let subst_named inst subst ctx = (fun (id, _, t) (ctx, k) -> (id, None, substnl inst k t) :: ctx, succ k) ctx' ([], 0) in ctx' - -let destClass c = - match kind_of_term c with - App (c, args) -> - (match kind_of_term c with - | Ind ind -> (try class_of_inductive ind, args with _ -> assert false) - | _ -> assert false) - | _ -> assert false - +(* let infer_super_instances env params params_ctx super = let super = subst_named params params_ctx super in List.fold_right @@ -346,7 +361,7 @@ let infer_super_instances env params params_ctx super = in let d = (na, Some inst, t) in inst :: sups, na :: ids, d :: supctx) - super ([], [], []) + super ([], [], [])*) (* let evars_of_context ctx id n env = *) (* List.fold_right (fun (na, _, t) (n, env, nc) -> *) @@ -374,6 +389,14 @@ let destClassApp cl = let refine_ref = ref (fun _ -> assert(false)) +let id_of_class cl = + match cl.cl_impl with + | ConstRef kn -> let _,_,l = repr_con kn in id_of_label l + | IndRef (kn,i) -> + let mip = (Environ.lookup_mind kn (Global.env ())).Declarations.mind_packets in + mip.(0).Declarations.mind_typename + | _ -> assert false + open Pp let ($$) g f = fun x -> g (f x) @@ -386,11 +409,8 @@ let new_instance ctx (instid, bk, cl) props pri hook = let tclass = match bk with | Explicit -> - let id, par = Implicit_quantifiers.destClassAppExpl cl in - let k = - try class_info (snd id) - with Not_found -> unbound_class env id - in + let loc, id, par = Implicit_quantifiers.destClassAppExpl cl in + let k = class_info (global id) in let applen = List.fold_left (fun acc (x, y) -> if y = None then succ acc else acc) 0 par in let needlen = List.fold_left (fun acc (x, y) -> if x = None then succ acc else acc) 0 k.cl_context in if needlen <> applen then @@ -407,7 +427,7 @@ let new_instance ctx (instid, bk, cl) props pri hook = in t, avoid | None -> failwith ("new instance: under-applied typeclass")) par (List.rev k.cl_context) - in Topconstr.CAppExpl (Util.dummy_loc, (None, Ident id), pars) + in Topconstr.CAppExpl (loc, (None, id), pars) | Implicit -> cl in @@ -421,13 +441,8 @@ let new_instance ctx (instid, bk, cl) props pri hook = let c = Command.generalize_constr_expr tclass ctx in let _imps, c' = interp_type_evars isevars env c in let ctx, c = decompose_named_assum c' in - (match kind_of_term c with - App (c, args) -> - let cl = Option.get (class_of_constr c) in - cl, ctx, substitution_of_constrs (List.map snd cl.cl_context) (List.rev (Array.to_list args)) - | _ -> - let cl = Option.get (class_of_constr c) in - cl, ctx, []) + let cl, args = Typeclasses.dest_class_app c in + cl, ctx, substitution_of_constrs (List.map snd cl.cl_context) (List.rev (Array.to_list args)) in let id = match snd instid with @@ -437,7 +452,7 @@ let new_instance ctx (instid, bk, cl) props pri hook = errorlabstrm "new_instance" (Nameops.pr_id id ++ Pp.str " already exists"); id | Anonymous -> - let i = Nameops.add_suffix k.cl_name "_instance_0" in + let i = Nameops.add_suffix (id_of_class k) "_instance_0" in Termops.next_global_ident_away false i (Termops.ids_of_context env) in let env' = push_named_context ctx' env in @@ -465,18 +480,17 @@ let new_instance ctx (instid, bk, cl) props pri hook = ([], props) k.cl_props in if rest <> [] then - unbound_method env' k.cl_name (fst (List.hd rest)) + unbound_method env' k.cl_impl (fst (List.hd rest)) else type_ctx_instance isevars env' k.cl_props props substctx in - let app = - applistc (mkConstruct (k.cl_impl, 1)) (List.rev_map snd subst) - in + let inst_constr, ty_constr = instance_constructor k in + let app = inst_constr (List.rev_map snd subst) in let term = Termops.it_mkNamedLambda_or_LetIn app ctx' in isevars := Evarutil.nf_evar_defs !isevars; let term = Evarutil.nf_isevar !isevars term in let termtype = - let app = applistc (mkInd (k.cl_impl)) (List.rev_map snd substctx) in + let app = applistc ty_constr (List.rev_map snd substctx) in let t = it_mkNamedProd_or_LetIn app ctx' in Evarutil.nf_isevar !isevars t in diff --git a/toplevel/classes.mli b/toplevel/classes.mli index 248ed8c95..6671eed72 100644 --- a/toplevel/classes.mli +++ b/toplevel/classes.mli @@ -29,10 +29,10 @@ type binder_def_list = (identifier located * identifier located list * constr_ex val binders_of_lidents : identifier located list -> local_binder list val declare_implicit_proj : typeclass -> constant -> Impargs.manual_explicitation list -> bool -> unit - +(* val infer_super_instances : env -> constr list -> named_context -> named_context -> types list * identifier list * named_context - +*) val new_class : identifier located -> local_binder list -> Vernacexpr.sort_expr located -> @@ -46,6 +46,9 @@ val new_instance : int option -> (constant -> unit) -> identifier + +(* For generation on names based on classes only *) +val id_of_class : typeclass -> identifier val context : ?hook:(Libnames.global_reference -> unit) -> typeclass_context -> unit @@ -76,3 +79,4 @@ val push_named_context : named_context -> env -> env val name_typeclass_binders : Idset.t -> Topconstr.local_binder list -> Topconstr.local_binder list * Idset.t + diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index 4d1b608e6..70441e50d 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -471,12 +471,12 @@ let explain_pretype_error env err = (* Typeclass errors *) -let explain_unbound_class env (_,id) = - str "Unbound class name " ++ Nameops.pr_id id +let explain_not_a_class env c = + pr_constr_env env c ++ str" is not a declared type class" let explain_unbound_method env cid id = str "Unbound method name " ++ Nameops.pr_id (snd id) ++ spc () ++ str"of class" ++ spc () ++ - Nameops.pr_id cid + pr_global cid let pr_constr_exprs exprs = hv 0 (List.fold_right @@ -495,7 +495,7 @@ let explain_mismatched_contexts env c i j = let explain_typeclass_error env err = match err with - | UnboundClass id -> explain_unbound_class env id + | NotAClass c -> explain_not_a_class env c | UnboundMethod (cid, id) -> explain_unbound_method env cid id | NoInstance (id, l) -> explain_no_instance env id l | MismatchedContextInstance (c, i, j) -> explain_mismatched_contexts env c i j diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 45a0f834b..4e2901319 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -227,6 +227,9 @@ let dump_universes s = with e -> close_out output; raise e +let print_instances c = + ppnl (Prettyp.print_instances (global c)) + (*********************) (* "Locate" commands *) @@ -974,7 +977,7 @@ let vernac_print = function | PrintGraph -> ppnl (Prettyp.print_graph()) | PrintClasses -> ppnl (Prettyp.print_classes()) | PrintTypeClasses -> ppnl (Prettyp.print_typeclasses()) - | PrintInstances c -> ppnl (Prettyp.print_instances c) + | PrintInstances c -> print_instances c | PrintLtac qid -> ppnl (Tacinterp.print_ltac (snd (qualid_of_reference qid))) | PrintCoercions -> ppnl (Prettyp.print_coercions()) | PrintCoercionPaths (cls,clt) -> |