IsabelleBuilder
This class (tools/isabuilder.py) contains all the macro functions, which take the JSON encoded calculus and generate Isabelle code that is replaced into the .thy theory files.
Add any macro functions for code generation in Isabelle theories to this file (tools/isabuilder.py). They will automatically be called if referenced in the processed theory file (i.e if a method foo is defined in tools/isabuilder.py, it will be called if (*foo*) appears in the processed theory file).
For passing arguments to foo, use (*foo?arg1?arg2?...*) in the processed 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_name_core(self) |
Returns calc_name from self.calc in the form {calc_name}_Core
Requires calc_name to be defined
| def calc_name(self) |
Returns calc_name from self.calc in the form {calc_name}
Requires calc_name to be defined
| def export_path(self) |
Returns a string of the form "{export_path}/{calc_name}.scala" (used in Isabelle export_code function)
Requires calc_name and export_path 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 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. Unused
| def __calc_structure_dependencies(structure) |
Given a dictionary (structure) of a calculus structure, returns a new dictionary of all the data types declared in the structure dictionary, along with their dependencies on any other data types.
Used in calc_structure and calc_structure_rules
| def __calc_structure_datatype(name, datatype, structure, shallow = False) |
Returns a definition of a datatype in Isabelle with syntactic sugar (if defined).
For example, the following entry in the JSON file:
"Formula_Bin_Op" : {
"Formula_And" : {
"isabelle" : "\\<and>\\<^sub>F",
"ascii" : "^",
"latex" : "\\wedge"
},
"Formula_ImpR" : {
"isabelle" : "\\<rightarrow>\\<^sub>F",
"ascii" : ">",
"latex" : "\\rightarrow"
}
}
would produce this output:
datatype Formula_Bin_Op = Formula_And ("\<and>\<^sub>F")
| Formula_ImpR ("\<rightarrow>\<^sub>F")
| def calc_structure(self) |
Called from the core calculus template. Generates Isabelle datatype definitions declared under calc_structure in the JSON calculus file.
Uses __calc_structure_datatype and __calc_structure_dependencies
| def calc_structure_se(self) |
Called from the core calculus SE template. Generates Isabelle datatype definitions declared under calc_structure in the JSON calculus file for the shallow embedding.
Uses __calc_structure_datatype and __calc_structure_dependencies
| def __calc_structure_se_to_de(name, datatype, structure, calc_name) |
Produces the definition for the SE_to_DE_ function for a given type, that translate terms of the shallow embedding into the terms of the deep embedding.
Uses __prefix_candidate, __infix_candidate and __is_terminal
| def __calc_structure_de_to_se(name, datatype, structure, calc_name) |
This function generates definitions, converse to __calc_structure_se_to_de, taking deep embedding terms into shallow embedding. Uses __prefix_candidate, __infix_candidate and __is_terminal
| def __calc_structure_translate(self, se_to_de = True) |
This function uses __calc_structure_se_to_de or __calc_structure_de_to_se (depending on the se_to_de flag passed in as an argument) to generate the translation functions for all the terms of the calculus.
| def __calc_structure_all_rules(rules) |
Given a dictionary of rule categories/groups (defined in calc_structure_rules) generates the datatype Rules and Prooftree.
Given the rule groups defined in the default JSON file, this function will produce:
datatype Rule = RuleZer RuleZer
| RuleCut RuleCut
| RuleU RuleU
| RuleDisp RuleDisp
| RuleOp RuleOp
| RuleBin RuleBin
| RuleMacro string Prooftree
| Fail
and Prooftree = Prooftree Sequent Rule "Prooftree list" ("_ \<Longleftarrow> PT ( _ ) _" [341,341] 350)
| def __calc_structure_rules_concl(self) |
Deprecated
| def calc_structure_rules(self) |
Called from the calculus rules template. Generates Isabelle datatype definitions declared under calc_structure_rules in the JSON calculus file.
Uses __calc_structure_datatype, __calc_structure_dependencies and __calc_structure_all_rules
| def __calc_structure_rules_rule_list_aux(name, rules, rule_def, parser_command) |
This function takes in the parser_command string, which it uses to parse the rules encoded in the rules dictionary and generate function of the following form:
primrec rule{name} :: "Locale \<Rightarrow> {name} \<Rightarrow> ruleder" where
"rule{name} x {name}.{rule} = ..."
Since the rule encoding in the JSON file is split into two parts, the declaration of the rule in calc_structure_rules and the ASCII encoding in rules, these two corresponding dictionaries are passed in as rules and rule_def.
| def rules_rule_fun(self) |
Generates a universal rule function that brings all the separate ruleBin/Op/etc functions under one call.
| def rules_rule_list(self) |
Generates the ruleList definition, used for proof search in Scala, as any rules not in this list will be omitted from the search.