summaryrefslogtreecommitdiff
path: root/plugins/subtac/subtac_utils.ml
blob: e32bb9e0869037e0ee8e535561a7091f22d7e0f1 (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
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
(** -*- compile-command: "make -C ../.. plugins/subtac/subtac_plugin.cma" -*- *)

open Evd
open Libnames
open Coqlib
open Term
open Names
open Util

let ($) f x = f x

(****************************************************************************)
(* Library linking *)

let contrib_name = "Program"

let subtac_dir = [contrib_name]
let fixsub_module = subtac_dir @ ["Wf"]
let utils_module = subtac_dir @ ["Utils"]
let tactics_module = subtac_dir @ ["Tactics"]
let init_constant dir s () = gen_constant contrib_name dir s
let init_reference dir s () = gen_reference contrib_name dir s

let safe_init_constant md name () =
  check_required_library ("Coq"::md);
  init_constant md name ()

let ex_pi1 = init_constant utils_module "ex_pi1"
let ex_pi2 = init_constant utils_module "ex_pi2"

let make_ref l s = init_reference l s
let well_founded_ref = make_ref ["Init";"Wf"] "Well_founded"
let acc_ref = make_ref  ["Init";"Wf"] "Acc"
let acc_inv_ref = make_ref  ["Init";"Wf"] "Acc_inv"
let fix_sub_ref = make_ref fixsub_module "Fix_sub"
let measure_on_R_ref = make_ref fixsub_module "MR"
let fix_measure_sub_ref = make_ref fixsub_module "Fix_measure_sub"
let refl_ref = make_ref ["Init";"Logic"] "refl_equal"

let make_ref s = Qualid (dummy_loc, qualid_of_string s)
let lt_ref = make_ref "Init.Peano.lt"
let sig_ref = make_ref "Init.Specif.sig"
let proj1_sig_ref = make_ref "Init.Specif.proj1_sig"
let proj2_sig_ref = make_ref "Init.Specif.proj2_sig"

let build_sig () =
  { proj1 = init_constant ["Init"; "Specif"] "proj1_sig" ();
    proj2 = init_constant ["Init"; "Specif"] "proj2_sig" ();
    elim = init_constant ["Init"; "Specif"] "sig_rec" ();
    intro = init_constant ["Init"; "Specif"] "exist" ();
    typ = init_constant ["Init"; "Specif"] "sig" () }

let sig_ = build_sig

let fix_proto = safe_init_constant tactics_module "fix_proto"

let hide_obligation = safe_init_constant tactics_module "obligation"

let eq_ind = init_constant ["Init"; "Logic"] "eq"
let eq_rec = init_constant ["Init"; "Logic"] "eq_rec"
let eq_rect = init_constant ["Init"; "Logic"] "eq_rect"
let eq_refl = init_constant ["Init"; "Logic"] "refl_equal"
let eq_ind_ref = init_reference ["Init"; "Logic"] "eq"
let refl_equal_ref = init_reference ["Init"; "Logic"] "refl_equal"

let not_ref = init_constant ["Init"; "Logic"] "not"

let and_typ = Coqlib.build_coq_and

let eqdep_ind = init_constant [ "Logic";"Eqdep"] "eq_dep"
let eqdep_rec = init_constant ["Logic";"Eqdep"] "eq_dep_rec"
let eqdep_ind_ref = init_reference [ "Logic";"Eqdep"] "eq_dep"
let eqdep_intro_ref = init_reference [ "Logic";"Eqdep"] "eq_dep_intro"

let jmeq_ind =
  safe_init_constant ["Logic";"JMeq"] "JMeq"

let jmeq_rec =
  init_constant ["Logic";"JMeq"] "JMeq_rec"

let jmeq_refl =
  init_constant ["Logic";"JMeq"] "JMeq_refl"

let ex_ind = init_constant ["Init"; "Logic"] "ex"
let ex_intro = init_reference ["Init"; "Logic"] "ex_intro"

let proj1 = init_constant ["Init"; "Logic"] "proj1"
let proj2 = init_constant ["Init"; "Logic"] "proj2"

let existS = build_sigma_type

let prod = build_prod


(* orders *)
let well_founded = init_constant ["Init"; "Wf"] "well_founded"
let fix = init_constant ["Init"; "Wf"] "Fix"
let acc = init_constant ["Init"; "Wf"] "Acc"
let acc_inv = init_constant ["Init"; "Wf"] "Acc_inv"

let extconstr = Constrextern.extern_constr true (Global.env ())
let extsort s = Constrextern.extern_constr true (Global.env ()) (mkSort s)

open Pp

let my_print_constr = Termops.print_constr_env
let my_print_constr_expr = Ppconstr.pr_constr_expr
let my_print_rel_context env ctx = Printer.pr_rel_context env ctx
let my_print_context = Termops.print_rel_context
let my_print_named_context = Termops.print_named_context
let my_print_env = Termops.print_env
let my_print_glob_constr = Printer.pr_glob_constr_env
let my_print_evardefs = Evd.pr_evar_map None

let my_print_tycon_type = Evarutil.pr_tycon_type

let debug_level = 2

let debug_on = true

let debug n s =
  if debug_on then
    if !Flags.debug && n >= debug_level then
      msgnl s
    else ()
  else ()

let debug_msg n s =
  if debug_on then
    if !Flags.debug  && n >= debug_level then s
    else mt ()
  else mt ()

let trace s =
  if debug_on then
    if !Flags.debug  && debug_level > 0 then msgnl s
    else ()
  else ()

let rec pp_list f = function
    [] -> mt()
  | x :: y -> f x ++ spc () ++ pp_list f y

let wf_relations = Hashtbl.create 10

let std_relations () =
  let add k v = Hashtbl.add wf_relations k v in
    add (init_constant ["Init"; "Peano"] "lt" ())
      (init_constant ["Arith"; "Wf_nat"] "lt_wf")

let std_relations = Lazy.lazy_from_fun std_relations

type binders = Topconstr.local_binder list

let app_opt c e =
  match c with
      Some constr -> constr e
    | None -> e

let print_args env args =
  Array.fold_right (fun a acc -> my_print_constr env a ++ spc () ++ acc) args (str "")

let make_existential loc ?(opaque = Define true) env isevars c =
  Evarutil.e_new_evar isevars env ~src:(loc, QuestionMark opaque) c

let no_goals_or_obligations = function
  | GoalEvar | QuestionMark _ -> false
  | _ -> true

let make_existential_expr loc env c =
  let key = Evarutil.new_untyped_evar () in
  let evar = Topconstr.CEvar (loc, key, None) in
    debug 2 (str "Constructed evar " ++ int key);
    evar

let string_of_hole_kind = function
  | ImplicitArg _ -> "ImplicitArg"
  | BinderType _ -> "BinderType"
  | QuestionMark _ -> "QuestionMark"
  | CasesType -> "CasesType"
  | InternalHole -> "InternalHole"
  | TomatchTypeParameter _ -> "TomatchTypeParameter"
  | GoalEvar -> "GoalEvar"
  | ImpossibleCase -> "ImpossibleCase"
  | MatchingVar _ -> "MatchingVar"

let evars_of_term evc init c =
  let rec evrec acc c =
    match kind_of_term c with
    | Evar (n, _) when Evd.mem evc n -> Evd.add acc n (Evd.find evc n)
    | Evar (n, _) -> assert(false)
    | _ -> fold_constr evrec acc c
  in
    evrec init c

let non_instanciated_map env evd evm =
  List.fold_left
    (fun evm (key, evi) ->
       let (loc,k) = evar_source key !evd in
	 debug 2 (str "evar " ++ int key ++ str " has kind " ++
		    str (string_of_hole_kind k));
	 match k with
	 | QuestionMark _ -> Evd.add evm key evi
	 | ImplicitArg (_,_,false) -> Evd.add evm key evi
	 | _ ->
	     debug 2 (str " and is an implicit");
	     Pretype_errors.error_unsolvable_implicit loc env evm (Evarutil.nf_evar_info evm evi) k None)
    Evd.empty (Evarutil.non_instantiated evm)

let global_kind = Decl_kinds.IsDefinition Decl_kinds.Definition
let goal_kind = Decl_kinds.Global, Decl_kinds.DefinitionBody Decl_kinds.Definition

let global_proof_kind = Decl_kinds.IsProof Decl_kinds.Lemma
let goal_proof_kind = Decl_kinds.Global, Decl_kinds.Proof Decl_kinds.Lemma

let global_fix_kind = Decl_kinds.IsDefinition Decl_kinds.Fixpoint
let goal_fix_kind = Decl_kinds.Global, Decl_kinds.DefinitionBody Decl_kinds.Fixpoint

open Tactics
open Tacticals

let filter_map f l =
  let rec aux acc = function
      hd :: tl -> (match f hd with Some t -> aux (t :: acc) tl
		     | None -> aux acc tl)
    | [] -> List.rev acc
  in aux [] l

let build_dependent_sum l =
  let rec aux names conttac conttype = function
      (n, t) :: ((_ :: _) as tl) ->
	let hyptype = substl names t in
	  trace (spc () ++ str ("treating evar " ^ string_of_id n));
	  (try trace (str " assert: " ++ my_print_constr (Global.env ()) hyptype)
	   with e when Errors.noncritical e -> ());
	let tac = assert_tac (Name n) hyptype in
	let conttac =
	  (fun cont ->
	     conttac
	     (tclTHENS tac
		([intros;
		  (tclTHENSEQ
		     [constructor_tac false (Some 1) 1
			(Glob_term.ImplicitBindings [mkVar n]);
		      cont]);
		 ])))
	in
	let conttype =
	  (fun typ ->
	     let tex = mkLambda (Name n, t, typ) in
	       conttype
		 (mkApp (ex_ind (), [| t; tex |])))
	in
	  aux (mkVar n :: names) conttac conttype tl
    | (n, t) :: [] ->
	(conttac intros, conttype t)
    | [] -> raise (Invalid_argument "build_dependent_sum")
  in aux [] identity identity (List.rev l)

open Proof_type
open Tacexpr

let mkProj1 a b c =
  mkApp (delayed_force proj1, [| a; b; c |])

let mkProj2 a b c =
  mkApp (delayed_force proj2, [| a; b; c |])

let mk_ex_pi1 a b c =
  mkApp (delayed_force ex_pi1, [| a; b; c |])

let mk_ex_pi2 a b c =
  mkApp (delayed_force ex_pi2, [| a; b; c |])

let mkSubset name typ prop =
  mkApp ((delayed_force sig_).typ,
	 [| typ; mkLambda (name, typ, prop) |])

let mk_eq typ x y = mkApp (delayed_force eq_ind, [| typ; x ; y |])
let mk_eq_refl typ x = mkApp (delayed_force eq_refl, [| typ; x |])
let mk_JMeq typ x typ' y = mkApp (delayed_force jmeq_ind, [| typ; x ; typ'; y |])
let mk_JMeq_refl typ x = mkApp (delayed_force jmeq_refl, [| typ; x |])

let unsafe_fold_right f = function
    hd :: tl -> List.fold_right f tl hd
  | [] -> raise (Invalid_argument "unsafe_fold_right")

let mk_conj l =
  let conj_typ = delayed_force and_typ in
    unsafe_fold_right
      (fun c conj ->
	 mkApp (conj_typ, [| c ; conj |]))
      l

let mk_not c =
  let notc = delayed_force not_ref in
    mkApp (notc, [| c |])

let and_tac l hook =
  let andc = Coqlib.build_coq_and () in
  let rec aux ((accid, goal, tac, extract) as acc) = function
    | [] -> (* Singleton *) acc

    | (id, x, elgoal, eltac) :: tl ->
	let tac' = tclTHEN simplest_split (tclTHENLIST [tac; eltac]) in
	let proj = fun c -> mkProj2 goal elgoal c in
	let extract = List.map (fun (id, x, y, f) -> (id, x, y, (fun c -> f (mkProj1 goal elgoal c)))) extract in
	  aux ((string_of_id id) ^ "_" ^ accid, mkApp (andc, [| goal; elgoal |]), tac',
	       (id, x, elgoal, proj) :: extract) tl

  in
  let and_proof_id, and_goal, and_tac, and_extract =
    match l with
      | [] -> raise (Invalid_argument "and_tac: empty list of goals")
      | (hdid, x, hdg, hdt) :: tl ->
	  aux (string_of_id hdid, hdg, hdt, [hdid, x, hdg, (fun c -> c)]) tl
  in
  let and_proofid = id_of_string (and_proof_id ^ "_and_proof") in
    Lemmas.start_proof and_proofid goal_kind and_goal
      (hook (fun c -> List.map (fun (id, x, t, f) -> (id, x, t, f c)) and_extract));
    trace (str "Started and proof");
    Pfedit.by and_tac;
    trace (str "Applied and tac")


let destruct_ex ext ex =
  let rec aux c acc =
    match kind_of_term c with
	App (f, args) ->
	  (match kind_of_term f with
	       Ind i when i = Term.destInd (delayed_force ex_ind) && Array.length args = 2 ->
		 let (dom, rng) =
		   try (args.(0), args.(1))
		   with e when Errors.noncritical e -> assert(false)
		 in
		 let pi1 = (mk_ex_pi1 dom rng acc) in
		 let rng_body =
		   match kind_of_term rng with
		       Lambda (_, _, t) -> subst1 pi1 t
		     | t -> rng
		 in
		   pi1 :: aux rng_body (mk_ex_pi2 dom rng acc)
	     | _ -> [acc])
      | _ -> [acc]
  in aux ex ext

open Glob_term

let id_of_name = function
    Name n -> n
  | Anonymous -> raise (Invalid_argument "id_of_name")

let definition_message id =
  Nameops.pr_id id ++ str " is defined"

let recursive_message v =
  match Array.length v with
    | 0 -> error "no recursive definition"
    | 1 -> (Printer.pr_constant (Global.env ()) v.(0) ++ str " is recursively defined")
    | _ -> hov 0 (prvect_with_sep pr_comma (Printer.pr_constant (Global.env ())) v ++
		    spc () ++ str "are recursively defined")

let print_message m =
  Flags.if_verbose ppnl m

(* Solve an obligation using tactics, return the corresponding proof term *)
let solve_by_tac evi t =
  let id = id_of_string "H" in
  try
    Pfedit.start_proof id goal_kind evi.evar_hyps evi.evar_concl
    (fun _ _ -> ());
    Pfedit.by (tclCOMPLETE t);
    let _,(const,_,_,_) = Pfedit.cook_proof ignore in
      Pfedit.delete_current_proof (); 
      Inductiveops.control_only_guard (Global.env ())
	const.Entries.const_entry_body;
      const.Entries.const_entry_body
  with reraise ->
    Pfedit.delete_current_proof();
    raise reraise

(* let apply_tac t goal = t goal *)

(* let solve_by_tac evi t = *)
(*   let ev = 1 in *)
(*   let evm = Evd.add Evd.empty ev evi in *)
(*   let goal = {it = evi; sigma = evm } in *)
(*   let (res, valid) = apply_tac t goal in *)
(*     if res.it = [] then *)
(*       let prooftree = valid [] in *)
(*       let proofterm, obls = Refiner.extract_open_proof res.sigma prooftree in *)
(* 	if obls = [] then proofterm *)
(* 	else raise Exit *)
(*     else raise Exit *)

let rec string_of_list sep f = function
    [] -> ""
  | x :: [] -> f x
  | x :: ((y :: _) as tl) -> f x ^ sep ^ string_of_list sep f tl

let string_of_intset d =
  string_of_list "," string_of_int (Intset.elements d)

(**********************************************************)
(* Pretty-printing *)
open Printer
open Ppconstr
open Nameops
open Evd

let pr_meta_map evd =
  let ml = meta_list evd in
  let pr_name = function
      Name id -> str"[" ++ pr_id id ++ str"]"
    | _ -> mt() in
  let pr_meta_binding = function
    | (mv,Cltyp (na,b)) ->
      	hov 0
	  (pr_meta mv ++ pr_name na ++ str " : " ++
           Termops.print_constr b.rebus ++ fnl ())
    | (mv,Clval(na,b,_)) ->
      	hov 0
	  (pr_meta mv ++ pr_name na ++ str " := " ++
             Termops.print_constr (fst b).rebus ++ fnl ())
  in
  prlist pr_meta_binding ml

let pr_idl idl = prlist_with_sep pr_spc pr_id idl

let pr_evar_info evi =
  let phyps =
    (*pr_idl (List.rev (ids_of_named_context (evar_context evi))) *)
    Printer.pr_named_context (Global.env()) (evar_context evi)
  in
  let pty = Termops.print_constr evi.evar_concl in
  let pb =
    match evi.evar_body with
      | Evar_empty -> mt ()
      | Evar_defined c -> spc() ++ str"=> "  ++ Termops.print_constr c
  in
  hov 2 (str"["  ++ phyps ++ spc () ++ str"|- "  ++ pty ++ pb ++ str"]")

let pr_evar_map sigma =
  h 0
    (prlist_with_sep pr_fnl
      (fun (ev,evi) ->
        h 0 (str(string_of_existential ev)++str"=="++ pr_evar_info evi))
      (to_list sigma))

let pr_constraints pbs =
  h 0
    (prlist_with_sep pr_fnl (fun (pbty,t1,t2) ->
      Termops.print_constr t1 ++ spc() ++
      str (match pbty with
	| Reduction.CONV -> "=="
	| Reduction.CUMUL -> "<=") ++
      spc() ++ Termops.print_constr t2) pbs)

let pr_evar_map evd =
  let pp_evm =
    let evars =  evd in
    if evars = empty then mt() else
      str"EVARS:"++brk(0,1)++pr_evar_map evars++fnl() in
  let pp_met =
    if meta_list evd = [] then mt() else
      str"METAS:"++brk(0,1)++pr_meta_map evd in
  v 0 (pp_evm ++ pp_met)

let contrib_tactics_path =
  make_dirpath (List.map id_of_string ["Tactics";contrib_name;"Coq"])

let tactics_tac s =
  lazy(make_kn (MPfile contrib_tactics_path) (make_dirpath []) (mk_label s))

let tactics_call tac args =
  TacArg(dummy_loc,TacCall(dummy_loc, ArgArg(dummy_loc, Lazy.force (tactics_tac tac)),args))