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
|
(* $Id$ *)
open Pp
open Util
open Names
(* open Generic *)
open Term
open Reduction
open Inductive
open Evd
open Environ
open Proof_trees
open Stock
open Clenv
open Pattern
(* The pattern table for tactics. *)
(* Description: see the interface. *)
(* First part : introduction of term patterns *)
type module_mark = Stock.module_mark
let parse_astconstr s =
try
Pcoq.parse_string Pcoq.Constr.constr_eoi s
with Stdpp.Exc_located (_ , (Stream.Failure | Stream.Error _)) ->
error "Syntax error : not a construction"
(* Patterns *)
let parse_pattern s =
Astterm.interp_constrpattern Evd.empty (Global.env()) (parse_astconstr s)
type marked_pattern = (int list * constr_pattern) Stock.stocked
let (pattern_stock : (int list * constr_pattern) Stock.stock) =
Stock.make_stock { name = "PATTERN"; proc = parse_pattern }
let put_pat = Stock.stock pattern_stock
let get_pat tm = snd (Stock.retrieve pattern_stock tm)
let make_module_marker = Stock.make_module_marker
(* Squeletons *)
let parse_squeleton s =
let c = Astterm.interp_constr Evd.empty (Global.env()) (parse_astconstr s) in
(collect_metas c, c)
type marked_term = (int list * constr) Stock.stocked
let (squeleton_stock : (int list * constr) Stock.stock) =
Stock.make_stock { name = "SQUELETON"; proc = parse_squeleton }
let put_squel = Stock.stock squeleton_stock
let get_squel_core = Stock.retrieve squeleton_stock
(* Sera mieux avec des noms qualifiés *)
let get_reference mods s =
if list_subset mods (Library.loaded_modules()) then
try Declare.global_reference CCI (id_of_string s)
with Not_found ->
error ("get_reference: "^s^"is not defined in the given modules")
else error "The required modules are not open"
let soinstance squel arglist =
let mvs,c = get_squel_core squel in
let mvb = List.combine mvs arglist in
Reduction.local_strong (Reduction.whd_meta mvb) c
let get_squel m =
let mvs, c = get_squel_core m in
if mvs = [] then c
else errorlabstrm "get_squel"
[< Printer.prterm c;
'sPC; 'sTR "is not a closed squeleton, use 'soinstance'" >]
(* I implemented the following functions which test whether a term t
is an inductive but non-recursive type, a general conjuction, a
general disjunction, or a type with no constructors.
They are more general than matching with or_term, and_term, etc,
since they do not depend on the name of the type. Hence, they
also work on ad-hoc disjunctions introduced by the user.
-- Eduardo (6/8/97). *)
let mmk = make_module_marker ["Prelude"]
type 'a matching_function = constr -> 'a option
type testing_function = constr -> bool
let op2bool = function Some _ -> true | None -> false
let match_with_non_recursive_type t =
match kind_of_term t with
| IsApp _ ->
let (hdapp,args) = decomp_app t in
(match kind_of_term hdapp with
| IsMutInd ind ->
if not (Global.mind_is_recursive ind) then
Some (hdapp,args)
else
None
| _ -> None)
| _ -> None
let is_non_recursive_type t = op2bool (match_with_non_recursive_type t)
(* A general conjunction type is a non-recursive inductive type with
only one constructor. *)
let match_with_conjunction t =
let (hdapp,args) = decomp_app t in
match kind_of_term hdapp with
| IsMutInd ind ->
let mispec = Global.lookup_mind_specif ind in
if (mis_nconstr mispec = 1)
&& (not (mis_is_recursive mispec)) && (mis_nrealargs mispec = 0)
then
Some (hdapp,args)
else
None
| _ -> None
let is_conjunction t = op2bool (match_with_conjunction t)
(* A general disjunction type is a non-recursive inductive type all
whose constructors have a single argument. *)
let match_with_disjunction t =
let (hdapp,args) = decomp_app t in
match kind_of_term hdapp with
| IsMutInd ind ->
let mispec = Global.lookup_mind_specif ind in
let constr_types = mis_nf_lc mispec in
let only_one_arg c =
((nb_prod c) - (mis_nparams mispec)) = 1 in
if (array_for_all only_one_arg constr_types) &&
(not (mis_is_recursive mispec))
then
Some (hdapp,args)
else
None
| _ -> None
let is_disjunction t = op2bool (match_with_disjunction t)
let match_with_empty_type t =
let (hdapp,args) = decomp_app t in
match (kind_of_term hdapp) with
| IsMutInd ind ->
let nconstr = Global.mind_nconstr ind in
if nconstr = 0 then Some hdapp else None
| _ -> None
let is_empty_type t = op2bool (match_with_empty_type t)
let match_with_unit_type t =
let (hdapp,args) = decomp_app t in
match (kind_of_term hdapp) with
| IsMutInd ind ->
let constr_types = Global.mind_nf_lc ind in
let nconstr = Global.mind_nconstr ind in
let zero_args c = ((nb_prod c) - (Global.mind_nparams ind)) = 0 in
if nconstr = 1 && (array_for_all zero_args constr_types) then
Some hdapp
else
None
| _ -> None
let is_unit_type t = op2bool (match_with_unit_type t)
(* Checks if a given term is an application of an
inductive binary relation R, so that R has only one constructor
stablishing its reflexivity. *)
let refl_rel_pat1 = put_pat mmk "(A : ?)(x:A)(? A x x)"
let refl_rel_pat2 = put_pat mmk "(x : ?)(? x x)"
let match_with_equation t =
let (hdapp,args) = decomp_app t in
match (kind_of_term hdapp) with
| IsMutInd ind ->
let constr_types = Global.mind_nf_lc ind in
let nconstr = Global.mind_nconstr ind in
if nconstr = 1 &&
(is_matching (get_pat refl_rel_pat1) constr_types.(0) ||
is_matching (get_pat refl_rel_pat2) constr_types.(0))
then
Some (hdapp,args)
else
None
| _ -> None
let is_equation t = op2bool (match_with_equation t)
let arrow_pat = put_pat mmk "(?1 -> ?2)"
let match_with_nottype t =
try
match matches (get_pat arrow_pat) t with
| [(1,arg);(2,mind)] ->
if is_empty_type mind then Some (mind,arg) else None
| _ -> anomaly "Incorrect pattern matching"
with PatternMatchingFailure -> None
let is_nottype t = op2bool (match_with_nottype t)
let is_imp_term c = match kind_of_term c with
| IsProd (_,_,b) -> not (dependent (mkRel 1) b)
| _ -> false
|