-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/


-- | Disciplined Disciple Compiler top-level driver.
--   
--   This defines the top-level commands supported by the compiler, such as
--   <tt>-make</tt> and <tt>-compile</tt>.
@package ddc-driver
@version 0.4.2.2

module DDC.Driver.Output

-- | Output a document to the console.
outDoc :: Doc -> IO ()

-- | Output a document and newline to the console.
outDocLn :: Doc -> IO ()

-- | Output a string to the console.
outStr :: String -> IO ()

-- | Output a string and newline to the console.
outStrLn :: String -> IO ()

-- | Output chatty <tt>ok</tt> type responses. These are only displayed in
--   the Interactive and Batch interfaces.
chatStrLn :: String -> IO ()

module DDC.Driver.Interface.Source

-- | Where some source code was obtained from.
--   
--   This is used when generating error messages.
data Source

-- | Read directly from a file.
SourceFile :: FilePath -> Source

-- | Supplied on the command line.
SourceArgs :: Source

-- | Typed into the console.
SourceConsole :: Int -> Source

-- | Part of a <tt>.dcx</tt> batch file.
SourceBatch :: FilePath -> Int -> Source

-- | Get the starting source line number to report for this source.
lineStartOfSource :: Source -> Int

-- | Get the name of a source.
nameOfSource :: Source -> String
instance GHC.Show.Show DDC.Driver.Interface.Source.Source
instance GHC.Classes.Eq DDC.Driver.Interface.Source.Source

module DDC.Driver.Command.RewriteRules

-- | Load and typecheck a module's rewrite rules, using exported and
--   imported definitions from module
cmdTryReadRules :: (Ord n, Show n, Pretty n, NFData n) => Fragment n err -> FilePath -> Module () n -> IO (NamedRewriteRules () n)

module DDC.Driver.Interface.Input

-- | What interface is being used.
data InputInterface

-- | Read commands from unix command-line args.
InputInterfaceArgs :: InputInterface

-- | Read commands interactively from the console.
InputInterfaceConsole :: InputInterface

-- | Read commands from the file with this name.
InputInterfaceBatch :: FilePath -> InputInterface
data InputState command
InputState :: (String -> Maybe (command, String)) -> Input -> Maybe (Maybe command, Int) -> Int -> String -> InputState command
[inputParseCommand] :: InputState command -> String -> Maybe (command, String)
[inputMode] :: InputState command -> Input
[inputCommand] :: InputState command -> Maybe (Maybe command, Int)
[inputLineNumber] :: InputState command -> Int
[inputAcc] :: InputState command -> String

-- | How we're reading the current expression.
data Input

-- | Read input line-by-line, using a backslash at the end of the line to
--   continue to the next.
InputLine :: Input

-- | Read input as a block terminated by a double semicolon (;;)
InputBlock :: Input

-- | Read input from a file specified on the prompt
InputFile :: FilePath -> Input

-- | Read the input mode from the front of a string.
readInput :: String -> (Input, String)
inputLine :: InputInterface -> InputState c -> String -> IO (InputState c, Maybe (Source, Maybe c, String))
instance GHC.Show.Show DDC.Driver.Interface.Input.Input
instance GHC.Classes.Eq DDC.Driver.Interface.Input.Input
instance GHC.Show.Show DDC.Driver.Interface.Input.InputInterface
instance GHC.Classes.Eq DDC.Driver.Interface.Input.InputInterface

module DDC.Driver.Config

-- | Configuration for main compiler stages.
data Config
Config :: Bool -> Bool -> Bool -> Simplifier Int () Name -> ViaBackend -> Config -> RuntimeLinkStrategy -> Builder -> ConfigPretty -> Bool -> [FilePath] -> Maybe FilePath -> Maybe FilePath -> Bool -> Bool -> Bool -> Bool -> Config

-- | Print status to console during builds.
[configLogBuild] :: Config -> Bool

-- | Dump intermediate code.
[configDump] :: Config -> Bool

-- | Use bidirectional type inference on the input code.
[configInferTypes] :: Config -> Bool

-- | Simplifiers to apply to intermediate code
[configSimplSalt] :: Config -> Simplifier Int () Name

-- | Backend code generator to use
[configViaBackend] :: Config -> ViaBackend

-- | Runtime system configuration
[configRuntime] :: Config -> Config

-- | Linking strategy for the runtime.
[configRuntimeLinkStrategy] :: Config -> RuntimeLinkStrategy

-- | The builder to use for the target architecture
[configBuilder] :: Config -> Builder

-- | Core langauge pretty printer configuration.
[configPretty] :: Config -> ConfigPretty

-- | Suppress the #import prelude in C modules
[configSuppressHashImports] :: Config -> Bool

-- | Base directories to look for modules sources during build.
[configModuleBaseDirectories] :: Config -> [FilePath]

-- | Override output file
[configOutputFile] :: Config -> Maybe FilePath

-- | Override directory for build products
[configOutputDir] :: Config -> Maybe FilePath

-- | Keep intermediate .ddc.ll files
[configKeepLlvmFiles] :: Config -> Bool

-- | Keep intermediate .ddc.c files
[configKeepSeaFiles] :: Config -> Bool

-- | Keep intermediate .ddc.s files
[configKeepAsmFiles] :: Config -> Bool

-- | Avoid running the type checker where possible. When debugging program
--   transformations, use this to get the invalid code rather than just the
--   type error message.
[configTaintAvoidTypeChecks] :: Config -> Bool

-- | Core language pretty printer configuration.
data ConfigPretty
ConfigPretty :: Bool -> Bool -> Bool -> Bool -> Bool -> Bool -> ConfigPretty
[configPrettyUseLetCase] :: ConfigPretty -> Bool
[configPrettyVarTypes] :: ConfigPretty -> Bool
[configPrettyConTypes] :: ConfigPretty -> Bool
[configPrettySuppressImports] :: ConfigPretty -> Bool
[configPrettySuppressExports] :: ConfigPretty -> Bool
[configPrettySuppressLetTypes] :: ConfigPretty -> Bool

-- | Default pretty printer configuration.
defaultConfigPretty :: ConfigPretty

-- | Convert a the pretty configuration into the mode to use to print a
--   module. We keep the <a>ConfigPretty</a> type separate from PrettyMode
--   because the former can be non-recursive with other types, and does not
--   need to be parameterised by the annotation or name types.
prettyModeOfConfig :: (Eq n, Pretty n) => ConfigPretty -> PrettyMode (Module a n)

-- | Given the name of a source file, determine the name of the associated
--   object file.
objectPathOfConfig :: Config -> FilePath -> FilePath

-- | Given the name of a source file, determine the name of an associated
--   executable file.
exePathOfConfig :: Config -> FilePath -> FilePath
data ViaBackend

-- | Compile via the C backend.
ViaC :: ViaBackend

-- | Compile via the LLVM backend.
ViaLLVM :: ViaBackend
data RuntimeLinkStrategy

-- | Use the platform's default strategy.
LinkDefault :: RuntimeLinkStrategy

-- | Link the runtime statically.
LinkStatic :: RuntimeLinkStrategy
instance GHC.Classes.Eq DDC.Driver.Config.RuntimeLinkStrategy
instance GHC.Show.Show DDC.Driver.Config.RuntimeLinkStrategy
instance GHC.Show.Show DDC.Driver.Config.ViaBackend

module DDC.Driver.Dump

-- | If the Dump mode is set then produce a SinkFile to write a module to a
--   file, otherwise produce SinkDiscard to drop it on the floor.
dump :: Config -> Source -> String -> Sink

module DDC.Driver.Command.Read

-- | Load and typecheck a module.
cmdReadModule :: (Ord n, Show n, Pretty n, Pretty (err (AnTEC SourcePos n)), NFData n) => Config -> Fragment n err -> FilePath -> IO (Maybe (Module (AnTEC SourcePos n) n))
cmdReadModule' :: (Ord n, Show n, Pretty n, Pretty (err (AnTEC SourcePos n)), NFData n) => Bool -> Config -> Fragment n err -> FilePath -> IO (Maybe (Module (AnTEC SourcePos n) n))

module DDC.Driver.Stage.Flow

-- | Type check Core Flow.
stageFlowLoad :: Config -> Source -> [PipeCore () Name] -> PipeText Name Error

-- | Prepare a Core Flow module for lowering.
stageFlowPrep :: Config -> Source -> [PipeCore () Name] -> PipeCore () Name

-- | Perform rate inference to transform vector operations to series
stageFlowRate :: Config -> Source -> [PipeCore () Name] -> PipeCore () Name

-- | Lower a Core Flow module. Is needs to already be prepped, and have
--   full type annotations.
stageFlowLower :: Config -> Config -> Source -> [PipeCore () Name] -> PipeCore (AnTEC () Name) Name

-- | Wind loop primops into tail recursive loops in a Core Flow module.
stageFlowWind :: Config -> Source -> [PipeCore () Name] -> PipeCore (AnTEC () Name) Name

-- | Wind loop primops into tail recursive loops in a Core Flow module.
stageFlowToTetra :: Config -> Source -> [PipeCore () Name] -> PipeCore (AnTEC () Name) Name

module DDC.Driver.Stage.Salt

-- | Load and type check a Core Salt module.
stageSaltLoad :: Config -> Source -> [PipeCore () Name] -> PipeText Name Error

-- | Optimise Core Salt.
stageSaltOpt :: Config -> Source -> [PipeCore () Name] -> PipeCore () Name

-- | Convert Core Salt to C code.
stageSaltToC :: Config -> Source -> Sink -> PipeCore () Name

-- | Convert Core Salt to LLVM.
stageSaltToLLVM :: Config -> Source -> [PipeLlvm] -> PipeCore () Name

-- | Compile Core Salt via C code.
stageCompileSalt :: Config -> Source -> FilePath -> Bool -> PipeCore () Name

-- | Compile LLVM code.
stageCompileLLVM :: Config -> Source -> FilePath -> Maybe [FilePath] -> PipeLlvm

module DDC.Driver.Stage.Tetra

-- | Load and type check a Source Tetra module.
stageSourceTetraLoad :: Config -> Source -> Store -> [PipeCore (AnTEC SourcePos Name) Name] -> PipeText Name Error

-- | Load and type check a Core Tetra module.
stageTetraLoad :: Config -> Source -> [PipeCore () Name] -> PipeText Name Error

-- | Convert a Core Tetra module to Core Salt.
--   
--   This includes performing the Boxing transform.
stageTetraToSalt :: Config -> Source -> [PipeCore () Name] -> PipeCore () Name


-- | Compiler stages.
--   
--   A compiler stage is a sequence of standard transformations. Each of
--   the individual transformations are expressed as a pipeline from
--   <a>DDC.Build.Pipeline</a>. The stages here run several pipelines each,
--   and contain the code that can dump the intermediate program after each
--   transformation.
module DDC.Driver.Stage

-- | Configuration for main compiler stages.
data Config
Config :: Bool -> Bool -> Bool -> Simplifier Int () Name -> ViaBackend -> Config -> RuntimeLinkStrategy -> Builder -> ConfigPretty -> Bool -> [FilePath] -> Maybe FilePath -> Maybe FilePath -> Bool -> Bool -> Bool -> Bool -> Config

-- | Print status to console during builds.
[configLogBuild] :: Config -> Bool

-- | Dump intermediate code.
[configDump] :: Config -> Bool

-- | Use bidirectional type inference on the input code.
[configInferTypes] :: Config -> Bool

-- | Simplifiers to apply to intermediate code
[configSimplSalt] :: Config -> Simplifier Int () Name

-- | Backend code generator to use
[configViaBackend] :: Config -> ViaBackend

-- | Runtime system configuration
[configRuntime] :: Config -> Config

-- | Linking strategy for the runtime.
[configRuntimeLinkStrategy] :: Config -> RuntimeLinkStrategy

-- | The builder to use for the target architecture
[configBuilder] :: Config -> Builder

-- | Core langauge pretty printer configuration.
[configPretty] :: Config -> ConfigPretty

-- | Suppress the #import prelude in C modules
[configSuppressHashImports] :: Config -> Bool

-- | Base directories to look for modules sources during build.
[configModuleBaseDirectories] :: Config -> [FilePath]

-- | Override output file
[configOutputFile] :: Config -> Maybe FilePath

-- | Override directory for build products
[configOutputDir] :: Config -> Maybe FilePath

-- | Keep intermediate .ddc.ll files
[configKeepLlvmFiles] :: Config -> Bool

-- | Keep intermediate .ddc.c files
[configKeepSeaFiles] :: Config -> Bool

-- | Keep intermediate .ddc.s files
[configKeepAsmFiles] :: Config -> Bool

-- | Avoid running the type checker where possible. When debugging program
--   transformations, use this to get the invalid code rather than just the
--   type error message.
[configTaintAvoidTypeChecks] :: Config -> Bool
data ViaBackend

-- | Compile via the C backend.
ViaC :: ViaBackend

-- | Compile via the LLVM backend.
ViaLLVM :: ViaBackend
data RuntimeLinkStrategy

-- | Use the platform's default strategy.
LinkDefault :: RuntimeLinkStrategy

-- | Link the runtime statically.
LinkStatic :: RuntimeLinkStrategy

-- | Load and type check a Source Tetra module.
stageSourceTetraLoad :: Config -> Source -> Store -> [PipeCore (AnTEC SourcePos Name) Name] -> PipeText Name Error

-- | Load and type check a Core Tetra module.
stageTetraLoad :: Config -> Source -> [PipeCore () Name] -> PipeText Name Error

-- | Convert a Core Tetra module to Core Salt.
--   
--   This includes performing the Boxing transform.
stageTetraToSalt :: Config -> Source -> [PipeCore () Name] -> PipeCore () Name

-- | Type check Core Flow.
stageFlowLoad :: Config -> Source -> [PipeCore () Name] -> PipeText Name Error

-- | Prepare a Core Flow module for lowering.
stageFlowPrep :: Config -> Source -> [PipeCore () Name] -> PipeCore () Name

-- | Perform rate inference to transform vector operations to series
stageFlowRate :: Config -> Source -> [PipeCore () Name] -> PipeCore () Name

-- | Lower a Core Flow module. Is needs to already be prepped, and have
--   full type annotations.
stageFlowLower :: Config -> Config -> Source -> [PipeCore () Name] -> PipeCore (AnTEC () Name) Name

-- | Wind loop primops into tail recursive loops in a Core Flow module.
stageFlowWind :: Config -> Source -> [PipeCore () Name] -> PipeCore (AnTEC () Name) Name

-- | Wind loop primops into tail recursive loops in a Core Flow module.
stageFlowToTetra :: Config -> Source -> [PipeCore () Name] -> PipeCore (AnTEC () Name) Name

-- | Load and type check a Core Salt module.
stageSaltLoad :: Config -> Source -> [PipeCore () Name] -> PipeText Name Error

-- | Optimise Core Salt.
stageSaltOpt :: Config -> Source -> [PipeCore () Name] -> PipeCore () Name

-- | Convert Core Salt to C code.
stageSaltToC :: Config -> Source -> Sink -> PipeCore () Name

-- | Convert Core Salt to LLVM.
stageSaltToLLVM :: Config -> Source -> [PipeLlvm] -> PipeCore () Name

-- | Compile Core Salt via C code.
stageCompileSalt :: Config -> Source -> FilePath -> Bool -> PipeCore () Name

-- | Compile LLVM code.
stageCompileLLVM :: Config -> Source -> FilePath -> Maybe [FilePath] -> PipeLlvm

module DDC.Driver.Command.Flow.Concretize

-- | Concretize rate variables to loop indices.
cmdFlowConcretize :: Config -> Source -> String -> ExceptT String IO ()

module DDC.Driver.Command.Flow.Lower

-- | Lower a flow program to loop code.
cmdFlowLower :: Config -> Config -> Source -> String -> ExceptT String IO ()

module DDC.Driver.Command.Flow.Melt

-- | Thread a state token through the given flow program. This can't be
--   generic in the language fragment because we need to provide a specific
--   type to use for the world token, and new types for the effectful
--   combinators.
cmdFlowMelt :: Config -> Source -> String -> ExceptT String IO ()

module DDC.Driver.Command.Flow.Prep

-- | Prepare a Disciple Core Flow module for lowering.
cmdFlowPrep :: Config -> Source -> String -> ExceptT String IO ()

module DDC.Driver.Command.Flow.Rate

-- | Perform rate inference to transform vector operations to series
cmdFlowRate :: Config -> Source -> String -> ExceptT String IO ()

-- | Perform rate inference, then lower
cmdFlowRateLower :: Config -> Config -> Source -> String -> ExceptT String IO ()

module DDC.Driver.Command.Flow.Thread

-- | Thread a state token through the given flow program. This can't be
--   generic in the language fragment because we need to provide a specific
--   type to use for the world token, and new types for the effectful
--   combinators.
cmdFlowThread :: Config -> Source -> String -> ExceptT String IO ()

module DDC.Driver.Command.Flow.ToTetra

-- | Convert a module to Core Tetra. The output is printed to
--   <tt>stdout</tt>. Any errors are thrown in the <a>ExceptT</a> monad.
cmdFlowToTetraFromFile :: Config -> Config -> FilePath -> ExceptT String IO ()

-- | Convert some fragment of Disciple Core to Core Tetra. Works for the
--   <tt>Flow</tt> fragment. The result is printed to <tt>stdout</tt>. Any
--   errors are thrown in the <a>ExceptT</a> monad.
cmdFlowToTetraCoreFromFile :: Config -> Config -> Language -> FilePath -> ExceptT String IO ()

-- | Convert some fragment of Disciple Core to Core Tetra. Works for the
--   <tt>Tetra</tt> fragment. The result is printed to <tt>stdout</tt>. Any
--   errors are thrown in the <a>ExceptT</a> monad.
cmdFlowToTetraCoreFromString :: Config -> Config -> Language -> Source -> String -> ExceptT String IO ()
pipelineFlowToTetra :: Config -> Config -> Source -> [PipeCore () Name] -> PipeText Name Error

module DDC.Driver.Command.Flow.Wind

-- | Lower a flow program to loop code.
cmdFlowWind :: Config -> Source -> String -> ExceptT String IO ()

module DDC.Driver.Command.Tetra.Boxing

-- | Manage boxing in a Tetra module.
cmdTetraBoxing :: Config -> Source -> String -> ExceptT String IO ()

module DDC.Driver.Command.Tetra.Curry

-- | Manage higher order functions in a Tetra module.
cmdTetraCurry :: Config -> Source -> String -> ExceptT String IO ()

module DDC.Driver.Command.Parse

-- | Parse a module. The result AST is printed to <tt>stdout</tt>. Any
--   errors are thrown in the <a>ExceptT</a> monad.
--   
--   This function handle fragments of Disciple Core, as well as Source
--   Tetra modules. The language to use is determined by inspecting the
--   file name extension.
cmdParseFromFile :: Config -> FilePath -> ExceptT String IO ()

-- | Parse a Disciple Source Tetra module from a file. The result AST is
--   printed to <tt>stdout</tt>. Any errors are thrown in the
--   <a>ExceptT</a> monad.
cmdParseSourceTetraFromFile :: Config -> FilePath -> ExceptT String IO ()

-- | Parse a Disciple Core module from a file. The AST is printed to
--   <tt>stdout</tt>. Any errors are thrown in the <a>ExceptT</a> monad.
cmdParseCoreFromFile :: Config -> Language -> FilePath -> ExceptT String IO ()

module DDC.Driver.Build.Locate

-- | Locate the source file for a module, starting from the given list of
--   base paths. If the module cannot be found, or is found from multiple
--   paths then throw an error in the monad.
locateModuleFromPaths :: [FilePath] -> ModuleName -> String -> ExceptT String IO FilePath

module DDC.Driver.Command.Compile

-- | Recursively compile source modules into <tt>.o</tt> files, or load
--   existing interfaces if we have them and the <tt>.o</tt> file is still
--   fresh.
--   
--   <ul>
--   <li>Interface files that are loaded or generated during compilation
--   are added to the interface store.</li>
--   </ul>
cmdCompileRecursive :: Config -> Bool -> Store -> FilePath -> ExceptT String IO ()

-- | Recursively compile <tt>.ds</tt> source modules into <tt>.o</tt>
--   files, or load existing interfaces if we have them and the <tt>.o</tt>
--   file is still fresh.
--   
--   <ul>
--   <li>Interface files that are loaded or generated during compilation
--   are added to the interface store.</li>
--   </ul>
cmdCompileRecursiveDS :: Config -> Bool -> Store -> [FilePath] -> [FilePath] -> ExceptT String IO ()

-- | Load the interface correponding to a source file, or re-compile the
--   source if it's fresher than the interface.
--   
--   <ul>
--   <li>Interfaces for dependent modules must already be in the interface
--   store.</li>
--   </ul>
cmdLoadOrCompile :: Config -> Bool -> Store -> FilePath -> ExceptT String IO ()

-- | Compile a source module into a <tt>.o</tt> file.
--   
--   <ul>
--   <li>Interfaces for dependent modules must already be in the interface
--   store.</li>
--   <li>This produces an <tt>.o</tt> file next to the source file, and may
--   also produce a <tt>.di</tt> interface, depending on what sort of
--   source file we're compiling.</li>
--   <li>If compilation produces an interface then it is added to the
--   existing store.</li>
--   </ul>
cmdCompile :: Config -> Bool -> Store -> FilePath -> ExceptT String IO ()

-- | If the given file exists then get its modification time, otherwise
--   Nothing.
getModificationTimeIfExists :: FilePath -> IO (Maybe UTCTime)

module DDC.Driver.Build.Main

-- | Build all the components defined by a build spec.
buildSpec :: Config -> Store -> Spec -> ExceptT String IO ()

-- | Build a single component of a build spec.
buildComponent :: Config -> Store -> Component -> ExceptT String IO ()

-- | Build a single module.
buildModule :: Config -> Store -> ModuleName -> ExceptT String IO ()

module DDC.Driver.Command.BaseBuild
cmdBaseBuild :: Config -> Store -> ExceptT String IO ()

module DDC.Driver.Command.Build
cmdBuild :: Config -> Store -> FilePath -> ExceptT String IO ()

module DDC.Driver.Command.Check

-- | Parse and type-check a core module from a file, printing any errors to
--   <tt>stdout</tt>.
--   
--   This function handle fragments of Disciple Core, as well as Source
--   Tetra modules. The language to use is determined by inspecting the
--   file name extension.
cmdCheckFromFile :: Config -> Store -> FilePath -> ExceptT String IO ()

-- | Check a Disciple Source Tetra module from a file.
cmdCheckSourceTetraFromFile :: Config -> Store -> FilePath -> ExceptT String IO ()

-- | Check a Disciple Source Tetra module from a string. Any errors are
--   thrown in the <a>ExceptT</a> monad.
cmdCheckSourceTetraFromString :: Config -> Store -> Source -> String -> ExceptT String IO ()

-- | Check some fragment of Disciple core from a file.
cmdCheckCoreFromFile :: Config -> Language -> FilePath -> ExceptT String IO ()

-- | Parse and type-check a core module from a string.
cmdCheckCoreFromString :: (Ord n, Show n, Pretty n, Pretty (err (AnTEC SourcePos n))) => Fragment n err -> Source -> String -> Mode n -> ExceptT String IO (Module (AnTEC SourcePos n) n)

-- | Show the type of a type in the given universe.
cmdShowType :: Language -> Universe -> Source -> String -> IO ()

-- | Check if two types are equivlant.
cmdTypeEquiv :: Language -> Source -> String -> IO ()

-- | Parse a core spec, and return its kind.
cmdParseCheckType :: (Ord n, Show n, Pretty n, Pretty (err (AnTEC SourcePos n))) => Fragment n err -> Universe -> Source -> String -> IO (Maybe (Type n, Kind n))

-- | What mode we're performing type checking/inference in.
data Mode n :: * -> *

-- | Reconstruct the type of the expression, requiring type annotations on
--   parameters as well as type applications to already be present.
Recon :: Mode n

-- | The ascending smoke of incense. Synthesise the type of the expression,
--   producing unification variables for bidirectional type inference.
Synth :: Mode n

-- | The descending tongue of flame. Check the type of an expression
--   against this expected type, and unify expected types into unification
--   variables for bidirecional type inference.
Check :: Type n -> Mode n

-- | What components of the checked type to display.
data ShowSpecMode
ShowSpecAll :: ShowSpecMode
ShowSpecData :: ShowSpecMode
ShowSpecEffect :: ShowSpecMode
ShowSpecClosure :: ShowSpecMode

-- | Show the spec of an expression.
cmdShowSpec :: Language -> ShowSpecMode -> Bool -> Bool -> Source -> String -> IO ()

-- | Check expression and reconstruct type annotations on binders.
cmdExpRecon :: Language -> Source -> String -> IO ()

-- | Parse the given core expression, and return it, along with its type,
--   effect and closure.
--   
--   If the expression had a parse error, undefined vars, or type error
--   then print this to the console.
--   
--   We include a flag to override the language profile to allow partially
--   applied primitives. Although a paticular evaluator (or backend) may
--   not support partially applied primitives, we want to accept them if we
--   are only loading an expression to check its type.
cmdParseCheckExp :: (Ord n, Show n, Pretty n, Pretty (err (AnTEC SourcePos n))) => Fragment n err -> ModuleMap (AnTEC () n) n -> Mode n -> Bool -> Bool -> Source -> String -> IO (Maybe (Exp (AnTEC SourcePos n) n), Maybe CheckTrace)

-- | Show the type of a witness.
cmdShowWType :: Language -> Source -> String -> IO ()
instance GHC.Show.Show DDC.Driver.Command.Check.ShowSpecMode
instance GHC.Classes.Eq DDC.Driver.Command.Check.ShowSpecMode

module DDC.Driver.Command.Trans

-- | Load and transform a module or expression, and print the result to
--   <tt>stdout</tt>.
--   
--   If the source starts with the 'module' keyword then treat it as one,
--   otherwise treat it as an expression.
cmdTransDetect :: Config -> Language -> Bool -> Source -> String -> ExceptT String IO ()

-- | Load and transform a module, and print the result to <tt>stdout</tt>.
cmdTransModule :: Config -> Language -> Bool -> Source -> String -> ExceptT String IO ()

-- | Load and transfrom an expression and print the result to
--   <tt>stdout</tt>.
cmdTransExp :: Config -> Language -> Bool -> Source -> String -> ExceptT String IO ()

-- | Load an expression and apply the current transformation.
cmdTransExpCont :: Config -> Bool -> Language -> (forall n. Typeable n => Exp (AnTEC () n) n -> IO ()) -> Source -> String -> IO ()

-- | Transform an expression, or display errors
transExp :: (Eq n, Ord n, Pretty n, Show n, CompoundName n) => Bool -> Profile n -> KindEnv n -> TypeEnv n -> s -> Simplifier s (AnTEC () n) n -> Exp (AnTEC () n) n -> IO (Maybe (Exp (AnTEC () n) n))

module DDC.Driver.Command.Load

-- | Load and transform source code, interface, or build file.
--   
--   The result is printed to <tt>stdout</tt>. Any errors are thrown in the
--   <a>ExceptT</a> monad.
--   
--   This function handle fragments of Disciple Core, as well as Source
--   Tetra modules. The language to use is determined by inspecting the
--   file name extension.
--   
--   We also take the specification of a simplifier to apply to the module.
--   
--   For Source Tetra modules, dependent modules will be compiled, or their
--   interfaces loaded as needed.
cmdLoadFromFile :: Config -> Store -> Maybe String -> [FilePath] -> FilePath -> ExceptT String IO ()

-- | Load a Disciple Source Tetra module from a file. The result is printed
--   to <tt>stdout</tt>. Any errors are thrown in the <a>ExceptT</a> monad.
cmdLoadSourceTetraFromFile :: Config -> Store -> Bundle Int Name Error -> FilePath -> ExceptT String IO ()

-- | Load a Disciple Source Tetra module from a string. The result is
--   printed to <tt>stdout</tt>. Any errors are thrown in the
--   <a>ExceptT</a> monad.
cmdLoadSourceTetraFromString :: Config -> Store -> Bundle Int Name Error -> Source -> String -> ExceptT String IO ()

-- | Load a Disciple Core module from a file. The result is printed to
--   <tt>stdout</tt>.
cmdLoadCoreFromFile :: Config -> Language -> FilePath -> ExceptT String IO ()

-- | Load a Disciple Core module from a string. The result it printed to
--   <tt>stdout</tt>.
cmdLoadCoreFromString :: Config -> Language -> Source -> String -> ExceptT String IO ()

-- | Parse the simplifier defined in this string, and load it and all the
--   inliner templates into the language bundle.
cmdLoadSimplifier :: Config -> Language -> String -> [FilePath] -> ExceptT String IO Language

-- | Parse the simplifier defined in this string, and load it and all the
--   inliner templates into the bundle
cmdLoadSimplifierIntoBundle :: (Ord n, Show n, NFData n, Pretty n, Pretty (err (AnTEC SourcePos n))) => Config -> Bundle s n err -> String -> [FilePath] -> ExceptT String IO (Bundle s n err)

module DDC.Driver.Command.ToC

-- | Convert a module to C. The output is printed to <tt>stdout</tt>. Any
--   errors are thrown in the <a>ExceptT</a> monad.
cmdToSeaFromFile :: Config -> Store -> FilePath -> ExceptT String IO ()

-- | Convert Disciple Source Tetra to C. The result is printed to
--   <tt>stdout</tt>. Any errors are thrown in the <a>ExceptT</a> monad.
cmdToSeaSourceTetraFromFile :: Config -> Store -> FilePath -> ExceptT String IO ()

-- | Convert Disciple Source Tetra to C. The result is printed to
--   <tt>stdout</tt>. Any errors are thrown in the <a>ExceptT</a> monad.
cmdToSeaSourceTetraFromString :: Config -> Store -> Source -> String -> ExceptT String IO ()

-- | Parse, check and convert a Core module to Sea. Works for the
--   <tt>Tetra</tt>, and <tt>Salt</tt> fragments. The result is printed to
--   <tt>stdout</tt>. Any errors are thrown in the <a>ExceptT</a> monad.
cmdToSeaCoreFromFile :: Config -> Language -> FilePath -> ExceptT String IO ()

-- | Parse, check, and convert a module to C. The output is printed to
--   <tt>stdout</tt>. Any errors are thrown in the <a>ExceptT</a> monad.
cmdToSeaCoreFromString :: Config -> Language -> Source -> String -> ExceptT String IO ()

module DDC.Driver.Command.ToLlvm

-- | Convert a module to LLVM. The output is printed to <tt>stdout</tt>.
--   Any errors are thrown in the <a>ExceptT</a> monad.
cmdToLlvmFromFile :: Config -> Store -> FilePath -> ExceptT String IO ()

-- | Convert Disciple Source Tetra to LLVM. The result is printed to
--   <tt>stdout</tt>. Any errors are thrown in the <a>ExceptT</a> monad.
cmdToLlvmSourceTetraFromFile :: Config -> Store -> FilePath -> ExceptT String IO ()

-- | Convert Disciple Source Tetra to LLVM. The result is printed to
--   <tt>stdout</tt>. Any errors are thrown in the <a>ExceptT</a> monad.
cmdToLlvmSourceTetraFromString :: Config -> Store -> Source -> String -> ExceptT String IO ()

-- | Parse, check and convert a Core module to LLVM. Works for the
--   <tt>Tetra</tt>, and <tt>Salt</tt> fragments. The result is printed to
--   <tt>stdout</tt>. Any errors are thrown in the <a>ExceptT</a> monad.
cmdToLlvmCoreFromFile :: Config -> Language -> FilePath -> ExceptT String IO ()

-- | Parse, check and convert a Core module to LLVM. Works for the
--   <tt>Tetra</tt>, and <tt>Salt</tt> fragments. The result is printed to
--   <tt>stdout</tt>. Any errors are thrown in the <a>ExceptT</a> monad.
cmdToLlvmCoreFromString :: Config -> Language -> Source -> String -> ExceptT String IO ()

module DDC.Driver.Command.ToPHP

-- | Convert a module to PHP. The output is printed to <tt>stdout</tt>. Any
--   errors are thrown in the <a>ExceptT</a> monad.
cmdToPHPFromFile :: Config -> Store -> FilePath -> ExceptT String IO ()

-- | Convert Disciple Source Tetra to PHP. The result is printed to
--   <tt>stdout</tt>. Any errors are thrown in the <a>ExceptT</a> monad.
cmdToPHPSourceTetraFromFile :: Config -> Store -> FilePath -> ExceptT String IO ()

-- | Convert Disciple Source Tetra to PHP. The result is printed to
--   <tt>stdout</tt>. Any errors are thrown in the <a>ExceptT</a> monad.
cmdToPHPSourceTetraFromString :: Config -> Store -> Source -> String -> ExceptT String IO ()

-- | Parse, check and convert a Core module to PHP. Works for the
--   <tt>Tetra</tt>, and <tt>Salt</tt> fragments. The result is printed to
--   <tt>stdout</tt>. Any errors are thrown in the <a>ExceptT</a> monad.
cmdToPHPCoreFromFile :: Config -> Language -> FilePath -> ExceptT String IO ()

-- | Parse, check, and convert a module to PHP. The output is printed to
--   <tt>stdout</tt>. Any errors are thrown in the <a>ExceptT</a> monad.
cmdToPHPCoreFromString :: Config -> Language -> Source -> String -> ExceptT String IO ()

module DDC.Driver.Command.ToSalt

-- | Convert a module to Core Salt. The output is printed to
--   <tt>stdout</tt>. Any errors are thrown in the <a>ExceptT</a> monad.
cmdToSaltFromFile :: Config -> Store -> FilePath -> ExceptT String IO ()

-- | Convert Disciple Core Tetra to Disciple Core Salt. The result is
--   printed to <tt>stdout</tt>. Any errors are thrown in the
--   <a>ExceptT</a> monad.
cmdToSaltSourceTetraFromFile :: Config -> Store -> FilePath -> ExceptT String IO ()

-- | Convert Disciple Source Tetra to Disciple Core Salt. The result is
--   printed to <tt>stdout</tt>. Any errors are thrown in the
--   <a>ExceptT</a> monad.
cmdToSaltSourceTetraFromString :: Config -> Store -> Source -> String -> ExceptT String IO ()

-- | Convert some fragment of Disciple Core to Core Salt. Works for the
--   <tt>Tetra</tt> fragment. The result is printed to <tt>stdout</tt>. Any
--   errors are thrown in the <a>ExceptT</a> monad.
cmdToSaltCoreFromFile :: Config -> Language -> FilePath -> ExceptT String IO ()

-- | Convert some fragment of Disciple Core to Core Salt. Works for the
--   <tt>Tetra</tt> fragment. The result is printed to <tt>stdout</tt>. Any
--   errors are thrown in the <a>ExceptT</a> monad.
cmdToSaltCoreFromString :: Config -> Language -> Source -> String -> ExceptT String IO ()