blob: 014739fcb70669e286a8d746a7958580967bd0a4 (
plain)
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
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(*i $Id$ i*)
(*i*)
open Util
open Names
open Sign
open Term
open Libnames
open Nametab
(*i*)
(* Untyped intermediate terms, after ASTs and before constr. *)
(* locs here refers to the ident's location, not whole pat *)
(* the last argument of PatCstr is a possible alias ident for the pattern *)
type cases_pattern =
| PatVar of loc * name
| PatCstr of loc * constructor * cases_pattern list * name
val pattern_loc : cases_pattern -> loc
type patvar = identifier
type rawsort = RProp of Term.contents | RType of Univ.universe option
type fix_kind = RFix of (int array * int) | RCoFix of int
type binder_kind = BProd | BLambda | BLetIn
type quantified_hypothesis = AnonHyp of int | NamedHyp of identifier
type 'a explicit_bindings = (loc * quantified_hypothesis * 'a) list
type 'a bindings =
| ImplicitBindings of 'a list
| ExplicitBindings of 'a explicit_bindings
| NoBindings
type 'a with_bindings = 'a * 'a bindings
type rawconstr =
| RRef of (loc * global_reference)
| RVar of (loc * identifier)
| REvar of loc * existential_key * rawconstr list option
| RPatVar of loc * (bool * patvar) (* Used for patterns only *)
| RApp of loc * rawconstr * rawconstr list
| RLambda of loc * name * rawconstr * rawconstr
| RProd of loc * name * rawconstr * rawconstr
| RLetIn of loc * name * rawconstr * rawconstr
| RCases of loc * rawconstr option *
(rawconstr * (name * (loc * inductive * name list) option)) list *
(loc * identifier list * cases_pattern list * rawconstr) list
| RLetTuple of loc * name list * (name * rawconstr option) *
rawconstr * rawconstr
| RIf of loc * rawconstr * (name * rawconstr option) * rawconstr * rawconstr
| RRec of loc * fix_kind * identifier array * rawdecl list array *
rawconstr array * rawconstr array
| RSort of loc * rawsort
| RHole of (loc * Evd.hole_kind)
| RCast of loc * rawconstr * cast_kind * rawconstr
| RDynamic of loc * Dyn.t
and rawdecl = name * rawconstr option * rawconstr
val cases_predicate_names :
(rawconstr * (name * (loc * inductive * name list) option)) list -> name list
(*i - if PRec (_, names, arities, bodies) is in env then arities are
typed in env too and bodies are typed in env enriched by the
arities incrementally lifted
[On pourrait plutot mettre les arit�s aves le type qu'elles auront
dans le contexte servant � typer les body ???]
- boolean in POldCase means it is recursive
- option in PHole tell if the "?" was apparent or has been implicitely added
i*)
val map_rawconstr : (rawconstr -> rawconstr) -> rawconstr -> rawconstr
(*i
val map_rawconstr_with_binders_loc : loc ->
(identifier -> 'a -> identifier * 'a) ->
('a -> rawconstr -> rawconstr) -> 'a -> rawconstr -> rawconstr
i*)
val occur_rawconstr : identifier -> rawconstr -> bool
val loc_of_rawconstr : rawconstr -> loc
type 'a raw_red_flag = {
rBeta : bool;
rIota : bool;
rZeta : bool;
rDelta : bool; (* true = delta all but rConst; false = delta only on rConst*)
rConst : 'a list
}
val all_flags : 'a raw_red_flag
type 'a occurrences = int list * 'a
type ('a,'b) red_expr_gen =
| Red of bool
| Hnf
| Simpl of 'a occurrences option
| Cbv of 'b raw_red_flag
| Lazy of 'b raw_red_flag
| Unfold of 'b occurrences list
| Fold of 'a list
| Pattern of 'a occurrences list
| ExtraRedExpr of string
| CbvVm
type ('a,'b) may_eval =
| ConstrTerm of 'a
| ConstrEval of ('a, 'b) red_expr_gen * 'a
| ConstrContext of (loc * identifier) * 'a
| ConstrTypeOf of 'a
|
