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]