diff options
Diffstat (limited to 'pkgs/development/compilers/idris/idris.context')
| -rw-r--r-- | pkgs/development/compilers/idris/idris.context | 586 |
1 files changed, 0 insertions, 586 deletions
diff --git a/pkgs/development/compilers/idris/idris.context b/pkgs/development/compilers/idris/idris.context deleted file mode 100644 index fad6749988358..0000000000000 --- a/pkgs/development/compilers/idris/idris.context +++ /dev/null @@ -1,586 +0,0 @@ - -Context: - -[Missed SCTrans source! -eb@cs.st-andrews.ac.uk**20090511120315] - -[Put RunIO in a more sensible place -eb@cs.st-andrews.ac.uk**20090426144418] - -[Update cabal details -eb@cs.st-andrews.ac.uk**20090426144101] - -[Convert things which look like Nats to Nats for optimisation -eb@cs.st-andrews.ac.uk**20090423220551] - -[Basic Nat optimisation -eb@cs.st-andrews.ac.uk**20090423185609] - -[need to check if arguments are still needed to discriminate on collapsing -eb@cs.st-andrews.ac.uk**20090309174234] - -[Using knowledge of collapsing to help forcing -eb@cs.st-andrews.ac.uk**20090309153744] - -[Make transforms part of state, and display of optimised terms -eb@cs.st-andrews.ac.uk**20090309145419] - -[Prettier time formatting -eb@cs.st-andrews.ac.uk**20090309131334] - -[Don't just crash if the command is invalid... -eb@cs.st-andrews.ac.uk**20090309125424] - -[Added global options -eb@cs.st-andrews.ac.uk**20090309124541 - :o sets, :o f- or :o f+ to turn forcing/collapsing off/on - :o r- or :o r+ to turn display of compile/run times off/on -] - -[Added collapsing optimisation -eb@cs.st-andrews.ac.uk**20090309112238] - -[Added unused argument elimination -eb@cs.st-andrews.ac.uk**20090309004741 - Can fit within the optimisation framework, but you need to remember - the transforms so far at each definition for maximum effect. -] - -[(Failed) effort at argument erasure -eb@cs.st-andrews.ac.uk**20090308222948 - Trying to get it into the same framework as constructor transformations, - but it isn't going to happen that easily. -] - -[Added forcing optimisation -eb@cs.st-andrews.ac.uk**20090308164110] - -[Decide tactic works out its arguments -eb@cs.st-andrews.ac.uk**20090305165743] - -[Allow redefining of do notation -eb@cs.st-andrews.ac.uk**20090228164646] - -[lookupIdx fix -eb@cs.st-andrews.ac.uk**20090227231257] - -[Added 'using' syntax -eb@cs.st-andrews.ac.uk**20090226003439 - For blocks where lots of things use the same implicit arguments, saving - lots of typing and clutter. - (also allowed forward declaration of datatypes) -] - -[Fix conflict -eb@cs.st-andrews.ac.uk**20090107121727] - -[Laziness annotations -eb@cs.st-andrews.ac.uk**20090107121328] - -[Added decide tactic -eb@cs.st-andrews.ac.uk**20081220221809] - -[Add 'collapsible' flag -eb@cs.st-andrews.ac.uk**20081219180742] - -[Add TODO -eb@cs.st-andrews.ac.uk**20081219180726] - -[Some compiler fiddling -eb@cs.st-andrews.ac.uk**20081219155920] - -[Keep track of names which are still to be proved -eb@cs.st-andrews.ac.uk**20081219143302] - -[File operations -eb@cs.st-andrews.ac.uk**20081218233527] - -[Can allow the system to make up names for metavariables -eb@cs.st-andrews.ac.uk**20081218233428] - -[Deal with c includes and external libraries -eb@cs.st-andrews.ac.uk**20081126150921] - -[Fix foreign functions for IO -eb@cs.st-andrews.ac.uk**20081102153832] - -[Added Ptr primitive -eb@cs.st-andrews.ac.uk**20081102134232] - -[Add unsafePerformIO -eb@cs.st-andrews.ac.uk**20081019171546 - Mostly meant for pure foreign functions, but of course you're free to abuse - it as you like... -] - -[Add flags on functions to denote special behaviour -eb@cs.st-andrews.ac.uk**20081019160020 - Specifically, so far: - * %nocg Never generate code when compling - * %eval Evaluate completely before compiling - - This allows some 'meta-programs' to be written, which are fully evaluated - before compiling. We use this for defining foreign functions easily. -] - -[Record paper changes! -eb@cs.st-andrews.ac.uk**20080916170851] - -[Added 'use' tactic -eb@cs.st-andrews.ac.uk**20080916170742 - Like 'believe' but instead of just believing the value, adds subgoals for - each required equality proof. -] - -[More of paper -eb@cs.st-andrews.ac.uk**20080901161738] - -[Added paper macros -eb@cs.st-andrews.ac.uk**20080901094433] - -[Starting on paper -eb@cs.st-andrews.ac.uk**20080829091345] - -[Compiling 'Foreign' constructor (but only when inline) -eb@cs.st-andrews.ac.uk**20080826123458] - -[Generate Idris functions from foreign function descriptions -eb@cs.st-andrews.ac.uk**20080825164523] - -[Some work towards constructor optimisations -eb@cs.st-andrews.ac.uk**20080825094709] - -[Basic foreign function framework -eb@cs.st-andrews.ac.uk**20080825094631] - -[Added test transformation on Vects -eb@cs.st-andrews.ac.uk**20080731155217] - -[Transformation application -eb@cs.st-andrews.ac.uk**20080730125618] - -['noElim' flag to allow big data types not to need elimination rules -eb@cs.st-andrews.ac.uk**20080729125140] - -[Added __toInt and __toString -eb@cs.st-andrews.ac.uk**20080710151313 - Hacky for now, until we work out a nice way of doing coercions between - primitives. But it makes some programs, like those which ask for an int - as input, possible. -] - -[If an operator returns a boolean, the compiler had better make code to build a boolean! -eb@cs.st-andrews.ac.uk**20080710145313] - -[Deal with weird names that Ivor generates in the compiler -eb@cs.st-andrews.ac.uk**20080709112032] - -[Some Nat theorems -eb@cs.st-andrews.ac.uk**20080709014158] - -[Generalise tactic -eb@cs.st-andrews.ac.uk**20080709014121] - -[Need to give all the definitions to addIvor -eb@cs.st-andrews.ac.uk**20080708203624] - -[Don't crash when there's an error in input! -eb@cs.st-andrews.ac.uk**20080708182610] - -[Only allow 'believe' to rewrite values -eb@cs.st-andrews.ac.uk**20080708165140 - This way at least the types have to be right before '?=' defined - programs will run. -] - -[Added 'believe' tactic -eb@cs.st-andrews.ac.uk**20080708160736 - For allowing the testing of programs before a complete proof term - exists. Obviously programs built this way are not trustworthy! They make - use of a "Suspend_Disbelief" function which just invents a rewrite rule - that works, but which doesn't have a proof. -] - -[Added '?=' syntax -eb@cs.st-andrews.ac.uk**20080708140505 - If you have a pattern clause, and don't know the definite type of the - right hand side, use; - foo patterns ?= def; [theoremName] - - This will add a theorem called theoremName which fixes up the type, - and you can prove it later, via :p or with the 'proof' syntax. Useful - if you want to hide details of the proof of a necessary rewriting. -] - -[Catch errors in proofs, and allow abandoning -eb@cs.st-andrews.ac.uk**20080708123202] - -[Identify parameters of data types to make elimination rule properly -eb@cs.st-andrews.ac.uk**20080708105930] - -[Reading of proof scripts -eb@cs.st-andrews.ac.uk**20080707010718] - -[Add Undo, require % before tactics, and output script when done -eb@cs.st-andrews.ac.uk**20080707004642] - -[Rudimentary theorem prover now working -eb@cs.st-andrews.ac.uk**20080706235523] - -[Parsing tactics and proofs -eb@cs.st-andrews.ac.uk**20080706222536] - -[Adding some tactics -eb@cs.st-andrews.ac.uk**20080706211202] - -[Added :e command and call to epic -eb@cs.st-andrews.ac.uk**20080702115125] - -[forking needs the argument to be lazily evaluated -eb@cs.st-andrews.ac.uk**20080630141845] - -[Added threading to compiler -eb@cs.st-andrews.ac.uk**20080630130045] - -[Compiling IORefs -eb@cs.st-andrews.ac.uk**20080630123521] - -[Add Prelude.e, and prepend it to epic output -eb@cs.st-andrews.ac.uk**20080630113450] - -[Added Prover.lhs (not that it does much yet) -eb@cs.st-andrews.ac.uk**20080623231341] - -[Fix constructor expansion -eb@cs.st-andrews.ac.uk**20080623111226] - -[Got the basic compilation working -eb@cs.st-andrews.ac.uk**20080622233141] - -[Added proof token to Lexer -eb@cs.st-andrews.ac.uk**20080516140747 - (not doing anything yet, it needs a separate parser) - Also fix minor lexing error, and added ':i' command to drop into Ivor - for debugging purposes. -] - -[Added 'normalise' command -eb@cs.st-andrews.ac.uk**20080523140332 - Useful if you want to normalise an IO computation without running it. -] - -[Small implicit argument change -eb@cs.st-andrews.ac.uk**20080513231721 - {a,b,c} now allowed (i.e no need for type label as in {a,b,c:_} - Also, implicit arguments can now, syntactically, only appear at the - left of types of top level declarations (since that is the only place they - make sense with our simple way of handling such arguments). -] - -['!' to stop implicit arguments being added to a name -eb@cs.st-andrews.ac.uk**20080513215523] - -[Outputting Epic code -eb@cs.st-andrews.ac.uk**20080511173955 - Still some things to sort out before this runs though -] - -[Removing IO boiler plate for compilation -eb@cs.st-andrews.ac.uk**20080510170038] - -[Lambda lifter -eb@cs.st-andrews.ac.uk**20080509161049] - -[Oops, broke the build *again* -eb@cs.st-andrews.ac.uk**20080508220834] - -[Data type for result of lambda lifting -eb@cs.st-andrews.ac.uk**20080508214635] - -[Compiler part 1 (pattern matching) -eb@cs.st-andrews.ac.uk**20080508200113] - -[partition -eb@cs.st-andrews.ac.uk**20080508132348] - -[Let's try not to apply patches which break the build... -eb@cs.st-andrews.ac.uk**20080508111341] - -[Patterns representation -eb@cs.st-andrews.ac.uk**20080508110025] - -[Added append to library -eb@cs.st-andrews.ac.uk**20080429111614] - -[Begin planning compiler -eb@cs.st-andrews.ac.uk**20080414123534] - -[brief note -eb@cs.st-andrews.ac.uk**20080414103207] - -[Minor LaTeX improvement -eb@cs.st-andrews.ac.uk**20080330151806 - Output placeholders correctly. Can you tell I'm writing a paper ;). -] - -[Even more LaTeX fixes -eb@cs.st-andrews.ac.uk**20080327115445] - -[Fix some LaTeXing -eb@cs.st-andrews.ac.uk**20080327113804] - -[Some latex tidying -eb@cs.st-andrews.ac.uk**20080325114709] - -[Latex of do notating -eb@cs.st-andrews.ac.uk**20080325110051] - -[Add %latex directive to parser -eb@cs.st-andrews.ac.uk**20080325105552] - -[Allow giving latex commands for particular names in :l -eb@cs.st-andrews.ac.uk**20080325103351] - -[Basic LaTeX generation working -eb@cs.st-andrews.ac.uk**20080324185632] - -[Started LaTeX generation -eb@cs.st-andrews.ac.uk**20080324170817] - -[Implement :t in REPL -eb@cs.st-andrews.ac.uk**20080324143135] - -[Use readline for REPL, add :commands -eb@cs.st-andrews.ac.uk**20080324141759] - -[Oops, didn't mean to record the trace -eb@cs.st-andrews.ac.uk**20080322115632] - -[Allow types on bindings in do notation -eb@cs.st-andrews.ac.uk**20080322114909] - -[Fix bug: add placeholders inside infix ops -eb@cs.st-andrews.ac.uk**20080320150127] - -[Pretty print refl -eb@cs.st-andrews.ac.uk**20080320134148] - -[Bind multiple names in one go in type declarations -eb@cs.st-andrews.ac.uk**20080320132941] - -[Locks are semaphores -eb@cs.st-andrews.ac.uk**20080319161532 - So allow them to be initialised with the number of processes allowed to - hold onto then, -] - -[Missed a case in constant show -eb@cs.st-andrews.ac.uk**20080318175442] - -[Add Maybe and Either to prelude -eb@cs.st-andrews.ac.uk**20080318224740] - -[Use 'fastCheck' since we already know our IO programs work -eb@cs.st-andrews.ac.uk**20080318161100] - -[Pretty printing and parsing tweaks -eb@cs.st-andrews.ac.uk**20080318161027] - -[No point in generating elimination rules since we don't use them -eb@cs.st-andrews.ac.uk**20080317162738 - Perhaps later, if linking to a theorem prover, it will be useful, but - it can be done on demand. -] - -[Dump environment for metavars in the right order -eb@cs.st-andrews.ac.uk**20080315230225] - -[Nicer display of metavariables -eb@cs.st-andrews.ac.uk**20080314174637] - -[Added a pretty ugly pretty-printer for terms -eb@cs.st-andrews.ac.uk**20080314154034] - -[Added metavariable syntax -eb@cs.st-andrews.ac.uk**20080314132802] - -[Back in sync with Ivor (addPatternDef type changed) -eb@cs.st-andrews.ac.uk**20080314011920] - -[Add modules to .cabal for executable -eb@cs.st-andrews.ac.uk**20080313134204] - -[imports in RunIO -eb@cs.st-andrews.ac.uk**20080312174755] - -[minor cabal format -gwern0@gmail.com**20080312041116] - -[improve cabal metadata for hackage, split into lib/main -gwern0@gmail.com**20080312041034] - -[fix sdist -gwern0@gmail.com**20080312040218] - -[+Extensions -gwern0@gmail.com**20080312035953] - -[Context.lhs -> Context.hs -gwern0@gmail.com**20080312035926 - Literate files are just wasteful if they aren't literate -] - -[dehaskell98 -gwern0@gmail.com**20080312035905] - -[Update ioref example -eb@cs.st-andrews.ac.uk**20080312125024] - -[Added IORefs -eb@cs.st-andrews.ac.uk**20080312123834] - -[Added some concurrency primitives -eb@cs.st-andrews.ac.uk**20080311205546 - fork, newLock, lock, unlock -] - -[Add simple stateful DSL -eb@cs.st-andrews.ac.uk**20080311151020] - -[Add placeholders in do expressions too! -eb@cs.st-andrews.ac.uk**20080311150824] - -[Be more implicit! -eb@cs.st-andrews.ac.uk**20080310135937] - -[Better if testVect has ints -eb@cs.st-andrews.ac.uk**20080310133325] - -[syntax tinker in partition.idr -eb@cs.st-andrews.ac.uk**20080310132921] - -[Syntax for let bindings -eb@cs.st-andrews.ac.uk**20080310025357] - -[if...then...else syntax -eb@cs.st-andrews.ac.uk**20080310024516] - -[Member predicate -eb@cs.st-andrews.ac.uk**20080310013200] - -[Syntax for _ patterns -eb@cs.st-andrews.ac.uk**20080310012608] - -[Rename List -eb@cs.st-andrews.ac.uk**20080310002023] - -[builtins needs bool -eb@cs.st-andrews.ac.uk**20080310001809] - -[Removed samples which should be in lib -eb@cs.st-andrews.ac.uk**20080309224149] - -[Added io example -eb@cs.st-andrews.ac.uk**20080309223957] - -[More keeping in sync with Ivor -eb@cs.st-andrews.ac.uk**20080309222931] - -[Take advantage of better ivor inference -eb@cs.st-andrews.ac.uk**20080309213603] - -[Added vect lib -eb@cs.st-andrews.ac.uk**20080308185405] - -[Added List to library -eb@cs.st-andrews.ac.uk**20080308185119] - -[Lambdas can take multiple arguments -eb@cs.st-andrews.ac.uk**20080308185050] - -[Added integer comparison operators -eb@cs.st-andrews.ac.uk**20080308134245] - -[Add polymorphic boolean equality -eb@cs.st-andrews.ac.uk**20080308133304] - -[Added library paths and a simple prelude -eb@cs.st-andrews.ac.uk**20080308132011] - -[Some primitive operators, and '=' for JM equality -eb@cs.st-andrews.ac.uk**20080307234257] - -[Use WHNF for evaluation now Ivor has it -eb@cs.st-andrews.ac.uk**20080307195902] - -[Added builtins -eb@cs.st-andrews.ac.uk**20080307173517] - -[add RunIO.hs -eb@cs.st-andrews.ac.uk**20080306114827] - -[Added more samples (IO not quite working yet due to Ivor bug though) -eb@cs.st-andrews.ac.uk**20080305170333] - -[Add do notation -eb@cs.st-andrews.ac.uk**20080305170312] - -['include' files -eb@cs.st-andrews.ac.uk**20080305112534] - -[Latest Ivor allows more implicitness -eb@cs.st-andrews.ac.uk**20080305104707] - -[Enough annotations to make interp work -eb@cs.st-andrews.ac.uk**20080305001951] - -[Allow forward declarations for functions, add quicksort example -eb@cs.st-andrews.ac.uk**20080305000656] - -[Added 'partition' example -eb@cs.st-andrews.ac.uk**20080304224512] - -[Easier to put implicit arguments in pattern clauses -eb@cs.st-andrews.ac.uk**20080304224425] - -[John Major equality syntax -eb@cs.st-andrews.ac.uk**20080304215146] - -[Added interpreter example, fixed simple sample -eb@cs.st-andrews.ac.uk**20080303164114] - -[Changed some syntax -eb@cs.st-andrews.ac.uk**20080303163946 - - Implicit arguments can now be named when applied, so that the parser - knows which argument you mean - - No need for {} around definitions - - Type of types is # - -] - -[make sure constructur arguments get new names generated -eb@cs.st-andrews.ac.uk**20080229003215] - -[Added samples directory -eb@cs.st-andrews.ac.uk**20080228232920] - -[First version which runs code! -eb@cs.st-andrews.ac.uk**20080228232820] - -[Some simple examples -eb@cs.st-andrews.ac.uk**20080228175453] - -[Now building terms and datatypes for Ivor with implicit args added -eb@cs.st-andrews.ac.uk**20080228161136] - -[More work on parser; constants, lambdas, new syntax tree -eb@cs.st-andrews.ac.uk**20080226111951] - -[Parser for datatypes and basic function definitions -eb@cs.st-andrews.ac.uk**20080108171829] - -[Started parser -eb@cs.st-andrews.ac.uk**20071214181416] - -[First chunk of code -eb@cs.st-andrews.ac.uk**20071212114523] |