Added Idris and updated fetchdarcs.
svn path=/nixpkgs/trunk/; revision=15595
This commit is contained in:
Andres Löh
parent
1ffa8f0c17
commit
677f91a6d1
6 changed files with 640 additions and 10 deletions
|
|
@ -5,11 +5,14 @@ tagflags=""
|
|||
if test -n "$tag"; then
|
||||
tagtext="(tag $tag) "
|
||||
tagflags="--tag=$tag"
|
||||
elif test -n "$context"; then
|
||||
tagtext="(context) "
|
||||
tagflags="--context=$context"
|
||||
fi
|
||||
|
||||
header "getting $url $partial ${tagtext} into $out"
|
||||
|
||||
darcs get --no-pristine-tree $partial $tagflags "$url" "$out"
|
||||
darcs get --lazy --ephemeral $tagflags "$url" "$out"
|
||||
# remove metadata, because it can change
|
||||
rm -rf "$out/_darcs"
|
||||
|
||||
|
|
|
|||
|
|
@ -1,17 +1,13 @@
|
|||
{stdenv, darcs, nix}: {url, tag ? null, md5, partial ? true}:
|
||||
{stdenv, darcs, nix}: {url, tag ? null, context ? null, md5 ? "", sha256 ? ""}:
|
||||
|
||||
stdenv.mkDerivation {
|
||||
name = "fetchdarcs";
|
||||
builder = ./builder.sh;
|
||||
buildInputs = [darcs nix];
|
||||
partial = if partial then "--partial" else "";
|
||||
buildInputs = [darcs];
|
||||
|
||||
# Nix <= 0.7 compatibility.
|
||||
id = md5;
|
||||
|
||||
outputHashAlgo = "md5";
|
||||
outputHashAlgo = if sha256 == "" then "md5" else "sha256";
|
||||
outputHashMode = "recursive";
|
||||
outputHash = md5;
|
||||
outputHash = if sha256 == "" then md5 else sha256;
|
||||
|
||||
inherit url tag;
|
||||
inherit url tag context;
|
||||
}
|
||||
|
|
|
|||
24
pkgs/development/compilers/idris/default.nix
Normal file
24
pkgs/development/compilers/idris/default.nix
Normal file
|
|
@ -0,0 +1,24 @@
|
|||
{fetchdarcs, cabal, mtl, parsec, readline, ivor, happy}:
|
||||
|
||||
cabal.mkDerivation (self : {
|
||||
pname = "idris";
|
||||
name = self.fname;
|
||||
version = "0.1.2";
|
||||
src = fetchdarcs {
|
||||
url = http://www-fp.dcs.st-and.ac.uk/~eb/darcs/Idris;
|
||||
sha256 = "de50ed4bedacee36d9942bf4db90deca3915cf6c106aa834d11e83972b2b639a";
|
||||
context = ./idris.context;
|
||||
};
|
||||
propagatedBuildInputs = [mtl parsec readline ivor];
|
||||
extraBuildInputs = [happy];
|
||||
preConfigure = ''
|
||||
echo "module Idris.Prefix where prefix = \"$out\"" > Idris/Prefix.hs
|
||||
'';
|
||||
postInstall = ''
|
||||
ensureDir $out/lib/idris
|
||||
install lib/*.idr lib/*.e $out/lib/idris
|
||||
'';
|
||||
meta = {
|
||||
description = "An experimental language with full dependent types";
|
||||
};
|
||||
})
|
||||
586
pkgs/development/compilers/idris/idris.context
Normal file
586
pkgs/development/compilers/idris/idris.context
Normal file
|
|
@ -0,0 +1,586 @@
|
|||
|
||||
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]
|
||||
12
pkgs/development/libraries/haskell/ivor/default.nix
Normal file
12
pkgs/development/libraries/haskell/ivor/default.nix
Normal file
|
|
@ -0,0 +1,12 @@
|
|||
{cabal, mtl, parsec}:
|
||||
|
||||
cabal.mkDerivation (self : {
|
||||
pname = "ivor";
|
||||
version = "0.1.8";
|
||||
sha256 = "e51ad07c78ea0cad6fce9253012258dbf7c740198792aa4a446e1f0269a9186d";
|
||||
propagatedBuildInputs = [mtl parsec];
|
||||
meta = {
|
||||
description = "Theorem proving library based on dependent type theory";
|
||||
};
|
||||
})
|
||||
|
||||
|
|
@ -153,6 +153,15 @@ rec {
|
|||
inherit cabal;
|
||||
};
|
||||
|
||||
idris = import ../development/compilers/idris {
|
||||
inherit cabal mtl parsec readline ivor happy;
|
||||
inherit (pkgs) fetchdarcs;
|
||||
};
|
||||
|
||||
ivor = import ../development/libraries/haskell/ivor {
|
||||
inherit cabal mtl parsec;
|
||||
};
|
||||
|
||||
json = import ../development/libraries/haskell/json {
|
||||
inherit cabal mtl;
|
||||
};
|
||||
|
|
|
|||
Loading…
Reference in a new issue