git.iko.soy/Idris-dev
on 86e32fb help sign in
history ofsrc/Core/TT.hs
all commits
2dc07faInduction on nat workingAhmad Salim Al-Sibahi 4a0eba1Add %name directive for naming hints in editing.Edwin Brady c1e2921Add missing error message Fixes #693Edwin Brady 7b8f3b4Merge branch 'feature/eliminators' of https://github.com/ahmadsalim/Idris-dev into ahmadsalim-feature/eliminatorsEdwin Brady 9900e63`showCG` should be recursive and not use `show`Brian McKenna 725587fFixed testing failures I accidentally introduced when showing a better naming for machine generated names (so that I could better debug)Ahmad Salim Al-Sibahi 9a89a8dEliminators working for some type - still experimental. Will create a way to make them work with the elim type classAhmad Salim Al-Sibahi 543cd7eStrictness improvementsEdwin Brady 7041f65Remove needless map in Core/TTEdwin Brady 8531634Set up more partial evaluation machineryEdwin Brady 521dc75Prune case trees properly on optimised NatEdwin Brady 3c32b65Whitespace cleanup.George Leontiev f34f0afBetter display of metavariable types in :tEdwin Brady 9e5c96fAdd error object for failure to load fileDavid Christiansen 8b17db3Fixed flaw with FC dependency by making FC equality always return true. If any fc equality is needed just use FC' fc to convert. Fixes idris-lang/Idris-dev#550Ahmad Salim Al-Sibahi 57c8657Added column name to sourceAhmad Salim Al-Sibahi ac33945Wrap Idris in an ErrorTDavid Christiansen 9cdf03aFix compilation of unqualified constructor namesEdwin Brady 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