ctlstar.asdl
4.9 KB
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
134
135
136
137
138
139
140
141
142
143
module CTLstar version "$Revision: 1 $"
{
ctlstar = Spec(ctldecl* atoms, ctldecl* properties, form? main)
attributes (int lineno, int col_offset)
ctldecl = Atom(identifier name, ctlarg* args, ctlparams* params,
stmt* body)
| Property(identifier name, ctlargs* args,
ctlparams* params, form body)
attributes (int lineno, int col_offset)
ctlarg = Place(identifier name, string place)
| Token(identifier name, string place)
| Argument(identifier name, expr value, identifier type)
attributes (int lineno, int col_offset)
ctlparam = Parameter(identifier name, identifier type)
attributes (int lineno, int col_offset)
form = atom
| CtlUnary(ctlunary op, form child)
| CtlBinary(ctlbinary op, form left, form right)
attributes (int lineno, int col_offset)
ctlunary = notop | All | Exists | Next | Future | Globally
notop = Not
ctlbinary = boolop | Imply | Iff | Until | WeakUntil | Release
atom = InPlace(expr* data, ctlarg place)
| NotInPlace(expr* data, ctlarg place)
| EmptyPlace(ctlarg place)
| MarkedPlace(ctlarg place)
| Deadlock
| Boolean(bool val)
| Instance(identifier name, arg* args)
| Quantifier(ctlunary op,
identifier* vars,
ctlarg place,
form child,
bool distinct)
attributes (int lineno, int col_offset)
--------------------------------------------------------------
-- the rest is copied from "snakes/lang/python/python.asdl" --
--------------------------------------------------------------
stmt = FunctionDef(identifier name, arguments args,
stmt* body, expr* decorator_list, expr? returns)
| ClassDef(identifier name,
expr* bases,
keyword* keywords,
expr? starargs,
expr? kwargs,
stmt* body,
expr *decorator_list)
| Return(expr? value)
| Delete(expr* targets)
| Assign(expr* targets, expr value)
| AugAssign(expr target, operator op, expr value)
| For(expr target, expr iter, stmt* body, stmt* orelse)
| While(expr test, stmt* body, stmt* orelse)
| If(expr test, stmt* body, stmt* orelse)
| With(expr context_expr, expr? optional_vars, stmt* body)
| Raise(expr? exc, expr? cause)
| TryExcept(stmt* body, excepthandler* handlers, stmt* orelse)
| TryFinally(stmt* body, stmt* finalbody)
| Assert(expr test, expr? msg)
| Import(alias* names)
| ImportFrom(identifier module, alias* names, int? level)
| Exec(expr body, expr? globals, expr? locals)
| Global(identifier* names)
| Nonlocal(identifier* names)
| Expr(expr value)
| Pass | Break | Continue
attributes (int lineno, int col_offset)
expr = BoolOp(boolop op, expr* values)
| BinOp(expr left, operator op, expr right)
| UnaryOp(unaryop op, expr operand)
| Lambda(arguments args, expr body)
| IfExp(expr test, expr body, expr orelse)
| Dict(expr* keys, expr* values)
| Set(expr* elts)
| ListComp(expr elt, comprehension* generators)
| SetComp(expr elt, comprehension* generators)
| DictComp(expr key, expr value, comprehension* generators)
| GeneratorExp(expr elt, comprehension* generators)
| Yield(expr? value)
| Compare(expr left, cmpop* ops, expr* comparators)
| Call(expr func, expr* args, keyword* keywords,
expr? starargs, expr? kwargs)
| Num(object n)
| Str(string s)
| Ellipsis
| Attribute(expr value, identifier attr, expr_context ctx)
| Subscript(expr value, slice slice, expr_context ctx)
| Starred(expr value, expr_context ctx)
| Name(identifier id, expr_context ctx)
| List(expr* elts, expr_context ctx)
| Tuple(expr* elts, expr_context ctx)
attributes (int lineno, int col_offset)
expr_context = Load | Store | Del | AugLoad | AugStore | Param
slice = Slice(expr? lower, expr? upper, expr? step)
| ExtSlice(slice* dims)
| Index(expr value)
boolop = And | Or
operator = Add | Sub | Mult | Div | Mod | Pow | LShift
| RShift | BitOr | BitXor | BitAnd | FloorDiv
unaryop = Invert | notop | UAdd | USub
cmpop = Eq | NotEq | Lt | LtE | Gt | GtE | Is | IsNot | In | NotIn
comprehension = (expr target, expr iter, expr* ifs)
excepthandler = ExceptHandler(expr? type, identifier? name, stmt* body)
attributes (int lineno, int col_offset)
arguments = (arg* args, identifier? vararg, expr? varargannotation,
arg* kwonlyargs, identifier? kwarg,
expr? kwargannotation, expr* defaults,
expr* kw_defaults)
arg = (identifier arg, expr? annotation)
keyword = (identifier arg, expr value)
alias = (identifier name, identifier? asname)
}