10
(****************************************************************************)
13
let contrib_name = "Program"
15
let subtac_dir = [contrib_name]
16
let fix_sub_module = "Wf"
17
let utils_module = "Utils"
18
let fixsub_module = subtac_dir @ [fix_sub_module]
19
let utils_module = subtac_dir @ [utils_module]
20
let init_constant dir s = gen_constant contrib_name dir s
21
let init_reference dir s = gen_reference contrib_name dir s
23
let fixsub = lazy (init_constant fixsub_module "Fix_sub")
24
let ex_pi1 = lazy (init_constant utils_module "ex_pi1")
25
let ex_pi2 = lazy (init_constant utils_module "ex_pi2")
27
let make_ref l s = lazy (init_reference l s)
28
let well_founded_ref = make_ref ["Init";"Wf"] "Well_founded"
29
let acc_ref = make_ref ["Init";"Wf"] "Acc"
30
let acc_inv_ref = make_ref ["Init";"Wf"] "Acc_inv"
31
let fix_sub_ref = make_ref fixsub_module "Fix_sub"
32
let fix_measure_sub_ref = make_ref fixsub_module "Fix_measure_sub"
33
let lt_ref = make_ref ["Init";"Peano"] "lt"
34
let lt_wf_ref = make_ref ["Wf_nat"] "lt_wf"
35
let refl_ref = make_ref ["Init";"Logic"] "refl_equal"
37
let make_ref s = Qualid (dummy_loc, qualid_of_string s)
38
let sig_ref = make_ref "Init.Specif.sig"
39
let proj1_sig_ref = make_ref "Init.Specif.proj1_sig"
40
let proj2_sig_ref = make_ref "Init.Specif.proj2_sig"
43
{ proj1 = init_constant ["Init"; "Specif"] "proj1_sig";
44
proj2 = init_constant ["Init"; "Specif"] "proj2_sig";
45
elim = init_constant ["Init"; "Specif"] "sig_rec";
46
intro = init_constant ["Init"; "Specif"] "exist";
47
typ = init_constant ["Init"; "Specif"] "sig" }
49
let sig_ = lazy (build_sig ())
51
let eq_ind = lazy (init_constant ["Init"; "Logic"] "eq")
52
let eq_rec = lazy (init_constant ["Init"; "Logic"] "eq_rec")
53
let eq_rect = lazy (init_constant ["Init"; "Logic"] "eq_rect")
54
let eq_refl = lazy (init_constant ["Init"; "Logic"] "refl_equal")
55
let eq_ind_ref = lazy (init_reference ["Init"; "Logic"] "eq")
56
let refl_equal_ref = lazy (init_reference ["Init"; "Logic"] "refl_equal")
58
let not_ref = lazy (init_constant ["Init"; "Logic"] "not")
60
let and_typ = lazy (Coqlib.build_coq_and ())
62
let eqdep_ind = lazy (init_constant [ "Logic";"Eqdep"] "eq_dep")
63
let eqdep_rec = lazy (init_constant ["Logic";"Eqdep"] "eq_dep_rec")
64
let eqdep_ind_ref = lazy (init_reference [ "Logic";"Eqdep"] "eq_dep")
65
let eqdep_intro_ref = lazy (init_reference [ "Logic";"Eqdep"] "eq_dep_intro")
68
check_required_library ["Coq";"Logic";"JMeq"];
69
init_constant ["Logic";"JMeq"] "JMeq"
72
check_required_library ["Coq";"Logic";"JMeq"];
73
init_constant ["Logic";"JMeq"] "JMeq_rec"
76
check_required_library ["Coq";"Logic";"JMeq"];
77
init_constant ["Logic";"JMeq"] "JMeq_refl"
79
let ex_ind = lazy (init_constant ["Init"; "Logic"] "ex")
80
let ex_intro = lazy (init_reference ["Init"; "Logic"] "ex_intro")
82
let proj1 = lazy (init_constant ["Init"; "Logic"] "proj1")
83
let proj2 = lazy (init_constant ["Init"; "Logic"] "proj2")
85
let boolind = lazy (init_constant ["Init"; "Datatypes"] "bool")
86
let sumboolind = lazy (init_constant ["Init"; "Specif"] "sumbool")
87
let natind = lazy (init_constant ["Init"; "Datatypes"] "nat")
88
let intind = lazy (init_constant ["ZArith"; "binint"] "Z")
89
let existSind = lazy (init_constant ["Init"; "Specif"] "sigS")
91
let existS = lazy (build_sigma_type ())
93
let prod = lazy (build_prod ())
97
let well_founded = lazy (init_constant ["Init"; "Wf"] "well_founded")
98
let fix = lazy (init_constant ["Init"; "Wf"] "Fix")
99
let acc = lazy (init_constant ["Init"; "Wf"] "Acc")
100
let acc_inv = lazy (init_constant ["Init"; "Wf"] "Acc_inv")
102
let extconstr = Constrextern.extern_constr true (Global.env ())
103
let extsort s = Constrextern.extern_constr true (Global.env ()) (mkSort s)
107
let my_print_constr = Termops.print_constr_env
108
let my_print_constr_expr = Ppconstr.pr_constr_expr
109
let my_print_rel_context env ctx = Printer.pr_rel_context env ctx
110
let my_print_context = Termops.print_rel_context
111
let my_print_named_context = Termops.print_named_context
112
let my_print_env = Termops.print_env
113
let my_print_rawconstr = Printer.pr_rawconstr_env
114
let my_print_evardefs = Evd.pr_evar_defs
116
let my_print_tycon_type = Evarutil.pr_tycon_type
124
if !Flags.debug && n >= debug_level then
131
if !Flags.debug && n >= debug_level then s
137
if !Flags.debug && debug_level > 0 then msgnl s
141
let rec pp_list f = function
143
| x :: y -> f x ++ spc () ++ pp_list f y
145
let wf_relations = Hashtbl.create 10
147
let std_relations () =
148
let add k v = Hashtbl.add wf_relations k v in
149
add (init_constant ["Init"; "Peano"] "lt")
150
(lazy (init_constant ["Arith"; "Wf_nat"] "lt_wf"))
152
let std_relations = Lazy.lazy_from_fun std_relations
154
type binders = Topconstr.local_binder list
158
Some constr -> constr e
161
let print_args env args =
162
Array.fold_right (fun a acc -> my_print_constr env a ++ spc () ++ acc) args (str "")
164
let make_existential loc ?(opaque = Define true) env isevars c =
165
let evar = Evarutil.e_new_evar isevars env ~src:(loc, QuestionMark opaque) c in
166
let (key, args) = destEvar evar in
167
(try trace (str "Constructed evar " ++ int key ++ str " applied to args: " ++
168
print_args env args ++ str " for type: "++
169
my_print_constr env c) with _ -> ());
172
let make_existential_expr loc env c =
173
let key = Evarutil.new_untyped_evar () in
174
let evar = Topconstr.CEvar (loc, key, None) in
175
debug 2 (str "Constructed evar " ++ int key);
178
let string_of_hole_kind = function
179
| ImplicitArg _ -> "ImplicitArg"
180
| BinderType _ -> "BinderType"
181
| QuestionMark _ -> "QuestionMark"
182
| CasesType -> "CasesType"
183
| InternalHole -> "InternalHole"
184
| TomatchTypeParameter _ -> "TomatchTypeParameter"
185
| GoalEvar -> "GoalEvar"
186
| ImpossibleCase -> "ImpossibleCase"
188
let evars_of_term evc init c =
189
let rec evrec acc c =
190
match kind_of_term c with
191
| Evar (n, _) when Evd.mem evc n -> Evd.add acc n (Evd.find evc n)
192
| Evar (n, _) -> assert(false)
193
| _ -> fold_constr evrec acc c
197
let non_instanciated_map env evd evm =
199
(fun evm (key, evi) ->
200
let (loc,k) = evar_source key !evd in
201
debug 2 (str "evar " ++ int key ++ str " has kind " ++
202
str (string_of_hole_kind k));
204
QuestionMark _ -> Evd.add evm key evi
206
debug 2 (str " and is an implicit");
207
Pretype_errors.error_unsolvable_implicit loc env evm (Evarutil.nf_evar_info evm evi) k None)
208
Evd.empty (Evarutil.non_instantiated evm)
210
let global_kind = Decl_kinds.IsDefinition Decl_kinds.Definition
211
let goal_kind = Decl_kinds.Global, Decl_kinds.DefinitionBody Decl_kinds.Definition
213
let global_proof_kind = Decl_kinds.IsProof Decl_kinds.Lemma
214
let goal_proof_kind = Decl_kinds.Global, Decl_kinds.Proof Decl_kinds.Lemma
216
let global_fix_kind = Decl_kinds.IsDefinition Decl_kinds.Fixpoint
217
let goal_fix_kind = Decl_kinds.Global, Decl_kinds.DefinitionBody Decl_kinds.Fixpoint
224
let rec aux acc = function
225
hd :: tl -> (match f hd with Some t -> aux (t :: acc) tl
226
| None -> aux acc tl)
230
let build_dependent_sum l =
231
let rec aux names conttac conttype = function
232
(n, t) :: ((_ :: _) as tl) ->
233
let hyptype = substl names t in
234
trace (spc () ++ str ("treating evar " ^ string_of_id n));
235
(try trace (str " assert: " ++ my_print_constr (Global.env ()) hyptype)
237
let tac = assert_tac (Name n) hyptype in
244
[constructor_tac false (Some 1) 1
245
(Rawterm.ImplicitBindings [inj_open (mkVar n)]);
251
let tex = mkLambda (Name n, t, typ) in
253
(mkApp (Lazy.force ex_ind, [| t; tex |])))
255
aux (mkVar n :: names) conttac conttype tl
257
(conttac intros, conttype t)
258
| [] -> raise (Invalid_argument "build_dependent_sum")
259
in aux [] id id (List.rev l)
265
mkApp (Lazy.force proj1, [| a; b; c |])
268
mkApp (Lazy.force proj2, [| a; b; c |])
270
let mk_ex_pi1 a b c =
271
mkApp (Lazy.force ex_pi1, [| a; b; c |])
273
let mk_ex_pi2 a b c =
274
mkApp (Lazy.force ex_pi2, [| a; b; c |])
276
let mkSubset name typ prop =
277
mkApp ((Lazy.force sig_).typ,
278
[| typ; mkLambda (name, typ, prop) |])
280
let mk_eq typ x y = mkApp (Lazy.force eq_ind, [| typ; x ; y |])
281
let mk_eq_refl typ x = mkApp (Lazy.force eq_refl, [| typ; x |])
282
let mk_JMeq typ x typ' y = mkApp (jmeq_ind (), [| typ; x ; typ'; y |])
283
let mk_JMeq_refl typ x = mkApp (jmeq_refl (), [| typ; x |])
285
let unsafe_fold_right f = function
286
hd :: tl -> List.fold_right f tl hd
287
| [] -> raise (Invalid_argument "unsafe_fold_right")
290
let conj_typ = Lazy.force and_typ in
293
mkApp (conj_typ, [| c ; conj |]))
297
let notc = Lazy.force not_ref in
298
mkApp (notc, [| c |])
301
let andc = Coqlib.build_coq_and () in
302
let rec aux ((accid, goal, tac, extract) as acc) = function
303
| [] -> (* Singleton *) acc
305
| (id, x, elgoal, eltac) :: tl ->
306
let tac' = tclTHEN simplest_split (tclTHENLIST [tac; eltac]) in
307
let proj = fun c -> mkProj2 goal elgoal c in
308
let extract = List.map (fun (id, x, y, f) -> (id, x, y, (fun c -> f (mkProj1 goal elgoal c)))) extract in
309
aux ((string_of_id id) ^ "_" ^ accid, mkApp (andc, [| goal; elgoal |]), tac',
310
(id, x, elgoal, proj) :: extract) tl
313
let and_proof_id, and_goal, and_tac, and_extract =
315
| [] -> raise (Invalid_argument "and_tac: empty list of goals")
316
| (hdid, x, hdg, hdt) :: tl ->
317
aux (string_of_id hdid, hdg, hdt, [hdid, x, hdg, (fun c -> c)]) tl
319
let and_proofid = id_of_string (and_proof_id ^ "_and_proof") in
320
Command.start_proof and_proofid goal_kind and_goal
321
(hook (fun c -> List.map (fun (id, x, t, f) -> (id, x, t, f c)) and_extract));
322
trace (str "Started and proof");
324
trace (str "Applied and tac")
327
let destruct_ex ext ex =
329
match kind_of_term c with
331
(match kind_of_term f with
332
Ind i when i = Term.destInd (Lazy.force ex_ind) && Array.length args = 2 ->
334
try (args.(0), args.(1))
335
with _ -> assert(false)
337
let pi1 = (mk_ex_pi1 dom rng acc) in
339
match kind_of_term rng with
340
Lambda (_, _, t) -> subst1 pi1 t
343
pi1 :: aux rng_body (mk_ex_pi2 dom rng acc)
350
let id_of_name = function
352
| Anonymous -> raise (Invalid_argument "id_of_name")
354
let definition_message id =
355
Nameops.pr_id id ++ str " is defined"
357
let recursive_message v =
358
match Array.length v with
359
| 0 -> error "no recursive definition"
360
| 1 -> (Printer.pr_constant (Global.env ()) v.(0) ++ str " is recursively defined")
361
| _ -> hov 0 (prvect_with_sep pr_coma (Printer.pr_constant (Global.env ())) v ++
362
spc () ++ str "are recursively defined")
364
let print_message m =
365
Flags.if_verbose ppnl m
367
(* Solve an obligation using tactics, return the corresponding proof term *)
368
let solve_by_tac evi t =
369
let id = id_of_string "H" in
371
Pfedit.start_proof id goal_kind evi.evar_hyps evi.evar_concl
373
Pfedit.by (tclCOMPLETE t);
374
let _,(const,_,_,_) = Pfedit.cook_proof ignore in
375
Pfedit.delete_current_proof (); const.Entries.const_entry_body
377
Pfedit.delete_current_proof();
380
(* let apply_tac t goal = t goal *)
382
(* let solve_by_tac evi t = *)
384
(* let evm = Evd.add Evd.empty ev evi in *)
385
(* let goal = {it = evi; sigma = evm } in *)
386
(* let (res, valid) = apply_tac t goal in *)
387
(* if res.it = [] then *)
388
(* let prooftree = valid [] in *)
389
(* let proofterm, obls = Refiner.extract_open_proof res.sigma prooftree in *)
390
(* if obls = [] then proofterm *)
391
(* else raise Exit *)
392
(* else raise Exit *)
394
let rec string_of_list sep f = function
397
| x :: ((y :: _) as tl) -> f x ^ sep ^ string_of_list sep f tl
399
let string_of_intset d =
400
string_of_list "," string_of_int (Intset.elements d)
402
(**********************************************************)
403
(* Pretty-printing *)
410
let pr_meta_map evd =
411
let ml = meta_list evd in
412
let pr_name = function
413
Name id -> str"[" ++ pr_id id ++ str"]"
415
let pr_meta_binding = function
416
| (mv,Cltyp (na,b)) ->
418
(pr_meta mv ++ pr_name na ++ str " : " ++
419
print_constr b.rebus ++ fnl ())
420
| (mv,Clval(na,b,_)) ->
422
(pr_meta mv ++ pr_name na ++ str " := " ++
423
print_constr (fst b).rebus ++ fnl ())
425
prlist pr_meta_binding ml
427
let pr_idl idl = prlist_with_sep pr_spc pr_id idl
429
let pr_evar_info evi =
431
(*pr_idl (List.rev (ids_of_named_context (evar_context evi))) *)
432
Printer.pr_named_context (Global.env()) (evar_context evi)
434
let pty = print_constr evi.evar_concl in
436
match evi.evar_body with
437
| Evar_empty -> mt ()
438
| Evar_defined c -> spc() ++ str"=> " ++ print_constr c
440
hov 2 (str"[" ++ phyps ++ spc () ++ str"|- " ++ pty ++ pb ++ str"]")
442
let pr_evar_map sigma =
444
(prlist_with_sep pr_fnl
446
h 0 (str(string_of_existential ev)++str"=="++ pr_evar_info evi))
449
let pr_constraints pbs =
451
(prlist_with_sep pr_fnl (fun (pbty,t1,t2) ->
452
print_constr t1 ++ spc() ++
454
| Reduction.CONV -> "=="
455
| Reduction.CUMUL -> "<=") ++
456
spc() ++ print_constr t2) pbs)
458
let pr_evar_defs evd =
460
let evars = evars_of evd in
461
if evars = empty then mt() else
462
str"EVARS:"++brk(0,1)++pr_evar_map evars++fnl() in
464
if meta_list evd = [] then mt() else
465
str"METAS:"++brk(0,1)++pr_meta_map evd in
466
v 0 (pp_evm ++ pp_met)
468
let contrib_tactics_path =
469
make_dirpath (List.map id_of_string ["Tactics";contrib_name;"Coq"])
471
lazy(make_kn (MPfile contrib_tactics_path) (make_dirpath []) (mk_label s))
473
let tactics_call tac args =
474
TacArg(TacCall(dummy_loc, ArgArg(dummy_loc, Lazy.force (tactics_tac tac)),args))
added
removed
contrib/subtac/subtac_utils.ml
