|
Type summary |
---|
|
Value summary |
---|
|
|
|
|
Type detail |
---|
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 typed program in a file ".rev.loop".*)
printTyped : bool,
(* asks the compiler to write the complete infered proof in a file ".proof".*)
printProof : bool,
(* asks the compiler to write the types as formulas.*) formula : bool,
(* asks the compiler to write the output for further tex compilation.*)
tex : bool,
(* asks the compiler to write the complete infered proof in a file ".loop.ott" for ott/twelf compilation.*)
ott : bool
}
Value detail |
---|
fun print_verb params level mess
params
level
mess
fun writeFile name strList
name
strList
fun printParams params
params
fun compile params : compilerParams -> unit
params
|