Idris2-boot/idris2.ipkg

package idris2

modules = 
    Compiler.Common,
    Compiler.CompileExpr,
    Compiler.Inline,
    Compiler.Scheme.Chez,
    Compiler.Scheme.Chicken,
    Compiler.Scheme.Racket,
    Compiler.Scheme.Common,

    Control.Delayed,

    Core.AutoSearch,
    Core.Binary,
    Core.CaseBuilder,
    Core.CaseTree,
    Core.Context,
    Core.CompileExpr,
    Core.Core,
    Core.Coverage,
    Core.Directory,
    Core.Env,
    Core.FC,
    Core.GetType,
    Core.Hash,
    Core.LinearCheck,
    Core.Metadata,
    Core.Name,
    Core.Normalise,
    Core.Options,
    Core.Termination,
    Core.TT,
    Core.TTC,
    Core.Unify,
    Core.UnifyState,
    Core.Value,

    Data.ANameMap,
    Data.Bool.Extra,
    Data.IntMap,
    Data.IOArray,
    Data.NameMap,
    Data.StringMap,

    Idris.CommandLine,
    Idris.Desugar,
    Idris.Elab.Implementation,
    Idris.Elab.Interface,
    Idris.Error,
    Idris.IDEMode.CaseSplit,
    Idris.IDEMode.Commands,
    Idris.IDEMode.MakeClause,
    Idris.IDEMode.Parser,
    Idris.IDEMode.REPL,
    Idris.IDEMode.TokenLine,
    Idris.ModTree,
    Idris.Package,
    Idris.Parser,
    Idris.ProcessIdr,
    Idris.REPL,
    Idris.REPLCommon,
    Idris.REPLOpts,
    Idris.Resugar,
    Idris.SetOptions,
    Idris.Socket,
    Idris.Socket.Data,
    Idris.Socket.Raw,
    Idris.Syntax,

    Parser.Lexer,
    Parser.Support,

    Text.Lexer,
    Text.Lexer.Core,
    Text.Parser,
    Text.Parser.Core,
    Text.Quantity,
    Text.Token,

    TTImp.BindImplicits,
    TTImp.Elab,
    TTImp.Elab.Ambiguity,
    TTImp.Elab.App,
    TTImp.Elab.As,
    TTImp.Elab.Binders,
    TTImp.Elab.Case,
    TTImp.Elab.Check,
    TTImp.Elab.Dot,
    TTImp.Elab.Hole,
    TTImp.Elab.ImplicitBind,
    TTImp.Elab.Lazy,
    TTImp.Elab.Local,
    TTImp.Elab.Prim,
    TTImp.Elab.Record,
    TTImp.Elab.Rewrite,
    TTImp.Elab.Term,
    TTImp.Interactive.CaseSplit,
    TTImp.Interactive.ExprSearch,
    TTImp.Interactive.GenerateDef,
    TTImp.Interactive.MakeLemma,
    TTImp.Parser,
    TTImp.ProcessData,
    TTImp.ProcessDecls,
    TTImp.ProcessDef,
    TTImp.ProcessParams,
    TTImp.ProcessRecord,
    TTImp.ProcessType,
    TTImp.TTImp,
    TTImp.Unelab,
    TTImp.Utils,

    Utils.Binary,
    Utils.Shunting,

    Yaffle.Main,
    Yaffle.REPL

sourcedir = src
executable = idris2
-- opts = "--cg-opt -O2 --partial-eval"
-- opts = "--cg-opt -pg --partial-eval"
opts = "--partial-eval"

main = Idris.Main
Added Idris.Main 2019-06-07 13:29:29 +03:00			`package idris2`
Initial structure TT types and values, some text manipulation, basics of Core 2019-03-08 02:04:55 +03:00
			`modules =`
Add Compiler.Common This is generic compiler infrastructure (mainly finding all the names used from a root expression) 2019-06-06 20:13:25 +03:00			`Compiler.Common,`
Compiling to CExp 2019-06-05 23:25:03 +03:00			`Compiler.CompileExpr,`
Add inlining for CExps 2019-06-06 11:51:30 +03:00			`Compiler.Inline,`
Add Scheme back ends from Blodwen 2019-06-06 20:33:50 +03:00			`Compiler.Scheme.Chez,`
			`Compiler.Scheme.Chicken,`
			`Compiler.Scheme.Racket,`
			`Compiler.Scheme.Common,`
Compiling to CExp 2019-06-05 23:25:03 +03:00
Initial structure TT types and values, some text manipulation, basics of Core 2019-03-08 02:04:55 +03:00			`Control.Delayed,`

Initial implementation of auto implicit search This only searches for lambdas and locals so far, and doesn't take into account that it shouldn't search for holes, but it does set up the basic mechanism. 2019-04-27 22:18:53 +03:00			`Core.AutoSearch,`
Make a start on TTC reading/writing 2019-04-07 23:12:04 +03:00			`Core.Binary,`
Remove 'Case' from Term structure It seems that this isn't going to buy us enough to be worth the complications of compiling case trees, dealing with 'with' etc. 2019-04-19 22:10:55 +03:00			`Core.CaseBuilder,`
			`Core.CaseTree,`
Added context for global names, store in an array 2019-03-10 18:14:38 +03:00			`Core.Context,`
Add CompileExpr 2019-06-02 19:54:55 +03:00			`Core.CompileExpr,`
Initial structure TT types and values, some text manipulation, basics of Core 2019-03-08 02:04:55 +03:00			`Core.Core,`
Add Core.Coverage Little of the recently added bits are wired up yet, but it'll all start coming together soon. 2019-06-02 22:03:41 +03:00			`Core.Coverage,`
More progress on TTCs Added Core.Directory (more or less directly from Blodwen) and now writing out TTCs from the test Main, but it's still not writing out definitions because we're not yet making a note of the names which need saving (this will be the defined names and any holes introduced). Also it's clear from logging that holes/guess/constraints aren't being cleared so this needs to be fixed next. 2019-04-22 01:20:10 +03:00			`Core.Directory,`
Initial structure TT types and values, some text manipulation, basics of Core 2019-03-08 02:04:55 +03:00			`Core.Env,`
			`Core.FC,`
Support eta in unification Also added (necessarily) a rule for lambdas 2019-05-07 17:06:00 +03:00			`Core.GetType,`
Make a start on TTC reading/writing 2019-04-07 23:12:04 +03:00			`Core.Hash,`
First attempt at linearity checking pass This slows things down a bit because to find the holes and give them the right multiplicities, we need to normalise all the arguments which might have been metavariables. Maybe we should skip this if we're not using anything linear, for efficiency? As patterns are handled by deciding which side of the as is considered 'used'. In case blocks, that should be the variable name, but in general it should be the pattern, so IAs now has a flag to say which one. 2019-05-19 22:24:14 +03:00			`Core.LinearCheck,`
Add Metadata type Metadata is now propagated through the elaborator, although we're not using it yet 2019-05-31 07:52:54 +03:00			`Core.Metadata,`
Initial structure TT types and values, some text manipulation, basics of Core 2019-03-08 02:04:55 +03:00			`Core.Name,`
Make a start on TTC reading/writing 2019-04-07 23:12:04 +03:00			`Core.Normalise,`
			`Core.Options,`
Add termination checking Still to do: mutual data definitions and proper testing 2019-06-05 17:59:35 +03:00			`Core.Termination,`
Initial structure TT types and values, some text manipulation, basics of Core 2019-03-08 02:04:55 +03:00			`Core.TT,`
Make a start on TTC reading/writing 2019-04-07 23:12:04 +03:00			`Core.TTC,`
A bit of reorganisation Better to have the elaborator across multiple files, for ease of navigation. Also abandon the idea of local unification variables - we'll keep them global, and try let binding them on leaving a scope. 2019-03-18 19:25:53 +03:00			`Core.Unify,`
Start on UnifyState Also removed 'MV' as a special name type, and added a Meta constructor in TT which is applied to exactly the right number of arguments for the environment the meta was constructed in. It's possible the local unification UCtxt may be more trouble than it's worth! Instead perhaps we can try let binding unification solutions where possible on leaving the scope in which they're introduced. 2019-03-17 23:27:43 +03:00			`Core.UnifyState,`
Initial structure TT types and values, some text manipulation, basics of Core 2019-03-08 02:04:55 +03:00			`Core.Value,`

Add Implementation and Interface It turns out we need a new kind of map, mapping possibly ambiguous names to values. This is what 'Context' does but we can only have one of them because it resolves names to a position in an array and it'd be confusing to have more than one index per name. 2019-06-01 20:13:19 +03:00			`Data.ANameMap,`
Initial structure TT types and values, some text manipulation, basics of Core 2019-03-08 02:04:55 +03:00			`Data.Bool.Extra,`
Implement inferLambda This checks lambdas where the type isn't immediately a pi binder. First normalises, if that doesn't work, just guesses and unifies with the expected type. 2019-04-07 19:16:44 +03:00			`Data.IntMap,`
Added context for global names, store in an array 2019-03-10 18:14:38 +03:00			`Data.IOArray,`
Add specialised maps for Int and Name The repetition is unfortunate, but worth it for avoiding the overhead of passing an Ord dictionary around 2019-03-08 02:28:45 +03:00			`Data.NameMap,`
Initial structure TT types and values, some text manipulation, basics of Core 2019-03-08 02:04:55 +03:00			`Data.StringMap,`

Add package files 2019-06-07 13:14:45 +03:00			`Idris.CommandLine,`
Added Idris.Desugar Mostly adapted from Blodwen, also added necessary bits to the context such as name directives and hiding. 2019-06-01 16:11:21 +03:00			`Idris.Desugar,`
Add package files 2019-06-07 13:14:45 +03:00			`Idris.Elab.Implementation,`
			`Idris.Elab.Interface,`
Add more of the high level stuff 2019-06-01 17:05:04 +03:00			`Idris.Error,`
Bring in more bits of IDE mode 2019-06-02 17:38:39 +03:00			`Idris.IDEMode.CaseSplit,`
Add more of the high level stuff 2019-06-01 17:05:04 +03:00			`Idris.IDEMode.Commands,`
Add REPL 2019-06-07 13:08:21 +03:00			`Idris.IDEMode.MakeClause,`
Bring in more bits of IDE mode 2019-06-02 17:38:39 +03:00			`Idris.IDEMode.Parser,`
Added Idris.Main 2019-06-07 13:29:29 +03:00			`Idris.IDEMode.REPL,`
Bring in more bits of IDE mode 2019-06-02 17:38:39 +03:00			`Idris.IDEMode.TokenLine,`
More of the Idris machinery ModTree and ProcessIdr 2019-06-02 19:24:39 +03:00			`Idris.ModTree,`
Add package files 2019-06-07 13:14:45 +03:00			`Idris.Package,`
Add parser for high level syntax Almost entirely unchanged from Blodwen 2019-05-31 20:50:07 +03:00			`Idris.Parser,`
More of the Idris machinery ModTree and ProcessIdr 2019-06-02 19:24:39 +03:00			`Idris.ProcessIdr,`
Add REPL 2019-06-07 13:08:21 +03:00			`Idris.REPL,`
Add more of the high level stuff 2019-06-01 17:05:04 +03:00			`Idris.REPLCommon,`
			`Idris.REPLOpts,`
			`Idris.Resugar,`
Add package files 2019-06-07 13:14:45 +03:00			`Idris.SetOptions,`
Added Idris.Socket In preparation for REPL and IDE mode 2019-06-01 16:13:28 +03:00			`Idris.Socket,`
			`Idris.Socket.Data,`
			`Idris.Socket.Raw,`
Start on the high level syntax Copied and adapted Idris.Syntax from Blodwen, updated to cope with new core. 2019-05-31 20:48:04 +03:00			`Idris.Syntax,`

Initial structure TT types and values, some text manipulation, basics of Core 2019-03-08 02:04:55 +03:00			`Parser.Lexer,`
			`Parser.Support,`

			`Text.Lexer,`
			`Text.Lexer.Core,`
			`Text.Parser,`
			`Text.Parser.Core,`
			`Text.Quantity,`
Added parser for most basic terms Just variables, binders, applications, and basic declarations (data, type and function definitions) 2019-03-10 20:56:08 +03:00			`Text.Token,`

Added record declarations Also, since it could need it when building types, added auto implicit binding (so no need for $ everywhere in the tests from now on...) 2019-05-27 01:51:20 +03:00			`TTImp.BindImplicits,`
Unification infrastructure all done Can instantiate metavariables, although there's a lot of cases still to deal with 2019-04-06 15:53:59 +03:00			`TTImp.Elab,`
Expand ambiguous names This has exposed an issue with resolved name indexes when reading from ttc, which will be addressed shortly... 2019-05-11 14:19:39 +03:00			`TTImp.Elab.Ambiguity,`
A bit of reorganisation Better to have the elaborator across multiple files, for ease of navigation. Also abandon the idea of local unification variables - we'll keep them global, and try let binding them on leaving a scope. 2019-03-18 19:25:53 +03:00			`TTImp.Elab.App,`
Add as patterns When we encounter them, not that they're a binding as normal, but also record the thing they expand to. Then bind as a PLet, and convert that to a Let on the RHS so it has computational force. The case tree compiler knows about as patterns, so they get compiled to use the appropriate name on the rhs (rather than a let). 2019-05-09 18:46:16 +03:00			`TTImp.Elab.As,`
Progress on elaborator Changed 'check' so that it returns the type as a 'Glued', which is a pair of a term and its normalised form (or, more accurately, the process to generate each in Core). Sometimes the elaborator needs Term, sometimes in needs NF; this way we can return both but only actually generate it when its needed. So far, mostly done applications, binders and variables. Unification is still to do. 2019-03-23 17:13:49 +03:00			`TTImp.Elab.Binders,`
Implement dot patterns Like Idris 1, these are implicitly added on encountering a repeated name or a non-constructor application. Unlike Idris 1 (and Blodwen) they are checking by unification rather than matching (which means in particular that function argument names can't be bound in dot patterns) which is slightly less expressive, but better overall because matching is potentially more error prone. 2019-05-25 20:39:21 +03:00			`TTImp.Elab.Case,`
A bit of reorganisation Better to have the elaborator across multiple files, for ease of navigation. Also abandon the idea of local unification variables - we'll keep them global, and try let binding them on leaving a scope. 2019-03-18 19:25:53 +03:00			`TTImp.Elab.Check,`
Implement dot patterns Like Idris 1, these are implicitly added on encountering a repeated name or a non-constructor application. Unlike Idris 1 (and Blodwen) they are checking by unification rather than matching (which means in particular that function argument names can't be bound in dot patterns) which is slightly less expressive, but better overall because matching is potentially more error prone. 2019-05-25 20:39:21 +03:00			`TTImp.Elab.Dot,`
Added named holes Unlike in blodwen, it is okay for a named hole to be solved by unification. (Is this the right choice?) 2019-05-18 13:47:57 +03:00			`TTImp.Elab.Hole,`
Progress towards pattern matching Checking IBindVar and IBindHere, and first check of left hand side with implicitly bound pattern variables. 2019-04-18 16:51:04 +03:00			`TTImp.Elab.ImplicitBind,`
Implement laziness Slight change of plan: instead of having special names, add Lazy, Inf, Delay and Force and keywords and elaborate them specially. Correspondingly, add DelayCase for case trees. Given that implicit laziness is important, it seems better to do it this way than constantly check whether the name we're working with is important. This turns out to make implicit laziness much easier, because the unifier can flag whether it had to go under a 'Delayed' to succeed, and report that back to the elaborator which can then insert the necessary coercion. 2019-05-22 21:42:43 +03:00			`TTImp.Elab.Lazy,`
Implement local function definitions Changed nested names (and case blocks) to store the resolved name as the outer name, rather than the unresolved name, otherwise we'll have issues when loading from TTC 2019-05-13 02:44:28 +03:00			`TTImp.Elab.Local,`
Progress towards pattern matching Checking IBindVar and IBindHere, and first check of left hand side with implicitly bound pattern variables. 2019-04-18 16:51:04 +03:00			`TTImp.Elab.Prim,`
Add (dependent) record update This is pretty much straight from Blodwen 2019-05-27 12:56:13 +03:00			`TTImp.Elab.Record,`
Implement 'rewrite' expressions Mostly direct from Blodwen (some minor modifications to deal with new way of going into a new scope in the elaborator as well as the usual bits dealing with name lookup and Glued terms) 2019-05-27 14:15:37 +03:00			`TTImp.Elab.Rewrite,`
Added 'quick' unify Unification based only on constructor arguments and matching - anything else fails. Idea is to solve 'easy' local unification problems quickly, without having to create a global metavar applied to the current context. 2019-03-17 16:34:22 +03:00			`TTImp.Elab.Term,`
Add CaseSplit Adapted from Blodwen version 2019-06-01 21:05:02 +03:00			`TTImp.Interactive.CaseSplit,`
First attempt at expression search Not quite there yet because we're not saving all the information about holes in TTCs but the basics work 2019-06-02 00:34:59 +03:00			`TTImp.Interactive.ExprSearch,`
Add definition generation 2019-06-02 16:28:26 +03:00			`TTImp.Interactive.GenerateDef,`
Add MakeLemma 2019-06-02 16:41:21 +03:00			`TTImp.Interactive.MakeLemma,`
Added parser for most basic terms Just variables, binders, applications, and basic declarations (data, type and function definitions) 2019-03-10 20:56:08 +03:00			`TTImp.Parser,`
Unification infrastructure all done Can instantiate metavariables, although there's a lot of cases still to deal with 2019-04-06 15:53:59 +03:00			`TTImp.ProcessData,`
Added 'quick' unify Unification based only on constructor arguments and matching - anything else fails. Idea is to solve 'easy' local unification problems quickly, without having to create a global metavar applied to the current context. 2019-03-17 16:34:22 +03:00			`TTImp.ProcessDecls,`
Unification infrastructure all done Can instantiate metavariables, although there's a lot of cases still to deal with 2019-04-06 15:53:59 +03:00			`TTImp.ProcessDef,`
Add parameters blocks 2019-06-30 01:55:17 +03:00			`TTImp.ProcessParams,`
Added record declarations Also, since it could need it when building types, added auto implicit binding (so no need for $ everywhere in the tests from now on...) 2019-05-27 01:51:20 +03:00			`TTImp.ProcessRecord,`
Unification infrastructure all done Can instantiate metavariables, although there's a lot of cases still to deal with 2019-04-06 15:53:59 +03:00			`TTImp.ProcessType,`
Make a start on TTC reading/writing 2019-04-07 23:12:04 +03:00			`TTImp.TTImp,`
Add TTImp.Unelab This unelaborates things we don't even elaborate yet :). But we'll get there... 2019-05-06 19:33:08 +03:00			`TTImp.Unelab,`
Added record declarations Also, since it could need it when building types, added auto implicit binding (so no need for $ everywhere in the tests from now on...) 2019-05-27 01:51:20 +03:00			`TTImp.Utils,`
Make a start on TTC reading/writing 2019-04-07 23:12:04 +03:00
Add simple REPL for TTImp 2019-04-26 12:16:23 +03:00			`Utils.Binary,`
Added Idris.Desugar Mostly adapted from Blodwen, also added necessary bits to the context such as name directives and hiding. 2019-06-01 16:11:21 +03:00			`Utils.Shunting,`
Add simple REPL for TTImp 2019-04-26 12:16:23 +03:00
Added Idris.Main 2019-06-07 13:29:29 +03:00			`Yaffle.Main,`
Add simple REPL for TTImp 2019-04-26 12:16:23 +03:00			`Yaffle.REPL`
Initial structure TT types and values, some text manipulation, basics of Core 2019-03-08 02:04:55 +03:00
			`sourcedir = src`
Added Idris.Main 2019-06-07 13:29:29 +03:00			`executable = idris2`
Add timing logs Just to allow tracking how long individual parts of processing a file take! 2019-04-26 01:41:56 +03:00			`-- opts = "--cg-opt -O2 --partial-eval"`
Cache whether a local is let bound, if we can Since lookup up a binding can be expensive in a big environment, and we only need to reduce it if it turns out to be a let, caching it can be a noticeable win 2019-06-24 01:12:27 +03:00			`-- opts = "--cg-opt -pg --partial-eval"`
Update makefiles and paths We can now build and install the prelude, and hello world has successfully compiled to chez 2019-06-13 18:50:24 +03:00			`opts = "--partial-eval"`
Initial structure TT types and values, some text manipulation, basics of Core 2019-03-08 02:04:55 +03:00
Added Idris.Main 2019-06-07 13:29:29 +03:00			`main = Idris.Main`
Initial structure TT types and values, some text manipulation, basics of Core 2019-03-08 02:04:55 +03:00