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
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
open Names
(** TODO: cleanup *)
(** {6 Declarations} *)
(** A {e declaration} has the form [(name,body,type)]. It is either an
{e assumption} if [body=None] or a {e definition} if
[body=Some actualbody]. It is referred by {e name} if [na] is an
identifier or by {e relative index} if [na] is not an identifier
(in the latter case, [na] is of type [name] but just for printing
purpose) *)
type named_declaration = Id.t * Constr.t option * Constr.t
type named_list_declaration = Id.t list * Constr.t option * Constr.t
type rel_declaration = Name.t * Constr.t option * Constr.t
val map_named_declaration :
(Constr.t -> Constr.t) -> named_declaration -> named_declaration
val map_named_list_declaration :
(Constr.t -> Constr.t) -> named_list_declaration -> named_list_declaration
val map_rel_declaration :
(Constr.t -> Constr.t) -> rel_declaration -> rel_declaration
val fold_named_declaration :
(Constr.t -> 'a -> 'a) -> named_declaration -> 'a -> 'a
val fold_rel_declaration :
(Constr.t -> 'a -> 'a) -> rel_declaration -> 'a -> 'a
val exists_named_declaration :
(Constr.t -> bool) -> named_declaration -> bool
val exists_rel_declaration :
(Constr.t -> bool) -> rel_declaration -> bool
val for_all_named_declaration :
(Constr.t -> bool) -> named_declaration -> bool
val for_all_rel_declaration :
(Constr.t -> bool) -> rel_declaration -> bool
val eq_named_declaration :
named_declaration -> named_declaration -> bool
val eq_rel_declaration :
rel_declaration -> rel_declaration -> bool
(** {6 Signatures of ordered named declarations } *)
type named_context = named_declaration list
type section_context = named_context
type named_list_context = named_list_declaration list
type rel_context = rel_declaration list
(** In [rel_context], more recent declaration is on top *)
val empty_named_context : named_context
val add_named_decl : named_declaration -> named_context -> named_context
val vars_of_named_context : named_context -> Id.Set.t
val lookup_named : Id.t -> named_context -> named_declaration
(** number of declarations *)
val named_context_length : named_context -> int
(** named context equality *)
val named_context_equal : named_context -> named_context -> bool
(** {6 Recurrence on [named_context]: older declarations processed first } *)
val fold_named_context :
(named_declaration -> 'a -> 'a) -> named_context -> init:'a -> 'a
val fold_named_list_context :
(named_list_declaration -> 'a -> 'a) -> named_list_context -> init:'a -> 'a
(** newer declarations first *)
val fold_named_context_reverse :
('a -> named_declaration -> 'a) -> init:'a -> named_context -> 'a
(** {6 Section-related auxiliary functions } *)
(** [instance_from_named_context Ω] builds an instance [args] such
that [Ω ⊢ args:Ω] where [Ω] is a named context and with the local
definitions of [Ω] skipped. Example: for [id1:T,id2:=c,id3:U], it
gives [Var id1, Var id3]. All [idj] are supposed distinct. *)
val instance_from_named_context : named_context -> Constr.t list
(** [extended_rel_list n Γ] builds an instance [args] such that [Γ,Δ ⊢ args:Γ]
with n = |Δ| and with the local definitions of [Γ] skipped in
[args]. Example: for [x:T,y:=c,z:U] and [n]=2, it gives [Rel 5, Rel 3]. *)
val extended_rel_list : int -> rel_context -> Constr.t list
(** [extended_rel_vect n Γ] does the same, returning instead an array. *)
val extended_rel_vect : int -> rel_context -> Constr.t array
(** {6 ... } *)
(** Signatures of ordered optionally named variables, intended to be
accessed by de Bruijn indices *)
(** {6 Recurrence on [rel_context]: older declarations processed first } *)
val fold_rel_context :
(rel_declaration -> 'a -> 'a) -> rel_context -> init:'a -> 'a
(** newer declarations first *)
val fold_rel_context_reverse :
('a -> rel_declaration -> 'a) -> init:'a -> rel_context -> 'a
(** {6 Map function of [rel_context] } *)
val map_rel_context : (Constr.t -> Constr.t) -> rel_context -> rel_context
(** {6 Map function of [named_context] } *)
val map_named_context : (Constr.t -> Constr.t) -> named_context -> named_context
(** {6 Map function of [rel_context] } *)
val iter_rel_context : (Constr.t -> unit) -> rel_context -> unit
(** {6 Map function of [named_context] } *)
val iter_named_context : (Constr.t -> unit) -> named_context -> unit
(** {6 Contexts of declarations referred to by de Bruijn indices } *)
val empty_rel_context : rel_context
val add_rel_decl : rel_declaration -> rel_context -> rel_context
val lookup_rel : int -> rel_context -> rel_declaration
(** Size of the [rel_context] including LetIns *)
val rel_context_length : rel_context -> int
(** Size of the [rel_context] without LetIns *)
val rel_context_nhyps : rel_context -> int
(** Indicates whether a LetIn or a Lambda, starting from oldest declaration *)
val rel_context_tags : rel_context -> bool list
|
