ScalaBuilder
This class (tools/scalabuilder.py
) contains all the macro functions, which take the JSON encoded calculus and generate Scala code that is replaced into .scala
files.
Add any macro functions for code generation in Scala to this file (tools/scalabuilder.py
). They will automatically be called if referenced in the processed scala file (i.e if a method foo
is defined in tools/scalabuilder.py
, it will be called if (*foo*)
appears in the processed scala file).
The return type for any function that can be referenced in the processed files must be string. For any functions that do not return a string, add two underscores before a function name. Also add two underscores if the function is going to be static or purposefully hidden from use in the processed file.
def __init__(self, file) |
Parses the file (under file
path) as a JSON file and stores the contents in self.calc
Also normalizes the values stored under the type
key, which can either be strings or list of strings
def add(self, key, val) |
Adds a (key, value) pair to the calculus definition dictionary (i.e. set ‘export_path’)
Use strings as keys, otherwise the pair won’t be added.
def get(self, key) |
Returns the value for key stored in self.calc
dictionary
def calc_import(self) |
Returns calc_name
from self.calc
in the form import {calc_name}._
Requires calc_name
to be defined
def __keywords(calc) |
Given a dictionary, this function returns all the keys of the dictionary and recursively returns keys of any sub-dictionaries
def __ascii_reserved(calc) |
Given a dictionary, this function returns all the values stored under the key “ascii” and will recursively descent into any other dictionaries stored within the main one.
def uncommentL(self, list) |
def uncommentR(self, list) |
These functions in pair uncomment a section enclosed in:
/*/*uncommentL?ident1?ident2?ident3?...*/ ... /*uncommentR?ident1?ident2?ident3?...*/*/
if ident1,ident2,ident3,...
is defined in calc_structure
(that is, {ident1,ident2,ident3,…} ⊆ set (__keywords(self.calc)) ), by turning into:
/*/*uncommentL?ident1?ident2?ident3?...-BEGIN*/*//*uncommentL?ident1?ident2?ident3?...-END*/ ... /*uncommentR?ident1?ident2?ident3?...-BEGIN*//*/*uncommentR?ident1?ident2?ident3?...-END*/*/
Otherwise they remain unchanged.
def __is_terminal(name, structure) |
Checks that the given structure is not recursive or encapsulates another type.
def __prefix_candidtate(name, constructor, structure) |
Checks that the given structure is a prefix constructor, by checking that the first argument is a terminal type (i.e. a type that encodes the operators) and the last argument is recursive.
Used in calc_structure_datatype
def __infix_candidtate(name, constructor, structure) |
Checks that the given structure is a infix constructor, by checking that the constructor only takes 3 arguments, with the middle one being a terminal type (the infix operator).
Used in calc_structure_datatype
def __is_recursive(name, structure) |
def __is_recursive_aux(name, current, structure) |
Checks that the given datatype is recursive.
def __constructor_parsers_build(name, structure) |
Builds a parser for a given type by constructing parsers for each type constructor and then calls __main_parser_build, which constructs the prefix and infix parsers.
def __main_parser_build(name, structure) |
This function produces the following code, using parsers generated by __constructor_parsers_build:
lazy val formulaParser:PackratParser[<Type>] = operators[Any,<Type>](
Prefix(<Op1_Precedence>)(<Op1_Parser>) { case (_, a) => <Un_constructor> (<Op1>, a) },
Infix(<Op2_Precedence>)(<Op2_Parser>) { (_, a, b) => <Bin_constructor> (a, <Op2>, b ) }
.
.
.
) ( <Term_parser1>, <Term_parser2>, ... )
def __parse_calc_structure_datatype(name, structure, add_structure={}) |
Builds a parser for a given type by constructing parsers for each type constructor and then calls __main_parser_build, which constructs the prefix and infix parsers.
def parser_calc_structure(self) |
Called from the parser template. Generates parsers for parsing ASCII terms of types declared under calc_structure
in the JSON calculus file.
Uses __parse_calc_structure_datatype and __constructor_parsers_build
def __print_calc_structure_datatype(name, structure) |
Builds a print function from a specified type, producing:
def <Type>ToString(in:<Type>, format:String = LATEX) : String = format match {
case ASCII =>
in match {
case <Constructor_1> => ...
.
.
.
}
case LATEX =>
case <Constructor_1> => ...
.
.
.
}
case ISABELLE =>
case <Constructor_1> => ...
.
.
.
}
case ISABELLE_SE =>
case <Constructor_1> => ...
.
.
.
}
}