Code Generation Utilities

This section will outline the core functionality of this toolbox generator, namely the utilities used for generating the calculus tools.

build.py

This is the main build script, which ties in all the utilities into a single script for easy calculus generation. The script takes the following set of parameters:

Flag   Arguments Description
--path -p   Specify an output path for the calculus.
--template -t   Specify a templates folder to be used.
--verbose -v   Verbose mode.
--build -b all, scala, isabelle Compile the specified files only. Defaults to all
--stage -s core_calc_gen, rule_calc_gen, calc_compile, add_gui Call a specific stage of the build.

Build Stages

The calculus toolbox is compiled from the calculus description file in several stages, which include compiling the core calculus Isabelle theory files, generating the ASCII parser and print classes in Scala, parsing and translating the encoded rules into Isabelle, generating the rule theory files and finally adding the UI Scala classes. Bellow is a short overview of these stages (you can manually call any stage of the build via the --stage flag) .

  • core_calc_gen

    Isabelle

    The core calculus theory file is generated from template/Calc_Core.thy, compiled in Isabelle and exported into Scala (using Isabelle’s code generation facilities).

    Scala

    The parsers for the terms of the calculus are generated using template/Parser.scala
    The print class for terms of the calculus is generated using template/Print.scala

  • calc_compile

    Scala

    This stage simply compiles all the Scala classes in <calculus_output_path>/src/scala

  • rule_calc_gen

    Isabelle

    The rules of the calculus encoded in the JSON file are parsed and encoded in the main Isabelle theory file (template/Calc_Rules.thy).

    Scala

    The parser class is rebuilt, now including parsers for proof trees and rule datatype definitions
    The print class is rebuilt, adding printing for proof trees and rule datatype definitions

  • add_gui

    Scala

    Generates the Scala UI from template/gui/ adding a separate compile script and a make file for the built calculus.
    Any libraries inside the libs folder will be copied to the calculus folder.

gui.py

this utility requires the npyscreen python module (install using pip)

gui.py screenshot

This utility provides some debugging tools when extending the calculus functionality. To use, simply run ./gui.py. The debugging tools currently include the following functionality:

  • Test build on single file…

    Allows the user to specify a template file and a JSON calculus description file to generate a specific Isabelle theory or Scala class. To get a better understanding of how code generation works have a look at how code generation works. If changes are made to the IsabelleBuilder or ScalaBuilder python classes, Reload Builder can be used to reload these into the utility.

  • Test unbuild on single file…

    Takes an already generated Isabelle theory file or Scala class and removes any code, generated by the calculus toolbox tools.
    The utility replaces any block of code enclosed in (*<identifier>-BEGIN*) .. (*<identifier>-END*) by (*<identifier>*) in .thy files and /*<identifier>-BEGIN*/ .. /*<identifier>-END*/ by /*<identifier>*/ in .scala files This functionality has been mostly superseded by the watcher.py utility.

watcher.py

this utility requires the watchdog python module (install using pip)

The watcher utility is useful when rewriting code within the generated calculus and wanting to propagate the changes back to the template files automatically. As mentioned, the gui.py utility provides a way to strip down generated classes back into templates. However, the watcher utility does this automatically whenever a file is changed. The following table lists the arguments that can be passed to the utility:

Flag   Description
--source -s Specify the folder to be watched
--dest -d Specify the output folder
--ext -e Specify file extensions to be monitored. The default are ‘*.scala’ and *.thy
--rules -r Specify path rewrite rules (currently just a dictionary of hard coded strings, there is no regular expression matching). The command uses bash-like redirect syntax "<old1> > <new1>, <old2> > <new2>, ..."
--ignore -i Specify paths (or substrings of a path) from the source folder to be ignored (currently no regular expressions matching)

To run, use the following command:

./watcher.py -s <path_to_built_calculus>/src -d <path_to_template_folder> -i "scala/<calculus_name>.scala, .thy#, .thy~" -r "scala/ > , isabelle/ > , <calculus_name>_Core.thy > Calc_Core.thy, <calculus_name>.thy > Calc_Rules.thy"

This configuration will strip all the generated code from Isabelle and Scala files in <path_to_built_calculus>/src and save them back into the specified template folder. The -i flag will ignore any temporary Isabelle theory files .thy# and .thy~ as well as the scala/<calculus_name>.scala file which is automatically generated from the Isabelle theory files and therefore doe not have a template file (this file should not be modified manually at all).
The -r flag introduces some path rewrite rules, specific to the structure of the source and/or destination folders (these should work for the default setup). Note that <calculus_name> should be replaced with the name of the calculus one is working in (as specified in the JSON file under calc_name)

IsabelleBuilder / ScalaBuilder

IsabelleBuilder and ScalaBuilder form the core of the code generation facilities for Isabelle theories and Scala classes respectively. The way code generation is set up is the following:

  • The template files include comments of the form (*<function_name>*) in Isabelle and /*<function_name>*/ and the corresponding identifier is used as a function name in Isabelle/Scala builder classes.
    This is a snippet from template/Calc_Core.thy where the calculus name is plugged in for (*calc_name_core*) when it is generated by the toolbox:

    theory (*calc_name_core*)
    imports Main "~~/src/HOL/Library/Code_Char" "~~/src/HOL/Code_Numeral"

    begin
    ...
    
The corresponding python function is defined in `IsabelleBuilder` and shown below:

<div markdown="1">

    def calc_name_core(self):
        if "calc_name" in self.calc: return self.calc["calc_name"]+"_Core"
        return ""
    
When run with the [default calculus description file](https://github.com/goodlyrottenapple/calculus-toolbox/blob/master/default.json), the code snippet above will be turned into:

<div markdown="1">

    theory (*calc_name_core-BEGIN*)DCPL(*calc_name_core-END*)
    imports Main "~~/src/HOL/Library/Code_Char" "~~/src/HOL/Code_Numeral"

    begin
    ...
    
- - -

The code generation leaves delimiters `(*<identifier>-BEGIN*)` and `(*<identifier>-END*)` for Isabelle theories or `/*<identifier>-BEGIN*/` and `/*<identifier>-END*/` for Scala around generated code. While this may look cluttered, it allows for the conversion of the generated files back into templates, as described in the documentation of the [gui.py](#guipyhttpsgithubcomgoodlyrottenapplecalculus-toolboxblobmasterguipy) and [watcher.py](#watcherpyhttpsgithubcomgoodlyrottenapplecalculus-toolboxblobmasterwatcherpy) utilities.  However, these comment delimiters can be removed entirely if need be (_this functionality is present in [`utils.py`](https://github.com/goodlyrottenapple/calculus-toolbox/blob/master/tools/utils.py) (function `clean`), but is currently not implemented as a stand-alone runnable script_).

- - -

  • Arguments can be passed to the defined python functions by appending them to the identifier in the comments with a question mark: (*<identifier>?<arg1>?<arg2>?<arg3>?...*). The corresponding python function must take an extra list parameter, where the arguments are stored in the order they were written (i.e. [arg1, arg2, arg3, ...]):

    def <identifier>(self, list):
        ...

  • The data from the calculus JSON file is accessible through self.calc dictionary in both IsabelleBuilder and ScalaBuilder classes. For example, the calculus name can be accessed through self.calc["calc_name"].

    Care should be taken not to override any data in self.calc. Even though the code generator tools do not write any changes to the JSON file, data may be reused by different functions at different times and any modification of the self.calc dictionary can lead to unexpected behavior.
  • To create an internal/hidden function which cannot be called directly through its identifier, prepend two underscores to the function name: def __<fun>(self): ...
  • To create a static function use the @staticmethod flag before function declaration