587 lines
15 KiB
Plaintext
587 lines
15 KiB
Plaintext
|
|
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]
|