blob: 72845f8967cc24045c8a5d2384ebf4b4514030c3 (
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
128
129
130
131
132
133
|
(***********************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
(* \VV/ *************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(***********************************************************************)
(* $Id$ *)
(*i*)
open Pp
open Util
open Names
open Libnames
open Rawterm
open Term
(*i*)
(*s This is the subtype of rawconstr allowed in syntactic extensions *)
(* No location since intended to be substituted at any place of a text *)
(* Complex expressions such as fixpoints, cofixpoints and pattern-matching *)
(* are excluded; non global expressions such as existential variables also *)
type aconstr =
| ARef of global_reference
| AVar of identifier
| AApp of aconstr * aconstr list
| ALambda of name * aconstr * aconstr
| AProd of name * aconstr * aconstr
| ALetIn of name * aconstr * aconstr
| AOldCase of case_style * aconstr option * aconstr * aconstr array
| ASort of rawsort
| AHole of hole_kind
| AMeta of int
| ACast of aconstr * aconstr
val map_aconstr_with_binders_loc : loc ->
(identifier -> 'a -> identifier * 'a) ->
('a -> aconstr -> rawconstr) -> 'a -> aconstr -> rawconstr
val subst_aconstr : Names.substitution -> aconstr -> aconstr
val aconstr_of_rawconstr : rawconstr -> aconstr
(*s Concrete syntax for terms *)
type scope_name = string
type notation = string
type explicitation = int
type cases_pattern_expr =
| CPatAlias of loc * cases_pattern_expr * identifier
| CPatCstr of loc * reference * cases_pattern_expr list
| CPatAtom of loc * reference option
| CPatNumeral of loc * Bignat.bigint
| CPatDelimiters of loc * scope_name * cases_pattern_expr
type constr_expr =
| CRef of reference
| CFix of loc * identifier located * fixpoint_expr list
| CCoFix of loc * identifier located * cofixpoint_expr list
| CArrow of loc * constr_expr * constr_expr
| CProdN of loc * (name located list * constr_expr) list * constr_expr
| CLambdaN of loc * (name located list * constr_expr) list * constr_expr
| CLetIn of loc * name located * constr_expr * constr_expr
| CAppExpl of loc * reference * constr_expr list
| CApp of loc * constr_expr * (constr_expr * explicitation option) list
| CCases of loc * constr_expr option * constr_expr list *
(loc * cases_pattern_expr list * constr_expr) list
| COrderedCase of loc * case_style * constr_expr option * constr_expr
* constr_expr list
| CHole of loc
| CMeta of loc * int
| CSort of loc * rawsort
| CCast of loc * constr_expr * constr_expr
| CNotation of loc * notation * (identifier * constr_expr) list
| CGrammar of loc * aconstr * (identifier * constr_expr) list
| CNumeral of loc * Bignat.bigint
| CDelimiters of loc * scope_name * constr_expr
| CDynamic of loc * Dyn.t
and fixpoint_binder = name located list * constr_expr
and fixpoint_expr = identifier * fixpoint_binder list * constr_expr * constr_expr
and cofixpoint_expr = identifier * constr_expr * constr_expr
val constr_loc : constr_expr -> loc
val cases_pattern_loc : cases_pattern_expr -> loc
val replace_vars_constr_expr :
(identifier * identifier) list -> constr_expr -> constr_expr
val occur_var_constr_expr : identifier -> constr_expr -> bool
val mkIdentC : identifier -> constr_expr
val mkRefC : reference -> constr_expr
val mkAppC : constr_expr * constr_expr list -> constr_expr
val mkCastC : constr_expr * constr_expr -> constr_expr
val mkLambdaC : name located list * constr_expr * constr_expr -> constr_expr
val mkLetInC : name located * constr_expr * constr_expr -> constr_expr
val mkProdC : name located list * constr_expr * constr_expr -> constr_expr
(* Used in correctness and interface; absence of var capture not guaranteed *)
(* in pattern-matching clauses and in binders of the form [x,y:T(x)] *)
val map_constr_expr_with_binders :
('a -> constr_expr -> constr_expr) ->
(identifier -> 'a -> 'a) -> 'a -> constr_expr -> constr_expr
(* For binders parsing *)
type local_binder =
| LocalRawDef of name located * constr_expr
| LocalRawAssum of name located list * constr_expr
(* Concrete syntax for modules and modules types *)
type with_declaration_ast =
| CWith_Module of identifier * qualid located
| CWith_Definition of identifier * constr_expr
type module_type_ast =
| CMTEident of qualid located
| CMTEwith of module_type_ast * with_declaration_ast
type module_ast =
| CMEident of qualid located
| CMEapply of module_ast * module_ast
|
