litex/common/
keywords.rs

1use std::collections::HashMap;
2use std::sync::OnceLock;
3
4pub const FACT_PREFIX: &str = "$";
5pub const STRUCT_VIEW_PREFIX: &str = "&";
6pub const TEMPLATE_INSTANCE_PREFIX: &str = "\\";
7pub const DOT_AKA_FIELD_ACCESS_SIGN: &str = ".";
8/// Infix closed integer interval: `lo ... hi` (same AST as `closed_range(lo, hi)`).
9pub const DOT_DOT_DOT: &str = "...";
10pub const MOD_SIGN: &str = "::";
11pub const ADD: &str = "+";
12pub const SUB: &str = "-";
13pub const MUL: &str = "*";
14pub const DIV: &str = "/";
15pub const MOD: &str = "%";
16pub const POW: &str = "^";
17pub const MATRIX_ADD: &str = "++";
18pub const MATRIX_SUB: &str = "--";
19pub const MATRIX_MUL: &str = "**";
20pub const MATRIX_SCALAR_MUL: &str = "*.";
21pub const MATRIX_POW: &str = "^^";
22pub const LEFT_BRACE: &str = "(";
23pub const RIGHT_BRACE: &str = ")";
24pub const COMMA: &str = ",";
25pub const LEFT_CURLY_BRACE: &str = "{";
26pub const RIGHT_CURLY_BRACE: &str = "}";
27pub const EQUAL: &str = "=";
28pub const NOT_EQUAL: &str = "!=";
29pub const LESS: &str = "<";
30pub const GREATER: &str = ">";
31pub const LESS_EQUAL: &str = "<=";
32pub const GREATER_EQUAL: &str = ">=";
33pub const RIGHT_ARROW: &str = "=>";
34pub const EQUIVALENT_SIGN: &str = "<=>";
35pub const LEFT_BRACKET: &str = "[";
36pub const RIGHT_BRACKET: &str = "]";
37pub const DOUBLE_QUOTE: &str = "\"";
38pub const COLON: &str = ":";
39// Infix operator: one backtick before the name, e.g. A `union B (same role as former A \union B).
40pub const INFIX_FN_NAME_SIGN: &str = "`";
41
42pub const UNION: &str = "union";
43pub const INTERSECT: &str = "intersect";
44pub const SET_MINUS: &str = "set_minus";
45pub const SET_DIFF: &str = "set_diff";
46pub const CUP: &str = "cup";
47pub const CAP: &str = "cap";
48pub const POWER_SET: &str = "power_set";
49pub const CHOOSE: &str = "choose";
50pub const FN_LOWER_CASE: &str = "fn";
51/// Prefix for anonymous function literals: `'(x S, …) T { … }` or `'S (x) { … }`.
52pub const ANONYMOUS_FN_PREFIX: &str = "'";
53pub const SET: &str = "set";
54pub const NONEMPTY_SET: &str = "nonempty_set";
55pub const FINITE_SET: &str = "finite_set";
56pub const N_POS: &str = "N_pos";
57pub const N: &str = "N";
58pub const Q: &str = "Q";
59pub const Z: &str = "Z";
60pub const R: &str = "R";
61pub const CART: &str = "cart";
62pub const CART_DIM: &str = "cart_dim";
63pub const TUPLE_DIM: &str = "tuple_dim";
64pub const PROJ: &str = "proj";
65pub const COUNT: &str = "count";
66pub const FINITE_SEQ: &str = "finite_seq";
67pub const SEQ: &str = "seq";
68pub const MATRIX: &str = "matrix";
69pub const RANGE: &str = "range";
70pub const CLOSED_RANGE: &str = "closed_range";
71pub const SUM: &str = "sum";
72pub const PRODUCT: &str = "product";
73pub const EXIST: &str = "exist";
74/// User-facing spelling for unique existence (`exist` + `!` as two tokens in the source).
75pub const EXIST_BANG: &str = "exist!";
76pub const ST: &str = "st";
77pub const FORALL: &str = "forall";
78/// User-facing spelling for inline universal quantification (`forall` + `!` as two tokens).
79pub const FORALL_BANG: &str = "forall!";
80pub const NOT: &str = "not";
81pub const IS_SET: &str = "is_set";
82pub const IS_NONEMPTY_SET: &str = "is_nonempty_set";
83pub const IS_FINITE_SET: &str = "is_finite_set";
84pub const IS_CART: &str = "is_cart";
85pub const IS_TUPLE: &str = "is_tuple";
86pub const IN: &str = "in";
87pub const OR: &str = "or";
88pub const AND: &str = "and";
89pub const SUBSET: &str = "subset";
90pub const SUPERSET: &str = "superset";
91pub const SUCCESS_COLON: &str = "Success:";
92pub const UNKNOWN_COLON: &str = "Unknown:";
93pub const LET: &str = "let";
94pub const PROP: &str = "prop";
95/// Predicate symbol declared by name and parameter list only (no `:` / definition body); cf. `prop` with iff body.
96pub const ABSTRACT_PROP: &str = "abstract_prop";
97pub const CLAIM: &str = "claim";
98pub const PROVE: &str = "prove";
99
100pub const BY: &str = "by";
101pub const DECREASING: &str = "decreasing";
102pub const CASES: &str = "cases";
103pub const CONTRA: &str = "contra";
104pub const ENUMERATE: &str = "enumerate";
105pub const INDUC: &str = "induc";
106/// Strong (complete) induction on integers: same shape as `by induc`, but the step uses a `forall` band hypothesis.
107pub const STRONG_INDUC: &str = "strong_induc";
108/// 保留名（旧版最后一项 `case` 曾用 `param = param_2 + n`）；当前语法最后一项为 `case >= n:`（n 为特例个数），不再登记此名。
109pub const INDUC_PARAM_2_NAME: &str = "param_2";
110pub const FOR: &str = "for";
111pub const EXTENSION: &str = "extension";
112pub const TRANSITIVE_PROP: &str = "transitive_prop";
113pub const SYMMETRIC_PROP: &str = "symmetric_prop";
114pub const REFLEXIVE_PROP: &str = "reflexive_prop";
115pub const ANTISYMMETRIC_PROP: &str = "antisymmetric_prop";
116pub const TUPLE: &str = "tuple";
117
118pub const CASE: &str = "case";
119pub const IMPORT: &str = "import";
120pub const AS: &str = "as";
121pub const HAVE: &str = "have";
122pub const KNOW: &str = "know";
123pub const CLEAR: &str = "clear";
124pub const DO_NOTHING: &str = "do_nothing";
125pub const RUN_FILE: &str = "run_file";
126pub const FROM: &str = "from";
127pub const EVAL: &str = "eval";
128pub const WITNESS: &str = "witness";
129pub const IMPOSSIBLE: &str = "impossible";
130pub const ALGO: &str = "algo";
131pub const ABS: &str = "abs";
132pub const SQRT: &str = "sqrt";
133pub const LOG: &str = "log";
134pub const MAX: &str = "max";
135pub const MIN: &str = "min";
136pub const Q_POS: &str = "Q_pos";
137pub const R_POS: &str = "R_pos";
138pub const Q_NEG: &str = "Q_neg";
139pub const Z_NEG: &str = "Z_neg";
140pub const R_NEG: &str = "R_neg";
141pub const Q_NZ: &str = "Q_nz";
142pub const Z_NZ: &str = "Z_nz";
143pub const R_NZ: &str = "R_nz";
144pub const STRUCT: &str = "struct";
145pub const TEMPLATE: &str = "template";
146pub const RESTRICT_FN_IN: &str = "restrict_fn_in";
147pub const STRATEGY: &str = "strategy";
148pub const USE_STRATEGY: &str = "use_strategy";
149pub const END_STRATEGY: &str = "end_strategy";
150/// `$fn_eq_in(f, g, S)`: f and g agree on domain set S (encoded as a forall; see verify builtin).
151pub const FN_EQ_IN: &str = "fn_eq_in";
152/// `$fn_eq(f, g)`: mutual function-space typing and pointwise equality on the shared dom (see verify).
153pub const FN_EQ: &str = "fn_eq";
154pub const INJECTIVE: &str = "injective";
155pub const SURJECTIVE: &str = "surjective";
156pub const BIJECTIVE: &str = "bijective";
157
158fn build_key_symbols_map() -> HashMap<&'static str, &'static str> {
159    let mut m = HashMap::new();
160    let symbols = [
161        STRUCT_VIEW_PREFIX,
162        TEMPLATE_INSTANCE_PREFIX,
163        EQUIVALENT_SIGN,
164        NOT_EQUAL,
165        LESS_EQUAL,
166        GREATER_EQUAL,
167        RIGHT_ARROW,
168        FACT_PREFIX,
169        DOT_AKA_FIELD_ACCESS_SIGN,
170        MOD_SIGN,
171        ADD,
172        SUB,
173        MUL,
174        DIV,
175        MOD,
176        POW,
177        MATRIX_POW,
178        MATRIX_MUL,
179        MATRIX_SCALAR_MUL,
180        MATRIX_ADD,
181        MATRIX_SUB,
182        DOT_DOT_DOT,
183        LEFT_BRACE,
184        RIGHT_BRACE,
185        COMMA,
186        LEFT_CURLY_BRACE,
187        RIGHT_CURLY_BRACE,
188        EQUAL,
189        LESS,
190        GREATER,
191        LEFT_BRACKET,
192        RIGHT_BRACKET,
193        DOUBLE_QUOTE,
194        COLON,
195        INFIX_FN_NAME_SIGN,
196        ANONYMOUS_FN_PREFIX,
197    ];
198    for &s in &symbols {
199        m.insert(s, s);
200    }
201    m
202}
203
204fn build_keywords_map() -> HashMap<&'static str, &'static str> {
205    let mut m = HashMap::new();
206    let words = [
207        UNION,
208        INTERSECT,
209        SET_MINUS,
210        SET_DIFF,
211        CUP,
212        CAP,
213        POWER_SET,
214        CHOOSE,
215        FN_LOWER_CASE,
216        SET,
217        NONEMPTY_SET,
218        FINITE_SET,
219        N_POS,
220        N,
221        Q,
222        Z,
223        R,
224        CART,
225        CART_DIM,
226        TUPLE_DIM,
227        PROJ,
228        COUNT,
229        SUM,
230        PRODUCT,
231        FINITE_SEQ,
232        SEQ,
233        MATRIX,
234        RANGE,
235        CLOSED_RANGE,
236        EXIST,
237        ST,
238        FORALL,
239        NOT,
240        IS_SET,
241        IS_NONEMPTY_SET,
242        IS_FINITE_SET,
243        IS_CART,
244        IS_TUPLE,
245        IN,
246        OR,
247        AND,
248        SUBSET,
249        SUPERSET,
250        SUCCESS_COLON,
251        UNKNOWN_COLON,
252        LET,
253        PROP,
254        ABSTRACT_PROP,
255        CLAIM,
256        PROVE,
257        BY,
258        DECREASING,
259        CASES,
260        CONTRA,
261        CASE,
262        IMPORT,
263        AS,
264        ENUMERATE,
265        HAVE,
266        KNOW,
267        CLEAR,
268        DO_NOTHING,
269        RUN_FILE,
270        INDUC,
271        STRONG_INDUC,
272        FROM,
273        EVAL,
274        FOR,
275        WITNESS,
276        EXTENSION,
277        TRANSITIVE_PROP,
278        IMPOSSIBLE,
279        TUPLE,
280        ALGO,
281        ABS,
282        SQRT,
283        LOG,
284        MAX,
285        MIN,
286        Q_POS,
287        R_POS,
288        Q_NEG,
289        Z_NEG,
290        R_NEG,
291        Q_NZ,
292        Z_NZ,
293        R_NZ,
294        STRUCT,
295        TEMPLATE,
296        RESTRICT_FN_IN,
297        STRATEGY,
298        USE_STRATEGY,
299        END_STRATEGY,
300        FN_EQ_IN,
301        FN_EQ,
302    ];
303    for &s in &words {
304        m.insert(s, s);
305    }
306    m
307}
308
309static KEY_SYMBOLS_MAP: OnceLock<HashMap<&'static str, &'static str>> = OnceLock::new();
310static KEYWORDS_MAP: OnceLock<HashMap<&'static str, &'static str>> = OnceLock::new();
311
312fn key_symbols_map() -> &'static HashMap<&'static str, &'static str> {
313    KEY_SYMBOLS_MAP.get_or_init(build_key_symbols_map)
314}
315
316fn keywords_map() -> &'static HashMap<&'static str, &'static str> {
317    KEYWORDS_MAP.get_or_init(build_keywords_map)
318}
319
320pub fn key_symbols_sorted_by_len_desc() -> Vec<&'static str> {
321    let mut v: Vec<&'static str> = key_symbols_map().keys().copied().collect();
322    v.sort_by(|a, b| b.len().cmp(&a.len()));
323    v
324}
325
326pub fn is_keyword(atom_name: &str) -> bool {
327    keywords_map().contains_key(atom_name)
328}
329
330fn is_key_symbol(atom_name: &str) -> bool {
331    key_symbols_map().contains_key(atom_name)
332}
333
334pub fn is_key_symbol_or_keyword(atom_name: &str) -> bool {
335    is_key_symbol(atom_name) || is_keyword(atom_name)
336}
337
338pub fn is_comparison_str(atom_name: &str) -> bool {
339    atom_name == EQUAL
340        || atom_name == NOT_EQUAL
341        || atom_name == LESS
342        || atom_name == GREATER
343        || atom_name == LESS_EQUAL
344        || atom_name == GREATER_EQUAL
345}
346
347pub fn is_builtin_predicate(atom_name: &str) -> bool {
348    atom_name == EQUAL
349        || atom_name == NOT_EQUAL
350        || atom_name == LESS
351        || atom_name == GREATER
352        || atom_name == LESS_EQUAL
353        || atom_name == GREATER_EQUAL
354        || atom_name == IS_SET
355        || atom_name == IS_NONEMPTY_SET
356        || atom_name == IS_FINITE_SET
357        || atom_name == IS_CART
358        || atom_name == IS_TUPLE
359        || atom_name == SUBSET
360        || atom_name == SUPERSET
361        || atom_name == IN
362        || atom_name == RESTRICT_FN_IN
363        || atom_name == FN_EQ_IN
364        || atom_name == FN_EQ
365}
366
367pub fn is_builtin_identifier_name(atom_name: &str) -> bool {
368    atom_name == ADD
369        || atom_name == SUB
370        || atom_name == MUL
371        || atom_name == DIV
372        || atom_name == MOD
373        || atom_name == POW
374        || atom_name == MATRIX_ADD
375        || atom_name == MATRIX_SUB
376        || atom_name == MATRIX_MUL
377        || atom_name == MATRIX_SCALAR_MUL
378        || atom_name == MATRIX_POW
379        || atom_name == Q_POS
380        || atom_name == R_POS
381        || atom_name == Q_NEG
382        || atom_name == Z_NEG
383        || atom_name == R_NEG
384        || atom_name == Q_NZ
385        || atom_name == Z_NZ
386        || atom_name == R_NZ
387        || atom_name == N_POS
388        || atom_name == N
389        || atom_name == Q
390        || atom_name == Z
391        || atom_name == R
392}
litex/common/keywords.rs

litex/common/
keywords.rs
