mirrors/nixpkgs
1
0
Fork 1
mirror of https://github.com/NixOS/nixpkgs.git synced 2024-11-25 15:11:35 +00:00
Code Issues Wiki Activity
nixpkgs/pkgs/development/compilers/idris/idris.context
Andres Löh 677f91a6d1 Added Idris and updated fetchdarcs. 
svn path=/nixpkgs/trunk/; revision=15595
2009-05-13 19:02:23 +00:00

587 lines
15 KiB
Plaintext
Raw Blame History

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]
View git blame Copy permalink