diff options
Diffstat (limited to 'contrib/subtac/subtac_classes.ml')
| -rw-r--r-- | contrib/subtac/subtac_classes.ml | 159 |
1 files changed, 79 insertions, 80 deletions
diff --git a/contrib/subtac/subtac_classes.ml b/contrib/subtac/subtac_classes.ml index 9a5539e2..0d44a0c0 100644 --- a/contrib/subtac/subtac_classes.ml +++ b/contrib/subtac/subtac_classes.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: subtac_classes.ml 11282 2008-07-28 11:51:53Z msozeau $ i*) +(*i $Id: subtac_classes.ml 11800 2009-01-18 18:34:15Z msozeau $ i*) open Pretyping open Evd @@ -92,104 +92,103 @@ let type_class_instance_params isevars env id n ctx inst subst = let substitution_of_constrs ctx cstrs = List.fold_right2 (fun c (na, _, _) acc -> (na, c) :: acc) cstrs ctx [] -let new_instance ?(global=false) ctx (instid, bk, cl) props ?(on_free_vars=Classes.default_on_free_vars) pri = +let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true) 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 - Classes.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.InternalHole) (* (Evd.ImplicitArg (IndRef 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) - + | Implicit -> + Implicit_quantifiers.implicit_application Idset.empty (* need no avoid *) + ~allow_partial:false (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.InternalHole) + else 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 - let bound = Idset.union (Implicit_quantifiers.ids_of_list gen_ids) ctx_bound in - on_free_vars (List.rev (gen_ids @ fvs)); - let gen_ctx = Implicit_quantifiers.binder_list_of_ids gen_ids in - let ctx, avoid = Classes.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 c', imps = interp_type_evars_impls ~evdref:isevars env c in let ctx, c = Sign.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 - Name id -> - let sp = Lib.make_path id in - if Nametab.exists_cci sp then - errorlabstrm "new_instance" (Nameops.pr_id id ++ Pp.str " already exists"); - id - | Anonymous -> - 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) + | Name id -> + let sp = Lib.make_path id in + if Nametab.exists_cci sp then + errorlabstrm "new_instance" (Nameops.pr_id id ++ Pp.str " already exists"); + id + | Anonymous -> + 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' = push_rel_context ctx' env in isevars := Evarutil.nf_evar_defs !isevars; isevars := resolve_typeclasses ~onlyargs:false ~fail:true env' !isevars; let sigma = Evd.evars_of !isevars in - let substctx = List.map (Evarutil.nf_evar sigma) subst in - let subst, _propsctx = + let subst = List.map (Evarutil.nf_evar sigma) subst in + let subst = let props = - List.map (fun (x, l, d) -> - x, Topconstr.abstract_constr_expr d (Classes.binders_of_lidents l)) - props + match props with + | CRecord (loc, _, fs) -> + if List.length fs > List.length k.cl_props then + Classes.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 - if List.length props > List.length k.cl_props then - Classes.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,_,_) -> + 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 + fst (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 inst_constr, ty_constr = instance_constructor k (List.rev subst) in - isevars := Evarutil.nf_evar_defs !isevars; - let term = Evarutil.nf_isevar !isevars (it_mkLambda_or_LetIn inst_constr ctx') - and termtype = Evarutil.nf_isevar !isevars (it_mkProd_or_LetIn ty_constr ctx') + let inst_constr, ty_constr = instance_constructor k subst in + isevars := Evarutil.nf_evar_defs !isevars; + let term = Evarutil.nf_isevar !isevars (it_mkLambda_or_LetIn inst_constr ctx') + and termtype = Evarutil.nf_isevar !isevars (it_mkProd_or_LetIn ty_constr ctx') + in + isevars := undefined_evars !isevars; + Evarutil.check_evars env Evd.empty !isevars termtype; + let hook gr = + let cst = match gr with ConstRef kn -> kn | _ -> assert false in + let inst = Typeclasses.new_instance k pri global cst in + Impargs.declare_manual_implicits false gr ~enriching:false imps; + Typeclasses.add_instance inst in - isevars := undefined_evars !isevars; - Evarutil.check_evars env Evd.empty !isevars termtype; - let hook gr = - let cst = match gr with ConstRef kn -> kn | _ -> assert false in - let inst = Typeclasses.new_instance k pri global cst in - Impargs.declare_manual_implicits false gr false imps; - Typeclasses.add_instance inst - in - let evm = Subtac_utils.evars_of_term (Evd.evars_of !isevars) Evd.empty term in - let obls, constr, typ = Eterm.eterm_obligations env id !isevars evm 0 term termtype in - ignore(Subtac_obligations.add_definition id constr typ ~kind:(Global,false,Instance) ~hook obls); - id + let evm = Subtac_utils.evars_of_term (Evd.evars_of !isevars) Evd.empty term in + let obls, constr, typ = Eterm.eterm_obligations env id !isevars evm 0 term termtype in + id, Subtac_obligations.add_definition id constr typ ~kind:(Global,false,Instance) ~hook obls + |