Compile (p.lambdapi.2.0.0.doc.lambdapi.handle.Handle.Compile)

Sourceval gen_obj : bool ref

gen_obj indicates whether we should generate object files when compiling source files. The default behaviour is not te generate them.

Sourceval parse_file : string -> Parsing.Syntax.ast

parse_file fname selects and runs the correct parser on file fname, by looking at its extension.

Source

val compile_with : 
  handle:
    (Command.compiler ->
      Core.Sig_state.t ->
      Parsing.Syntax.p_command ->
      Core.Sig_state.t) ->
  force:bool ->
  Command.compiler

compile_with ~handle ~force mp compiles the file corresponding to module path mp using function ~handle to process commands. Module mp is processed when it is necessary, i.e. the corresponding object file does not exist, or it must be updated, or ~force is true. In that case, the produced signature is stored in the corresponding object file if the option --gen_obj or -c is set.

Sourceval compile : bool -> Command.compiler

compile force mp compiles module path mp using compile_with, forcing compilation of up-to-date files if force is true.

Sourceval recompile : bool ref

recompile indicates whether we should recompile files who have an object file that is already up to date. Note that this flag only applies to files that are given on the command line explicitly, not their dependencies.

Sourceval compile_file : string -> Core.Sign.t

compile_file fname is the main compiling function. It is called from the main program exclusively.

Sourcemodule Pure : sig ... end

Pure wrappers around compilation functions. Functions provided perform the same computations as the ones defined earlier, but restores the state when they have finished. An optional library mapping or state can be passed as argument to change the settings.