diff options
Diffstat (limited to 'toplevel/classes.ml')
| -rw-r--r-- | toplevel/classes.ml | 343 |
1 files changed, 73 insertions, 270 deletions
diff --git a/toplevel/classes.ml b/toplevel/classes.ml index 511befd8..04945040 100644 --- a/toplevel/classes.ml +++ b/toplevel/classes.ml @@ -7,7 +7,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: classes.ml 11309 2008-08-06 10:30:35Z herbelin $ i*) +(*i $Id: classes.ml 11800 2009-01-18 18:34:15Z msozeau $ i*) (*i*) open Names @@ -32,19 +32,23 @@ open Topconstr open Decl_kinds open Entries -let hint_db = "typeclass_instances" +let typeclasses_db = "typeclass_instances" let qualid_of_con c = Qualid (dummy_loc, shortest_qualid_of_global Idset.empty (ConstRef c)) +let set_rigid c = + Auto.add_hints false [typeclasses_db] + (Vernacexpr.HintsTransparency ([qualid_of_con c], false)) + let _ = Typeclasses.register_add_instance_hint (fun inst pri -> Flags.silently (fun () -> - Auto.add_hints false [hint_db] + Auto.add_hints false [typeclasses_db] (Vernacexpr.HintsResolve - [pri, CAppExpl (dummy_loc, (None, qualid_of_con inst), [])])) ()) - + [pri, false, CAppExpl (dummy_loc, (None, qualid_of_con inst), [])])) ()) + let declare_instance_cst glob con = let instance = Typeops.type_of_constant (Global.env ()) con in let _, r = decompose_prod_assum instance in @@ -67,207 +71,27 @@ type binder_list = (identifier located * bool * constr_expr) list (* Calls to interpretation functions. *) -let interp_binders_evars isevars env avoid l = - List.fold_left - (fun (env, ids, params) ((loc, i), t) -> - let n = Name i in - let t' = interp_binder_evars isevars env n t in - let d = (i,None,t') in - (push_named d env, i :: ids, d::params)) - (env, avoid, []) l - -let interp_typeclass_context_evars isevars env avoid l = - List.fold_left - (fun (env, ids, params) (iid, bk, l) -> - let t' = interp_binder_evars isevars env (snd iid) l in - let i = match snd iid with - | Anonymous -> Nameops.next_name_away (Termops.named_hd env t' Anonymous) ids - | Name id -> id - in - let d = (i,None,t') in - (push_named d env, i :: ids, d::params)) - (env, avoid, []) l - let interp_type_evars evdref env ?(impls=([],[])) typ = let typ' = intern_gen true ~impls (Evd.evars_of !evdref) env typ in let imps = Implicit_quantifiers.implicits_of_rawterm typ' in imps, Pretyping.Default.understand_tcc_evars evdref env Pretyping.IsType typ' - -let mk_interning_data env na impls typ = - let impl = Impargs.compute_implicits_with_manual env typ (Impargs.is_implicit_args()) impls - in (na, ([], impl, Notation.compute_arguments_scope typ)) -let interp_fields_evars isevars env avoid l = - List.fold_left - (fun (env, uimpls, ids, params, impls) ((loc, i), _, t) -> - let impl, t' = interp_type_evars isevars env ~impls t in - let data = mk_interning_data env i impl t' in - let d = (Name i,None,t') in - (push_rel d env, impl :: uimpls, Idset.add i ids, d::params, ([], data :: snd impls))) - (env, [], avoid, [], ([], [])) l - (* Declare everything in the parameters as implicit, and the class instance as well *) open Topconstr - -let implicits_of_context ctx = - list_map_i (fun i name -> - let explname = - match name with - | Name n -> Some n - | Anonymous -> None - in ExplByPos (i, explname), (true, true)) - 1 (List.rev (Anonymous :: (List.map pi1 ctx))) - -let degenerate_decl (na,b,t) = - let id = match na with - | Name id -> id - | Anonymous -> anomaly "Unnamed record variable" in - match b with - | None -> (id, Entries.LocalAssum t) - | Some b -> (id, Entries.LocalDef b) - -let name_typeclass_binder avoid = function - | LocalRawAssum ([loc, Anonymous], bk, c) -> - let name = - let id = - match c with - CApp (_, (_, CRef (Ident (loc,id))), _) -> id - | _ -> id_of_string "assum" - in Implicit_quantifiers.make_fresh avoid (Global.env ()) id - in LocalRawAssum ([loc, Name name], bk, c), Idset.add name avoid - | x -> x, avoid - -let name_typeclass_binders avoid l = - let l', avoid = - List.fold_left - (fun (binders, avoid) b -> let b', avoid = name_typeclass_binder avoid b in - b' :: binders, avoid) - ([], avoid) l - in List.rev l', avoid - -let new_class id par ar sup props = - let env0 = Global.env() in - let isevars = ref (Evd.create_evar_defs Evd.empty) in - let bound = Implicit_quantifiers.ids_of_list (Termops.ids_of_context env0) in - let bound, ids = Implicit_quantifiers.free_vars_of_binders ~bound [] (sup @ par) in - let bound = Idset.union bound (Implicit_quantifiers.ids_of_list ids) in - let sup, bound = name_typeclass_binders bound sup in - let supnames = - List.fold_left (fun acc b -> - match b with - LocalRawAssum (nl, _, _) -> nl @ acc - | LocalRawDef _ -> assert(false)) - [] sup - in - - (* Interpret the arity *) - let arity_imps, fullarity = - let ar = - match ar with - Some ar -> ar | None -> (dummy_loc, Rawterm.RType None) - in - let arity = CSort (fst ar, snd ar) in - let term = prod_constr_expr (prod_constr_expr arity par) sup in - interp_type_evars isevars env0 term - in - let ctx_params, arity = decompose_prod_assum fullarity in - let env_params = push_rel_context ctx_params env0 in - (* Interpret the definitions and propositions *) - let env_props, prop_impls, bound, ctx_props, _ = - interp_fields_evars isevars env_params bound props - in - let subs = List.map (fun ((loc, id), b, _) -> b) props in - (* Instantiate evars and check all are resolved *) - let isevars,_ = Evarconv.consider_remaining_unif_problems env_props !isevars in - let isevars = Typeclasses.resolve_typeclasses env_props isevars in - let sigma = Evd.evars_of isevars in - let ctx_params = Evarutil.nf_rel_context_evar sigma ctx_params in - let ctx_props = Evarutil.nf_rel_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 fieldimpls = - (* Make the class and all params implicits in the projections *) - let ctx_impls = implicits_of_context ctx_params in - let len = succ (List.length ctx_params) in - List.map (fun x -> ctx_impls @ Impargs.lift_implicits len x) prop_impls - in - let impl, projs = - let params = ctx_params and fields = ctx_props in - List.iter (fun (_,c,t) -> ce t; match c with Some c -> ce c | None -> ()) (params @ fields); - match fields with - [(Name proj_name, _, field)] -> - let class_body = it_mkLambda_or_LetIn field params in - let class_type = - match ar with - Some _ -> Some (it_mkProd_or_LetIn arity params) - | None -> None - in - let class_entry = - { const_entry_body = class_body; - const_entry_type = 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 - let cref = ConstRef cst in - Impargs.declare_manual_implicits false cref (Impargs.is_implicit_args()) arity_imps; - Impargs.declare_manual_implicits false (ConstRef proj_cst) (Impargs.is_implicit_args()) (List.hd fieldimpls); - cref, [proj_name, proj_cst] - | _ -> - let idb = id_of_string ("Build_" ^ (string_of_id (snd id))) in - let idarg = Nameops.next_ident_away (snd id) (ids_of_context (Global.env())) in - let kn = Record.declare_structure (snd id) idb arity_imps - params arity fieldimpls fields ~kind:Method ~name:idarg false (List.map (fun _ -> false) fields) - in - IndRef (kn,0), (List.map2 (fun (id, _, _) y -> Nameops.out_name id, Option.get y) - fields (Recordops.lookup_projections (kn,0))) - in - let ctx_context = - List.map (fun ((na, b, t) as d) -> - match Typeclasses.class_of_constr t with - | Some cl -> (Some (cl.cl_impl, List.exists (fun (_, n) -> n = na) supnames), d) - | None -> (None, d)) - ctx_params - in - let k = - { cl_impl = impl; - cl_context = ctx_context; - cl_props = ctx_props; - cl_projs = projs } - in - List.iter2 (fun p sub -> if sub then declare_instance_cst true (snd p)) - k.cl_projs subs; - add_class k - -type binder_def_list = (identifier located * identifier located list * constr_expr) list - -let binders_of_lidents l = - List.map (fun (loc, id) -> LocalRawAssum ([loc, Name id], Default Rawterm.Implicit, CHole (loc, None))) l - let type_ctx_instance isevars env ctx inst subst = let (s, _) = List.fold_left2 - (fun (subst, instctx) (na, _, t) ce -> + (fun (subst, instctx) (na, b, t) ce -> let t' = substl subst t in - let c = interp_casted_constr_evars isevars env ce t' in - let d = na, Some c, t' in - c :: subst, d :: instctx) + let c' = + match b with + | None -> interp_casted_constr_evars isevars env ce t' + | Some b -> substl subst b + in + let d = na, Some c', t' in + c' :: subst, d :: instctx) (subst, []) (List.rev ctx) inst in s @@ -284,27 +108,10 @@ let id_of_class cl = open Pp let ($$) g f = fun x -> g (f x) - -let default_on_free_vars = - Flags.if_verbose - (fun fvs -> - match fvs with - [] -> () - | l -> msgnl (str"Implicitly generalizing " ++ - prlist_with_sep (fun () -> str", ") Nameops.pr_id l ++ str".")) - -let fail_on_free_vars = function - [] -> () - | [fv] -> - errorlabstrm "Classes" - (str"Unbound variable " ++ Nameops.pr_id fv ++ str".") - | fvs -> errorlabstrm "Classes" - (str"Unbound variables " ++ - prlist_with_sep (fun () -> str", ") Nameops.pr_id fvs ++ str".") let instance_hook k pri global imps ?hook cst = let inst = Typeclasses.new_instance k pri global cst in - Impargs.maybe_declare_manual_implicits false (ConstRef cst) false imps; + Impargs.maybe_declare_manual_implicits false (ConstRef cst) ~enriching:false imps; Typeclasses.add_instance inst; (match hook with Some h -> h cst | None -> ()) @@ -323,51 +130,30 @@ let declare_instance_constant k pri global imps ?hook id term termtype = instance_hook k pri global imps ?hook kn; id -let new_instance ?(global=false) ctx (instid, bk, cl) props ?(on_free_vars=default_on_free_vars) +let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true) ?(tac:Proof_type.tactic option) ?(hook:(Names.constant -> unit) option) pri = let env = Global.env() in let isevars = ref (Evd.create_evar_defs Evd.empty) in - let bound = Implicit_quantifiers.ids_of_list (Termops.ids_of_context env) in - let bound, fvs = Implicit_quantifiers.free_vars_of_binders ~bound [] ctx in let tclass = match bk with - | Implicit -> - 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 - mismatched_params env (List.map fst par) (List.map snd k.cl_context); - let pars, _ = Implicit_quantifiers.combine_params Idset.empty (* need no avoid *) - (fun avoid (clname, (id, _, t)) -> - match clname with - Some (cl, b) -> - let t = - if b then - let _k = class_info cl in - CHole (Util.dummy_loc, Some (Evd.ImplicitArg (k.cl_impl, (1, None)))) - else CHole (Util.dummy_loc, None) - in t, avoid - | None -> failwith ("new instance: under-applied typeclass")) - par (List.rev k.cl_context) - in Topconstr.CAppExpl (loc, (None, id), pars) - - | Explicit -> cl + | Implicit -> + Implicit_quantifiers.implicit_application Idset.empty ~allow_partial:false + (fun avoid (clname, (id, _, t)) -> + match clname with + | Some (cl, b) -> + let t = CHole (Util.dummy_loc, None) in + t, avoid + | None -> failwith ("new instance: under-applied typeclass")) + cl + | Explicit -> cl in - let ctx_bound = Idset.union bound (Implicit_quantifiers.ids_of_list fvs) in - let gen_ids = Implicit_quantifiers.free_vars_of_constr_expr ~bound:ctx_bound tclass [] in - on_free_vars (List.rev fvs @ List.rev gen_ids); - let gen_idset = Implicit_quantifiers.ids_of_list gen_ids in - let bound = Idset.union gen_idset ctx_bound in - let gen_ctx = Implicit_quantifiers.binder_list_of_ids gen_ids in - let ctx, avoid = name_typeclass_binders bound ctx in - let ctx = List.append ctx (List.rev gen_ctx) in + let tclass = if generalize then CGeneralization (dummy_loc, Implicit, Some AbsPi, tclass) else tclass in let k, ctx', imps, subst = let c = Command.generalize_constr_expr tclass ctx in let imps, c' = interp_type_evars isevars env c in let ctx, c = decompose_prod_assum c' in - let cl, args = Typeclasses.dest_class_app c in - cl, ctx, imps, List.rev (Array.to_list args) + let cl, args = Typeclasses.dest_class_app (push_rel_context ctx env) c in + cl, ctx, imps, List.rev args in let id = match snd instid with @@ -384,7 +170,7 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(on_free_vars=defau isevars := Evarutil.nf_evar_defs !isevars; isevars := resolve_typeclasses env !isevars; let sigma = Evd.evars_of !isevars in - let substctx = List.map (Evarutil.nf_evar sigma) subst in + let subst = List.map (Evarutil.nf_evar sigma) subst in if Lib.is_modtype () then begin let _, ty_constr = instance_constructor k (List.rev subst) in @@ -399,31 +185,48 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(on_free_vars=defau end else begin + let props = + match props with + | CRecord (loc, _, fs) -> + if List.length fs > List.length k.cl_props then + mismatched_props env' (List.map snd fs) k.cl_props; + fs + | _ -> + if List.length k.cl_props <> 1 then + errorlabstrm "new_instance" (Pp.str "Expected a definition for the instance body") + else [(dummy_loc, Nameops.out_name (pi1 (List.hd k.cl_props))), props] + in let subst = - let props = - List.map (fun (x, l, d) -> - x, Topconstr.abstract_constr_expr d (binders_of_lidents l)) - props - in - if List.length props > List.length k.cl_props then - mismatched_props env' (List.map snd props) k.cl_props; - let props, rest = - List.fold_left - (fun (props, rest) (id,_,_) -> - try - let ((loc, mid), c) = List.find (fun ((_,id'), c) -> Name id' = id) rest in - let rest' = List.filter (fun ((_,id'), c) -> Name id' <> id) rest in - Constrintern.add_glob loc (ConstRef (List.assoc mid k.cl_projs)); - c :: props, rest' - with Not_found -> (CHole (Util.dummy_loc, None) :: props), rest) - ([], props) k.cl_props - in - if rest <> [] then - unbound_method env' k.cl_impl (fst (List.hd rest)) - else - type_ctx_instance isevars env' k.cl_props props substctx + match k.cl_props with + | [(na,b,ty)] -> + let term = match props with [] -> CHole (Util.dummy_loc, None) + | [(_,f)] -> f | _ -> assert false in + let ty' = substl subst ty in + let c = interp_casted_constr_evars isevars env' term ty' in + c :: subst + | _ -> + let props, rest = + List.fold_left + (fun (props, rest) (id,b,_) -> + try + let ((loc, mid), c) = List.find (fun ((_,id'), c) -> Name id' = id) rest in + let rest' = List.filter (fun ((_,id'), c) -> Name id' <> id) rest in + Option.iter (fun x -> Dumpglob.add_glob loc (ConstRef x)) (List.assoc mid k.cl_projs); + c :: props, rest' + with Not_found -> + (CHole (Util.dummy_loc, None) :: props), rest) + ([], props) k.cl_props + in + if rest <> [] then + unbound_method env' k.cl_impl (fst (List.hd rest)) + else + type_ctx_instance isevars env' k.cl_props props subst + in + let subst = List.fold_left2 + (fun subst' s (_, b, _) -> if b = None then s :: subst' else subst') + [] subst (k.cl_props @ snd k.cl_context) in - let app, ty_constr = instance_constructor k (List.rev subst) in + let app, ty_constr = instance_constructor k subst in let termtype = let t = it_mkProd_or_LetIn ty_constr ctx' in Evarutil.nf_isevar !isevars t |