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
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
open Loc
open Pp
open Names
open Libnames
open Term
open Misctypes
open Decl_kinds
(** {6 Concrete syntax for terms } *)
(** [constr_expr] is the abstract syntax tree produced by the parser *)
type notation = string
type explicitation =
| ExplByPos of int * identifier option
| ExplByName of identifier
type binder_kind =
| Default of binding_kind
| Generalized of binding_kind * binding_kind * bool
(** Inner binding, outer bindings, typeclass-specific flag
for implicit generalization of superclasses *)
type abstraction_kind = AbsLambda | AbsPi
type proj_flag = int option (** [Some n] = proj of the n-th visible argument *)
type prim_token = Numeral of Bigint.bigint | String of string
type raw_cases_pattern_expr =
| RCPatAlias of Loc.t * raw_cases_pattern_expr * identifier
| RCPatCstr of Loc.t * Globnames.global_reference
* raw_cases_pattern_expr list * raw_cases_pattern_expr list
(** [CPatCstr (_, Inl c, l1, l2)] represents (@c l1) l2 *)
| RCPatAtom of Loc.t * identifier option
| RCPatOr of Loc.t * raw_cases_pattern_expr list
type cases_pattern_expr =
| CPatAlias of Loc.t * cases_pattern_expr * identifier
| CPatCstr of Loc.t * reference
* cases_pattern_expr list * cases_pattern_expr list
(** [CPatCstr (_, Inl c, l1, l2)] represents (@c l1) l2 *)
| CPatAtom of Loc.t * reference option
| CPatOr of Loc.t * cases_pattern_expr list
| CPatNotation of Loc.t * notation * cases_pattern_notation_substitution
* cases_pattern_expr list (** CPatNotation (_, n, l1 ,l2) represents
(notation n applied with substitution l1)
applied to arguments l2 *)
| CPatPrim of Loc.t * prim_token
| CPatRecord of Loc.t * (reference * cases_pattern_expr) list
| CPatDelimiters of Loc.t * string * cases_pattern_expr
and cases_pattern_notation_substitution =
cases_pattern_expr list * (** for constr subterms *)
cases_pattern_expr list list (** for recursive notations *)
type constr_expr =
| CRef of reference
| CFix of Loc.t * identifier located * fix_expr list
| CCoFix of Loc.t * identifier located * cofix_expr list
| CProdN of Loc.t * (name located list * binder_kind * constr_expr) list * constr_expr
| CLambdaN of Loc.t * (name located list * binder_kind * constr_expr) list * constr_expr
| CLetIn of Loc.t * name located * constr_expr * constr_expr
| CAppExpl of Loc.t * (proj_flag * reference) * constr_expr list
| CApp of Loc.t * (proj_flag * constr_expr) *
(constr_expr * explicitation located option) list
| CRecord of Loc.t * constr_expr option * (reference * constr_expr) list
| CCases of Loc.t * case_style * constr_expr option *
(constr_expr * (name located option * cases_pattern_expr option)) list *
(Loc.t * cases_pattern_expr list located list * constr_expr) list
| CLetTuple of Loc.t * name located list * (name located option * constr_expr option) *
constr_expr * constr_expr
| CIf of Loc.t * constr_expr * (name located option * constr_expr option)
* constr_expr * constr_expr
| CHole of Loc.t * Evar_kinds.t option
| CPatVar of Loc.t * (bool * patvar)
| CEvar of Loc.t * existential_key * constr_expr list option
| CSort of Loc.t * glob_sort
| CCast of Loc.t * constr_expr * constr_expr cast_type
| CNotation of Loc.t * notation * constr_notation_substitution
| CGeneralization of Loc.t * binding_kind * abstraction_kind option * constr_expr
| CPrim of Loc.t * prim_token
| CDelimiters of Loc.t * string * constr_expr
and fix_expr =
identifier located * (identifier located option * recursion_order_expr) *
local_binder list * constr_expr * constr_expr
and cofix_expr =
identifier located * local_binder list * constr_expr * constr_expr
and recursion_order_expr =
| CStructRec
| CWfRec of constr_expr
| CMeasureRec of constr_expr * constr_expr option (** measure, relation *)
(** Anonymous defs allowed ?? *)
and local_binder =
| LocalRawDef of name located * constr_expr
| LocalRawAssum of name located list * binder_kind * constr_expr
and constr_notation_substitution =
constr_expr list * (** for constr subterms *)
constr_expr list list * (** for recursive notations *)
local_binder list list (** for binders subexpressions *)
type typeclass_constraint = name located * binding_kind * constr_expr
and typeclass_context = typeclass_constraint list
type constr_pattern_expr = constr_expr
(** Concrete syntax for modules and module types *)
type with_declaration_ast =
| CWith_Module of identifier list located * qualid located
| CWith_Definition of identifier list located * constr_expr
type module_ast =
| CMident of qualid located
| CMapply of Loc.t * module_ast * module_ast
| CMwith of Loc.t * module_ast * with_declaration_ast
|
