mazeppa.mli

module Checked_oint = Checked_oint
module Symbol = Symbol
module Const = Const
module Raw_term = Raw_term
module Raw_program = Raw_program
module Gensym = Gensym

(** Something went wrong... *)
exception Panic of string

(** Supercompiles an input program to an equivalent output program. May raise {!Panic}
    during the process.

    You can call this function as many times as you want, including in parallel. *)
val supercompile : Raw_program.t -> Raw_program.t

(** Raises {!Panic} if a given program is not well-formed. To be used as a sanity check
    before {!supercompile} and {!eval}. *)
val check : Raw_program.t -> unit

(** Evaluates a given program to a value, as defined by the language semantics. May raise
    {!Panic} during the process.

    The input program must be well-formed as per the language definition. The [main]
    function must be defined with zero parameters. If any of these conditions is violated,
    the result is either {!Panic} or an incorrect value.

    Just as {!supercompile}, this function can be called in parallel. *)
val eval : Raw_program.t -> Raw_term.t

(** Translates a given Mazeppa program to C11 (with GNU extensions).

    [oc] is the output channel to which the resulting C code will be written. The input
    program must have the [main] function defined (otherwise, {!Panic} will be raised);
    [entry] will be the name of an [extern] C function that will correspond to your
    original [main]. If there is a scoping violation (such as referencing an undefined
    variable), {!Panic} will be raised.

    [entry] will be the only generated function with external linkage. For example, if
    your [main] function looks like this:

    [main(xs, ys, zs) := append(append(xs, ys), zs);]

    then the corresponding C function will have the following prototype:

    [extern mz_Value entry(mz_Value, mz_Value, mz_Value);]

    where [mz_Value] refers to the type definition from [mazeppa.h]. *)
val translate_to_c : oc:out_channel -> entry:Symbol.t -> Raw_program.t -> unit

(** Writes the contents of [mazeppa.h] to [oc].

    This header is required to compile any source file generated by {!translate_to_c}. *)
val mazeppa_h : out_channel -> unit

(**/**)

module Internals : sig
  module Parser = Parser
  module Lexer = Lexer
  module Util = Util
  module Symbol_map = Symbol_map
  module Subst = Subst
  module Term = Term
  module Program = Program
  module Homeomorphic_emb = Homeomorphic_emb
  module Msg = Msg
  module Converter = Converter
  module Supervisor = Supervisor
  module Visualizer = Visualizer
  module Residualizer = Residualizer
  module Pretty = Pretty
end

(**/**)