← Back to branch summary

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

« back to all changes in this revision

Viewing changes to pretyping/evarutil.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:
pretyping/evarutil.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: evarutil.mli 12053 2009-04-06 16:20:42Z msozeau $ i*)
 
10
 
 
11
(*i*)
 
12
open Util
 
13
open Names
 
14
open Rawterm
 
15
open Term
 
16
open Sign
 
17
open Evd
 
18
open Environ
 
19
open Reductionops
 
20
(*i*)
 
21
 
 
22
(*s This modules provides useful functions for unification modulo evars *)
 
23
 
 
24
(***********************************************************)
 
25
(* Metas *)
 
26
 
 
27
(* [new_meta] is a generator of unique meta variables *)
 
28
val new_meta : unit -> metavariable
 
29
val mk_new_meta : unit -> constr
 
30
 
 
31
(* [new_untyped_evar] is a generator of unique evar keys *)
 
32
val new_untyped_evar : unit -> existential_key
 
33
 
 
34
(***********************************************************)
 
35
(* Creating a fresh evar given their type and context *)
 
36
val new_evar :
 
37
  evar_defs -> env -> ?src:loc * hole_kind -> ?filter:bool list -> types -> evar_defs * constr
 
38
(* the same with side-effects *)
 
39
val e_new_evar :
 
40
  evar_defs ref -> env -> ?src:loc * hole_kind -> ?filter:bool list -> types -> constr
 
41
 
 
42
(* Create a fresh evar in a context different from its definition context:
 
43
   [new_evar_instance sign evd ty inst] creates a new evar of context
 
44
   [sign] and type [ty], [inst] is a mapping of the evar context to
 
45
   the context where the evar should occur. This means that the terms 
 
46
   of [inst] are typed in the occurrence context and their type (seen
 
47
   as a telescope) is [sign] *)
 
48
val new_evar_instance :
 
49
 named_context_val -> evar_defs -> types -> ?src:loc * hole_kind -> ?filter:bool list -> constr list -> evar_defs * constr
 
50
 
 
51
val make_pure_subst : evar_info -> constr array -> (identifier * constr) list
 
52
 
 
53
(***********************************************************)
 
54
(* Instantiate evars *)
 
55
 
 
56
(* [evar_define choose env ev c] try to instantiate [ev] with [c] (typed in [env]),
 
57
   possibly solving related unification problems, possibly leaving open
 
58
   some problems that cannot be solved in a unique way (except if choose is
 
59
   true); fails if the instance is not valid for the given [ev] *)
 
60
val evar_define : ?choose:bool -> env -> existential -> constr -> evar_defs -> evar_defs
 
61
 
 
62
(***********************************************************)
 
63
(* Evars/Metas switching... *)
 
64
 
 
65
(* [evars_to_metas] generates new metavariables for each non dependent
 
66
   existential and performs the replacement in the given constr; it also
 
67
   returns the evar_map extended with dependent evars *)
 
68
val evars_to_metas : evar_map -> open_constr -> (evar_map * constr)
 
69
 
 
70
val non_instantiated : evar_map -> (evar * evar_info) list
 
71
 
 
72
(***********************************************************)
 
73
(* Unification utils *)
 
74
 
 
75
val is_ground_term :  evar_defs -> constr -> bool
 
76
val is_ground_env  :  evar_defs -> env -> bool
 
77
val solve_refl : 
 
78
  (env ->  evar_defs -> conv_pb -> constr -> constr -> evar_defs * bool)
 
79
  -> env ->  evar_defs -> existential_key -> constr array -> constr array ->
 
80
    evar_defs
 
81
val solve_simple_eqn :
 
82
  (env ->  evar_defs -> conv_pb -> constr -> constr -> evar_defs * bool)
 
83
  -> ?choose:bool -> env ->  evar_defs -> conv_pb * existential * constr ->
 
84
    evar_defs * bool
 
85
 
 
86
(* [check_evars env initial_sigma extended_sigma c] fails if some
 
87
   new unresolved evar remains in [c] *)
 
88
val check_evars : env -> evar_map -> evar_defs -> constr -> unit
 
89
 
 
90
val define_evar_as_product : evar_defs -> existential -> evar_defs * types
 
91
val define_evar_as_lambda : evar_defs -> existential -> evar_defs * types
 
92
val define_evar_as_sort : evar_defs -> existential -> evar_defs * sorts
 
93
 
 
94
val is_unification_pattern_evar : env -> existential -> constr list -> 
 
95
  constr -> bool
 
96
val is_unification_pattern : env * int -> constr -> constr array ->
 
97
  constr -> bool
 
98
val solve_pattern_eqn : env -> constr list -> constr -> constr
 
99
 
 
100
val evars_of_term : constr -> Intset.t
 
101
val evars_of_named_context : named_context -> Intset.t
 
102
val evars_of_evar_info : evar_info -> Intset.t
 
103
 
 
104
(***********************************************************)
 
105
(* Value/Type constraints *)
 
106
 
 
107
val judge_of_new_Type : unit -> unsafe_judgment
 
108
 
 
109
type type_constraint_type = (int * int) option * constr
 
110
type type_constraint = type_constraint_type option
 
111
 
 
112
type val_constraint = constr option
 
113
 
 
114
val empty_tycon : type_constraint
 
115
val mk_tycon_type : constr -> type_constraint_type
 
116
val mk_abstr_tycon_type : int -> constr -> type_constraint_type
 
117
val mk_tycon : constr -> type_constraint
 
118
val mk_abstr_tycon : int -> constr -> type_constraint
 
119
val empty_valcon : val_constraint
 
120
val mk_valcon : constr -> val_constraint
 
121
 
 
122
val split_tycon :
 
123
  loc -> env ->  evar_defs -> type_constraint -> 
 
124
    evar_defs * (name * type_constraint * type_constraint)
 
125
 
 
126
val valcon_of_tycon : type_constraint -> val_constraint
 
127
 
 
128
val lift_abstr_tycon_type : int -> type_constraint_type -> type_constraint_type
 
129
 
 
130
val lift_tycon_type : int -> type_constraint_type -> type_constraint_type
 
131
val lift_tycon : int -> type_constraint -> type_constraint
 
132
 
 
133
(***********************************************************)
 
134
 
 
135
(* [whd_ise] raise [Uninstantiated_evar] if an evar remains uninstantiated; *)
 
136
(* *[whd_evar]* and *[nf_evar]* leave uninstantiated evar as is *)
 
137
 
 
138
val nf_evar :  evar_map -> constr -> constr
 
139
val j_nf_evar :  evar_map -> unsafe_judgment -> unsafe_judgment
 
140
val jl_nf_evar :
 
141
   evar_map -> unsafe_judgment list -> unsafe_judgment list
 
142
val jv_nf_evar :
 
143
   evar_map -> unsafe_judgment array -> unsafe_judgment array
 
144
val tj_nf_evar :
 
145
   evar_map -> unsafe_type_judgment -> unsafe_type_judgment
 
146
 
 
147
val nf_evar_info : evar_map -> evar_info -> evar_info
 
148
val nf_evars : evar_map -> evar_map
 
149
 
 
150
val nf_named_context_evar : evar_map -> named_context -> named_context
 
151
val nf_rel_context_evar : evar_map -> rel_context -> rel_context
 
152
val nf_env_evar : evar_map -> env -> env
 
153
 
 
154
(* Same for evar defs *)
 
155
val nf_isevar :  evar_defs -> constr -> constr
 
156
val j_nf_isevar :  evar_defs -> unsafe_judgment -> unsafe_judgment
 
157
val jl_nf_isevar :
 
158
   evar_defs -> unsafe_judgment list -> unsafe_judgment list
 
159
val jv_nf_isevar :
 
160
   evar_defs -> unsafe_judgment array -> unsafe_judgment array
 
161
val tj_nf_isevar :
 
162
   evar_defs -> unsafe_type_judgment -> unsafe_type_judgment
 
163
 
 
164
val nf_evar_defs : evar_defs -> evar_defs
 
165
 
 
166
(* Replacing all evars *)
 
167
exception Uninstantiated_evar of existential_key
 
168
val whd_ise :  evar_map -> constr -> constr
 
169
val whd_castappevar :  evar_map -> constr -> constr
 
170
 
 
171
(* Replace the vars and rels that are aliases to other vars and rels by *)
 
172
(* their representative that is most ancient in the context *)
 
173
val expand_vars_in_term : env -> constr -> constr 
 
174
 
 
175
(*********************************************************************)
 
176
(* debug pretty-printer: *)
 
177
 
 
178
val pr_tycon_type : env -> type_constraint_type -> Pp.std_ppcmds
 
179
val pr_tycon : env -> type_constraint -> Pp.std_ppcmds
 
180
 
 
181
 
 
182
(*********************************************************************)
 
183
(* Removing hyps in evars'context;                                   *)
 
184
(* raise OccurHypInSimpleClause if the removal breaks dependencies   *)
 
185
 
 
186
type clear_dependency_error =
 
187
| OccurHypInSimpleClause of identifier option
 
188
| EvarTypingBreak of existential
 
189
 
 
190
exception ClearDependencyError of identifier * clear_dependency_error
 
191
 
 
192
val clear_hyps_in_evi : evar_defs ref -> named_context_val -> types ->
 
193
  identifier list -> named_context_val * types