blob: 7bc0b607aa106bfb5a47505cb978d2c70eaa2a28 (
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
|
(************************************************************************)
(* 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: ast.mli,v 1.17.2.1 2004/07/16 19:30:37 herbelin Exp $ i*)
(*i*)
open Pp
open Util
open Names
open Libnames
open Coqast
open Topconstr
open Genarg
(*i*)
(* Abstract syntax trees. *)
val loc : Coqast.t -> loc
(* ast constructors with dummy location *)
val ope : string * Coqast.t list -> Coqast.t
val slam : identifier option * Coqast.t -> Coqast.t
val nvar : identifier -> Coqast.t
val ide : string -> Coqast.t
val num : int -> Coqast.t
val string : string -> Coqast.t
val path : kernel_name -> Coqast.t
val dynamic : Dyn.t -> Coqast.t
val set_loc : loc -> Coqast.t -> Coqast.t
val path_section : loc -> kernel_name -> Coqast.t
val section_path : kernel_name -> kernel_name
(* ast destructors *)
val num_of_ast : Coqast.t -> int
val id_of_ast : Coqast.t -> string
val nvar_of_ast : Coqast.t -> identifier
val meta_of_ast : Coqast.t -> string
(* patterns of ast *)
type astpat =
| Pquote of t
| Pmeta of string * tok_kind
| Pnode of string * patlist
| Pslam of identifier option * astpat
| Pmeta_slam of string * astpat
and patlist =
| Pcons of astpat * patlist
| Plmeta of string
| Pnil
and tok_kind = Tnum | Tid | Tstr | Tpath | Tvar | Tany | Tlist
type pat =
| AstListPat of patlist
| PureAstPat of astpat
(* semantic actions of grammar rules *)
type act =
| Act of constr_expr
| ActCase of act * (pat * act) list
| ActCaseList of act * (pat * act) list
(* values associated to variables *)
type typed_ast =
| AstListNode of Coqast.t list
| PureAstNode of Coqast.t
type ast_action_type = ETast | ETastl
type dynamic_grammar =
| ConstrNode of constr_expr
| CasesPatternNode of cases_pattern_expr
type grammar_action =
| SimpleAction of loc * dynamic_grammar
| CaseAction of
loc * grammar_action * ast_action_type * (t list * grammar_action) list
type env = (string * typed_ast) list
val coerce_to_id : constr_expr -> identifier located
val coerce_global_to_id : reference -> identifier
val coerce_reference_to_id : reference -> identifier
exception No_match of string
val isMeta : string -> bool
val print_ast : Coqast.t -> std_ppcmds
val print_astl : Coqast.t list -> std_ppcmds
val print_astpat : astpat -> std_ppcmds
val print_astlpat : patlist -> std_ppcmds
(* Meta-syntax operations: matching and substitution *)
type entry_env = (string * ast_action_type) list
val grammar_type_error : loc * string -> 'a
(* Converting and checking free meta-variables *)
(* For old ast printer *)
val pat_sub : loc -> env -> astpat -> Coqast.t
val val_of_ast : entry_env -> Coqast.t -> astpat
val alpha_eq : Coqast.t * Coqast.t -> bool
val alpha_eq_val : typed_ast * typed_ast -> bool
val occur_var_ast : identifier -> Coqast.t -> bool
val find_all_matches : ('a -> astpat) -> env -> t -> 'a list -> ('a * env) list
val first_matchl : ('a -> patlist) -> env -> Coqast.t list -> 'a list ->
('a * env) option
val to_pat : entry_env -> Coqast.t -> (astpat * entry_env)
(* Object substitution in modules *)
val subst_astpat : Names.substitution -> astpat -> astpat
|
