aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac/classes.ml
blob: c577fe6e3854983817f8d89d53aa49c80b207441 (plain)
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)