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
|
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* v * Copyright INRIA, CNRS and contributors *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
(* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *)
open Names
open Constr
open Context
open Termops
open Proofview.Notations
open Ssrast
open Ssrcommon
module RelDecl = Context.Rel.Declaration
module NamedDecl = Context.Named.Declaration
(** Tacticals (+, -, *, done, by, do, =>, first, and last). *)
let get_index = function Locus.ArgArg i -> i | _ ->
anomaly "Uninterpreted index"
(* Toplevel constr must be globalized twice ! *)
(** The "first" and "last" tacticals. *)
let tclPERM perm tac =
Proofview.Goal.enter begin fun gls ->
tac <*> (Proofview.Unsafe.tclGETGOALS >>= fun gls -> Proofview.Unsafe.tclSETGOALS (perm gls))
end
let rot_hyps dir i hyps =
let n = List.length hyps in
if i = 0 then List.rev hyps else
if i > n then CErrors.user_err (Pp.str "Not enough goals") else
let rec rot i l_hyps = function
| hyp :: hyps' when i > 0 -> rot (i - 1) (hyp :: l_hyps) hyps'
| hyps' -> hyps' @ (List.rev l_hyps) in
rot (match dir with L2R -> i | R2L -> n - i) [] hyps
let tclSEQAT ist atac1 dir (ivar, ((_, atacs2), atac3)) =
let i = get_index ivar in
let evtac t = ssrevaltac ist t in
let tac1 = evtac atac1 in
if atacs2 = [] && atac3 <> None then tclPERM (rot_hyps dir i) tac1 else
let evotac = function Some atac -> evtac atac | _ -> Tacticals.tclIDTAC in
let tac3 = evotac atac3 in
let rec mk_pad n = if n > 0 then tac3 :: mk_pad (n - 1) else [] in
match dir, mk_pad (i - 1), List.map evotac atacs2 with
| L2R, [], [tac2] when atac3 = None -> Tacticals.tclTHENFIRST tac1 tac2
| L2R, [], [tac2] when atac3 = None -> Tacticals.tclTHENLAST tac1 tac2
| L2R, pad, tacs2 -> Tacticals.tclTHENSFIRSTn tac1 (Array.of_list (pad @ tacs2)) tac3
| R2L, pad, tacs2 -> Tacticals.tclTHENSLASTn tac1 tac3 (Array.of_list (tacs2 @ pad))
(** The "in" pseudo-tactical *)(* {{{ **********************************************)
let hidden_goal_tag = "the_hidden_goal"
let check_wgen_uniq gens =
let clears = List.flatten (List.map fst gens) in
check_hyps_uniq [] clears;
let ids = CList.map_filter
(function (_,Some ((id,_),_)) -> Some (hoi_id id) | _ -> None) gens in
let rec check ids = function
| id :: _ when List.mem id ids ->
errorstrm Pp.(str"Duplicate generalization " ++ Id.print id)
| id :: hyps -> check (id :: ids) hyps
| [] -> () in
check [] ids
let pf_clauseids gens clseq =
let keep_clears = List.map (fun (x, _) -> x, None) in
if gens <> [] then (check_wgen_uniq gens; gens) else
if clseq <> InAll && clseq <> InAllHyps then keep_clears gens else
CErrors.user_err (Pp.str "assumptions should be named explicitly")
let hidden_clseq = function InHyps | InHypsSeq | InAllHyps -> true | _ -> false
let posetac id cl = Tactics.pose_tac (Name id) cl
let hidetacs clseq idhide cl0 =
if not (hidden_clseq clseq) then [] else
[posetac idhide cl0;
convert_concl_no_check (EConstr.mkVar idhide)]
let endclausestac id_map clseq gl_id cl0 =
let open Tacmach in
Proofview.Goal.enter begin fun gl ->
let not_hyp' id = not (List.mem_assoc id id_map) in
let orig_id id = try List.assoc id id_map with Not_found -> id in
let dc, c = EConstr.decompose_prod_assum (project gl) (pf_concl gl) in
let hide_goal = hidden_clseq clseq in
let c_hidden =
hide_goal && EConstr.eq_constr (project gl) c (EConstr.mkVar gl_id) in
let rec fits forced = function
| (id, _) :: ids, decl :: dc' when RelDecl.get_name decl = Name id ->
fits true (ids, dc')
| ids, dc' ->
forced && ids = [] && (not hide_goal || dc' = [] && c_hidden) in
let rec unmark c = match EConstr.kind (project gl) c with
| Var id when hidden_clseq clseq && id = gl_id -> cl0
| Prod ({binder_name=Name id} as na, t, c') when List.mem_assoc id id_map ->
EConstr.mkProd ({na with binder_name=Name (orig_id id)}, unmark t, unmark c')
| LetIn ({binder_name=Name id} as na, v, t, c') when List.mem_assoc id id_map ->
EConstr.mkLetIn ({na with binder_name=Name (orig_id id)}, unmark v, unmark t, unmark c')
| _ -> EConstr.map (project gl) unmark c in
let utac hyp =
Tactics.convert_hyp ~check:false ~reorder:false (NamedDecl.map_constr unmark hyp) in
let utacs = List.map utac (Proofview.Goal.hyps gl) in
let ugtac =
Proofview.Goal.enter begin fun gl ->
convert_concl_no_check (unmark (pf_concl gl))
end
in
let ctacs =
if hide_goal then [Tactics.clear [gl_id]]
else [] in
let mktac itacs = Tacticals.tclTHENLIST (itacs @ utacs @ ugtac :: ctacs) in
let itac (_, id) = Tactics.introduction id in
if fits false (id_map, List.rev dc) then mktac (List.map itac id_map) else
let all_ids = ids_of_rel_context dc @ pf_ids_of_hyps gl in
if List.for_all not_hyp' all_ids && not c_hidden then mktac [] else
errorstrm Pp.(str "tampering with discharged assumptions of \"in\" tactical")
end
let tclCLAUSES tac (gens, clseq) =
let open Proofview.Notations in
Proofview.Goal.enter begin fun gl ->
if clseq = InGoal || clseq = InSeqGoal then tac else
let clr_gens = pf_clauseids gens clseq in
let clear = Tacticals.tclTHENLIST (List.rev(List.fold_right clr_of_wgen clr_gens [])) in
let gl_id = mk_anon_id hidden_goal_tag (Tacmach.pf_ids_of_hyps gl) in
let cl0 = Proofview.Goal.concl gl in
let dtac =
Proofview.Goal.enter begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = Proofview.Goal.sigma gl in
let c = Proofview.Goal.concl gl in
let fold gen (sigma, args, c) = abs_wgen env sigma true mk_discharged_id gen (args, c) in
let sigma, args, c = List.fold_right fold gens (sigma, [], c) in
Proofview.Unsafe.tclEVARS sigma <*>
Tactics.apply_type ~typecheck:true c args
end
in
let endtac =
let id_map = CList.map_filter (function
| _, Some ((x,_),_) -> let id = hoi_id x in Some (mk_discharged_id id, id)
| _, None -> None) gens in
endclausestac id_map clseq gl_id cl0 in
Tacticals.tclTHENLIST (hidetacs clseq gl_id cl0 @ [dtac; clear; tac; endtac])
end
(** The "do" tactical. ********************************************************)
let hinttac ist is_by (is_or, atacs) =
Proofview.Goal.enter begin fun _ ->
let dtac = if is_by then donetac ~-1 else Tacticals.tclIDTAC in
let mktac = function
| Some atac -> Tacticals.tclTHEN (ssrevaltac ist atac) dtac
| _ -> dtac in
match List.map mktac atacs with
| [] -> if is_or then dtac else Tacticals.tclIDTAC
| [tac] -> tac
| tacs -> Tacticals.tclFIRST tacs
end
let ssrdotac ist (((n, m), tac), clauses) =
let mul = get_index n, m in
tclCLAUSES (tclMULT mul (hinttac ist false tac)) clauses
|
