2 * Copyright 2012, INRIA
3 * Julia Lawall, Gilles Muller
4 * Copyright 2010-2011, INRIA, University of Copenhagen
5 * Julia Lawall, Rene Rydhof Hansen, Gilles Muller, Nicolas Palix
6 * Copyright 2005-2009, Ecole des Mines de Nantes, University of Copenhagen
7 * Yoann Padioleau, Julia Lawall, Rene Rydhof Hansen, Henrik Stuart, Gilles Muller, Nicolas Palix
8 * This file is part of Coccinelle.
10 * Coccinelle is free software: you can redistribute it and/or modify
11 * it under the terms of the GNU General Public License as published by
12 * the Free Software Foundation, according to version 2 of the License.
14 * Coccinelle is distributed in the hope that it will be useful,
15 * but WITHOUT ANY WARRANTY; without even the implied warranty of
16 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
17 * GNU General Public License for more details.
19 * You should have received a copy of the GNU General Public License
20 * along with Coccinelle. If not, see <http://www.gnu.org/licenses/>.
22 * The authors reserve the right to distribute this or future versions of
23 * Coccinelle under other licenses.
27 (* --------------------------------------------------------------------- *)
30 type added_string
= Noindent
of string | Indent
of string | Space
of string
32 type info
= { line
: int; column
: int;
33 strbef
: (added_string
* int (* line *) * int (* col *)) list
;
34 straft
: (added_string
* int (* line *) * int (* col *)) list
}
36 type meta_name
= string * string
40 free_vars
: meta_name list
; (*free vars*)
41 minus_free_vars
: meta_name list
; (*minus free vars*)
42 fresh_vars
: (meta_name
* seed
) list
; (*fresh vars*)
43 inherited
: meta_name list
; (*inherited vars*)
44 saved_witness
: meta_name list
; (*witness vars*)
45 bef_aft
: dots_bef_aft
;
46 pos_info
: meta_name mcode
option; (* pos info, try not to duplicate *)
47 true_if_test_exp
: bool;(* true if "test_exp from iso", only for exprs *)
48 (* the following is only for declarations *)
49 safe_for_multi_decls
: bool;
50 (* isos relevant to the term; ultimately only used for rule_elems *)
51 iso_info
: (string*anything
) list
}
54 BEFORE
of 'a list list
* count
55 | AFTER
of 'a list list
* count
56 | BEFOREAFTER
of 'a list list
* 'a list list
* count
59 and 'a replacement
= REPLACEMENT
of 'a list list
* count
| NOREPLACEMENT
61 and 'a mcode
= 'a
* info
* mcodekind
* meta_pos list
(* pos variables *)
62 (* pos is an offset indicating where in the C code the mcodekind has an
64 and adjacency
= ALLMINUS
| ADJ
of int
66 MINUS
of pos
* int list
* adjacency
* anything replacement
67 | CONTEXT
of pos
* anything befaft
69 and count
= ONE
(* + *) | MANY
(* ++ *)
71 Real
of int (* charpos *) | Virt
of int * int (* charpos + offset *)
72 and pos
= NoPos
| DontCarePos
| FixPos
of (fixpos
* fixpos
)
76 | AddingBetweenDots
of statement
* int (*index of let var*)
77 | DroppingBetweenDots
of statement
* int (*index of let var*)
79 and inherited
= Type_cocci.inherited
80 and keep_binding
= Type_cocci.keep_binding
81 and multi
= bool (*true if a nest is one or more, false if it is zero or more*)
84 meta_name list
(*free vars*) * (meta_name
* seed
) list
(*fresh*) *
85 meta_name list
(*inherited vars*) * mcodekind
87 (* --------------------------------------------------------------------- *)
90 and arity
= UNIQUE
| OPT
| MULTI
| NONE
93 MetaMetaDecl
of arity
* meta_name
(* name *)
94 | MetaIdDecl
of arity
* meta_name
(* name *)
95 | MetaFreshIdDecl
of meta_name
(* name *) * seed
(* seed *)
96 | MetaTypeDecl
of arity
* meta_name
(* name *)
97 | MetaInitDecl
of arity
* meta_name
(* name *)
98 | MetaInitListDecl
of arity
* meta_name
(* name *) * list_len
(*len*)
99 | MetaListlenDecl
of meta_name
(* name *)
100 | MetaParamDecl
of arity
* meta_name
(* name *)
101 | MetaParamListDecl
of arity
* meta_name
(*name*) * list_len
(*len*)
103 arity
* meta_name
(* name *) * Type_cocci.typeC list
option
104 | MetaErrDecl
of arity
* meta_name
(* name *)
106 arity
* meta_name
(* name *) * Type_cocci.typeC list
option
108 arity
* meta_name
(* name *) * Type_cocci.typeC list
option
109 | MetaLocalIdExpDecl
of
110 arity
* meta_name
(* name *) * Type_cocci.typeC list
option
111 | MetaExpListDecl
of arity
* meta_name
(*name*) * list_len
(*len*)
112 | MetaDeclDecl
of arity
* meta_name
(* name *)
113 | MetaFieldDecl
of arity
* meta_name
(* name *)
114 | MetaFieldListDecl
of arity
* meta_name
(* name *) * list_len
(*len*)
115 | MetaStmDecl
of arity
* meta_name
(* name *)
116 | MetaStmListDecl
of arity
* meta_name
(* name *)
117 | MetaFuncDecl
of arity
* meta_name
(* name *)
118 | MetaLocalFuncDecl
of arity
* meta_name
(* name *)
119 | MetaPosDecl
of arity
* meta_name
(* name *)
120 | MetaDeclarerDecl
of arity
* meta_name
(* name *)
121 | MetaIteratorDecl
of arity
* meta_name
(* name *)
123 and list_len
= AnyLen
| MetaLen
of meta_name
| CstLen
of int
125 and seed
= NoVal
| StringSeed
of string | ListSeed
of seed_elem list
126 and seed_elem
= SeedString
of string | SeedId
of meta_name
128 (* --------------------------------------------------------------------- *)
129 (* --------------------------------------------------------------------- *)
137 and 'a dots
= 'a base_dots wrap
139 (* --------------------------------------------------------------------- *)
144 | MetaId
of meta_name mcode
* idconstraint
* keep_binding
* inherited
145 | MetaFunc
of meta_name mcode
* idconstraint
* keep_binding
* inherited
146 | MetaLocalFunc
of meta_name mcode
* idconstraint
* keep_binding
* inherited
148 | DisjId
of ident list
150 | UniqueIdent
of ident
152 and ident
= base_ident wrap
154 (* --------------------------------------------------------------------- *)
157 and base_expression
=
159 | Constant
of constant mcode
160 | FunCall
of expression
* string mcode
(* ( *) *
161 expression dots
* string mcode
(* ) *)
162 | Assignment
of expression
* assignOp mcode
* expression
* bool
163 | Sequence
of expression
* string mcode
(* , *) * expression
164 | CondExpr
of expression
* string mcode
(* ? *) * expression
option *
165 string mcode
(* : *) * expression
166 | Postfix
of expression
* fixOp mcode
167 | Infix
of expression
* fixOp mcode
168 | Unary
of expression
* unaryOp mcode
169 | Binary
of expression
* binaryOp mcode
* expression
170 | Nested
of expression
* binaryOp mcode
* expression
171 | ArrayAccess
of expression
* string mcode
(* [ *) * expression
*
173 | RecordAccess
of expression
* string mcode
(* . *) * ident
174 | RecordPtAccess
of expression
* string mcode
(* -> *) * ident
175 | Cast
of string mcode
(* ( *) * fullType
* string mcode
(* ) *) *
178 | SizeOfExpr
of string mcode
(* sizeof *) * expression
179 | SizeOfType
of string mcode
(* sizeof *) * string mcode
(* ( *) *
180 fullType
* string mcode
(* ) *)
181 | TypeExp
of fullType
183 | Paren
of string mcode
(* ( *) * expression
*
186 | Constructor
of string mcode
(* ( *) * fullType
* string mcode
(* ) *) *
188 | MetaErr
of meta_name mcode
* constraints
* keep_binding
*
190 | MetaExpr
of meta_name mcode
* constraints
* keep_binding
*
191 Type_cocci.typeC list
option * form
* inherited
192 | MetaExprList
of meta_name mcode
* listlen
*
193 keep_binding
* inherited
(* only in arg lists *)
194 | AsExpr
of expression
* expression
(* as expr, always metavar *)
196 | EComma
of string mcode
(* only in arg lists *)
198 | DisjExpr
of expression list
199 | NestExpr
of string mcode
(* <.../<+... *) *
201 string mcode
(* ...>/...+> *) *
202 expression
option * multi
204 (* can appear in arg lists, and also inside Nest, as in:
205 if(< ... X ... Y ...>)
206 In the following, the expression option is the WHEN *)
207 | Edots
of string mcode
(* ... *) * expression
option
208 | Ecircles
of string mcode
(* ooo *) * expression
option
209 | Estars
of string mcode
(* *** *) * expression
option
211 | OptExp
of expression
212 | UniqueExp
of expression
216 | NotIdCstrt
of reconstraint
217 | NotExpCstrt
of expression list
218 | SubExpCstrt
of meta_name list
220 (* Constraints on Meta-* Identifiers, Functions *)
223 | IdNegIdSet
of string list
* meta_name list
224 | IdRegExpConstraint
of reconstraint
227 | IdRegExp
of string * Regexp.regexp
228 | IdNotRegExp
of string * Regexp.regexp
230 and form
= ANY
| ID
| LocalID
| CONST
(* form for MetaExp *)
232 and expression
= base_expression wrap
235 MetaListLen
of meta_name mcode
* keep_binding
* inherited
239 and unaryOp
= GetRef
| GetRefLabel
| DeRef
| UnPlus
| UnMinus
| Tilde
| Not
240 and assignOp
= SimpleAssign
| OpAssign
of arithOp
241 and fixOp
= Dec
| Inc
243 and binaryOp
= Arith
of arithOp
| Logical
of logicalOp
245 Plus
| Minus
| Mul
| Div
| Mod
| DecLeft
| DecRight
| And
| Or
| Xor
246 and logicalOp
= Inf
| Sup
| InfEq
| SupEq
| Eq
| NotEq
| AndLog
| OrLog
254 (* --------------------------------------------------------------------- *)
258 Type
of bool (* true if all minus *) *
259 const_vol mcode
option * typeC
260 | AsType
of fullType
* fullType
(* as type, always metavar *)
261 | DisjType
of fullType list
(* only after iso *)
262 | OptType
of fullType
263 | UniqueType
of fullType
266 BaseType
of baseType
* string mcode list
(* Yoann style *)
267 | SignedT
of sign mcode
* typeC
option
268 | Pointer
of fullType
* string mcode
(* * *)
269 | FunctionPointer
of fullType
*
270 string mcode
(* ( *)*string mcode
(* * *)*string mcode
(* ) *)*
271 string mcode
(* ( *)*parameter_list
*string mcode
(* ) *)
272 | FunctionType
of bool (* true if all minus for dropping return type *) *
274 string mcode
(* ( *) * parameter_list
*
276 | Array
of fullType
* string mcode
(* [ *) *
277 expression
option * string mcode
(* ] *)
278 | EnumName
of string mcode
(*enum*) * ident
option (* name *)
279 | EnumDef
of fullType
(* either EnumName or metavar *) *
280 string mcode
(* { *) * expression dots
* string mcode
(* } *)
281 | StructUnionName
of structUnion mcode
* ident
option (* name *)
282 | StructUnionDef
of fullType
(* either StructUnionName or metavar *) *
283 string mcode
(* { *) * declaration dots
* string mcode
(* } *)
284 | TypeName
of string mcode
286 | MetaType
of meta_name mcode
* keep_binding
* inherited
288 and fullType
= base_fullType wrap
289 and typeC
= base_typeC wrap
291 and baseType
= VoidType
| CharType
| ShortType
| ShortIntType
| IntType
292 | DoubleType
| LongDoubleType
| FloatType
293 | LongType
| LongIntType
| LongLongType
| LongLongIntType
294 | SizeType
| SSizeType
| PtrDiffType
296 and structUnion
= Struct
| Union
298 and sign
= Signed
| Unsigned
300 and const_vol
= Const
| Volatile
302 (* --------------------------------------------------------------------- *)
303 (* Variable declaration *)
304 (* Even if the Cocci program specifies a list of declarations, they are
305 split out into multiple declarations of a single variable each. *)
307 and base_declaration
=
308 Init
of storage mcode
option * fullType
* ident
* string mcode
(*=*) *
309 initialiser
* string mcode
(*;*)
310 | UnInit
of storage mcode
option * fullType
* ident
* string mcode
(* ; *)
311 | TyDecl
of fullType
* string mcode
(* ; *)
312 | MacroDecl
of ident
(* name *) * string mcode
(* ( *) *
313 expression dots
* string mcode
(* ) *) * string mcode
(* ; *)
314 | MacroDeclInit
of ident
(* name *) * string mcode
(* ( *) *
315 expression dots
* string mcode
(* ) *) * string mcode
(*=*) *
316 initialiser
* string mcode
(* ; *)
317 | Typedef
of string mcode
(*typedef*) * fullType
* typeC
* string mcode
(*;*)
318 | DisjDecl
of declaration list
319 | Ddots
of string mcode
(* ... *) * declaration
option (* whencode *)
321 | MetaDecl
of meta_name mcode
* keep_binding
* inherited
322 | MetaField
of meta_name mcode
* keep_binding
* inherited
323 | MetaFieldList
of meta_name mcode
* listlen
* keep_binding
* inherited
324 | AsDecl
of declaration
* declaration
326 | OptDecl
of declaration
327 | UniqueDecl
of declaration
329 and declaration
= base_declaration wrap
331 (* --------------------------------------------------------------------- *)
334 and base_initialiser
=
335 MetaInit
of meta_name mcode
* keep_binding
* inherited
336 | MetaInitList
of meta_name mcode
* listlen
* keep_binding
* inherited
337 | AsInit
of initialiser
* initialiser
(* as init, always metavar *)
338 | InitExpr
of expression
339 | ArInitList
of string mcode
(*{*) * initialiser dots
* string mcode
(*}*)
340 | StrInitList
of bool (* true if all are - *) *
341 string mcode
(*{*) * initialiser list
* string mcode
(*}*) *
342 initialiser list
(* whencode: elements that shouldn't appear in init *)
344 designator list
(* name *) * string mcode
(*=*) *
345 initialiser
(* gccext: *)
346 | InitGccName
of ident
(* name *) * string mcode
(*:*) *
348 | IComma
of string mcode
(* , *)
349 | Idots
of string mcode
(* ... *) * initialiser
option (* whencode *)
350 | OptIni
of initialiser
351 | UniqueIni
of initialiser
354 DesignatorField
of string mcode
(* . *) * ident
355 | DesignatorIndex
of string mcode
(* [ *) * expression
* string mcode
(* ] *)
357 string mcode
(* [ *) * expression
* string mcode
(* ... *) *
358 expression
* string mcode
(* ] *)
360 and initialiser
= base_initialiser wrap
362 (* --------------------------------------------------------------------- *)
365 and base_parameterTypeDef
=
366 VoidParam
of fullType
367 | Param
of fullType
* ident
option
369 | MetaParam
of meta_name mcode
* keep_binding
* inherited
370 | MetaParamList
of meta_name mcode
* listlen
* keep_binding
* inherited
372 | PComma
of string mcode
374 | Pdots
of string mcode
(* ... *)
375 | Pcircles
of string mcode
(* ooo *)
377 | OptParam
of parameterTypeDef
378 | UniqueParam
of parameterTypeDef
380 and parameterTypeDef
= base_parameterTypeDef wrap
382 and parameter_list
= parameterTypeDef dots
384 (* --------------------------------------------------------------------- *)
385 (* #define Parameters *)
387 and base_define_param
=
389 | DPComma
of string mcode
390 | DPdots
of string mcode
(* ... *)
391 | DPcircles
of string mcode
(* ooo *)
392 | OptDParam
of define_param
393 | UniqueDParam
of define_param
395 and define_param
= base_define_param wrap
397 and base_define_parameters
=
399 | DParams
of string mcode
(*( *) * define_param dots
* string mcode
(* )*)
401 and define_parameters
= base_define_parameters wrap
403 (* --------------------------------------------------------------------- *)
406 (* PER = keep bindings separate, ANY = collect them *)
407 and meta_collect
= PER
| ALL
410 MetaPos
of meta_name mcode
* meta_name list
*
411 meta_collect
* keep_binding
* inherited
413 (* --------------------------------------------------------------------- *)
414 (* Function declaration *)
416 and storage
= Static
| Auto
| Register
| Extern
418 (* --------------------------------------------------------------------- *)
422 FunHeader
of mcodekind
(* before the function header *) *
423 bool (* true if all minus, for dropping static, etc *) *
424 fninfo list
* ident
(* name *) *
425 string mcode
(* ( *) * parameter_list
*
427 | Decl
of mcodekind
(* before the decl *) *
428 bool (* true if all minus *) * declaration
430 | SeqStart
of string mcode
(* { *)
431 | SeqEnd
of string mcode
(* } *)
433 | ExprStatement
of expression
option * string mcode
(*;*)
434 | IfHeader
of string mcode
(* if *) * string mcode
(* ( *) *
435 expression
* string mcode
(* ) *)
436 | Else
of string mcode
(* else *)
437 | WhileHeader
of string mcode
(* while *) * string mcode
(* ( *) *
438 expression
* string mcode
(* ) *)
439 | DoHeader
of string mcode
(* do *)
440 | WhileTail
of string mcode
(* while *) * string mcode
(* ( *) *
441 expression
* string mcode
(* ) *) *
443 | ForHeader
of string mcode
(* for *) * string mcode
(* ( *) *
444 expression
option * string mcode
(*;*) *
445 expression
option * string mcode
(*;*) *
446 expression
option * string mcode
(* ) *)
447 | IteratorHeader
of ident
(* name *) * string mcode
(* ( *) *
448 expression dots
* string mcode
(* ) *)
449 | SwitchHeader
of string mcode
(* switch *) * string mcode
(* ( *) *
450 expression
* string mcode
(* ) *)
451 | Break
of string mcode
(* break *) * string mcode
(* ; *)
452 | Continue
of string mcode
(* continue *) * string mcode
(* ; *)
453 | Label
of ident
* string mcode
(* : *)
454 | Goto
of string mcode
(* goto *) * ident
* string mcode
(* ; *)
455 | Return
of string mcode
(* return *) * string mcode
(* ; *)
456 | ReturnExpr
of string mcode
(* return *) * expression
*
459 | MetaRuleElem
of meta_name mcode
* keep_binding
* inherited
460 | MetaStmt
of meta_name mcode
* keep_binding
* metaStmtInfo
*
462 | MetaStmtList
of meta_name mcode
* keep_binding
* inherited
465 | TopExp
of expression
(* for macros body *)
466 | Ty
of fullType
(* only at top level *)
467 | TopInit
of initialiser
(* only at top level *)
468 | Include
of string mcode
(*#include*) * inc_file mcode
(*file *)
469 | Undef
of string mcode
(* #define *) * ident
(* name *)
470 | DefineHeader
of string mcode
(* #define *) * ident
(* name *) *
471 define_parameters
(*params*)
472 | Case
of string mcode
(* case *) * expression
* string mcode
(*:*)
473 | Default
of string mcode
(* default *) * string mcode
(*:*)
474 | DisjRuleElem
of rule_elem list
477 FStorage
of storage mcode
479 | FInline
of string mcode
480 | FAttr
of string mcode
483 NotSequencible
| SequencibleAfterDots
of dots_whencode list
| Sequencible
485 and rule_elem
= base_rule_elem wrap
488 Seq
of rule_elem
(* { *) *
489 statement dots
* rule_elem
(* } *)
490 | IfThen
of rule_elem
(* header *) * statement
* end_info
491 | IfThenElse
of rule_elem
(* header *) * statement
*
492 rule_elem
(* else *) * statement
* end_info
493 | While
of rule_elem
(* header *) * statement
* end_info
494 | Do
of rule_elem
(* do *) * statement
* rule_elem
(* tail *)
495 | For
of rule_elem
(* header *) * statement
* end_info
496 | Iterator
of rule_elem
(* header *) * statement
* end_info
(*enditer*)
497 | Switch
of rule_elem
(* header *) * rule_elem
(* { *) *
498 statement
(*decl*) dots
* case_line list
* rule_elem
(*}*)
499 | Atomic
of rule_elem
500 | Disj
of statement dots list
501 | Nest
of string mcode
(* <.../<+... *) * statement dots
*
502 string mcode
(* ...>/...+> *) *
503 (statement dots
,statement
) whencode list
* multi
*
504 dots_whencode list
* dots_whencode list
505 | FunDecl
of rule_elem
(* header *) * rule_elem
(* { *) *
506 statement dots
* rule_elem
(* } *)
507 | Define
of rule_elem
(* header *) * statement dots
508 | AsStmt
of statement
* statement
(* as statement, always metavar *)
509 | Dots
of string mcode
(* ... *) *
510 (statement dots
,statement
) whencode list
*
511 dots_whencode list
* dots_whencode list
512 | Circles
of string mcode
(* ooo *) *
513 (statement dots
,statement
) whencode list
*
514 dots_whencode list
* dots_whencode list
515 | Stars
of string mcode
(* *** *) *
516 (statement dots
,statement
) whencode list
*
517 dots_whencode list
* dots_whencode list
518 | OptStm
of statement
519 | UniqueStm
of statement
521 and ('a
,'b
) whencode
=
524 | WhenModifier
of when_modifier
525 | WhenNotTrue
of rule_elem
526 | WhenNotFalse
of rule_elem
535 WParen
of rule_elem
* meta_name
(*pren_var*)
537 | Other_dots
of statement dots
539 and statement
= base_statement wrap
542 CaseLine
of rule_elem
(* case/default header *) * statement dots
543 | OptCase
of case_line
545 and case_line
= base_case_line wrap
548 Local
of inc_elem list
549 | NonLocal
of inc_elem list
556 NONDECL
of statement
(* cannot match all of a top-level declaration *)
557 | CODE
of statement dots
558 | FILEINFO
of string mcode
(* old file *) * string mcode
(* new file *)
559 | ERRORWORDS
of expression list
561 and top_level
= base_top_level wrap
564 CocciRulename
of string option * dependency
* string list
* string list
*
566 (* true if the whole thing is an expression *)
567 | GeneratedRulename
of string option * dependency
*
568 string list
* string list
* exists
* bool
569 (* true if the whole thing is an expression *)
570 | ScriptRulename
of string option (* name *) * string (* language *) *
572 | InitialScriptRulename
of string option (* name *) * string (* language *) *
574 | FinalScriptRulename
of string option (* name *) * string (* language *) *
577 and ruletype
= Normal
| Generated
580 CocciRule
of string (* name *) *
581 (dependency
* string list
(* dropped isos *) * exists
) *
582 top_level list
* bool list
(* true if generates an exp *) * ruletype
583 | ScriptRule
of string (* name *) *
584 string * dependency
*
585 (script_meta_name
* meta_name
* metavar
) list
*
586 meta_name list
(*script vars*) * string
587 | InitialScriptRule
of string (* name *) *
588 string * dependency
* string
589 | FinalScriptRule
of string (* name *) *
590 string * dependency
* string
592 and script_meta_name
= string option (*string*) * string option (*ast*)
595 Dep
of string (* rule applies for the current binding *)
596 | AntiDep
of string (* rule doesn't apply for the current binding *)
597 | EverDep
of string (* rule applies for some binding *)
598 | NeverDep
of string (* rule never applies for any binding *)
599 | AndDep
of dependency
* dependency
600 | OrDep
of dependency
* dependency
603 and rule_with_metavars
= metavar list
* rule
606 FullTypeTag
of fullType
607 | BaseTypeTag
of baseType
608 | StructUnionTag
of structUnion
611 | ExpressionTag
of expression
612 | ConstantTag
of constant
613 | UnaryOpTag
of unaryOp
614 | AssignOpTag
of assignOp
616 | BinaryOpTag
of binaryOp
617 | ArithOpTag
of arithOp
618 | LogicalOpTag
of logicalOp
619 | DeclarationTag
of declaration
620 | InitTag
of initialiser
621 | StorageTag
of storage
622 | IncFileTag
of inc_file
623 | Rule_elemTag
of rule_elem
624 | StatementTag
of statement
625 | CaseLineTag
of case_line
626 | ConstVolTag
of const_vol
627 | Token
of string * info
option
628 | Pragma
of added_string list
630 | ExprDotsTag
of expression dots
631 | ParamDotsTag
of parameterTypeDef dots
632 | StmtDotsTag
of statement dots
633 | DeclDotsTag
of declaration dots
635 | ParamTag
of parameterTypeDef
636 | SgrepStartTag
of string
637 | SgrepEndTag
of string
639 (* --------------------------------------------------------------------- *)
641 and exists
= Exists
| Forall
| Undetermined
643 (* --------------------------------------------------------------------- *)
645 val mkToken
: string -> anything
647 val undots
: 'a dots
-> 'a list
649 val lub_count
: count
-> count
-> count
651 (* --------------------------------------------------------------------- *)
653 val rewrap
: 'a wrap
-> 'b
-> 'b wrap
654 val rewrap_mcode
: 'a mcode
-> 'a
-> 'a mcode
655 val unwrap
: 'a wrap
-> 'a
656 val unwrap_mcode
: 'a mcode
-> 'a
657 val get_mcodekind
: 'a mcode
-> mcodekind
658 val get_line
: 'a wrap
-> line
659 val get_mcode_line
: 'a mcode
-> line
660 val get_mcode_col
: 'a mcode
-> int
661 val get_fvs
: 'a wrap
-> meta_name list
662 val get_wcfvs
: ('a wrap
,'b wrap
) whencode list
-> meta_name list
663 val set_fvs
: meta_name list
-> 'a wrap
-> 'a wrap
664 val get_mfvs
: 'a wrap
-> meta_name list
665 val set_mfvs
: meta_name list
-> 'a wrap
-> 'a wrap
666 val get_fresh
: 'a wrap
-> (meta_name
* seed
) list
667 val get_inherited
: 'a wrap
-> meta_name list
668 val get_saved
: 'a wrap
-> meta_name list
669 val get_dots_bef_aft
: statement
-> dots_bef_aft
670 val set_dots_bef_aft
: dots_bef_aft
-> statement
-> statement
671 val get_pos
: 'a wrap
-> meta_name mcode
option
672 val set_pos
: 'a wrap
-> meta_name mcode
option -> 'a wrap
673 val get_test_exp
: 'a wrap
-> bool
674 val set_test_exp
: expression
-> expression
675 val get_safe_decl
: 'a wrap
-> bool
676 val get_isos
: 'a wrap
-> (string*anything
) list
677 val set_isos
: 'a wrap
-> (string*anything
) list
-> 'a wrap
678 val get_pos_var
: 'a mcode
-> meta_pos list
679 val set_pos_var
: meta_pos list
-> 'a mcode
-> 'a mcode
680 val drop_pos
: 'a mcode
-> 'a mcode
682 val get_meta_name
: metavar
-> meta_name
684 val tag2c
: anything
-> string
688 val make_meta_rule_elem
:
689 string -> mcodekind
->
690 (meta_name list
* (meta_name
* seed
) list
* meta_name list
) ->
694 string -> mcodekind
->
695 (meta_name list
* (meta_name
* seed
) list
* meta_name list
) ->
698 val make_term
: 'a
-> 'a wrap
699 val make_inherited_term
: 'a
-> meta_name list
(* inherited vars *) -> 'a wrap
700 val make_mcode
: 'a
-> 'a mcode
702 val equal_pos
: fixpos
-> fixpos
-> bool