Idris2-boot/yaffle.ipkg

package yaffle

modules = 
    Control.Delayed,

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

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

    Parser.Lexer,
    Parser.Support,

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

    TTImp.Elab,
    TTImp.Elab.App,
    TTImp.Elab.Binders,
    TTImp.Elab.Check,
    TTImp.Elab.ImplicitBind,
    TTImp.Elab.Prim,
    TTImp.Elab.Term,
    TTImp.Parser,
    TTImp.ProcessData,
    TTImp.ProcessDecls,
    TTImp.ProcessDef,
    TTImp.ProcessType,
    TTImp.TTImp,

    Utils.Binary

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,`

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,`
Make a start on TTC reading/writing 2019-04-07 23:12:04 +03:00			`Core.Hash,`
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,`

			`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,`

			`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,`

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,`
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,`
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,`
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,`
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,`
			`TTImp.Elab.Prim,`
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,`
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,`
			`TTImp.ProcessType,`
Make a start on TTC reading/writing 2019-04-07 23:12:04 +03:00			`TTImp.TTImp,`

			`Utils.Binary`
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