git.iko.soy/Idris-dev
on 8c19e30 help sign in
history ofsrc/Idris/AbsSyntax.hs
all commits
8c19e30Record internal name of 'with' functionsEdwin Brady bc0ebeeMerge branch 'feature/columntracking' of https://github.com/ahmadsalim/Idris-dev into ahmadsalim-feature/columntrackingEdwin Brady fafe598Fix bug in scoping rules for pattern matchesEdwin Brady 57c8657Added column name to sourceAhmad Salim Al-Sibahi f185e63Merge branch 'master' of github.com:edwinb/Idris-dev into implicit-bindEdwin Brady b5eee09Convert IO errors into erros in the Idris monadDavid Christiansen 8c9ec38Added 'implicit bind' syntaxEdwin Brady 63038b3Use the ErrorT failure functions and attempt to preserve error structureDavid Christiansen ac33945Wrap Idris in an ErrorTDavid Christiansen 0e76ac9Remember whether implicits are machine generatedEdwin Brady 1bc3002Some Eff experimentation, adding a 'test' commandEdwin Brady 3db1e91Added flag for error reflection extensionDavid Christiansen 39bc4c4Merge pull request #485 from lambdadomain/masterEdwin Brady daab1a3Partially defined names should not reduce at compile-timeEdwin Brady ed8114eUpdated dependencies and types for Haskell llvm bindings v3.3.8.1.lambdadomain 0a1b9d8Prevent duplicate dynamic linkingDavid Christiansen e3bd62bColourise REPL promptDavid Christiansen fe20bf1Allow colour options from REPLDavid Christiansen e8f4bb1Some packaging fixesEdwin Brady 966ef43Check for duplicates when adding object files/libs/flagsEdwin Brady af4fda7%flag directiveEdwin Brady 52073d1Make --quiet imply --nocolourDavid Christiansen c0342c7Add command line option to control REPL coloursDavid Christiansen b762f14Basic colourisation in REPLDavid Christiansen ffb9ea9Semantic colouring of identifiers in REPLDavid Christiansen 959e7b1Tweak scoping rules in 'where' Check whether function names are rebound in patternsEdwin Brady 5ce8ee7Fix shadowing bug with dependent pair bindingsEdwin Brady 6dc5ea2Fix name shadowing in whereEdwin Brady 0aca9f2New module chaser, for better dependency checking and rebuilding Now treats each source file separately, building a tree of dependencies, and rebuilding if any dependencies have updated. In particular, this fixes a problem with stale definitions hanging around when building packages, and has required some fixes to imports in the library.Edwin Brady ecb42f0Resolve names/expand implicits inside refl Fixes #447Edwin 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 6f88ecdAdd syntax for transformation rules %transform lhs ==> rhs Unbound names on the lhs are treated as patterns. Transformation behaviour not yet implemented.Edwin Brady c0ff0e8Fix type class index propagation bug ...which lead to implicit arguments not being spotted. Fixes #402Edwin Brady 9b4b7dccleanupsHannes Mehnert 50086acabstract set-prompt into isetPrompt -- and use itHannes Mehnert d7c8e63define and use iputGoal instead of putStrLnHannes Mehnert 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 7b6448eOptimization level selectionBenjamin Saunders f149970Rename --target to --codegen and add options to specify target triple and CPU, defaulting to that of hostBenjamin 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 db18c51Add scriptsDavid Christiansen f885274Fix ordering of auto-implicits with 'using' 'using' arguments always now appear before fully implicit arguments, rather than the order we happen to find them in. TODO: Better would be to sort according to which ones we know depend on each other...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 d6d5634be more precise when to emit a warning (still a workaround - fix involves to not parse the string)Hannes Mehnert 9505a71cleanups, rename List to SexpList to disambiguateHannes Mehnert f608369Merge pull request #312 from hannesm/ideslaveEdwin Brady 99a8a66Check that explicitly given implicit args unify with inferred versions Also exposed a unification bug which unified things which shouldn't be: f x = f y does not imply x = y unless f is injective, and this was not properly checked.Edwin Brady 674c8b8IdeSlave mode improvements: - introduce iResult and iFail to report success and failure of a REPLcommand - send warnings for occuring warnings during parsing / typechecking - introduce ideslaveProcess function, which guards process with iResult/iFail (and does not support all operations) - revert commit which removed IState from ideslaveStart/ideslave functionsHannes Mehnert