1 ///////////////////////////////////////////////////////////////////////////////
3 // This file defines the lexical structure of the Prop language.
5 ///////////////////////////////////////////////////////////////////////////////
9 ///////////////////////////////////////////////////////////////////////////////
11 // Here are some regular expression abbreviations.
13 ///////////////////////////////////////////////////////////////////////////////
14 lexeme digits = /[0-9]+/
16 | integer = /{digits}/
17 | exponent = /[eE]{sign}?{digits}/
18 | mantissa = /({digits}\.{digits}?|\.{digits})/
19 | real = /{mantissa}{exponent}?/
20 | ident = /([a-zA-Z\$][a-zA-Z0-9_\$]*|[a-zA-Z_][a-zA-Z0-9_]+)/
21 | patvar = /([\?\#\$]*{ident}[\'\?]*|\#\#)/
22 | string = /"([^\\"\n]|\\.)*"/
23 | character = /'([^\\'\n]|\\.[0-9a-f]*)'/
24 | regexp = /\/([^\/\n*]|\\.)([^\/\n]|\\.)*\//
25 | logical_var = /\'{ident}/
26 | meta = /`([^`]|\\.)*`/
29 ///////////////////////////////////////////////////////////////////////////////
31 // Main keywords are keywords that can start Prop constructs.
33 ///////////////////////////////////////////////////////////////////////////////
34 lexeme class MainKeywords =
35 "rewrite" | "inference" | "match" | "matchall" | "matchscan"
36 | "refine" | "classof" | "type" | "datatype" | "instantiate"
37 | "lexeme" | "bitfield" | "begin" | "syntax"
38 | "dataflow" | "module" | "signature" | "constraint" | "declare"
39 | "procedure" | "fun" | "function"
40 | "graphtype" | "graphrewrite" | "cutrewrite" | "failrewrite"
43 ///////////////////////////////////////////////////////////////////////////////
45 // Keywords are the normal kinds of keywords
47 ///////////////////////////////////////////////////////////////////////////////
49 "if" | "then" | "else" | "elsif" | "while" | "loop" | "is"
50 | "class" | "unifiable" | "of"
51 | "do" | "break" | "continue" | "goto"
52 | "where" | "as" | "public" | "protected"
53 | "private" | "const" | "extern" | "mutable" | "applicative"
54 | "virtual" | "true" | "false" | "collectable" | "finalizable"
55 | "printable" | "traced" | "persistent"
56 | "treeparser" | "inline" | "with" | "switch" | "unsigned"
57 | "signed" | "for" | "category" | "functor" | "feature"
58 | "sharing" | "relation" | "view" | "inherited" | "return"
59 | "synthesized" | "law" | "left:" | "right:" | "expect:" | "prec:"
60 | "mapof" | "setof" | "bagof" | "multimapof" | "listof" | "priqueueof"
61 | "queueof" | "dequeof" | "tupleof" | "forall" | "exists"
62 | "dom" | "ran" | "arb" | "less" | "include"
63 | "lfp" | "gfp" | "hom"
64 | "implies:" | "xor:" | "equiv:" | "time:" | "space:"
65 | "nodes:" | "edges:" | "index:" | "hash:" | "equality:"
66 | "preorder:" | "postorder:" | "before:"
67 | "topdown:" | "bottomup:" | "strategy:" | "order:"
70 and SepKeywords = "case" | "and" | "end"
72 ///////////////////////////////////////////////////////////////////////////////
74 // Symbols are multi-character symbols used in Prop.
75 // Single character symbols are implicit and unlisted here.
77 ///////////////////////////////////////////////////////////////////////////////
79 ".." | "..." | "<->" | "::" | "&&" | "||" | "++" | "--" | "->"
80 | "<<" | ">>" | ">=" | "<=" | "+=" | "-=" | "*=" | "/=" | "%=" | "=="
81 | "!=" | "<<=" | ">>=" | "&=" | "|=" | "^=" | "=>" | "<-" | "<=>"
82 | ":=" | ":-" | LONG_BAR /\-\-\-\-\-+/
84 ///////////////////////////////////////////////////////////////////////////////
86 // Special symbols are symbols that is used for ad hoc syntactic features.
88 ///////////////////////////////////////////////////////////////////////////////
90 CONS_TOK | DOMAIN_TOK | CONS_EXP | META_QUOTE | POLY_DATATYPE | ATTRIB_ID
91 | "(|" | "|)" | "[|" | "|]" | "{|" | "|}" | ".(" | ".[" | "``" | "''"
93 ///////////////////////////////////////////////////////////////////////////////
97 ///////////////////////////////////////////////////////////////////////////////
101 | CHAR_TOK /{character}/
102 | STRING_TOK /{string}/
105 ///////////////////////////////////////////////////////////////////////////////
107 // PropToken is the class of all terminals in Prop.
109 ///////////////////////////////////////////////////////////////////////////////
110 datatype PropToken :: lexeme =
111 lexeme class MainKeywords
112 | lexeme class Keywords
113 | lexeme class SepKeywords
114 | lexeme class Symbols
115 | lexeme class Special
116 | lexeme class Literals
118 | REGEXP_TOK /{regexp}/
119 | QUARK_TOK /#{string}/
120 | BIGINT_TOK /#{sign}{integer}/
121 | PUNCTUATIONS /[\<\>\,\.\;\&\|\^\!\~\+\-\*\/\%\?\=\:\\]/