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
|
(* $Id$ *)
open Pp
open Util
open Names
open Term
open Reduction
open Inductive
open Evd
open Environ
open Proof_trees
open Clenv
open Pattern
open Coqlib
(* 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). *)
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 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 (build_coq_refl_rel1_pattern ()) constr_types.(0) ||
is_matching (build_coq_refl_rel1_pattern ()) constr_types.(0))
then
Some (hdapp,args)
else
None
| _ -> None
let is_equation t = op2bool (match_with_equation t)
let match_with_nottype t =
try
match matches (build_coq_arrow_pattern ()) 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
|
