← Back to branch summary

~ubuntu-branches/ubuntu/wily/coq-doc/wily

« back to all changes in this revision

Viewing changes to kernel/closure.mli

  • Committer: Bazaar Package Importer
  • Author(s): Stéphane Glondu, Stéphane Glondu, Samuel Mimram
  • Date: 2010-01-07 22:50:39 UTC
  • mfrom: (1.2.2 upstream)
  • Revision ID: james.westby@ubuntu.com-20100107225039-n3cq82589u0qt0s2
Tags: 8.2pl1-1
http://bugs.debian.org/563669
http://bugs.debian.org/543545
[ Stéphane Glondu ]
* New upstream release (Closes: #563669)
  - remove patches
* Packaging overhaul:
  - use git, advertise it in Vcs-* fields of debian/control
  - use debhelper 7 and dh with override
  - use source format 3.0 (quilt)
* debian/control:
  - set Maintainer to d-o-m, set Uploaders to Sam and myself
  - add Homepage field
  - bump Standards-Version to 3.8.3
* Register PDF documentation into doc-base
* Add debian/watch
* Update debian/copyright

[ Samuel Mimram ]
* Change coq-doc's description to mention that it provides documentation in
  pdf format, not postscript, closes: #543545.

Show diffs side-by-side

added added

removed removed

Lines of Context:
kernel/closure.mli
 
1
(************************************************************************)
 
2
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
 
4
(*   \VV/  **************************************************************)
 
5
(*    //   *      This file is distributed under the terms of the       *)
 
6
(*         *       GNU Lesser General Public License Version 2.1        *)
 
7
(************************************************************************)
 
8
 
 
9
(*i $Id: closure.mli 11897 2009-02-09 19:28:02Z barras $ i*)
 
10
 
 
11
(*i*)
 
12
open Pp
 
13
open Names
 
14
open Term
 
15
open Environ
 
16
open Esubst
 
17
(*i*)
 
18
 
 
19
(* Flags for profiling reductions. *)
 
20
val stats : bool ref
 
21
val share : bool ref
 
22
 
 
23
val with_stats: 'a Lazy.t -> 'a
 
24
 
 
25
(*s Delta implies all consts (both global (= by
 
26
  [kernel_name]) and local (= by [Rel] or [Var])), all evars, and letin's.
 
27
  Rem: reduction of a Rel/Var bound to a term is Delta, but reduction of 
 
28
  a LetIn expression is Letin reduction *)
 
29
 
 
30
 
 
31
 
 
32
val all_opaque      : transparent_state
 
33
val all_transparent : transparent_state
 
34
 
 
35
(* Sets of reduction kinds. *)
 
36
module type RedFlagsSig = sig
 
37
  type reds
 
38
  type red_kind
 
39
 
 
40
  (* The different kinds of reduction *)
 
41
  val fBETA : red_kind
 
42
  val fDELTA : red_kind
 
43
  val fIOTA : red_kind
 
44
  val fZETA : red_kind
 
45
  val fCONST : constant -> red_kind
 
46
  val fVAR : identifier -> red_kind
 
47
 
 
48
  (* No reduction at all *)
 
49
  val no_red : reds
 
50
 
 
51
  (* Adds a reduction kind to a set *)
 
52
  val red_add : reds -> red_kind -> reds
 
53
 
 
54
  (* Removes a reduction kind to a set *)
 
55
  val red_sub : reds -> red_kind -> reds
 
56
 
 
57
  (* Adds a reduction kind to a set *)
 
58
  val red_add_transparent : reds -> transparent_state -> reds
 
59
 
 
60
  (* Build a reduction set from scratch = iter [red_add] on [no_red] *)
 
61
  val mkflags : red_kind list -> reds
 
62
 
 
63
  (* Tests if a reduction kind is set *)
 
64
  val red_set : reds -> red_kind -> bool
 
65
 
 
66
  (* Gives the constant list *)
 
67
  val red_get_const : reds -> bool * evaluable_global_reference list
 
68
end
 
69
 
 
70
module RedFlags : RedFlagsSig
 
71
open RedFlags
 
72
 
 
73
val beta               : reds
 
74
val betaiota           : reds
 
75
val betadeltaiota      : reds
 
76
val betaiotazeta       : reds
 
77
val betadeltaiotanolet : reds
 
78
 
 
79
val unfold_side_red : reds
 
80
val unfold_red : evaluable_global_reference -> reds
 
81
 
 
82
(***********************************************************************)
 
83
type table_key = id_key
 
84
 
 
85
type 'a infos
 
86
val ref_value_cache: 'a infos -> table_key -> 'a option
 
87
val info_flags: 'a infos -> reds
 
88
val create: ('a infos -> constr -> 'a) -> reds -> env ->
 
89
  (existential -> constr option) -> 'a infos
 
90
val evar_value : 'a infos -> existential -> constr option
 
91
 
 
92
(************************************************************************)
 
93
(*s Lazy reduction. *)
 
94
 
 
95
(* [fconstr] is the type of frozen constr *)
 
96
 
 
97
type fconstr
 
98
 
 
99
(* [fconstr] can be accessed by using the function [fterm_of] and by
 
100
   matching on type [fterm] *)
 
101
 
 
102
type fterm =
 
103
  | FRel of int
 
104
  | FAtom of constr (* Metas and Sorts *)
 
105
  | FCast of fconstr * cast_kind * fconstr 
 
106
  | FFlex of table_key
 
107
  | FInd of inductive
 
108
  | FConstruct of constructor
 
109
  | FApp of fconstr * fconstr array
 
110
  | FFix of fixpoint * fconstr subs
 
111
  | FCoFix of cofixpoint * fconstr subs
 
112
  | FCases of case_info * fconstr * fconstr * fconstr array
 
113
  | FLambda of int * (name * constr) list * constr * fconstr subs
 
114
  | FProd of name * fconstr * fconstr
 
115
  | FLetIn of name * fconstr * fconstr * constr * fconstr subs
 
116
  | FEvar of existential * fconstr subs
 
117
  | FLIFT of int * fconstr
 
118
  | FCLOS of constr * fconstr subs
 
119
  | FLOCKED
 
120
 
 
121
(************************************************************************)
 
122
(*s A [stack] is a context of arguments, arguments are pushed by
 
123
   [append_stack] one array at a time but popped with [decomp_stack]
 
124
   one by one *)
 
125
 
 
126
type stack_member =
 
127
  | Zapp of fconstr array
 
128
  | Zcase of case_info * fconstr * fconstr array
 
129
  | Zfix of fconstr * stack
 
130
  | Zshift of int
 
131
  | Zupdate of fconstr
 
132
 
 
133
and stack = stack_member list
 
134
 
 
135
val empty_stack : stack
 
136
val append_stack : fconstr array -> stack -> stack
 
137
 
 
138
val decomp_stack : stack -> (fconstr * stack) option
 
139
val array_of_stack : stack -> fconstr array
 
140
val stack_assign : stack -> int -> fconstr -> stack
 
141
val stack_args_size : stack -> int
 
142
val stack_tail : int -> stack -> stack
 
143
val stack_nth : stack -> int -> fconstr
 
144
val zip_term : (fconstr -> constr) -> constr -> stack -> constr
 
145
 
 
146
(* To lazy reduce a constr, create a [clos_infos] with
 
147
   [create_clos_infos], inject the term to reduce with [inject]; then use
 
148
   a reduction function *)
 
149
 
 
150
val inject : constr -> fconstr
 
151
(* mk_atom: prevents a term from being evaluated *)
 
152
val mk_atom : constr -> fconstr
 
153
 
 
154
val fterm_of : fconstr -> fterm
 
155
val term_of_fconstr : fconstr -> constr
 
156
val destFLambda :
 
157
  (fconstr subs -> constr -> fconstr) -> fconstr -> name * fconstr * fconstr
 
158
 
 
159
(* Global and local constant cache *)
 
160
type clos_infos
 
161
val create_clos_infos :
 
162
  ?evars:(existential->constr option) -> reds -> env -> clos_infos
 
163
 
 
164
(* Reduction function *)
 
165
 
 
166
(* [norm_val] is for strong normalization *)
 
167
val norm_val : clos_infos -> fconstr -> constr
 
168
 
 
169
(* [whd_val] is for weak head normalization *)
 
170
val whd_val : clos_infos -> fconstr -> constr
 
171
 
 
172
(* [whd_stack] performs weak head normalization in a given stack. It
 
173
   stops whenever a reduction is blocked. *)
 
174
val whd_stack :
 
175
  clos_infos -> fconstr -> stack -> fconstr * stack
 
176
 
 
177
(* Conversion auxiliary functions to do step by step normalisation *)
 
178
 
 
179
(* [unfold_reference] unfolds references in a [fconstr] *)
 
180
val unfold_reference : clos_infos -> table_key -> fconstr option
 
181
 
 
182
(* [mind_equiv] checks whether two inductive types are intentionally equal *)
 
183
val mind_equiv : env -> inductive -> inductive -> bool
 
184
val mind_equiv_infos : clos_infos -> inductive -> inductive -> bool
 
185
 
 
186
(************************************************************************)
 
187
(*i This is for lazy debug *)
 
188
 
 
189
val lift_fconstr      : int -> fconstr -> fconstr
 
190
val lift_fconstr_vect : int -> fconstr array -> fconstr array
 
191
 
 
192
val mk_clos      : fconstr subs -> constr -> fconstr
 
193
val mk_clos_vect : fconstr subs -> constr array -> fconstr array
 
194
val mk_clos_deep :
 
195
  (fconstr subs -> constr -> fconstr) ->
 
196
   fconstr subs -> constr -> fconstr
 
197
 
 
198
val kni: clos_infos -> fconstr -> stack -> fconstr * stack
 
199
val knr: clos_infos -> fconstr -> stack -> fconstr * stack
 
200
val kl : clos_infos -> fconstr -> constr
 
201
 
 
202
val to_constr : (lift -> fconstr -> constr) -> lift -> fconstr -> constr
 
203
val optimise_closure : fconstr subs -> constr -> fconstr subs * constr
 
204
 
 
205
(* End of cbn debug section i*)