diff options
Diffstat (limited to 'toplevel/classes.ml')
| -rw-r--r-- | toplevel/classes.ml | 418 |
1 files changed, 235 insertions, 183 deletions
diff --git a/toplevel/classes.ml b/toplevel/classes.ml index 3843ea83..f44ac367 100644 --- a/toplevel/classes.ml +++ b/toplevel/classes.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -8,80 +8,77 @@ (*i*) open Names -open Decl_kinds open Term -open Sign -open Entries -open Evd +open Vars open Environ open Nametab -open Mod_subst +open Errors open Util open Typeclasses_errors open Typeclasses open Libnames +open Globnames open Constrintern -open Glob_term -open Topconstr +open Constrexpr (*i*) open Decl_kinds open Entries +let refine_instance = ref true + +let _ = Goptions.declare_bool_option { + Goptions.optsync = true; + Goptions.optdepr = false; + Goptions.optname = "definition of instances by refining"; + Goptions.optkey = ["Refine";"Instance";"Mode"]; + Goptions.optread = (fun () -> !refine_instance); + Goptions.optwrite = (fun b -> refine_instance := b) +} + let typeclasses_db = "typeclass_instances" let set_typeclass_transparency c local b = - Auto.add_hints local [typeclasses_db] - (Auto.HintsTransparencyEntry ([c], b)) + Hints.add_hints local [typeclasses_db] + (Hints.HintsTransparencyEntry ([c], b)) let _ = - Typeclasses.register_add_instance_hint - (fun inst local pri -> - let path = - try Auto.PathHints [global_of_constr inst] - with e when Errors.noncritical e -> Auto.PathAny + Hook.set Typeclasses.add_instance_hint_hook + (fun inst path local pri poly -> + let inst' = match inst with IsConstr c -> Hints.IsConstr (c, Univ.ContextSet.empty) + | IsGlobal gr -> Hints.IsGlobRef gr in Flags.silently (fun () -> - Auto.add_hints local [typeclasses_db] - (Auto.HintsResolveEntry - [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 - | 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") - + Hints.add_hints local [typeclasses_db] + (Hints.HintsResolveEntry + [pri, poly, false, Hints.PathHints path, inst'])) ()); + Hook.set Typeclasses.set_typeclass_transparency_hook set_typeclass_transparency; + Hook.set Typeclasses.classes_transparent_state_hook + (fun () -> Hints.Hint_db.transparent_state (Hints.searchtable_map typeclasses_db)) + (** TODO: add subinstances *) -let existing_instance glob g = +let existing_instance glob g pri = let c = global g in - let instance = Typing.type_of (Global.env ()) Evd.empty (constr_of_global c) in + let instance = Global.type_of_global_unsafe 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,u), _)) -> add_instance (new_instance tc pri glob + (*FIXME*) (Flags.use_polymorphic_flag ()) c) | None -> user_err_loc (loc_of_reference g, "declare_instance", Pp.str "Constant does not build instances of a declared type class.") 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 -type binder_list = (identifier located * bool * constr_expr) list - (* Declare everything in the parameters as implicit, and the class instance as well *) -open Topconstr - 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 + | None -> interp_casted_constr_evars env evars (List.hd l) t', List.tl l | Some b -> substl subst b, l in let d = na, Some c', t' in @@ -89,11 +86,9 @@ let type_ctx_instance evars env ctx inst subst = | [] -> 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 + | ConstRef kn -> let _,_,l = repr_con kn in Label.to_id l | IndRef (kn,i) -> let mip = (Environ.lookup_mind kn (Global.env ())).Declarations.mind_packets in mip.(0).Declarations.mind_typename @@ -101,55 +96,53 @@ let id_of_class cl = open Pp -let ($$) g f = fun x -> g (f x) - let instance_hook k pri global imps ?hook cst = 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 } - in DefinitionEntry entry, kind +let declare_instance_constant k pri global imps ?hook id poly uctx term termtype = + let kind = IsDefinition Instance in + let entry = + Declare.definition_entry ~types:termtype ~poly ~univs:uctx term in + let cdecl = (DefinitionEntry entry, kind) in let kn = Declare.declare_constant id cdecl in Declare.definition_message id; instance_hook k pri global imps ?hook (ConstRef kn); id -let new_instance ?(abstract=false) ?(global=false) ctx (instid, bk, cl) props +let new_instance ?(abstract=false) ?(global=false) poly ctx (instid, bk, cl) props ?(generalize=true) - ?(tac:Proof_type.tactic option) ?(hook:(global_reference -> unit) option) pri = + ?(tac:unit Proofview.tactic option) ?hook pri = let env = Global.env() in - let evars = ref Evd.empty in + let evars = ref (Evd.from_env env) in let tclass, ids = match bk with | Implicit -> - Implicit_quantifiers.implicit_application Idset.empty ~allow_partial:false + Implicit_quantifiers.implicit_application Id.Set.empty ~allow_partial:false (fun avoid (clname, (id, _, t)) -> match clname with | Some (cl, b) -> - let t = CHole (Util.dummy_loc, None) in + let t = CHole (Loc.ghost, None, Misctypes.IntroAnonymous, None) in t, avoid | None -> failwith ("new instance: under-applied typeclass")) cl - | Explicit -> cl, Idset.empty + | Explicit -> cl, Id.Set.empty + in + let tclass = + if generalize then CGeneralization (Loc.ghost, Implicit, Some AbsPi, tclass) + else tclass 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 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 k, u, cty, ctx', ctx, len, imps, subst = + let impls, ((env', ctx), imps) = interp_context_evars env evars ctx in + let c', imps' = interp_type_evars_impls ~impls env' evars 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 k, args = Typeclasses.dest_class_app (push_rel_context ctx'' env) c in + let cl, u = Typeclasses.typeclass_univ_instance k in let _, args = List.fold_right (fun (na, b, t) (args, args') -> match b with @@ -157,7 +150,7 @@ let new_instance ?(abstract=false) ?(global=false) ctx (instid, bk, cl) props | Some b -> (args, substl args' b :: args')) (snd cl.cl_context) (args, []) in - cl, c', ctx', ctx, len, imps, args + cl, u, c', ctx', ctx, len, imps, args in let id = match snd instid with @@ -172,158 +165,217 @@ let new_instance ?(abstract=false) ?(global=false) ctx (instid, bk, cl) props 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 + evars := resolve_typeclasses ~filter:Typeclasses.no_goals ~fail:true env !evars; + let subst = List.map (Evarutil.nf_evar !evars) subst in 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 subst = List.fold_left2 + (fun subst' s (_, b, _) -> if Option.is_empty b then s :: subst' else subst') + [] subst (snd k.cl_context) + in + let (_, ty_constr) = instance_constructor (k,u) subst in + let nf, subst = Evarutil.e_nf_evars_and_universes evars in let termtype = let t = it_mkProd_or_LetIn ty_constr (ctx' @ ctx) in - Evarutil.nf_evar !evars t + nf t in Evarutil.check_evars env Evd.empty !evars termtype; + let ctx = Evd.universe_context !evars in let cst = Declare.declare_constant ~internal:Declare.KernelSilent id (Entries.ParameterEntry - (None,termtype,None), Decl_kinds.IsAssumption Decl_kinds.Logical) + (None,poly,(termtype,ctx),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 - | Some (CRecord (loc, _, fs)) -> - if List.length fs > List.length k.cl_props then - mismatched_props env' (List.map snd fs) k.cl_props; - Some (Inl fs) - | Some t -> Some (Inr t) - | None -> None - in - let subst = - match props with - | 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 - Some (Inr (c, subst)) - | Some (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,_) -> - 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 - 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 - else props, rest) - ([], props) k.cl_props - in - if rest <> [] then - unbound_method env' k.cl_impl (get_id (fst (List.hd rest))) - else - Some (Inl (type_ctx_instance evars (push_rel_context ctx' env') k.cl_props props subst)) - in + else ( + let props = + match props with + | Some (true, CRecord (loc, _, fs)) -> + if List.length fs > List.length k.cl_props then + mismatched_props env' (List.map snd fs) k.cl_props; + Some (Inl fs) + | Some (_, t) -> Some (Inr t) + | None -> + if Flags.is_program_mode () then Some (Inl []) + else None + in + let subst = + match props with + | None -> if List.is_empty k.cl_props then Some (Inl subst) else None + | Some (Inr term) -> + let c = interp_casted_constr_evars env' evars term cty in + Some (Inr (c, subst)) + | Some (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,_) -> + if Option.is_empty b then + try + let is_id (id', _) = match id, get_id id' with + | Name id, (_, id') -> Id.equal id id' + | Anonymous, _ -> false + in + let (loc_mid, c) = + List.find is_id rest + in + let rest' = + List.filter (fun v -> not (is_id v)) rest + in + let (loc, mid) = get_id loc_mid in + List.iter (fun (n, _, x) -> + if Name.equal 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 (Loc.ghost, Some Evar_kinds.GoalEvar, Misctypes.IntroAnonymous, None) :: props), rest + else props, rest) + ([], props) k.cl_props + in + match rest with + | (n, _) :: _ -> + unbound_method env' k.cl_impl (get_id n) + | _ -> + Some (Inl (type_ctx_instance evars (push_rel_context ctx' env') + k.cl_props props subst)) + in + let term, termtype = + match subst with + | 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 Option.is_empty b then s :: subst' else subst') + [] subst (k.cl_props @ snd k.cl_context) + in + let (app, ty_constr) = instance_constructor (k,u) 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 + 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 + Some term, termtype + in + let _ = evars := Evarutil.nf_evar_map !evars; - let term, termtype = - match subst with - | 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) + evars := Typeclasses.resolve_typeclasses ~filter:Typeclasses.no_goals_or_obligations ~fail:true + env !evars; + (* Try resolving fields that are typeclasses automatically. *) + evars := Typeclasses.resolve_typeclasses ~filter:Typeclasses.all_evars ~fail:false + env !evars + in + let _ = evars := Evarutil.nf_evar_map_undefined !evars in + let evm, nf = Evarutil.nf_evar_map_universes !evars in + let termtype = nf termtype in + let _ = (* Check that the type is free of evars now. *) + Evarutil.check_evars env Evd.empty evm termtype + in + let term = Option.map nf term in + if not (Evd.has_undefined evm) && not (Option.is_empty term) then + let ctx = Evd.universe_context evm in + declare_instance_constant k pri global imps ?hook id + poly ctx (Option.get term) termtype + else if !refine_instance || Option.is_empty term then begin + let kind = Decl_kinds.Global, poly, Decl_kinds.DefinitionBody Decl_kinds.Instance in + if Flags.is_program_mode () then + let hook vis gr = + let cst = match gr with ConstRef kn -> kn | _ -> assert false in + Impargs.declare_manual_implicits false gr ~enriching:false [imps]; + Typeclasses.declare_instance pri (not global) (ConstRef cst) 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 (Option.get app) (ctx' @ ctx) in - 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 - Some term, termtype - in - let _ = - evars := Evarutil.nf_evar_map !evars; - evars := Typeclasses.resolve_typeclasses ~filter:Typeclasses.no_goals ~fail:true - env !evars; - (* Try resolving fields that are typeclasses automatically. *) - evars := Typeclasses.resolve_typeclasses ~filter:Typeclasses.all_evars ~fail:false - env !evars - in - let termtype = Evarutil.nf_evar !evars termtype 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 && term <> None then - declare_instance_constant k pri global imps ?hook id (Option.get term) termtype - else begin - 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 term <> None then - Pfedit.by (!refine_ref (evm, Option.get term)) + let obls, constr, typ = + match term with + | Some t -> + let obls, _, constr, typ = + Obligations.eterm_obligations env id evm 0 t termtype + in obls, Some constr, typ + | None -> [||], None, termtype + in + let hook = Lemmas.mk_hook hook in + let ctx = Evd.evar_universe_context evm in + ignore (Obligations.add_definition id ?term:constr + typ ctx ~kind:(Global,poly,Instance) ~hook obls); + id + else + (Flags.silently + (fun () -> + (* spiwack: it is hard to reorder the actions to do + the pretyping after the proof has opened. As a + consequence, we use the low-level primitives to code + the refinement manually.*) + let gls = List.rev (Evd.future_goals evm) in + let evm = Evd.reset_future_goals evm in + Lemmas.start_proof id kind evm termtype + (Lemmas.mk_hook + (fun _ -> instance_hook k pri global imps ?hook)); + (* spiwack: I don't know what to do with the status here. *) + if not (Option.is_empty term) then + let init_refine = + Tacticals.New.tclTHENLIST [ + Proofview.Refine.refine (fun evm -> evm, Option.get term); + Proofview.Unsafe.tclNEWGOALS gls; + Tactics.New.reduce_after_refine; + ] + in + ignore (Pfedit.by init_refine) 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 + ignore (Pfedit.by (Tacticals.New.tclDO len Tactics.intro)); + (match tac with Some tac -> ignore (Pfedit.by tac) | None -> ())) (); + id) + end + else Errors.error "Unsolved obligations remaining.") let named_of_rel_context l = 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 id = match na with Anonymous -> invalid_arg "named_of_rel_context" | Name id -> id in let d = (id, Option.map (substl subst) b, substl subst t) in (mkVar id :: subst, d :: ctx)) l ([], []) in ctx -let string_of_global r = - string_of_qualid (Nametab.shortest_qualid_of_global Idset.empty r) - -let context l = +let context poly l = let env = Global.env() 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 !evars fullctx in + let _, ((env', fullctx), impls) = interp_context_evars env evars l in + let subst = Evarutil.evd_comb0 Evarutil.nf_evars_and_universes evars in + let fullctx = Context.map_rel_context subst 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 () = List.iter (fun (n, b, t) -> Option.iter ce b; ce t) fullctx in let ctx = try named_of_rel_context fullctx with e when Errors.noncritical e -> error "Anonymous variables not allowed in contexts." in - let fn (id, _, t) = + let uctx = Evd.universe_context_set !evars in + let fn status (id, b, t) = if Lib.is_modtype () && not (Lib.sections_are_opened ()) then - let cst = Declare.declare_constant ~internal:Declare.KernelSilent id - (ParameterEntry (None,t,None), IsAssumption Logical) - in + let uctx = Univ.ContextSet.to_context uctx in + let decl = (ParameterEntry (None,poly,(t,uctx),None), IsAssumption Logical) in + let cst = Declare.declare_constant ~internal:Declare.KernelSilent id decl in match class_of_constr t with - | Some (rels, (tc, args) as _cl) -> - add_instance (Typeclasses.new_instance tc None false (ConstRef cst)) + | Some (rels, ((tc,_), args) as _cl) -> + add_instance (Typeclasses.new_instance tc None false (*FIXME*) + poly (ConstRef cst)); + status (* declare_subclasses (ConstRef cst) cl *) - | None -> () - else ( - let impl = List.exists - (fun (x,_) -> - match x with ExplByPos (_, Some id') -> id = id' | _ -> false) impls + | None -> status + else + let test (x, _) = match x with + | ExplByPos (_, Some id') -> Id.equal id id' + | _ -> false + in + let impl = List.exists test impls in + let decl = (Discharge, poly, Definitional) in + let nstatus = + pi3 (Command.declare_assumption false decl (t, uctx) [] impl + Vernacexpr.NoInline (Loc.ghost, id)) in - Command.declare_assumption false (Local (* global *), Definitional) t - [] impl (* implicit *) None (* inline *) (dummy_loc, id)) - in List.iter fn (List.rev ctx) - + status && nstatus + in List.fold_left fn true (List.rev ctx) |