git.iko.soy/Idris-dev
on aa7262e help sign in
history ofsrc/Core/Elaborate.hs
all commits
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 d1d672eCollect all unification errors instead of immediately reporting failureEdwin Brady 38732d8Heuristic for picking best error message when overloaded alternatives all failEdwin Brady baaba44Run-time forcing optimisationEdwin Brady 3af0ae0Elaborator tweak, dealing better with values that are inferred automaticallyEdwin Brady 67c5734Added case and pattern matching let bindings Also pattern matching bind in do notation case notation currently has limitations: - only works on simple types (each pattern must have the same type, more specifically) - return type needs to be known at the point of elaborationEdwin Brady 1823cf9Postpone injectivity check until after unificationEdwin Brady d6c53d9Fix pattern name bug where name is already a CAFEdwin Brady 7384683Fiddle with elaborator; update interp sample and testEdwin Brady f2e3a76Default definitions in classes, plus some bug fixingEdwin Brady fa5f1cdNamespacesEdwin Brady 8cd093fChanged lookup to return a list (preparation for namespaces)Edwin Brady 94d888bParsing and elaboration of alternativesEdwin Brady 5b08cc9Add PAlternativeEdwin Brady b26716aCollect cumulativity constraints on universesEdwin Brady 03d7d5eAllow type labels on lambdasEdwin Brady e473c2eExists namingEdwin Brady bbaa193Better representation of namesEdwin Brady 1c49219Added provisional definitionsEdwin Brady e0e52f1simple_app should try both elaboration ordersEdwin Brady f31caf5unique_hole needs to check whole contextEdwin Brady 71c1a0eExtension parsing, now deferring checks name is uniqueEdwin Brady 2c05448Give invented pattern variables unique namesEdwin Brady f2368e9More care with naming in where clausesEdwin Brady 229a99cBetter elaboration order; also changed instance argument syntax slightlyEdwin Brady ed64e76Better type class resolutionsEdwin Brady be3a53aType class instance resolution, and some Num overloadingEdwin Brady 188dda5Tinkering with tactics and deferred definitionsEdwin Brady 58bd7c4Added rewrite tacticEdwin Brady 10b88aeAdded refine, focus, undoEdwin Brady 551548cBeginning theorem prover interfaceEdwin Brady