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


@staticmethod
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.


@staticmethod
def __is_terminal(name, structure)

Checks that the given structure is not recursive or encapsulates another type.


@staticmethod
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


@staticmethod
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


@staticmethod
def __is_recursive(name, structure)
def __is_recursive_aux(name, current, structure)

Checks that the given datatype is recursive.


@staticmethod
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.


@staticmethod
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>, ... )


@staticmethod
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


@staticmethod

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> => ...
	  .
      .
      .
	}
}