diff options
Diffstat (limited to 'toplevel/classes.ml')
| -rw-r--r-- | toplevel/classes.ml | 131 |
1 files changed, 61 insertions, 70 deletions
diff --git a/toplevel/classes.ml b/toplevel/classes.ml index 28c1ab75..1e83e4b8 100644 --- a/toplevel/classes.ml +++ b/toplevel/classes.ml @@ -1,19 +1,15 @@ -(* -*- compile-command: "make -C .. bin/coqtop.byte" -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: classes.ml 14641 2011-11-06 11:59:10Z herbelin $ i*) - (*i*) open Names open Decl_kinds open Term -open Termops open Sign open Entries open Evd @@ -25,7 +21,7 @@ open Typeclasses_errors open Typeclasses open Libnames open Constrintern -open Rawterm +open Glob_term open Topconstr (*i*) @@ -34,18 +30,21 @@ open Entries let typeclasses_db = "typeclass_instances" -let set_typeclass_transparency c b = - Auto.add_hints false [typeclasses_db] +let set_typeclass_transparency c local b = + Auto.add_hints local [typeclasses_db] (Auto.HintsTransparencyEntry ([c], b)) let _ = Typeclasses.register_add_instance_hint - (fun inst pri -> + (fun inst local pri -> + let path = try Auto.PathHints [global_of_constr inst] with _ -> Auto.PathAny in Flags.silently (fun () -> - Auto.add_hints false [typeclasses_db] + Auto.add_hints local [typeclasses_db] (Auto.HintsResolveEntry - [pri, false, constr_of_global inst])) ()); - Typeclasses.register_set_typeclass_transparency set_typeclass_transparency + [pri, false, path, inst])) ()); + Typeclasses.register_set_typeclass_transparency set_typeclass_transparency; + Typeclasses.register_classes_transparent_state + (fun () -> Auto.Hint_db.transparent_state (Auto.searchtable_map typeclasses_db)) let declare_class g = match global g with @@ -54,12 +53,13 @@ let declare_class g = | _ -> user_err_loc (loc_of_reference g, "declare_class", Pp.str"Unsupported class type, only constants and inductives are allowed") -let declare_instance glob g = +(** TODO: add subinstances *) +let existing_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 c) + | 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.") @@ -68,13 +68,6 @@ let mismatched_props env n m = mismatched_ctx_inst env Properties n m type binder_list = (identifier located * bool * constr_expr) list -(* Calls to interpretation functions. *) - -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 @@ -108,19 +101,18 @@ open Pp let ($$) g f = fun x -> g (f x) 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 cst ~enriching:false imps; - Typeclasses.add_instance inst; - (match hook with Some h -> h cst | None -> ()) + Impargs.maybe_declare_manual_implicits false cst ~enriching:false imps; + Typeclasses.declare_instance pri (not global) cst; + (match hook with Some h -> h cst | None -> ()) let declare_instance_constant k pri global imps ?hook id term termtype = let cdecl = let kind = IsDefinition Instance in let entry = { const_entry_body = term; + const_entry_secctx = None; const_entry_type = Some termtype; - const_entry_opaque = false; - const_entry_boxed = false } + const_entry_opaque = false } in DefinitionEntry entry, kind in let kn = Declare.declare_constant id cdecl in @@ -148,8 +140,8 @@ let new_instance ?(abstract=false) ?(global=false) ctx (instid, bk, cl) props in let tclass = if generalize then CGeneralization (dummy_loc, Implicit, Some AbsPi, tclass) else tclass in 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 ~fail_evar:false env' tclass in + let impls, ((env', ctx), imps) = interp_context_evars evars env ctx in + let c', imps' = interp_type_evars_impls ~impls ~evdref:evars ~fail_evar:false 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 @@ -190,26 +182,29 @@ let new_instance ?(abstract=false) ?(global=false) ctx (instid, bk, cl) props Evarutil.nf_evar !evars t in 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 (ConstRef cst); id + let cst = Declare.declare_constant ~internal:Declare.KernelSilent id + (Entries.ParameterEntry + (None,termtype,None), Decl_kinds.IsAssumption Decl_kinds.Logical) + in instance_hook k None global imps ?hook (ConstRef cst); id end else begin let props = match props with - | CRecord (loc, _, fs) -> + | Some (CRecord (loc, _, fs)) -> if List.length fs > List.length k.cl_props then mismatched_props env' (List.map snd fs) k.cl_props; - Inl fs - | _ -> Inr props + Some (Inl fs) + | Some t -> Some (Inr t) + | None -> None in let subst = match props with - | Inr term -> + | None -> if k.cl_props = [] then Some (Inl subst) else None + | Some (Inr term) -> let c = interp_casted_constr_evars evars env' term cty in - Inr (c, subst) - | Inl props -> + Some (Inr (c, subst)) + | Some (Inl props) -> let get_id = function | Ident id' -> id' @@ -223,7 +218,10 @@ let new_instance ?(abstract=false) ?(global=false) ctx (instid, bk, cl) props 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); + List.iter (fun (n, _, x) -> + if n = Name mid then + Option.iter (fun x -> Dumpglob.add_glob loc (ConstRef x)) x) + k.cl_projs; c :: props, rest' with Not_found -> (CHole (Util.dummy_loc, None) :: props), rest @@ -233,12 +231,14 @@ let new_instance ?(abstract=false) ?(global=false) ctx (instid, bk, cl) props if rest <> [] then unbound_method env' k.cl_impl (get_id (fst (List.hd rest))) else - Inl (type_ctx_instance evars (push_rel_context ctx' env') k.cl_props props subst) + Some (Inl (type_ctx_instance evars (push_rel_context ctx' env') k.cl_props props subst)) in evars := Evarutil.nf_evar_map !evars; let term, termtype = match subst with - | Inl subst -> + | None -> let termtype = it_mkProd_or_LetIn cty ctx in + None, termtype + | Some (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) @@ -246,26 +246,25 @@ let new_instance ?(abstract=false) ?(global=false) ctx (instid, bk, cl) props 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 (Option.get app) (ctx' @ ctx) in - term, termtype - | Inr (def, subst) -> + Some term, termtype + | Some (Inr (def, subst)) -> let termtype = it_mkProd_or_LetIn cty ctx in let term = Termops.it_mkLambda_or_LetIn def ctx in - term, termtype + Some term, termtype in let termtype = Evarutil.nf_evar !evars termtype in - let term = Evarutil.nf_evar !evars term in + let term = Option.map (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 + if Evd.is_empty evm && term <> None then + declare_instance_constant k pri global imps ?hook id (Option.get term) termtype else begin 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 () -> 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)) + if term <> None then + Pfedit.by (!refine_ref (evm, Option.get term)) else if Flags.is_auto_intros () then Pfedit.by (Refiner.tclDO len Tactics.intro); (match tac with Some tac -> Pfedit.by tac | None -> ())) (); @@ -284,18 +283,13 @@ let named_of_rel_context l = l ([], []) in ctx -let push_named_context = List.fold_right push_named - -let rec list_filter_map f = function - | [] -> [] - | hd :: tl -> match f hd with - | None -> list_filter_map f tl - | Some x -> x :: list_filter_map f tl - -let context ?(hook=fun _ -> ()) l = +let string_of_global r = + string_of_qualid (Nametab.shortest_qualid_of_global Idset.empty r) + +let context l = let env = Global.env() in let evars = ref Evd.empty in - let (env', fullctx), impls = interp_context_evars evars env l in + let _, ((env', fullctx), impls) = interp_context_evars evars env l 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; @@ -304,13 +298,13 @@ let context ?(hook=fun _ -> ()) l = in 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) + let cst = Declare.declare_constant ~internal:Declare.KernelSilent id + (ParameterEntry (None,t,None), IsAssumption Logical) in match class_of_constr t with - | Some tc -> - add_instance (Typeclasses.new_instance tc None false (ConstRef cst)); - hook (ConstRef cst) + | Some (rels, (tc, args) as _cl) -> + add_instance (Typeclasses.new_instance tc None false (ConstRef cst)) + (* declare_subclasses (ConstRef cst) cl *) | None -> () else ( let impl = List.exists @@ -318,9 +312,6 @@ let context ?(hook=fun _ -> ()) l = 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)) + [] impl (* implicit *) None (* inline *) (dummy_loc, id)) in List.iter fn (List.rev ctx) - + |