blob: 5f67a8a92732f73088f4327db1e18f99f0df0b5b (
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
|
(* $Id$ *)
(*i*)
open Names
open Sign
open Type_errors
(*i*)
(* Untyped intermediate terms, after ASTs and before constr. *)
type loc = int * int
(* 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_path * identifier list) * cases_pattern list * name
type binder_kind = BProd | BLambda
type fix_kind = RFix of int array * int | RCofix of int
type rawsort = RProp of Term.contents | RType
type 'ctxt reference =
| RConst of section_path * 'ctxt
| RInd of inductive_path * 'ctxt
| RConstruct of constructor_path * 'ctxt
| RAbst of section_path
| RVar of identifier
| REVar of int * 'ctxt
| RMeta of int
type rawconstr =
| RRef of loc * Term.constr array reference
| RApp of loc * rawconstr * rawconstr list
| RBinder of loc * binder_kind * name * rawconstr * rawconstr
| RCases of loc * Term.case_style * rawconstr option * rawconstr list *
(identifier list * cases_pattern list * rawconstr) list
| ROldCase of loc * bool * rawconstr option * rawconstr *
rawconstr array
| RRec of loc * fix_kind * identifier array *
rawconstr array * rawconstr array
| RSort of loc * rawsort
| RHole of loc option
| RCast of loc * rawconstr * rawconstr
(*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 dummy_loc : loc
val loc_of_rawconstr : rawconstr -> loc
type constr_pattern =
| PRef of Term.constr array reference
| PRel of int
| PApp of constr_pattern * constr_pattern array
| PSoApp of int * int list
| PBinder of binder_kind * name * constr_pattern * constr_pattern
| PSort of rawsort
| PMeta of int
val occur_meta_pattern : constr_pattern -> bool
type constr_label =
| ConstNode of section_path
| IndNode of inductive_path
| CstrNode of constructor_path
| VarNode of identifier
(* [head_pattern_bound t] extracts the head variable/constant of the
type [t] or raises [BoundPattern] (even if a sort); it raises an anomaly
if [t] is an abstraction *)
exception BoundPattern
val head_pattern_bound : constr_pattern -> constr_label
(* [head_of_constr_reference c] assumes [r] denotes a reference and
returns its label; raises an anomaly otherwise *)
val head_of_constr_reference : Term.constr -> constr_label
|
