Idris2-boot/yaffle.ipkg

package yaffle

modules = 
    Control.Delayed,

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

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

    Idris.Desugar,
    Idris.Error,
    Idris.IDEMode.Commands,
    Idris.Parser,
    Idris.REPLCommon,
    Idris.REPLOpts,
    Idris.Resugar,
    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.Parser,
    TTImp.ProcessData,
    TTImp.ProcessDecls,
    TTImp.ProcessDef,
    TTImp.ProcessRecord,
    TTImp.ProcessType,
    TTImp.TTImp,
    TTImp.Unelab,
    TTImp.Utils,

    Utils.Binary,
    Utils.Shunting,

    Yaffle.REPL

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

main = Yaffle.Main
Initial structure TT types and values, some text manipulation, basics of Core 2019-03-08 02:04:55 +03:00			`package yaffle`

			`modules =`
			`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,`
Initial structure TT types and values, some text manipulation, basics of Core 2019-03-08 02:04:55 +03:00			`Core.Core,`
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,`
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,`

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 more of the high level stuff 2019-06-01 17:05:04 +03:00			`Idris.Error,`
			`Idris.IDEMode.Commands,`
Add parser for high level syntax Almost entirely unchanged from Blodwen 2019-05-31 20:50:07 +03:00			`Idris.Parser,`
Add more of the high level stuff 2019-06-01 17:05:04 +03:00			`Idris.REPLCommon,`
			`Idris.REPLOpts,`
			`Idris.Resugar,`
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,`
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,`
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
			`Yaffle.REPL`
Initial structure TT types and values, some text manipulation, basics of Core 2019-03-08 02:04:55 +03:00
			`sourcedir = src`
Add a main program which processes a source file 2019-03-10 21:20:26 +03:00			`executable = yaffle`
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"`
Initial structure TT types and values, some text manipulation, basics of Core 2019-03-08 02:04:55 +03:00			`opts = "--partial-eval"`

Add a main program which processes a source file 2019-03-10 21:20:26 +03:00			`main = Yaffle.Main`
Initial structure TT types and values, some text manipulation, basics of Core 2019-03-08 02:04:55 +03:00