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
|
(************************************************************************)
(* * The Rocq Prover / The Rocq 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) *)
(************************************************************************)
open Names
(** Locus : positions in hypotheses and goals *)
type 'a or_var =
| ArgArg of 'a
| ArgVar of lident
(** {6 Occurrences} *)
type 'a occurrences_gen =
| AllOccurrences
| AtLeastOneOccurrence
| AllOccurrencesBut of 'a list (** non-empty *)
| NoOccurrences
| OnlyOccurrences of 'a list (** non-empty *)
type occurrences_expr = (int or_var) occurrences_gen
type 'a with_occurrences_expr = occurrences_expr * 'a
type occurrences = int occurrences_gen
type 'a with_occurrences = occurrences * 'a
(** {6 Locations}
Selecting the occurrences in body (if any), in type, or in both *)
type hyp_location_flag = InHyp | InHypTypeOnly | InHypValueOnly
(** {6 Abstract clauses expressions}
A [clause_expr] (and its instance [clause]) denotes occurrences and
hypotheses in a goal in an abstract way; in particular, it can refer
to the set of all hypotheses independently of the effective contents
of the current goal
Concerning the field [onhyps]:
- [None] means *on every hypothesis*
- [Some l] means on hypothesis belonging to l *)
type 'a hyp_location_expr = 'a with_occurrences_expr * hyp_location_flag
type 'id clause_expr =
{ onhyps : 'id hyp_location_expr list option;
concl_occs : occurrences_expr }
type clause = Id.t clause_expr
(** {6 Concrete view of occurrence clauses} *)
(** [clause_atom] refers either to an hypothesis location (i.e. an
hypothesis with occurrences and a position, in body if any, in type
or in both) or to some occurrences of the conclusion *)
type clause_atom =
| OnHyp of Id.t * occurrences_expr * hyp_location_flag
| OnConcl of occurrences_expr
(** A [concrete_clause] is an effective collection of occurrences
in the hypotheses and the conclusion *)
type concrete_clause = clause_atom list
(** {6 A weaker form of clause with no mention of occurrences} *)
(** A [hyp_location] is an hypothesis together with a location *)
type hyp_location = Id.t * hyp_location_flag
(** A [goal_location] is either an hypothesis (together with a location)
or the conclusion (represented by None) *)
type goal_location = hyp_location option
(** {6 Simple clauses, without occurrences nor location} *)
(** A [simple_clause] is a set of hypotheses, possibly extended with
the conclusion (conclusion is represented by None) *)
type simple_clause = Id.t option list
(** {6 A notion of occurrences allowing to express "all occurrences
convertible to the first which matches"} *)
type 'a or_like_first = AtOccs of 'a | LikeFirst
|
