1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(*i*)
open Names
open Term
open Vars
open Environ
open Nametab
open CErrors
open Util
open Typeclasses_errors
open Typeclasses
open Libnames
open Globnames
open Constrintern
open Constrexpr
open Sigma.Notations
open Context.Rel.Declaration
module RelDecl = Context.Rel.Declaration
(*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 =
Hints.add_hints local [typeclasses_db]
(Hints.HintsTransparencyEntry ([c], b))
let _ =
Hook.set Typeclasses.add_instance_hint_hook
(fun inst path local info poly ->
let inst' = match inst with IsConstr c -> Hints.IsConstr (c, Univ.ContextSet.empty)
| IsGlobal gr -> Hints.IsGlobRef gr
in
let info =
let open Vernacexpr in
{ info with hint_pattern =
Option.map
(Constrintern.intern_constr_pattern (Global.env()))
info.hint_pattern } in
Flags.silently (fun () ->
Hints.add_hints local [typeclasses_db]
(Hints.HintsResolveEntry
[info, 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))
open Vernacexpr
(** TODO: add subinstances *)
let existing_instance glob g info =
let c = global g in
let info = Option.default Hints.empty_hint_info info 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,u), _)) -> add_instance (new_instance tc info glob
(*FIXME*) (Flags.use_polymorphic_flag ()) c)
| None -> user_err ~loc:(loc_of_reference g)
~hdr:"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
(* Declare everything in the parameters as implicit, and the class instance as well *)
let type_ctx_instance evars env ctx inst subst =
let rec aux (subst, instctx) l = function
decl :: ctx ->
let t' = substl subst (RelDecl.get_type decl) in
let c', l =
match decl with
| LocalAssum _ -> interp_casted_constr_evars env evars (List.hd l) t', List.tl l
| LocalDef (_,b,_) -> substl subst b, l
in
let d = RelDecl.get_name decl, Some c', t' in
aux (c' :: subst, d :: instctx) l ctx
| [] -> subst
in aux (subst, []) inst (List.rev ctx)
let id_of_class cl =
match cl.cl_impl with
| 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
| _ -> assert false
open Pp
let instance_hook k info global imps ?hook cst =
Impargs.maybe_declare_manual_implicits false cst ~enriching:false imps;
Typeclasses.declare_instance (Some info) (not global) cst;
(match hook with Some h -> h cst | None -> ())
let declare_instance_constant k info global imps ?hook id pl poly evm term termtype =
let kind = IsDefinition Instance in
let evm =
let levels = Univ.LSet.union (Universes.universes_of_constr termtype)
(Universes.universes_of_constr term) in
Evd.restrict_universe_context evm levels
in
let pl, uctx = Evd.universe_context ?names:pl evm 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;
Universes.register_universe_binders (ConstRef kn) pl;
instance_hook k info global imps ?hook (ConstRef kn);
id
let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) poly ctx (instid, bk, cl) props
?(generalize=true)
?(tac:unit Proofview.tactic option) ?hook pri =
let env = Global.env() in
let ((loc, instid), pl) = instid in
let uctx = Evd.make_evar_universe_context env pl in
let evars = ref (Evd.from_ctx uctx) in
let tclass, ids =
match bk with
| Decl_kinds.Implicit ->
Implicit_quantifiers.implicit_application Id.Set.empty ~allow_partial:false
(fun avoid (clname, _) ->
match clname with
| Some (cl, b) ->
let t = CHole (Loc.ghost, None, Misctypes.IntroAnonymous, None) in
t, avoid
| None -> failwith ("new instance: under-applied typeclass"))
cl
| Explicit -> cl, Id.Set.empty
in
let tclass =
if generalize then CGeneralization (Loc.ghost, Implicit, Some AbsPi, tclass)
else 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 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 decl (args, args') ->
match decl with
| LocalAssum _ -> (List.tl args, List.hd args :: args')
| LocalDef (_,b,_) -> (args, substl args' b :: args'))
(snd cl.cl_context) (args, [])
in
cl, u, c', ctx', ctx, len, imps, args
in
let id =
match instid with
Name id ->
let sp = Lib.make_path id in
if Nametab.exists_cci sp then
user_err ~hdr:"new_instance" (Nameops.pr_id id ++ Pp.str " already exists.");
id
| Anonymous ->
let i = Nameops.add_suffix (id_of_class k) "_instance_0" in
Namegen.next_global_ident_away i (Termops.ids_of_context env)
in
let env' = push_rel_context ctx env in
evars := Evarutil.nf_evar_map !evars;
evars := resolve_typeclasses ~filter:Typeclasses.all_evars ~fail:true env !evars;
let subst = List.map (Evarutil.nf_evar !evars) subst in
if abstract then
begin
let subst = List.fold_left2
(fun subst' s decl -> if is_local_assum decl 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
nf t
in
Pretyping.check_evars env Evd.empty !evars termtype;
let pl, ctx = Evd.universe_context ?names:pl !evars in
let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest id
(ParameterEntry
(None,poly,(termtype,ctx),None), Decl_kinds.IsAssumption Decl_kinds.Logical)
in
Universes.register_universe_binders (ConstRef cst) pl;
instance_hook k pri global imps ?hook (ConstRef cst); id
end
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'
| Qualid (loc,id') -> (loc, snd (repr_qualid id'))
in
let props, rest =
List.fold_left
(fun (props, rest) decl ->
if is_local_assum decl then
try
let is_id (id', _) = match RelDecl.get_name decl, 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, None(* 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 decl -> if is_local_assum decl 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;
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. *)
Pretyping.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
declare_instance_constant k pri global imps ?hook id pl
poly evm (Option.get term) termtype
else if Flags.is_program_mode () || refine || 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 (Some pri) (not global) (ConstRef cst)
in
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
?pl 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 ?pl 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 [
Refine.refine { run = fun evm -> Sigma (Option.get term, evm, Sigma.refl) };
Proofview.Unsafe.tclNEWGOALS gls;
Tactics.New.reduce_after_refine;
]
in
ignore (Pfedit.by init_refine)
else if Flags.is_auto_intros () then
ignore (Pfedit.by (Tacticals.New.tclDO len Tactics.intro));
(match tac with Some tac -> ignore (Pfedit.by tac) | None -> ())) ();
id)
end
else CErrors.error "Unsolved obligations remaining.")
let named_of_rel_context l =
let acc, ctx =
List.fold_right
(fun decl (subst, ctx) ->
let id = match RelDecl.get_name decl with Anonymous -> invalid_arg "named_of_rel_context" | Name id -> id in
let d = match decl with
| LocalAssum (_,t) -> id, None, substl subst t
| LocalDef (_,b,t) -> id, Some (substl subst b), substl subst t in
(mkVar id :: subst, d :: ctx))
l ([], [])
in ctx
let context poly l =
let env = Global.env() in
let evars = ref (Evd.from_env env) 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.Rel.map subst fullctx in
let ce t = Pretyping.check_evars env Evd.empty !evars t in
let () = List.iter (fun decl -> Context.Rel.Declaration.iter_constr ce decl) fullctx in
let ctx =
try named_of_rel_context fullctx
with e when CErrors.noncritical e ->
error "Anonymous variables not allowed in contexts."
in
let uctx = ref (Evd.universe_context_set !evars) in
let fn status (id, b, t) =
if Lib.is_modtype () && not (Lib.sections_are_opened ()) then
let ctx = Univ.ContextSet.to_context !uctx in
(* Declare the universe context once *)
let () = uctx := Univ.ContextSet.empty in
let decl = (ParameterEntry (None,poly,(t,ctx),None), IsAssumption Logical) in
let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest id decl in
match class_of_constr t with
| Some (rels, ((tc,_), args) as _cl) ->
add_instance (Typeclasses.new_instance tc Hints.empty_hint_info false (*FIXME*)
poly (ConstRef cst));
status
(* declare_subclasses (ConstRef cst) cl *)
| 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
let () = uctx := Univ.ContextSet.empty in
status && nstatus
in List.fold_left fn true (List.rev ctx)
|