6. Internal aspects of the Resource Analysis

6.1. Translation from Hume to Schopenhauer

This section discusses aspects of the internal program transformation from Hume to Schopenhauer, that are relevant for the user of the resource analysis.

6.1.1. Input language restrictions

The translation of Hume code to Schopenhauer code, as a pre-requisite to resource analysis, imposes some restrictions on the input program that are not part of the Hume specification. Here we document these restrictions.

  • Upper-case constructors: Constructors of algebraic data-types, and \emph{only these\/}, must start with an upper-case letter.

  • No type polymorphism: In order to yield a suitable format for the resource analysis, all translated functions must have a monomorphic type. The translation generates monomorpic instances for all polymorphic, built-in types. However, it will fail on polymorphic, user-defined types. These have to be manually instantiated to their monomorphic types in the source program.

  • Type declarations for functions: In principle, all top-level defintions have to be accompanied by an explicit type declaration. In many cases Hume's type inference can infer the monomorphic type, and in these cases the translation will succeed. Common error messages from the translation, due to missing type declarations, complain about an unknown type or about having found a polymorphic type.

  • No vector size polymorphism: All vectors must have a fixed, explicitly declared type including a fixed size i.e.\ size polymorphism over vectors is not supported.

  • Deprecated 0-ary functions: 0-ary functions and constants are deprecated, since these can be problematic for the analysis. Instead, macros should be used when defining constants. In fact, the Hume compiler treats constants like macros, so the costs will be preserved.

  • Exceptions: Exceptions are supported in principle, but have not been tested thoroughly or validated, yet. In particular, raising an exception in a function, which is called from a box, will cause problems. By default, all \verb+raise+ expressions are translated to calls of special functions, which encode the exception handler code associated to the box. For uncaught, or expression-level exceptions, generic code is generated.

  • Pre-defined keywords and functions: Be aware of The symbols in Figure~\ref{fig:keywords} are Keywords and builtin function in Schopenhauer must not be used as identifiers in the source program. Note that some of these symbols are keywords only in Schopenhauer but not in Hume. See the ART3 Manual for full details

6.1.2. Limitations of the translation

Some known problems with the translation of general Hume code to Schopenhauer are documented here:

  • Nested patterns in functions and boxes can cause problems in the transformation, due to missing type information. Using explicit case expressions should get around this problem.

  • Groups of mutually recursive functions have to be placed in the same { ... } block in Schopenhauer. The experimental option -X to the phamc-an should group the functions appropriately. If this grouping doesn't succeed, and the type-checker of the analysis reports an ``unknown function'' which is part of the set of mutually recursive functions, the generated code must be edited manually to put all these functions into one group.

  • Using vecdef to define a vector can be difficult to cost, since it is a higher-order function. For the special case, that the initialisation function doesn't depend on the index, e.g. it is a constant for all slots in the vector, the option --vecdef-hack can be used with the phamc-an to produce tighter bounds.

6.2. Cost tables

The inference engine of the resource analysis is generic in the resource to be analysed. It is parameterised with a cost table, that models basic costs of the instruction in the Hume Abstract Machine. This section will eventually discuss the available cost tables.

6.3. Hume Abstract Machine

Hume code is compiled to code of the (Hume Abstract Machine).