git.iko.soy/Idris-dev
on c614366 help sign in
history ofsrc/Idris/AbsSyntaxTree.hs
all commits
67fb9ccSplit Parser.hs into several filesEdwin Brady 3db1e91Added flag for error reflection extensionDavid Christiansen 39bc4c4Merge pull request #485 from lambdadomain/masterEdwin Brady c55f8c2Unification fix to avoid giving up on recoverable errorsEdwin Brady ed8114eUpdated dependencies and types for Haskell llvm bindings v3.3.8.1.lambdadomain fe20bf1Allow colour options from REPLDavid Christiansen 7c45129Colour theme in Idris REPL stateDavid Christiansen 2a0885eBetter representation and rendering of generated namesEdwin Brady af4fda7%flag directiveEdwin Brady ddc137eColourise some error messagesDavid Christiansen fddebcaHave :t colourise the left side of the colonDavid Christiansen c0342c7Add command line option to control REPL coloursDavid Christiansen 6c14565Move colourisation to a separate moduleDavid Christiansen 7226659Colourise implicit params with underlineDavid Christiansen f48e88fColourisation fix for replDavid Christiansen b762f14Basic colourisation in REPLDavid Christiansen ffb9ea9Semantic colouring of identifiers in REPLDavid Christiansen 1d4d226Optimise datatypes with one constructor and one argument No need to pack them up (because we're strict!) so just treat them as a newtype would be in Haskell.Edwin Brady 8eb2087Separate IO and PrimIO PrimIO is the internal primitive, IO is the user version which requires an explicit World token to be passed in which programmers have no access to directly. Fixes #185 and fixes #325Edwin Brady 3aa61b3Delete unused codeBenjamin Saunders c182c92Allow simple function types to be reflectedEdwin Brady d43a279Change TCGen flag to Dictionary, update evaluator accordinglyEdwin Brady 48d1105Added 'quoteGoal x by p in e' syntax meaning, let x = p [current goal] in e Additionally, the value of x is normalised, which means p can be a compile-time only %reflection function used to prove something interesting in e. See test030 for an example of automated proof by reflection.Edwin Brady fd9bd68Add '%reflection' option for functions A reflection function can evaluate at compile-time only, and pattern matches on *syntax* rather than on constructor forms. Also add 'prim__syntactic_eq' for a compile-time syntactic equality check.Edwin Brady e410ab3Fix missing cases in 'tldeclared' to allow class/instance in parameter blocks Fixes #436Edwin Brady 2311d55rename O into Zraichoo 6f88ecdAdd syntax for transformation rules %transform lhs ==> rhs Unbound names on the lhs are treated as patterns. Transformation behaviour not yet implemented.Edwin Brady ad66486Add %specialise annotation for functions (Part 1 of partial evaluation) %specialise [n1 t1, n2 t2 ...] as an annotation before a function type means that the r.h.s. of all the clauses will be evaluated, but with the name n1 reduced at most t1 times, etc. The t1 part is optional, and means unlimited (which is the default for all names at the minute anyway)Edwin Brady 7fc4865Allow 'rewrite ... in' to assert the resulting type "rewrite f ==> t in x" means that after applying the rewrite f, the required type of x must be t. This is primarily for readability of proofs built by successive rewritings.Edwin Brady 3448469Add "equiv" tactic "equiv t" asserts that the current goal has a type equivalent (by conversion) to tEdwin Brady 7b6448eOptimization level selectionBenjamin Saunders f149970Rename --target to --codegen and add options to specify target triple and CPU, defaulting to that of hostBenjamin Saunders 14ee023Skeleton of stub-generating LLVM codegenBenjamin Saunders be36353Merge pull request #362 from david-christiansen/cmdline-execEdwin Brady 9c11754Added %unifyLog construct For debugging purposes %unifyLof t will give a trace of unification problems while elaborating t Also, log levels 6 and above will give the traceEdwin Brady ce7e45bEXPERIMENTAL: Syntax for applying functions by expected type "t <== f" applies a function f to arguments in such a way that it returns something of type t. The <== is a placeholder syntax until someone comes up with something better. (Alternative: t by f, but that uses up a new keyword)Edwin Brady db18c51Add scriptsDavid Christiansen c7fded1Added 'mrefine' tactic Like refine, but uses matching instead of unification to resolve implicit arguments. All will become clear, I hope :). This is intended for an additional style of pattern matching (on types) for better explanation of proofs.Edwin Brady eacfe5cAdded backend target specification to %lib, %link and %include directivesJan Bessai 5b2f091Allow type class constraints in 'using' clauses e.g. if a using block is given asEdwin Brady 425c97achanged defaultOpts to use field names for assignmentjoe9 c96561bdon't use a field in IOption and a field in IState, only one of themHannes Mehnert 4118b79implement outputmode in IState, which either prints it raw or sexpressions (for ideslave support)Hannes Mehnert 6d01828put ideslave_counter into IStateHannes Mehnert 1b65f6ause process in ideslave loopHannes Mehnert e0783efinitial ideslaveHannes Mehnert 700759fCache missing cases found by totality checker, for display Now :missing works correctly (fixes issue #210) Also, remove a large chunk of unused code in coverage checker.Edwin Brady 8af32d4squash potential space leaks by using strict foldlraichoo 2a17e4fFix scoping rules on lhs of with clauseEdwin Brady d1e450fPrint Nats as numeralsAndy Morris