git.iko.soy/Idris-dev
on 7afa310 help sign in
history ofsrc/Idris/TypeSearch.hs
all commits
37292e1Save terms in docstringsDavid Raymond Christiansen 7ce4d90Add annotations for :search result classificationbmsherman 185f808Fix logical error in :search's unification resolutionbmsherman aa98ab1Try symmetry of equality in :searchbmsherman 886bac0Refactor :search to remove code duplication and name shadowingbmsherman 7e7368dStore kind in Pi bindersEdwin Brady 480024cRemove all the handle argumentsDavid Raymond Christiansen 1add7b7provide a Handle for IdeSlave, used to read from and write to (instead of hardcoded stdin/stdout) also send protocol-version message when the client connects also accept a single client connection when --ideslave-socket is provided (I don't see any reason to have multiple clients at all!)Hannes Mehnert c72d0f4Split elaborator into multiple source filesEdwin Brady 7d95becMake type search work in the proverDavid Raymond Christiansen 78b2923Correctly count applications of variables in :searchbmsherman d7f6164Ignore believe_me in :search since its type is a lie!bmsherman e1ba862Find best matching types first in :search with a priority queue.bmsherman d19891cDiscover typeclass introduction/elimination in :searchbmsherman eec9953In :search, check injectivity to prevent erroneous resultsbmsherman e1ef65dUse a priority queue to improve performance when matching types in :searchbmsherman 114a307Prevent possibility of unbounded computation in :searchbmsherman f91051aIgnore default class methods in :searchbmsherman 852301dImprovements to :search, primarily in handling typeclassesbmsherman 9c3fefeImprove appearance of type search results.bmsherman 7395bdeIn type-directed search, handle an additional possible case when processing unification results.bmsherman 60a0c7aNow we can handle typeclasses!bmsherman ee02ae9Preliminary version of type-directed searchbmsherman