search

Drup / dowsing

᚛ A type of divination employed in attempts to locate identifiers matching a given type expression
ISC License
35 stars 4 forks source link

Wip: repair hullot #2

Closed c-cube closed 3 years ago

c-cube commented 3 years ago

unification is still not correct, it fails to detect some constructor conflicts. Example:

./main.sh unif "('a list * 'b option) list " "(bool * int list) list"
t1: ( \0 list, \1 option ) list
t2: ( bool, int list ) list
Unification: 0.000015

Quasi:
  \3 = \1 option
  \4 = int list
Pure:
  \2,\3 = bool,\4
Arrows:

Occur-check: true
System: -1, 1, 1, -1
Bitvars: [|0b1100; 0b1010; 0b101; 0b11|]
Symbols: [|\5; \6; bool; bool|]
Solutions[4]:
  0b110: { (\2 := \6)| (\3 := bool)| (\4 := \6) }
  0b111: { (\2 := \6)| (\3 := (bool, \5))| (\4 := (\6, \5)) }
  0b1001: { (\2 := bool)| (\3 := \5)| (\4 := \5) }
  0b1011: { (\2 := (bool, \6))| (\3 := \5)| (\4 := (\6, \5)) }