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
|
(************************************************************************)
(* * 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) *)
(************************************************************************)
open Names
open Libnames
open Constrexpr
(** Constrexpr_ops: utilities on [constr_expr] *)
val expr_Type_sort : sort_expr
val expr_SProp_sort : sort_expr
val expr_Prop_sort : sort_expr
val expr_Set_sort : sort_expr
(** {6 Equalities on [constr_expr] related types} *)
val sort_name_expr_eq : sort_name_expr -> sort_name_expr -> bool
val univ_level_expr_eq : univ_level_expr -> univ_level_expr -> bool
val sort_expr_eq : sort_expr -> sort_expr -> bool
val relevance_info_expr_eq : relevance_info_expr -> relevance_info_expr -> bool
val explicitation_eq : explicitation -> explicitation -> bool
(** Equality on [explicitation]. *)
val constr_expr_eq_gen : (constr_expr -> constr_expr -> bool) -> constr_expr -> constr_expr -> bool
val constr_expr_eq : constr_expr -> constr_expr -> bool
(** Equality on [constr_expr]. This is a syntactical one, which is oblivious to
some parsing details, including locations. *)
val local_binder_eq : local_binder_expr -> local_binder_expr -> bool
(** Equality on [local_binder_expr]. Same properties as [constr_expr_eq]. *)
val binder_kind_eq : binder_kind -> binder_kind -> bool
(** Equality on [binder_kind] *)
(** {6 Retrieving locations} *)
val constr_loc : constr_expr -> Loc.t option
val cases_pattern_expr_loc : cases_pattern_expr -> Loc.t option
val local_binders_loc : local_binder_expr list -> Loc.t option
(** {6 Constructors} *)
(** {7 Term constructors} *)
(** Basic form of the corresponding constructors *)
val mkIdentC : Id.t -> constr_expr
val mkRefC : qualid -> constr_expr
val mkCastC : constr_expr * Constr.cast_kind option * constr_expr -> constr_expr
val mkLambdaC : lname list * binder_kind * constr_expr * constr_expr -> constr_expr
val mkLetInC : lname * constr_expr * constr_expr option * constr_expr -> constr_expr
val mkProdC : lname list * binder_kind * constr_expr * constr_expr -> constr_expr
val mkAppC : constr_expr * constr_expr list -> constr_expr
(** Basic form of application, collapsing nested applications *)
(** Optimized constructors: does not add a constructor for an empty binder list *)
val mkLambdaCN : ?loc:Loc.t -> local_binder_expr list -> constr_expr -> constr_expr
val mkProdCN : ?loc:Loc.t -> local_binder_expr list -> constr_expr -> constr_expr
(** Aliases for the corresponding constructors; generally [mkLambdaCN] and
[mkProdCN] should be preferred *)
val mkCLambdaN : ?loc:Loc.t -> local_binder_expr list -> constr_expr -> constr_expr
val mkCProdN : ?loc:Loc.t -> local_binder_expr list -> constr_expr -> constr_expr
(** {7 Pattern constructors} *)
(** Interpretation of a list of patterns as a disjunctive pattern (optimized) *)
val mkCPatOr : ?loc:Loc.t -> cases_pattern_expr list -> cases_pattern_expr
val mkAppPattern : ?loc:Loc.t -> cases_pattern_expr -> cases_pattern_expr list -> cases_pattern_expr
(** Apply a list of pattern arguments to a pattern *)
(** {6 Destructors}*)
val coerce_reference_to_id : qualid -> Id.t
(** FIXME: nothing to do here *)
val coerce_to_id : constr_expr -> lident
(** Destruct terms of the form [CRef (Ident _)]. *)
val coerce_to_name : constr_expr -> lname
(** Destruct terms of the form [CRef (Ident _)] or [CHole _]. *)
val coerce_to_cases_pattern_expr : constr_expr -> cases_pattern_expr
(** {6 Binder manipulation} *)
val default_binder_kind : binder_kind
val names_of_local_binders : local_binder_expr list -> lname list
(** Retrieve a list of binding names from a list of binders. *)
val names_of_local_assums : local_binder_expr list -> lname list
(** Same as [names_of_local_binder_exprs], but does not take the [let] bindings into
account. *)
(** {6 Folds and maps} *)
(** Used in typeclasses *)
val fold_constr_expr_with_binders : (Id.t -> 'a -> 'a) ->
('a -> 'b -> constr_expr -> 'b) -> 'a -> 'b -> constr_expr -> 'b
(** Used in correctness and interface; absence of var capture not guaranteed
in pattern-matching clauses and in binders of the form [x,y:T(x)] *)
val map_constr_expr_with_binders :
(Id.t -> 'a -> 'a) -> ('a -> constr_expr -> constr_expr) ->
'a -> constr_expr -> constr_expr
(** {6 Miscellaneous}*)
val replace_vars_constr_expr :
Id.t Id.Map.t -> constr_expr -> constr_expr
val free_vars_of_constr_expr : constr_expr -> Id.Set.t
val occur_var_constr_expr : Id.t -> constr_expr -> bool
(** Return all (non-qualified) names treating binders as names *)
val names_of_constr_expr : constr_expr -> Id.Set.t
val ntn_loc : ?loc:Loc.t -> constr_notation_substitution -> notation -> (int * int) list
val patntn_loc : ?loc:Loc.t -> cases_pattern_notation_substitution -> notation -> (int * int) list
val isCSort : constr_expr -> bool
(** For cases pattern parsing errors *)
val error_invalid_pattern_notation : ?loc:Loc.t -> unit -> 'a
|
