Overview  Index  Help 

COMPILER

All Known Implementing Modules:

Compiler


The First-Order LoopW Proof Checker compiler. The compiler calls several modules in order to perform the requested tasks.

     
Type summary

type compilerParams =
     {
        sourceFile : string,
        fileNamePrefix : string,
        verbLevel : int,
        printUntyped : bool,
        printFun : bool
     }

           The type of compiling parameters.

     
Value summary

val compile : compilerParams -> unit
           performs type inference and on-demand functional translation.

 

 
Type detail

compilerParams

type compilerParams =
     {
       (* the path of the source file which contains the imperative program ".proof".*)
       sourceFile : string,
       (* the source file name prefix.*) fileNamePrefix : string,
       (* the verbosity level (0: nothing, ..., 3: very verbose).*) verbLevel : int,
       (* asks the compiler to write the untyped program in a file ".pcs".*)
       printUntyped : bool,
       (* asks the compiler to write the translated functional program in a file ".sml".*)
       printFun : bool
     }

The type of compiling parameters.

     
Value detail

compile

fun compile params : compilerParams -> unit

performs type inference and on-demand functional translation.

Parameters:
params
the compiling parameters.

 


Overview  Index  Help