File: classes.ml

package info (click to toggle)
coq-doc 8.2pl1-1
  • links: PTS, VCS
  • area: non-free
  • in suites: squeeze
  • size: 19,240 kB
  • ctags: 22,737
  • sloc: ml: 132,933; ansic: 1,960; sh: 1,366; lisp: 456; makefile: 327
file content (315 lines) | stat: -rw-r--r-- 11,067 bytes parent folder | download | duplicates (2)
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
(* -*- compile-command: "make -C .. bin/coqtop.byte" -*- *)
(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)

(*i $Id: classes.ml 12187 2009-06-13 19:36:59Z msozeau $ i*)

(*i*)
open Names
open Decl_kinds
open Term
open Termops
open Sign
open Entries
open Evd
open Environ
open Nametab
open Mod_subst
open Util
open Typeclasses_errors
open Typeclasses
open Libnames
open Constrintern
open Rawterm
open Topconstr
(*i*)

open Decl_kinds
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 = 
  Auto.add_hints false [typeclasses_db] 
    (Vernacexpr.HintsTransparency ([qualid_of_con c], false))

let _ =
  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), [])])) ())
    
let declare_instance_cst glob con =
  let instance = Typeops.type_of_constant (Global.env ()) con 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.")

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

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 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 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) -> 
	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 inst = Typeclasses.new_instance k pri global cst in
    Impargs.maybe_declare_manual_implicits false (ConstRef 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 kind = IsDefinition Instance in
    let entry = 
      { const_entry_body   = term;
	const_entry_type   = Some termtype;
	const_entry_opaque = false;
	const_entry_boxed  = false }
    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;
    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 env = Global.env() in
  let isevars = ref (Evd.create_evar_defs Evd.empty) in
  let tclass = 
    match bk with
    | Implicit ->
	Implicit_quantifiers.implicit_application Idset.empty ~allow_partial:false
	  (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
  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
  in
  let id = 
    match snd instid with
	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 -> 
	  let i = Nameops.add_suffix (id_of_class k) "_instance_0" in
	    Termops.next_global_ident_away false 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 subst = List.map (Evarutil.nf_evar sigma) subst in
    if Lib.is_modtype () then
      begin
	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
	in
	Evarutil.check_evars env Evd.empty !isevars 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
      end
    else
      begin
	let props = 
	  match props with
	  | 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]
	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 = 
		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)
		  ([], props) k.cl_props
	      in
		if rest <> [] then 
		  unbound_method env' k.cl_impl (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
	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
	    declare_instance_constant k pri global imps ?hook id term termtype
	  else begin
	    isevars := Typeclasses.resolve_typeclasses ~onlyargs:true ~fail:true env !isevars;
	    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));
		(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 
      (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
	  (mkVar id :: subst, d :: ctx))
      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 env = Global.env() in
  let evars = ref (Evd.create_evar_defs 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 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 _ -> 
    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)