Goto Chapter: Top 1 2 3 Ind
 [Top of Book]  [Contents]   [Previous Chapter]   [Next Chapter] 

1 Using the compiler
 1.1 Terminology
 1.2 Capabilities of the compiler
 1.3 Requirements
 1.4 Precompiling categories
 1.5 Compiling a function manually
 1.6 Giving hints to the compiler
 1.7 Stopping the compiler at a certain level
 1.8 Disabling the automatic inference of data types
 1.9 Compiling step-by-step
 1.10 Proof assistant mode
 1.11 Getting information about the compilation process
 1.12 FAQ

1 Using the compiler

1.1 Terminology

The compiler was started as a just-in-time compiler, that is, it needed some arguments to infer types of variables. Although the compiler now supports precompilation and type signatures can be explicitly given, it still is a just-in-time compiler in the following sense: Only methods for operations getting a CAP category as the first argument can be found by the compiler, and an instance of a CAP category is needed for method selection.

The compiler uses GAP's syntax trees for optimizing functions. The term tree always refers to the syntax tree of the function to be compiled. Note that a node of the tree always knows its children, so technically it is also a tree. That is, the terms tree, subtree, and node technically describe the same thing but we use them for different emphases.

We often replace a node in the tree by another tree representing the "value" of the original node. Examples:

We call this resolving the global variable, operation, etc. Note that this does not change the basic "layout" of the tree.

On the contrary, in the following examples we change the "layout" of the tree:

We call this inlining the function arguments, functions, or variable assignments.

1.2 Capabilities of the compiler

The compilation process has two phases: the resolving phase and the rule phase.

During the resolving phase, operations and global variables are resolved.

For details see CapJitResolvedOperations (2.5-21) and CapJitResolvedGlobalVariables (2.5-20). If no operation or global variable can be resolved anymore, we continue with the rule phase.

In the rule phase, the tree is optimized using several rules and techniques. Function arguments, functions, and assignments to local variables are inlined. Unused variables are dropped. Handled edge cases are dropped, that is, if the same edge case is caught multiple times via if condition then return ...; fi; statements, only the first such statement is kept. Finally, "logic" is applied to the tree. For example, calls of CallFuncList are replaced by calls to the actual function. The logic can be extended by the user, see chapter 2.

For all details, see the list of compilations steps in 2.5.

1.3 Requirements

There are some requirements for the steps described above to be correct.

The code must be purely functional, that is, it must have the following properties:

GAP has strict semantics, that is, the evaluation of an expression first evaluates all subexpressions, and if an error occurs during the evaluation of a subexpression, the evaluation of the outer expression also stops. However, CompilerForCAP has some optimizations which are only valid with non-strict semantics. These optimizations produce subexpression which are not computed in the original code and are not needed for the final result. With GAP's strict semantics, those subexpressions are still evaluated despite not being needed for the final result. Hence, those subexpressions must not throw an error when evaluated. In particular:

Furthermore, there are some technical restrictions:

Also note that technically the result of the compilation is only valid for the concrete CAP category which was used to resolve CAP operations and get typing information. That is, for parametric categories you must check manually for which parameters the result is valid.

1.4 Precompiling categories

The main mode of application of the compiler is precompiling categories and storing the result in a file for later use via CapJitPrecompileCategory (1.4-1).

1.4-1 CapJitPrecompileCategory
‣ CapJitPrecompileCategory( category_constructor, given_arguments, package_name, compiled_category_name )( function )

Compiles operations of the CAP category returned by the function category_constructor applied to given_arguments. The result is available via a global function called ADD_FUNCTIONS_FOR_compiled_category_name which is written to the file package_name/precompiled_categories/ and adds the compiled functions to the category given as the only argument. For testing purposes, there is also a global function called compiled_category_name which takes the same arguments as category_constructor and returns the category with the compiled functions installed (note: category_constructor is called with no_precompiled_code := true, which might lead to uncompiled code being present in lower categories of a tower of categories). If a list of operations is given via the option operations, only operations in this list are precompiled. Else all installed operations (excluding operations which are part of suggested dependencies) of the category are precompiled. Furthermore, the options number_of_objectified_objects_in_data_structure_of_object, number_of_objectified_morphisms_in_data_structure_of_object, number_of_objectified_objects_in_data_structure_of_morphism, and number_of_objectified_morphisms_in_data_structure_of_morphism can optionally be set to allow the compiler to warn about about bad compilation results. For example, number_of_objectified_objects_in_data_structure_of_object should be the number of calls to CreateCapCategoryObjectWithAttributes or AsCapCategoryObject required for creating an object in the tower defined by category_constructor, e.g. 1 if the tower has height one, or 2 if the tower has height two and the objects of the category at the top are given by objects in the category one level below. Warnings will be displayed if this number is exceeded (because this implies that not all wrap-unwrap-pairs could be canceled). Technical requirements:

1.4-2 CapJitPrecompileCategoryAndCompareResult
‣ CapJitPrecompileCategoryAndCompareResult( category_constructor, given_arguments, package_name, compiled_category_name )( function )

Calls CapJitPrecompileCategory (1.4-1) with the given arguments and displays a warning if this changes the contents of package_name/precompiled_categories/

1.5 Compiling a function manually

One can also compile a function func manually via CapJitCompiledFunction (1.5-2).

1.5-1 CapJitCompiledCAPOperationAsEnhancedSyntaxTree
‣ CapJitCompiledCAPOperationAsEnhancedSyntaxTree( cat, operation_name, post_processing_enabled )( function )

A special version of CapJitCompiledFunctionAsEnhancedSyntaxTree (1.5-3) compiling the operation given by operation_name in cat. The boolean post_processing_enabled decides whether the tree before or after post-processing should be returned.

1.5-2 CapJitCompiledFunction
‣ CapJitCompiledFunction( func[, type_signature] )( function )

Returns: a function

Returns a compiled version of the function func with signature type_signature (see CapJitInferredDataTypes (2.5-10)). If func is an operation or a kernel function, it is returned unchanged. If type_signature is not given, all steps which require knowledge about the types of variables are skipped. If the first argument of func is a CAP category, the type signature can also be given by three separate arguments: an instance of a CAP category, a list of input filters (as in filter_list in the method name record) and an output filter (as in return_type in the method name record). If a full type signature is not available but the first argument of func is a CAP category, an instance of a CAP category can be given as the second argument. In this case, the category is used to get the type information required to resolve CAP operations.

1.5-3 CapJitCompiledFunctionAsEnhancedSyntaxTree
‣ CapJitCompiledFunctionAsEnhancedSyntaxTree( func, post_processing[, type_signature] )( function )

Returns: a record

Like CapJitCompiledFunction (1.5-2), but returns an enhanced syntax tree of the compiled function. func must not be an operation or a kernel function because those cannot properly be represented as a syntax tree. post_processing can be one of the following strings:

1.6 Giving hints to the compiler

You can give hints to the compiler to improve the result of the compilation. Compiler hints are attached to the category by making category!.compiler_hints a record with one or more of the following keys:

Note: The compiler can only discover the hints if the category is the first argument of the function.

1.7 Stopping the compiler at a certain level

You can use StopCompilationAtCategory to prevent the compiler from inlining and optimizing code of a given category. You can revert this decision using ContinueCompilationAtCategory.

1.7-1 StopCompilationAtCategory
‣ StopCompilationAtCategory( category )( function )

Stops the compiler from inlining and optimizing code of category.

1.7-2 ContinueCompilationAtCategory
‣ ContinueCompilationAtCategory( category )( function )

Allows the compiler to inline and optimize code of category (this is the default).

1.7-3 StopCompilationAtPrimitivelyInstalledOperationsOfCategory
‣ StopCompilationAtPrimitivelyInstalledOperationsOfCategory( category )( function )

Stops the compiler from inlining and optimizing code of primitively installed operations of category. Warning: Due to caching of compiled CAP operations, this has to be called before any compilation involving category.

1.7-4 ContinueCompilationAtPrimitivelyInstalledOperationsOfCategory
‣ ContinueCompilationAtPrimitivelyInstalledOperationsOfCategory( category )( function )

Allows the compiler to inline and optimize code of primitively installed operations of category (this is the default).

1.8 Disabling the automatic inference of data types

1.8-1 CapJitDisableDataTypeInference
‣ CapJitDisableDataTypeInference( )( function )
‣ CapJitEnableDataTypeInference( )( function )

In case of errors, the automatic inference of data types can be disabled (and re-enabled later on).

1.9 Compiling step-by-step

1.9-1 CapJitEnableStepByStepCompilation
‣ CapJitEnableStepByStepCompilation( )( function )
‣ CapJitDisableStepByStepCompilation( )( function )

Enables or disables step-by-step compilation for demonstration or debugging purposes. If enabled, only the first level of CAP operations and known methods is resolved (instead of resolving recursively). Caveats:

1.10 Proof assistant mode

1.10-1 CapJitEnableProofAssistantMode
‣ CapJitEnableProofAssistantMode( )( function )
‣ CapJitDisableProofAssistantMode( )( function )

(experimental) Enables or disables the (experimental) proof assistant mode. For example, in this mode the compiler will display warnings if the code involves CAP operations which are not known to be compatible with the congruence of morphisms, and expressions will not be hoisted or deduplicated.

1.10-2 StateLemma
‣ StateLemma( description, claim, category, filter_strings, preconditions )( operation )

(experimental) States a new categorical lemma to be proven in proof assistant mode.

The aim is to reduce the function claim to {...} -> true by applying logic templates via ApplyLogicTemplate (1.10-5).

1.10-3 PrintLemma
‣ PrintLemma( )( operation )

(experimental) Prints the state of the current lemma.

1.10-4 AttestValidInputs
‣ AttestValidInputs( )( operation )

(experimental) Lets the user attest that all arguments in function calls in the state of the current lemma form valid inputs for the functions, for example, that two morphisms passed to PreCompose are actually composable. This allows CompilerForCAP to simplify type checks, for example, that the return value of the call to PreCompose is a well-defined morphism.

1.10-5 ApplyLogicTemplate
‣ ApplyLogicTemplate( logic_template )( operation )

(experimental) Applies a logic template to the state of the current lemma. If number_of_applications is not set, it defaults to 1.

1.10-6 ApplyLogicTemplateNTimes
‣ ApplyLogicTemplateNTimes( n, logic_template )( operation )

(experimental) Applies a logic template n times to the state of the current lemma. Note: number_of_applications must not be set.

1.10-7 AssertLemma
‣ AssertLemma( )( operation )

(experimental) Asserts that the current lemma is proven, that is, that the state of the current lemma is {...} -> true. If this is the case, the current lemma is cleared, which allows a new lemma to be stated.

1.10-8 StateProposition
‣ StateProposition( category, proposition_id )( operation )

(experimental) States a new proposition to be proven for the category category. Valid IDs are the entries of RecNames( CAP_JIT_INTERNAL_PROOF_ASSISTANT_PROPOSITIONS ). A proposition is a collection of lemmata which can be stated using StateNextLemma (1.10-9) and can then be proven in the same way as a lemma stated using StateLemma (1.10-2).

1.10-9 StateNextLemma
‣ StateNextLemma( )( operation )

(experimental) States the next lemma of the current proposition.

1.10-10 AssertProposition
‣ AssertProposition( )( operation )

(experimental) Asserts that the current proposition is proven, that is, that all lemmata of the current proposition are proven.

1.11 Getting information about the compilation process

You can increase the info level of InfoCapJit to get information about the compilation process.

1.11-1 InfoCapJit
‣ InfoCapJit( info class )

Info class used for info messsages of the CAP compiler.

1.11-2 CapJitSetDebugLevel
‣ CapJitSetDebugLevel( level )( function )

Set the debug level. At level 0, no debug information is printed. At level 1 (or higher), compiled functions are printed at the beginning of the compilation, before the resolving phase, before the rule phase, before the post-processing starts, and at the end of the compilation. At level 2 (or higher), compiled functions are printed after every compilation step. These levels are not fixed and may change in the future.

1.12 FAQ

A: During compilation, attributes of categories are resolved, that is, their values are stored in global variables without keeping track of which category they belong to. After the compilation, CompilerForCAP tries to replace those global variables again by attributes registered via category_attribute_names to the current category (for details, see 1.6). If some attributes of the current category are categories themselves, their attributes are also taken into account (recursively). In this case, if two categories cat1 and cat2 have attributes Attr1 and Attr2, respectively, with the same value, it is undefined whether Attr1( cat1 ) or Attr2( cat2 ) will be used. So even if only Attr2( cat2 ) appeared in the original code, Attr1( cat1 ) might appear in the compiled code.

A: The function might be listed in CAP_JIT_NON_RESOLVABLE_GLOBAL_VARIABLE_NAMES or it might be missing an annotation with the pragma CAP_JIT_RESOLVE_FUNCTION. Additionally, a function can only be resolved if it appears as a global variable in the tree during the resolving phase of the compilation. That is, it must be referenced from a global variable from the beginning on, or after global variables are resolved by CapJitResolvedGlobalVariables (2.5-20). Possibly you have adapt CapJitResolvedGlobalVariables (2.5-20) to your setting.

A: For reasons of correctness, variables cannot be inlined if a variable is assigned more than once in the body of a function (this includes function arguments which are assigned at least once, namely when the function is called). An exception is made for "rapid reassignments": if the same variable is assigned and then reassigned immediately in the next statement, this only counts as a single assignment.

A: We can only drop unused variables, inline variables, etc. if we assume that the code contains no side effects. Statements like STAT_PROCCALL or assignment to higher variables cause (or at least indicate) side effects, so continuing with the compilation would probably not lead to a correct result.

A: There are various possible reasons for this:

 [Top of Book]  [Contents]   [Previous Chapter]   [Next Chapter] 
Goto Chapter: Top 1 2 3 Ind

generated by GAPDoc2HTML