← Back to branch summary

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

« back to all changes in this revision

Viewing changes to pretyping/clenv.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/clenv.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: clenv.mli 10856 2008-04-27 16:15:34Z herbelin $ i*)
 
10
 
 
11
(*i*)
 
12
open Util
 
13
open Names
 
14
open Term
 
15
open Sign
 
16
open Environ
 
17
open Evd
 
18
open Evarutil
 
19
open Mod_subst
 
20
open Rawterm
 
21
open Unification
 
22
(*i*)
 
23
 
 
24
(***************************************************************)
 
25
(* The Type of Constructions clausale environments. *)
 
26
 
 
27
(* [env] is the typing context
 
28
 * [evd] is the mapping from metavar and evar numbers to their types
 
29
 *       and values.
 
30
 * [templval] is the template which we are trying to fill out.
 
31
 * [templtyp] is its type.
 
32
 *)
 
33
type clausenv = {
 
34
  env      : env;
 
35
  evd      : evar_defs;
 
36
  templval : constr freelisted;
 
37
  templtyp : constr freelisted }
 
38
 
 
39
(* Substitution is not applied on templenv (because [subst_clenv] is
 
40
   applied only on hints which typing env is overwritten by the
 
41
   goal env) *)
 
42
val subst_clenv : substitution -> clausenv -> clausenv
 
43
 
 
44
(* subject of clenv (instantiated) *)
 
45
val clenv_value     : clausenv -> constr
 
46
(* type of clenv (instantiated) *)
 
47
val clenv_type      : clausenv -> types
 
48
(* substitute resolved metas *)
 
49
val clenv_nf_meta   : clausenv -> constr -> constr
 
50
(* type of a meta in clenv context *)
 
51
val clenv_meta_type : clausenv -> metavariable -> types
 
52
 
 
53
val mk_clenv_from : evar_info sigma -> constr * types -> clausenv
 
54
val mk_clenv_from_n :
 
55
  evar_info sigma -> int option -> constr * types -> clausenv
 
56
val mk_clenv_type_of : evar_info sigma -> constr -> clausenv
 
57
val mk_clenv_from_env : env -> evar_map -> int option -> constr * types -> clausenv
 
58
 
 
59
(***************************************************************)
 
60
(* linking of clenvs *)
 
61
 
 
62
val connect_clenv : evar_info sigma -> clausenv -> clausenv
 
63
val clenv_fchain : 
 
64
  ?allow_K:bool -> ?flags:unify_flags -> metavariable -> clausenv -> clausenv -> clausenv
 
65
 
 
66
(***************************************************************)
 
67
(* Unification with clenvs *)
 
68
 
 
69
(* Unifies two terms in a clenv. The boolean is [allow_K] (see [Unification]) *)
 
70
val clenv_unify : 
 
71
  bool -> ?flags:unify_flags -> conv_pb -> constr -> constr -> clausenv -> clausenv
 
72
 
 
73
(* unifies the concl of the goal with the type of the clenv *)
 
74
val clenv_unique_resolver :
 
75
  bool -> ?flags:unify_flags -> clausenv -> evar_info sigma -> clausenv
 
76
 
 
77
(* same as above ([allow_K=false]) but replaces remaining metas
 
78
   with fresh evars if [evars_flag] is [true] *)
 
79
val evar_clenv_unique_resolver :
 
80
  bool -> ?flags:unify_flags -> clausenv -> evar_info sigma -> clausenv
 
81
 
 
82
val clenv_dependent : bool -> clausenv -> metavariable list
 
83
 
 
84
val clenv_pose_metas_as_evars : clausenv -> metavariable list -> clausenv
 
85
 
 
86
(***************************************************************)
 
87
(* Bindings *)
 
88
 
 
89
type arg_bindings = open_constr explicit_bindings
 
90
 
 
91
(* bindings where the key is the position in the template of the
 
92
   clenv (dependent or not). Positions can be negative meaning to
 
93
   start from the rightmost argument of the template. *)
 
94
val clenv_independent : clausenv -> metavariable list
 
95
val clenv_missing : clausenv -> metavariable list
 
96
 
 
97
val clenv_constrain_last_binding : constr -> clausenv -> clausenv
 
98
 
 
99
(* defines metas corresponding to the name of the bindings *)
 
100
val clenv_match_args : arg_bindings -> clausenv -> clausenv
 
101
 
 
102
val clenv_unify_meta_types : ?flags:unify_flags -> clausenv -> clausenv
 
103
 
 
104
(* start with a clenv to refine with a given term with bindings *)
 
105
 
 
106
(* the arity of the lemma is fixed *)
 
107
(* the optional int tells how many prods of the lemma have to be used *)
 
108
(* use all of them if None *)
 
109
val make_clenv_binding_apply :
 
110
  evar_info sigma -> int option -> constr * constr -> open_constr bindings ->
 
111
   clausenv
 
112
val make_clenv_binding :
 
113
  evar_info sigma -> constr * constr -> open_constr bindings -> clausenv
 
114
 
 
115
(* [clenv_environments sigma n t] returns [sigma',lmeta,ccl] where
 
116
   [lmetas] is a list of metas to be applied to a proof of [t] so that
 
117
   it produces the unification pattern [ccl]; [sigma'] is [sigma]
 
118
   extended with [lmetas]; if [n] is defined, it limits the size of
 
119
   the list even if [ccl] is still a product; otherwise, it stops when
 
120
   [ccl] is not a product; example: if [t] is [forall x y, x=y -> y=x]
 
121
   and [n] is [None], then [lmetas] is [Meta n1;Meta n2;Meta n3] and
 
122
   [ccl] is [Meta n1=Meta n2]; if [n] is [Some 1], [lmetas] is [Meta n1]
 
123
   and [ccl] is [forall y, Meta n1=y -> y=Meta n1] *)
 
124
val clenv_environments :
 
125
 evar_defs -> int option -> types -> evar_defs * constr list * types
 
126
 
 
127
(* [clenv_environments_evars env sigma n t] does the same but returns
 
128
   a list of Evar's defined in [env] and extends [sigma] accordingly *)
 
129
val clenv_environments_evars :
 
130
 env -> evar_defs -> int option -> types -> evar_defs * constr list * types
 
131
 
 
132
(* [clenv_conv_leq env sigma t c n] looks for c1...cn s.t. [t <= c c1...cn] *)
 
133
val clenv_conv_leq :
 
134
 env -> evar_map -> types -> constr -> int -> constr list
 
135
 
 
136
(* if the clause is a product, add an extra meta for this product *)
 
137
exception NotExtensibleClause
 
138
val clenv_push_prod : clausenv -> clausenv
 
139
 
 
140
(***************************************************************)
 
141
(* Pretty-print *)
 
142
val pr_clenv : clausenv -> Pp.std_ppcmds
 
143