dowsing
dowsing copied to clipboard
Drup
᚛ A type of divination employed in attempts to locate identifiers matching a given type expression
To understand better the behaviour of the program, several parts of the program should be benchmarked. - the complete unification procedure - each part of the unification loop - the...
Currently, the normal form is not stable by substitution. Tuples are represented as sorted arrays, this property is not preserved by substitution. There are 3 possible ways to fix it:...
To avoid crash when reading the database from the disk, a magic number corresponding to the version of Dowsing could be added at the start of the file.
Software engineering - [x] Add tests - [x] Implement a proper notion of printing environment - [x] Use proper logging - [x] Plug together the unification and the database again...
There are cases where we have to fall down to proper unification. In this cases, it would be nice if it was fast. Ideally, the `stat` function would have an...
Par l'axiome (Ass-0) et curryfication, les types "a -> 'a -> b" et "a -> b" devraient être unifiables avec { 'a = unit } ; de même pour "a...
Currently, the handling of unifiers is a bit rough: 1. Unifier simplification simply "inlines" all the unnamed variables. It could do a bit more, like simplify alpha-conversions. 2. Unnamed variables...
Currently, with `'a -> 'b` `c1 * c2 * c3 * c4 * c5 * c6 * c7 * c8 -> 'b` the number of AC solutions tried and the...