git.iko.soy/Idris-dev
on d1663cc help sign in
history ofsrc/Core/ProofState.hs
all commits
3c32b65Whitespace cleanup.George Leontiev f34f0afBetter display of metavariable types in :tEdwin Brady d120141Add a final unification stepEdwin Brady f54c665EXPERIMENTAL: Solve more implicits by matchingEdwin Brady db96d75Add a 'compute' before elaboration to expand type synonyms etcEdwin Brady 70a041fAnother minor efficiency gain in elaboratorEdwin Brady 2c588b9Reorder goal search for efficiencyEdwin Brady 1d8003dSpeed up elaboration of larger functionsEdwin Brady c55f8c2Unification fix to avoid giving up on recoverable errorsEdwin Brady 6d7dc4eSimplify evaluator It tries to support too much, but since it's part of the kernel it should do as little clever stuff as possible. Now just normalises, simplifies or specialises, the latter two simply meaning that certain names are blocked from being reduced.Edwin 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 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 7bfa10cSome unification fixesEdwin 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 6857a2cMake 'count' partial/abstract to prevent compile-time reduction Deals with issue #171Edwin Brady fd9e0fbFix some INTERNAL ERRORs which aren't (non-function type, nothing to introduce) (And the crowd goes wild)Edwin Brady e3a4097Fix eta problemEdwin Brady 35034dbChange forall tactic to use unify rather than isType Fixes issue #189Edwin Brady 93819edUnification fixEdwin Brady 8b96fc7Fix another unification problem (solving things which shouldn't be)Edwin Brady 2686158Be more careful when unifying metavariable applications Otherwise things get solved which shouldn't be. Fixes issue #227Edwin Brady 14cce81Normalise before looking for coercionsEdwin Brady 8f76315Changed approach to unification Instead of failing immediately, maintain a list of blocked problems and refine during elaboration.Edwin Brady 7a66adcMake unification faster by computing HNF rather than normalisingEdwin Brady dd5001fmake TT aware of Set -> Typeraichoo 4a9c0f4Fix argument names in generated types for where blocksEdwin Brady 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 1677c30Better dealing with name shadowing while building instances ...and while type checking completed termsEdwin Brady 56223efDon't normalise everywhere!Edwin Brady ca684b6Fix pToV scoping bugEdwin Brady f9a1dabFix pattern variable problem when patterns generated by unificationEdwin 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 611dd97Improve speed of type checking by spotting unification failure quickerEdwin Brady 6cb70bcFix for simple function applicationsEdwin Brady 96031d1Normalise rewrite rule so that they apply more easilyEdwin Brady 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 4bcfa68Tinker with specialisationEdwin Brady 33baa44More on errors; propagate line numbersEdwin Brady 6682ebbPropagate solutions properlyEdwin Brady 558d226Update elaborator for application of local variablesEdwin Brady 33bf2bdUnification tweakEdwin Brady d1d672eCollect all unification errors instead of immediately reporting failureEdwin Brady 02881b1Implemented forcing optimisation Constructor arguments which are inferrable from the indices in the constructor type are erased both at compile-time and run-timeEdwin Brady 1823cf9Postpone injectivity check until after unificationEdwin Brady