git.iko.soy/Idris-dev
on de0bcbd help sign in
history ofsrc/Core/TT.hs
all commits
aa8ab8fGenerate simpler names with showCGEdwin Brady 2a0885eBetter representation and rendering of generated namesEdwin Brady df41e3dGive a bit more context for error messagesEdwin Brady 7875005Change treatment of underscore in lambda Treat as unnamed variables, rather than as patternsEdwin Brady c710867Better unification errors when name is out of scope In particular, a unification problem which cannot be solved because it uses a variable not in scope where the metavariable is bound. Fixes #342Edwin Brady fa80591Fix let scope leakage bugEdwin Brady 0b25ad1Change default Num typeclass to integer Fixes #391Edwin Brady 773e454Make ChType a member of IntTy ITChar.Jan Bessai 62a3ebaImprove the "...is not solved" internal error to display something useful Fixes #361 Fixes #321Edwin Brady 0aa3fd6Beginnings of integer SIMD support (no backend yet)Benjamin Saunders 45272d9Fix term size calculation for inlining Now counting binders other than Let, so lots of things previously inlined over-aggressively are now not inlined.Edwin Brady 127cc70Implement 'pretty' for B{8,16,32,64}Edwin Brady e6d48b6Take care with 'let' in specialiser - avoid duplicating a redex Let now only reduces if the binding appears at most once in scope during specialisationEdwin Brady 00ae7feMerge branch 'master' into providersDavid Christiansen a807a34Remove the unused arg from lookup functionsDavid Christiansen 4807b0eDocumentation improvementDavid Christiansen 9af2d93Add type provider errors + test caseDavid Christiansen fd9e0fbFix some INTERNAL ERRORs which aren't (non-function type, nothing to introduce) (And the crowd goes wild)Edwin Brady db5973bAdded rewrite ... in ... construct rewrite prf in v rewrites the goal type using prf. It is equivalent to applying replace, without the need to provide a predicate. It works by applying the rewrite tactic with prf before elaborating v.Edwin Brady 22c355aDocumentation comment additionsDavid Christiansen 306a451Reformat existing comments for Haddock and add Haddock commentsDavid Christiansen 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 4c5b1bdMerge branch 'master' into bitstringBenjamin Saunders 8f76315Changed approach to unification Instead of failing immediately, maintain a list of blocked problems and refine during elaboration.Edwin Brady b896224Primitive types for groups of 8, 16, 32, and 64 bits, and basic arithmetic and mutual conversion operations on themBenjamin Saunders bfd5b51Make sure names are not defined more than once Fixes issue #124Edwin Brady 8d83f38Abstract matched terms from goal type in with clauses (like 'magic with' in Agda)Edwin Brady dd5001fmake TT aware of Set -> Typeraichoo f6451efword 8/16 primitive typesraichoo b1cdd04Added postulate declarations postulate foo : type -- 'type' must return something of a collapsible type, i.e. a type with at most one instancei determined entirely by the indices, to ensure that it is unused at run-time.Edwin Brady 1677c30Better dealing with name shadowing while building instances ...and while type checking completed termsEdwin Brady ca684b6Fix pToV scoping bugEdwin Brady f9a1dabFix pattern variable problem when patterns generated by unificationEdwin Brady 9e58e28Type safe message passing concurrencyEdwin Brady 895b323Allow forward declaration of data structures To support induction-recursion and mutual data definitions Syntax is as a normal data declaration, but without the 'where' or '=' sectionsEdwin Brady 9affb75Totality checker improvements Now does a better job of checking type class instances for totality, by inlining dictionaries where possible. Added %default total declarations to some libraries where possibleEdwin Brady b894841Improve some error messagesEdwin 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 0f957f6Add Proj operator to runtime version of TT Allows extracting arguments without checking constructor first which will make erasing unused values easier shortlyEdwin Brady bb76c6cMore aggressive simplification; fix case generation bugEdwin Brady dde7fc3Report error for missing type declarationEdwin 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 7c75851Test file for new VM, hook up parserEdwin Brady 59d07f7Quicker resolution of overloaded names By checking the name's type against the goal type rather than fully checking.Edwin Brady 6554c7dTowards primitives in new VMEdwin Brady 6cb70bcFix for simple function applicationsEdwin Brady e1c7b0fAdd "--errorcontext" flag, and :set and :unset in the REPL. :set errorcontext will cause unification errors to also dump the current context.Edwin Brady 19495edCheck patterns are inaccessibleEdwin Brady 5602ea7A small cleanup after missing some stray ends in the diff.Dominic Mulligan c824099Major improvement to pretty printing of proof states, especially when the goal is a large term.Dominic Mulligan