git.iko.soy/Idris-dev
on d66da21 help sign in
history ofsrc/Core/Elaborate.hs
all commits
c1e2921Add missing error message Fixes #693Edwin Brady 3c32b65Whitespace cleanup.George Leontiev d120141Add a final unification stepEdwin Brady f54c665EXPERIMENTAL: Solve more implicits by matchingEdwin Brady 2a0885eBetter representation and rendering of generated namesEdwin Brady df41e3dGive a bit more context for error messagesEdwin 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 fa80591Fix let scope leakage bugEdwin Brady 3448469Add "equiv" tactic "equiv t" asserts that the current goal has a type equivalent (by conversion) to tEdwin Brady 62a3ebaImprove the "...is not solved" internal error to display something useful Fixes #361 Fixes #321Edwin Brady 6924cebGive Pi bindings the proper name when elaborating lambdas Fixes #360Edwin 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 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 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 809683bDon't allow unification problems to be introduced in :p modeEdwin Brady a807a34Remove the unused arg from lookup functionsDavid Christiansen f1e61daIf the goal is not a function type when elaborating \, invent one ...and attempt to solve it by unificationEdwin Brady 1a87674Improved type-directed name disambiguationEdwin Brady 8b96fc7Fix another unification problem (solving things which shouldn't be)Edwin Brady adf51f4Make Haddock able to parse Idris's sourceDavid Christiansen 98599b5Only apply unique implicit conversions (and add test)Edwin Brady 022d4dfAdded 'implicit' conversions implicit f : a -> b Then, when a function needs a 'b' but has an 'a', f will be called implicitly. This is probably scary and fragile. Use with extreme caution!Edwin Brady 8f76315Changed approach to unification Instead of failing immediately, maintain a list of blocked problems and refine during elaboration.Edwin Brady 187f42fUndo unification changes... because it's broken...Edwin Brady 6be4eb2Fix compile errorEdwin Brady 7a66adcMake unification faster by computing HNF rather than normalisingEdwin Brady 04d6f00A small amount of proof automation, via tactic reflectionEdwin Brady d06d473Fix injectivity checkEdwin Brady dd5001fmake TT aware of Set -> Typeraichoo c10146bLimited type inference of types in where clauses Type signatures can now be omitted *only* if the type of the function can be determined completely from the first call.Edwin Brady f833918(Experimental) Create deferred definitions by applicationEdwin Brady c71ce04Marginally improve unification errorsEdwin Brady 1677c30Better dealing with name shadowing while building instances ...and while type checking completed termsEdwin Brady 56223efDon't normalise everywhere!Edwin Brady f9a1dabFix pattern variable problem when patterns generated by unificationEdwin Brady 671d39aFix name clashes between holes and bound variablesEdwin Brady 28ecd81Erase unused arguments when compilingEdwin Brady 5a6299bUnification fix Specifically to stop it filling in things which are given by the programmer (caused by a bug replacing nullary constructors with terms!)Edwin Brady 23ab26fSpeed improvements when code contains type errors Identify "unrecoverable" unification failures so that type checking doesn't continue to search all the alternative overloadings and orderings.Edwin Brady ef3aed2Fix FLOATOP properlyEdwin Brady b70780frename rts include fileEdwin Brady cb92598Unification tweak Use the code the programmer gives, not code the unifier finds.Edwin Brady 59d07f7Quicker resolution of overloaded names By checking the name's type against the goal type rather than fully checking.Edwin Brady 6cb70bcFix for simple function applicationsEdwin Brady 5602ea7A small cleanup after missing some stray ends in the diff.Dominic Mulligan 8c64e9cGot pretty printing partially working using the Pretty type class as a replacement for Show. Now need to tweak it in order to make everything look nice, and to get terms printing correctly!Dominic Mulligan 81f2c89Small error message fixEdwin Brady 09f2abdFix let overloading bug with do blocksEdwin Brady 21c3a30Give up type class resolution soonerEdwin Brady 33bf2bdUnification tweakEdwin Brady