yaffle.ipkg

package yaffle

version = 0.6.0
sourcedir = "src"

modules
  = 
    -- Idris-specific compiler back ends
    Compiler.ANF,
    Compiler.CaseOpts,
    Compiler.Common,
    Compiler.CompileExpr,
    Compiler.Generated,
    Compiler.Inline,
    Compiler.LambdaLift,
    Compiler.NoMangle,
    Compiler.Separate,
    Compiler.VMCode,

    Compiler.Opts.ConstantFold,
    Compiler.Opts.CSE,
    Compiler.Opts.Identity,
    Compiler.Opts.InlineHeuristics,
    Compiler.Opts.ToplevelConstants,

-- Rest of this needs Idris pretty printing, so come back to it later
    Compiler.ES.Ast,
--     Compiler.ES.Codegen,
    Compiler.ES.Doc,
--     Compiler.ES.Javascript,
--     Compiler.ES.Node,
    Compiler.ES.State,
    Compiler.ES.TailRec,
    Compiler.ES.ToAst,

    Compiler.Interpreter.VMCode,

    Compiler.RefC,
    Compiler.RefC.CC,
    Compiler.RefC.RefC,

    Compiler.Scheme.Chez,
    Compiler.Scheme.ChezSep,
    Compiler.Scheme.Racket,
    Compiler.Scheme.Common,

    -- The Core 'Monad', a specialised IO+errors
    Core.Core,

    -- The core type theory and support
    Core.Binary,
    Core.Case.Builder,
    Core.Case.Patterns,
    Core.Case.Tree,
    Core.Case.Util,
    Core.Check.Erase,
    Core.Check.Linear,
    Core.Check.Typecheck,
    Core.Check.Support,
    Core.CompileExpr,
    Core.Context,
    Core.Context.Ctxt,
    Core.Context.CtxtData,
    Core.Context.Data,
    Core.Context.Def, -- top level definition forms live here
    Core.Error,
    Core.Evaluate,
    Core.Evaluate.Builtins,
    Core.Evaluate.Compile,
    Core.Evaluate.Convert,
    Core.Evaluate.Normalise,
    Core.Evaluate.Quote,
    Core.Evaluate.ToScheme,
    Core.Evaluate.Value,
    Core.FC,
    Core.InitPrimitives,
    Core.Options,
    Core.Ord,
    Core.Primitives,
    Core.Reflect,
    Core.Search,
    Core.Syntax.Decls, -- adding raw declarations to the context
    Core.Syntax.Lexer,
    Core.Syntax.Parser,
    Core.Syntax.Raw, -- raw unchecked syntax lives here
    Core.Syntax.Support,
    Core.Termination.CallGraph,
    Core.Termination.Positivity,
    Core.Termination.References,
    Core.Termination.SizeChange,
    Core.Termination,
    Core.Transform,
    Core.TT,
    Core.TT.Name,
    Core.TT.Namespace,
    Core.TT.RigCount,
    Core.TT.Traversals,
    Core.TT.TT, -- typechecked core language lives here
    Core.TT.Universes,
    Core.TT.Views,
    Core.TTC,
    Core.TTCFile,
    Core.Unify,
    Core.Unify.SolveMeta,
    Core.Unify.State,
    Core.Unify.Unify,
    Core.Warning,

    -- Idris front end
    Idris.CommandLine,
    Idris.Desugar,
    Idris.Desugar.Mutual,

    Idris.Doc.Annotations,
    Idris.Doc.Brackets,
    Idris.Doc.Display,
    Idris.Doc.Keywords,
    Idris.Doc.HTML,
    Idris.Doc.String,
    Idris.Driver,

    Idris.Elab.Interface,
    Idris.Elab.Implementation,

    Idris.Env,
    Idris.Error,
    Idris.Interactive.Completion,
    Idris.ModTree,

    Idris.Package,
    Idris.Package.Init,
    Idris.Package.Types,

    Idris.Parser,
    Idris.Parser.Let,
    Idris.Pretty,
    Idris.Pretty.Annotations,
    Idris.Pretty.CompileExpr,
    Idris.Pretty.Context,
    Idris.Pretty.Render,
    Idris.Pretty.TT,
    Idris.ProcessIdr,
    Idris.REPL,
    Idris.REPL.Common,
    Idris.REPL.FuzzySearch,
    Idris.REPL.Opts,
    Idris.Resugar,
    Idris.SetOptions,
    Idris.Syntax,
    Idris.Syntax.Builtin,
    Idris.Syntax.Pragmas,
    Idris.Syntax.TTC,
    Idris.Syntax.Traversals,
    Idris.Syntax.Views,

    Idris.Version,

    Idris.IDEMode.CaseSplit,
    Idris.IDEMode.Commands,
    Idris.IDEMode.Holes,
    Idris.IDEMode.MakeClause,
    Idris.IDEMode.Parser,
    Idris.IDEMode.Pretty,
    Idris.IDEMode.REPL,
    Idris.IDEMode.SyntaxHighlight,
    Idris.IDEMode.TokenLine,

    -- The language of TT with implicits
    TTImp.BindImplicits,
    TTImp.Impossible,
    TTImp.ProcessBuiltin,
    TTImp.ProcessData,
    TTImp.ProcessDecls.Totality,
    TTImp.ProcessDef,
    TTImp.ProcessDirective,
    TTImp.ProcessFailing,
    TTImp.ProcessFile,
    TTImp.ProcessRecord,
    TTImp.ProcessRunElab,
    TTImp.ProcessTransform,
    TTImp.ProcessType,
    TTImp.Reflect,
    TTImp.TTImp,
    TTImp.TTImp.Functor,
    TTImp.TTImp.Traversals,
    TTImp.TTImp.TTC,
    TTImp.Unelab,
    TTImp.Utils,
    TTImp.WithClause,

    -- Elaborating TTImp to the Core TT 
    TTImp.Elab,
    TTImp.Elab.Ambiguity,
    TTImp.Elab.App,
    TTImp.Elab.Binders,
    TTImp.Elab.Case,
    TTImp.Elab.Check,
    TTImp.Elab.Delayed,
    TTImp.Elab.Dot,
    TTImp.Elab.Hole,
    TTImp.Elab.ImplicitBind,
    TTImp.Elab.Lazy,
    TTImp.Elab.Local,
    TTImp.Elab.Prim,
    TTImp.Elab.Quote,
    TTImp.Elab.Record,
    TTImp.Elab.Rewrite,
    TTImp.Elab.RunElab,
    TTImp.Elab.Term,
    TTImp.Elab.Utils,

    -- Interactive editing machinery
    TTImp.Interactive.CaseSplit,
    TTImp.Interactive.ExprSearch,
    TTImp.Interactive.GenerateDef,
    TTImp.Interactive.Intro,
    TTImp.Interactive.MakeLemma,

    -- Parsing support
    Parser.Lexer.Common,
    Parser.Lexer.Package,
    Parser.Lexer.Source,

    Parser.Rule.Package,
    Parser.Rule.Source,

    Parser.Package,
    Parser.Source,
    Parser.Support,
    Parser.Unlit,

    Protocol.Hex,
    Protocol.IDE,
    Protocol.IDE.Command,
    Protocol.IDE.Decoration,
    Protocol.IDE.FileContext,
    Protocol.IDE.Formatting,
    Protocol.IDE.Highlight,
    Protocol.IDE.Holes,
    Protocol.IDE.Result,
    Protocol.SExp,
    Protocol.SExp.Parser,

    -- Things we'd expect in a base library, but since this project is the
    -- core of everything, include them here for bootstrapping.

    -- These are just copied from Idris 2. It will turn out that we don't
    -- need all of them, so (TODO) prune later.
    Libraries.Control.ANSI,
    Libraries.Control.ANSI.CSI,
    Libraries.Control.ANSI.SGR,
    Libraries.Control.Delayed,

    Libraries.Data.ANameMap,
    Libraries.Data.DList,
    Libraries.Data.Fin,
    Libraries.Data.Graph,
    Libraries.Data.IMaybe,
    Libraries.Data.IntMap,
    Libraries.Data.IOArray,
    Libraries.Data.IOMatrix,
    Libraries.Data.LengthMatch,
    Libraries.Data.List.Extra,
    Libraries.Data.List.Quantifiers.Extra,
    Libraries.Data.List.Lazy,
    Libraries.Data.List1,
    Libraries.Data.NameMap,
    Libraries.Data.NameMap.Traversable,
    Libraries.Data.PosMap,
    Libraries.Data.Primitives,
    Libraries.Data.Span,
    Libraries.Data.SortedMap,
    Libraries.Data.SortedSet,
    Libraries.Data.String.Extra,
    Libraries.Data.String.Iterator,
    Libraries.Data.StringMap,
    Libraries.Data.StringTrie,
    Libraries.Data.UserNameMap,
    Libraries.Data.Version,

    Libraries.System.File,
    Libraries.System.File.Buffer,
    Libraries.System.Directory.Tree,

    Libraries.Text.Bounded,
    Libraries.Text.Distance.Levenshtein,
    Libraries.Text.Lexer,
    Libraries.Text.Lexer.Core,
    Libraries.Text.Lexer.Tokenizer,
    Libraries.Text.Literate,
    Libraries.Text.Parser,
    Libraries.Text.Parser.Core,
    Libraries.Text.PrettyPrint.Prettyprinter,
    Libraries.Text.PrettyPrint.Prettyprinter.Doc,
    Libraries.Text.PrettyPrint.Prettyprinter.Render.HTML,
    Libraries.Text.PrettyPrint.Prettyprinter.Render.String,
    Libraries.Text.PrettyPrint.Prettyprinter.Render.Terminal,
    Libraries.Text.PrettyPrint.Prettyprinter.SimpleDocTree,
    Libraries.Text.PrettyPrint.Prettyprinter.Symbols,
    Libraries.Text.PrettyPrint.Prettyprinter.Util,
    Libraries.Text.Quantity,
    Libraries.Text.Token,

    Libraries.Utils.Octal,
    Libraries.Utils.Path,
    Libraries.Utils.Scheme,
    Libraries.Utils.Shunting,
    Libraries.Utils.String,
    Libraries.Utils.Term,

    TTMain.ProcessTT,
    TTMain.REPL,

    Yaffle.REPL

main = Idris.Main
executable = yaffle

depends = network

-- opts = "--profile"