diff options
author | Stephane Glondu <steph@glondu.net> | 2010-07-21 09:46:51 +0200 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2010-07-21 09:46:51 +0200 |
commit | 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 (patch) | |
tree | 631ad791a7685edafeb1fb2e8faeedc8379318ae /toplevel/classes.ml | |
parent | da178a880e3ace820b41d38b191d3785b82991f5 (diff) |
Imported Upstream snapshot 8.3~beta0+13298
Diffstat (limited to 'toplevel/classes.ml')
-rw-r--r-- | toplevel/classes.ml | 345 |
1 files changed, 178 insertions, 167 deletions
diff --git a/toplevel/classes.ml b/toplevel/classes.ml index 1a1640a4..90daca12 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 12187 2009-06-13 19:36:59Z msozeau $ i*) +(*i $Id$ i*) (*i*) open Names @@ -34,36 +34,35 @@ open Entries 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 = +let set_typeclass_transparency c b = Auto.add_hints false [typeclasses_db] - (Vernacexpr.HintsTransparency ([qualid_of_con c], false)) - + (Auto.HintsTransparencyEntry ([c], b)) + let _ = - Typeclasses.register_add_instance_hint + Typeclasses.register_add_instance_hint (fun inst pri -> - Flags.silently (fun () -> - Auto.add_hints false [typeclasses_db] - (Vernacexpr.HintsResolve - [pri, false, CAppExpl (dummy_loc, (None, qualid_of_con inst), [])])) ()) + Flags.silently (fun () -> + Auto.add_hints false [typeclasses_db] + (Auto.HintsResolveEntry + [pri, false, constr_of_global inst])) ()); + Typeclasses.register_set_typeclass_transparency set_typeclass_transparency + +let declare_class g = + match global g with + | ConstRef x -> Typeclasses.add_constant_class x + | IndRef x -> Typeclasses.add_inductive_class x + | _ -> user_err_loc (loc_of_reference g, "declare_class", + Pp.str"Unsupported class type, only constants and inductives are allowed") -let declare_instance_cst glob con = - let instance = Typeops.type_of_constant (Global.env ()) con in +let declare_instance glob g = + let c = global g in + let instance = Typing.type_of (Global.env ()) Evd.empty (constr_of_global c) in let _, r = decompose_prod_assum instance in match class_of_constr r with - | Some tc -> add_instance (new_instance tc None glob con) - | None -> errorlabstrm "" (Pp.strbrk "Constant does not build instances of a declared type class.") + | Some tc -> add_instance (new_instance tc None glob c) + | None -> user_err_loc (loc_of_reference g, "declare_instance", + Pp.str "Constant does not build instances of a declared type class.") -let declare_instance glob idl = - let con = - try (match global (Ident idl) with - | ConstRef x -> x - | _ -> raise Not_found) - with _ -> error "Instance definition not found." - in declare_instance_cst glob con - let mismatched_params env n m = mismatched_ctx_inst env Parameters n m let mismatched_props env n m = mismatched_ctx_inst env Properties n m @@ -71,54 +70,53 @@ type binder_list = (identifier located * bool * constr_expr) list (* Calls to interpretation functions. *) -let interp_type_evars evdref env ?(impls=([],[])) typ = - let typ' = intern_gen true ~impls (Evd.evars_of !evdref) env typ in +let interp_type_evars evdref env ?(impls=empty_internalization_env) typ = + let typ' = intern_gen true ~impls !evdref env typ in let imps = Implicit_quantifiers.implicits_of_rawterm typ' in imps, Pretyping.Default.understand_tcc_evars evdref env Pretyping.IsType typ' - + (* Declare everything in the parameters as implicit, and the class instance as well *) open Topconstr - -let type_ctx_instance isevars env ctx inst subst = - let (s, _) = - List.fold_left2 - (fun (subst, instctx) (na, b, t) ce -> - let t' = substl subst t in - 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 + +let type_ctx_instance evars env ctx inst subst = + let rec aux (subst, instctx) l = function + (na, b, t) :: ctx -> + let t' = substl subst t in + let c', l = + match b with + | None -> interp_casted_constr_evars evars env (List.hd l) t', List.tl l + | Some b -> substl subst b, l + in + let d = na, Some c', t' in + aux (c' :: subst, d :: instctx) l ctx + | [] -> subst + in aux (subst, []) inst (List.rev ctx) 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) -> + | 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) - -let instance_hook k pri global imps ?hook cst = + +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) ~enriching:false imps; + Impargs.maybe_declare_manual_implicits false cst ~enriching:false imps; Typeclasses.add_instance inst; (match hook with Some h -> h cst | None -> ()) let declare_instance_constant k pri global imps ?hook id term termtype = - let cdecl = + let cdecl = let kind = IsDefinition Instance in - let entry = + let entry = { const_entry_body = term; const_entry_type = Some termtype; const_entry_opaque = false; @@ -126,137 +124,159 @@ let declare_instance_constant k pri global imps ?hook id term termtype = in DefinitionEntry entry, kind in let kn = Declare.declare_constant id cdecl in - Flags.if_verbose Command.definition_message id; - instance_hook k pri global imps ?hook kn; + Declare.definition_message id; + instance_hook k pri global imps ?hook (ConstRef kn); id -let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true) - ?(tac:Proof_type.tactic option) ?(hook:(Names.constant -> unit) option) pri = +let new_instance ?(abstract=false) ?(global=false) ctx (instid, bk, cl) props + ?(generalize=true) + ?(tac:Proof_type.tactic option) ?(hook:(global_reference -> unit) option) pri = let env = Global.env() in - let isevars = ref (Evd.create_evar_defs Evd.empty) in - let tclass = + let evars = ref Evd.empty in + let tclass, ids = match bk with | Implicit -> Implicit_quantifiers.implicit_application Idset.empty ~allow_partial:false - (fun avoid (clname, (id, _, t)) -> - match clname with - | Some (cl, b) -> + (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 + | Explicit -> cl, Idset.empty 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 (push_rel_context ctx env) c in - cl, ctx, imps, List.rev args + let k, cty, ctx', ctx, len, imps, subst = + let (env', ctx), imps = interp_context_evars evars env ctx in + let c', imps' = interp_type_evars_impls ~evdref:evars env' tclass in + let len = List.length ctx in + let imps = imps @ Impargs.lift_implicits len imps' in + let ctx', c = decompose_prod_assum c' in + let ctx'' = ctx' @ ctx in + let cl, args = Typeclasses.dest_class_app (push_rel_context ctx'' env) c in + let _, args = + List.fold_right (fun (na, b, t) (args, args') -> + match b with + | None -> (List.tl args, List.hd args :: args') + | Some b -> (args, substl args' b :: args')) + (snd cl.cl_context) (args, []) + in + cl, c', ctx', ctx, len, imps, args in - let id = + let id = match snd instid with - Name id -> + 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 -> + | Anonymous -> let i = Nameops.add_suffix (id_of_class k) "_instance_0" in - Termops.next_global_ident_away false i (Termops.ids_of_context env) + Namegen.next_global_ident_away i (Termops.ids_of_context env) in - let env' = push_rel_context ctx' env in - isevars := Evarutil.nf_evar_defs !isevars; - isevars := resolve_typeclasses env !isevars; - let sigma = Evd.evars_of !isevars in + let env' = push_rel_context ctx env in + evars := Evarutil.nf_evar_map !evars; + evars := resolve_typeclasses env !evars; + let sigma = !evars in let subst = List.map (Evarutil.nf_evar sigma) subst in - if Lib.is_modtype () then + if abstract then begin + if not (Lib.is_modtype ()) then + error "Declare Instance while not in Module Type."; let _, ty_constr = instance_constructor k (List.rev subst) in - let termtype = - let t = it_mkProd_or_LetIn ty_constr ctx' in - Evarutil.nf_isevar !isevars t + let termtype = + let t = it_mkProd_or_LetIn ty_constr (ctx' @ ctx) in + Evarutil.nf_evar !evars t in - Evarutil.check_evars env Evd.empty !isevars termtype; + Evarutil.check_evars env Evd.empty !evars termtype; let cst = Declare.declare_internal_constant id (Entries.ParameterEntry (termtype,false), Decl_kinds.IsAssumption Decl_kinds.Logical) - in instance_hook k None false imps ?hook cst; id + in instance_hook k None false imps ?hook (ConstRef cst); id end else begin - let props = + let props = match props with - | CRecord (loc, _, fs) -> - if List.length fs > List.length k.cl_props then + | 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] + Inl fs + | _ -> Inr props in - let subst = - 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 = + let subst = + match props with + | Inr term -> + let c = interp_casted_constr_evars evars env' term cty in + Inr (c, subst) + | Inl props -> + let get_id = + function + | Ident id' -> id' + | _ -> errorlabstrm "new_instance" (Pp.str "Only local structures are handled") + in + 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) + (fun (props, rest) (id,b,_) -> + if b = None then + try + let (loc_mid, c) = List.find (fun (id', _) -> Name (snd (get_id id')) = id) rest in + let rest' = List.filter (fun (id', _) -> Name (snd (get_id id')) <> id) rest in + let (loc, mid) = get_id loc_mid 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 + else props, rest) ([], props) k.cl_props in - if rest <> [] then - unbound_method env' k.cl_impl (fst (List.hd rest)) + if rest <> [] then + unbound_method env' k.cl_impl (get_id (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 subst in - let termtype = - let t = it_mkProd_or_LetIn ty_constr ctx' in - Evarutil.nf_isevar !isevars t + Inl (type_ctx_instance evars env' k.cl_props props subst) + in + evars := Evarutil.nf_evar_map !evars; + let term, termtype = + match subst with + | Inl subst -> + 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 subst in + let termtype = it_mkProd_or_LetIn ty_constr (ctx' @ ctx) in + let term = Termops.it_mkLambda_or_LetIn app (ctx' @ ctx) in + term, termtype + | Inr (def, subst) -> + let termtype = it_mkProd_or_LetIn cty ctx in + let term = Termops.it_mkLambda_or_LetIn def ctx in + term, termtype in - let term = Termops.it_mkLambda_or_LetIn app ctx' in - isevars := Evarutil.nf_evar_defs !isevars; - let term = Evarutil.nf_isevar !isevars term in - let evm = Evd.evars_of (undefined_evars !isevars) in - Evarutil.check_evars env Evd.empty !isevars termtype; - if evm = Evd.empty then + let termtype = Evarutil.nf_evar !evars termtype in + let term = Evarutil.nf_evar !evars term in + let evm = undefined_evars !evars in + Evarutil.check_evars env Evd.empty !evars termtype; + if Evd.is_empty evm then declare_instance_constant k pri global imps ?hook id term termtype else begin - isevars := Typeclasses.resolve_typeclasses ~onlyargs:true ~fail:true env !isevars; + evars := Typeclasses.resolve_typeclasses ~onlyargs:true ~fail:true env !evars; let kind = Decl_kinds.Global, Decl_kinds.DefinitionBody Decl_kinds.Instance in Flags.silently (fun () -> - Command.start_proof id kind termtype - (fun _ -> function ConstRef cst -> instance_hook k pri global imps ?hook cst - | _ -> assert false); - if props <> [] then - Pfedit.by (* (Refiner.tclTHEN (Refiner.tclEVARS (Evd.evars_of !isevars)) *) - (!refine_ref (evm, term)); + Lemmas.start_proof id kind termtype (fun _ -> instance_hook k pri global imps ?hook); + if props <> Inl [] then + Pfedit.by (* (Refiner.tclTHEN (Refiner.tclEVARS ( !isevars)) *) + (!refine_ref (evm, term)) + else if Flags.is_auto_intros () then + Pfedit.by (Refiner.tclDO len Tactics.intro); (match tac with Some tac -> Pfedit.by tac | None -> ())) (); Flags.if_verbose (msg $$ Printer.pr_open_subgoals) (); id end end - + let named_of_rel_context l = - let acc, ctx = - List.fold_right + let acc, ctx = + List.fold_right (fun (na, b, t) (subst, ctx) -> let id = match na with Anonymous -> raise (Invalid_argument "named_of_rel_context") | Name id -> id in let d = (id, Option.map (substl subst) b, substl subst t) in @@ -274,42 +294,33 @@ let rec list_filter_map f = function let context ?(hook=fun _ -> ()) l = let env = Global.env() in - let evars = ref (Evd.create_evar_defs Evd.empty) in + let evars = ref Evd.empty in let (env', fullctx), impls = interp_context_evars evars env l in - let fullctx = Evarutil.nf_rel_context_evar (Evd.evars_of !evars) fullctx in + let fullctx = Evarutil.nf_rel_context_evar !evars fullctx in let ce t = Evarutil.check_evars env Evd.empty !evars t in List.iter (fun (n, b, t) -> Option.iter ce b; ce t) fullctx; - let ctx = try named_of_rel_context fullctx with _ -> + let ctx = try named_of_rel_context fullctx with _ -> error "Anonymous variables not allowed in contexts." in - let env = push_named_context ctx env in - let keeps = - List.fold_left (fun acc (id,_,t) -> - match class_of_constr t with - | None -> acc - | Some _ -> List.map pi1 (keep_hyps env (Idset.singleton id)) :: acc) - [] ctx - in - List.iter (function (id,_,t) -> - if Lib.is_modtype () then - let cst = Declare.declare_internal_constant id - (ParameterEntry (t,false), IsAssumption Logical) - in - match class_of_constr t with - | Some tc -> - add_instance (Typeclasses.new_instance tc None false cst); - hook (ConstRef cst) - | None -> () - else ( - let impl = List.exists (fun (x,_) -> - match x with ExplByPos (_, Some id') -> id = id' | _ -> false) impls - and keep = - let l = list_filter_map (fun ids -> if List.mem id ids then Some ids else None) keeps in - List.concat l - in - Command.declare_one_assumption false (Local (* global *), Definitional) t - [] impl (* implicit *) keep (* always kept *) false (* inline *) (dummy_loc, id); - match class_of_constr t with - | None -> () - | Some tc -> hook (VarRef id))) - (List.rev ctx) + let fn (id, _, t) = + if Lib.is_modtype () && not (Lib.sections_are_opened ()) then + let cst = Declare.declare_internal_constant id + (ParameterEntry (t,false), IsAssumption Logical) + in + match class_of_constr t with + | Some tc -> + add_instance (Typeclasses.new_instance tc None false (ConstRef cst)); + hook (ConstRef cst) + | None -> () + else ( + let impl = List.exists + (fun (x,_) -> + match x with ExplByPos (_, Some id') -> id = id' | _ -> false) impls + in + Command.declare_assumption false (Local (* global *), Definitional) t + [] impl (* implicit *) false (* inline *) (dummy_loc, id); + match class_of_constr t with + | None -> () + | Some tc -> hook (VarRef id)) + in List.iter fn (List.rev ctx) + |