git.iko.soy/Idris-dev
on ace080c help sign in
history ofsrc/Core/TT.hs
all commits
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 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 9a54230Started adding pretty printing capabilities for core data types to improve rendering of proof state.Dominic Mulligan 00d7c69Work towards making {static} arguments and specialisation work properlyEdwin Brady 392c225Check definitions structurally as well as by name in conversionEdwin Brady 21c3a30Give up type class resolution soonerEdwin Brady 3b13341Better error reporting for unresolved type classesEdwin Brady 1112fe4Coverage checker Not quite complete - a bug (which I know how to fix) makes some things appear not covering even though they are. Results currently used only for pruning case trees in compiled code. There is a small performance penalty - coverage checking can be disable with --nocoverageEdwin Brady 38732d8Heuristic for picking best error message when overloaded alternatives all failEdwin 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 2ce525eintros tactic; some library tinkeringEdwin 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 dcc09e0Fix metavariable naming in namespacesEdwin Brady