search

ucsd-progsys / liquid-fixpoint

Horn Clause Constraint Solving for Liquid Types
BSD 3-Clause "New" or "Revised" License
141 stars 61 forks source link

Maps #135

Closed BenjaminCosman closed 9 years ago

BenjaminCosman commented 9 years ago

See:

https://github.com/ucsd-progsys/liquid-fixpoint/blob/9885756db01815a4457ac4a4725a82f870aabe4c/tests/todo/maps1.hs.fq

Haskell solver must never have been taught the dark secrets Ocaml knows about the theory of Maps (similar to #83).

ranjitjhala commented 9 years ago

Yes , this is easy...

On Sep 16, 2015, at 12:10 AM, bmcfluff notifications@github.com wrote:

See:

https://github.com/ucsd-progsys/liquid-fixpoint/blob/9885756db01815a4457ac4a4725a82f870aabe4c/tests/todo/maps1.hs.fq

Haskell solver must never have been taught the dark secrets Ocaml knows about the theory of Maps (similar to #83).

— Reply to this email directly or view it on GitHub.

ranjitjhala commented 9 years ago
  1. Look at external/fixpoint/{smtLIB2, theories.ml} and make the corresponding addition in Theories.hs
  2. See the corresponding thing for smt_set_* and
  3. Make the relevant additions for smt_map_*.
BenjaminCosman commented 9 years ago

Fixed by 8b8d497

ranjitjhala commented 9 years ago

Nice!! Thanks!