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 checking and on-demand functional translation.
|
val printParams
prints the compiling parameters values.
|
val print_verb
prints a message according to its importance and the requested verbosity.
|
val writeFile
prints a string list to a file.
|
compilerParams
type compilerParams =
{
(* the path of the source file which contains the imperative program ".loop".*)
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 ".cs".*)
printUntyped : bool,
(* asks the compiler to write the translated functional program in a file ".sml".*)
printFun : bool
}
-
The type of compiling parameters.
-
print_verb
fun print_verb params level mess
-
prints a message according to its importance and the requested verbosity.
-
- Parameters:
-
-
params
-
the compiling parameters containing the requested verbosity level.
-
level
-
the message verbosity level.
-
mess
-
the message to be printed.
writeFile
fun writeFile name strList
-
prints a string list to a file.
-
- Parameters:
-
-
name
-
the file name.
-
strList
-
the string list.
printParams
fun printParams params
-
prints the compiling parameters values.
-
- Parameters:
-
-
params
-
the compiling parameters.
compile
fun compile params : compilerParams -> unit
-
performs type checking and on-demand functional translation.
-
- Parameters:
-
-
params
-
the compiling parameters.