diff options
Diffstat (limited to 'src/api/python/genkinds.py')
| -rw-r--r-- | src/api/python/genkinds.py | 187 |
1 files changed, 33 insertions, 154 deletions
diff --git a/src/api/python/genkinds.py b/src/api/python/genkinds.py index c19364559..30ee18708 100644 --- a/src/api/python/genkinds.py +++ b/src/api/python/genkinds.py @@ -22,41 +22,22 @@ handle nested '#if 0' pairs. """ import argparse -from collections import OrderedDict +import os +import sys -#################### Default Filenames ################ -DEFAULT_HEADER = 'cvc4cppkind.h' -DEFAULT_PREFIX = 'kinds' +# the following command in CVC4/build/src/api/python/CMakeFiles/gen-pycvc4-kinds.dir/build.make +# cd CVC4/build/src/api/python && /usr/bin/python3 CVC4/src/api/python/genkinds.py ... +# indicates we are in directory CVC4/build/src/api/python +# so we use ../../../../src/api to access CVC4/src/api/parsekinds.py +sys.path.insert(0, os.path.abspath('../../../../src/api')) -##################### Useful Constants ################ -OCB = '{' -CCB = '}' -SC = ';' -EQ = '=' -C = ',' -US = '_' -NL = '\n' +from parsekinds import * -#################### Enum Declarations ################ -ENUM_START = 'enum CVC4_EXPORT Kind' -ENUM_END = CCB+SC +#################### Default Filenames ################ +DEFAULT_PREFIX = 'kinds' ################ Comments and Macro Tokens ############ PYCOMMENT = '#' -COMMENT = '//' -BLOCK_COMMENT_BEGIN = '/*' -BLOCK_COMMENT_END = '*/' -MACRO_BLOCK_BEGIN = '#if 0' -MACRO_BLOCK_END = '#endif' - -#################### Format Kind Names ################ -# special cases for format_name -_IS = '_IS' -# replacements after some preprocessing -replacements = { - 'Bitvector' : 'BV', - 'Floatingpoint': 'FP' -} ####################### Code Blocks ################### CDEF_KIND = " cdef Kind " @@ -126,130 +107,28 @@ cdef kind {name} = kind(<int> {kind}) setattr(kinds, "{name}", {name}) """ -class KindsParser: - tokenmap = { - BLOCK_COMMENT_BEGIN : BLOCK_COMMENT_END, - MACRO_BLOCK_BEGIN : MACRO_BLOCK_END - } - - def __init__(self): - self.kinds = OrderedDict() - self.endtoken = None - self.endtoken_stack = [] - self.in_kinds = False - - def format_name(self, name): - ''' - In the Python API, each Kind name is reformatted for easier use - - The naming scheme is: - 1. capitalize the first letter of each word (delimited by underscores) - 2. make the rest of the letters lowercase - 3. replace Floatingpoint with FP - 4. replace Bitvector with BV - - There is one exception: - FLOATINGPOINT_ISNAN --> FPIsNan - - For every "_IS" in the name, there's an underscore added before step 1, - so that the word after "Is" is capitalized - - Examples: - BITVECTOR_PLUS --> BVPlus - APPLY_SELECTOR --> ApplySelector - FLOATINGPOINT_ISNAN --> FPIsNan - SETMINUS --> Setminus - - See the generated .pxi file for an explicit mapping - ''' - name = name.replace(_IS, _IS+US) - words = [w.capitalize() for w in name.lower().split(US)] - name = "".join(words) - - for og, new in replacements.items(): - name = name.replace(og, new) - - return name - - def ignore_block(self, line): - ''' - Returns a boolean telling self.parse whether to ignore a line or not. - It also updates all the necessary state to track comments and macro - blocks - ''' - - # check if entering block comment or macro block - for token in self.tokenmap: - if token in line: - if self.tokenmap[token] not in line: - if self.endtoken is not None: - self.endtoken_stack.append(self.endtoken) - self.endtoken = self.tokenmap[token] - return True - - # check if currently in block comment or macro block - if self.endtoken is not None: - # check if reached the end of block comment or macro block - if self.endtoken in line: - if self.endtoken_stack: - self.endtoken = self.endtoken_stack.pop() - else: - self.endtoken =None - return True - - return False - - def parse(self, filename): - f = open(filename, "r") - - for line in f.read().split(NL): - line = line.strip() - if COMMENT in line: - line = line[:line.find(COMMENT)] - if not line: - continue - - if self.ignore_block(line): - continue - - if ENUM_END in line: - self.in_kinds = False - break - elif self.in_kinds: - if line == OCB: - continue - if EQ in line: - line = line[:line.find(EQ)].strip() - elif C in line: - line = line[:line.find(C)].strip() - self.kinds[line] = self.format_name(line) - elif ENUM_START in line: - self.in_kinds = True - continue - - f.close() - - def gen_pxd(self, filename): - f = open(filename, "w") - f.write(KINDS_PXD_TOP) - # include the format_name docstring in the generated file - # could be helpful for users to see the formatting rules - for line in self.format_name.__doc__.split(NL): - f.write(PYCOMMENT) - if not line.isspace(): - f.write(line) - f.write(NL) - for kind in self.kinds: - f.write(CDEF_KIND + kind + NL) - f.close() - def gen_pxi(self, filename): - f = open(filename, "w") - pxi = KINDS_PXI_TOP - for kind, name in self.kinds.items(): - pxi += KINDS_ATTR_TEMPLATE.format(name=name, kind=kind) - f.write(pxi) - f.close() +def gen_pxd(parser: KindsParser, filename): + f = open(filename, "w") + f.write(KINDS_PXD_TOP) + # include the format_name docstring in the generated file + # could be helpful for users to see the formatting rules + for line in parser.format_name.__doc__.split(NL): + f.write(PYCOMMENT) + if not line.isspace(): + f.write(line) + f.write(NL) + for kind in parser.kinds: + f.write(CDEF_KIND + kind + NL) + f.close() + +def gen_pxi(parser : KindsParser, filename): + f = open(filename, "w") + pxi = KINDS_PXI_TOP + for kind, name in parser.kinds.items(): + pxi += KINDS_ATTR_TEMPLATE.format(name=name, kind=kind) + f.write(pxi) + f.close() if __name__ == "__main__": @@ -270,5 +149,5 @@ if __name__ == "__main__": kp = KindsParser() kp.parse(kinds_header) - kp.gen_pxd(kinds_file_prefix + ".pxd") - kp.gen_pxi(kinds_file_prefix + ".pxi") + gen_pxd(kp, kinds_file_prefix + ".pxd") + gen_pxi(kp, kinds_file_prefix + ".pxi") |