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

Replace String with Text #37

Closed gridaphobe closed 10 years ago

gridaphobe commented 10 years ago

We use Strings all over the place, especially as Symbols. This is super inefficient, which becomes apparent once you start treating liquidhaskell/fixpoint as more than a pre-processor for the ocaml fixpoint binary.

We should just use Text instead. @ranjitjhala, btw is lazy text really necesary in L.F.SmtLib2? I think we'd be fine sticking to the strict version, any individual smt command/response ought to be fairly small.

gridaphobe commented 10 years ago

Although, since we're already tied to GHC, we might as well just use FastString

ranjitjhala commented 10 years ago

I have wanted to do this for a LONG time.

Best not to tie fixpoint to GHC, so text is much better.

On Thu, Jun 26, 2014 at 2:50 AM, Eric Seidel notifications@github.com wrote:

Although, since we're already tied to GHC, we might as well just use FastString http://www.haskell.org/ghc/docs/latest/html/libraries/ghc/FastString.html#t:FastString

Reply to this email directly or view it on GitHub https://github.com/ucsd-progsys/liquid-fixpoint/issues/37#issuecomment-47176826 .

-- Ranjit.

gridaphobe commented 10 years ago

Good point, I thought fixpoint was actually tied to GHC somehow since it's got ghc-7.6.3 as a hard dependency, but it's not actually used anywhere... I'll remove the dependency.

On Wed, Jun 25, 2014 at 11:32 PM, Ranjit Jhala notifications@github.com wrote:

I have wanted to do this for a LONG time.

Best not to tie fixpoint to GHC, so text is much better.

On Thu, Jun 26, 2014 at 2:50 AM, Eric Seidel notifications@github.com wrote:

Although, since we're already tied to GHC, we might as well just use FastString < http://www.haskell.org/ghc/docs/latest/html/libraries/ghc/FastString.html#t:FastString

Reply to this email directly or view it on GitHub < https://github.com/ucsd-progsys/liquid-fixpoint/issues/37#issuecomment-47176826

.

-- Ranjit.

— Reply to this email directly or view it on GitHub https://github.com/ucsd-progsys/liquid-fixpoint/issues/37#issuecomment-47192065 .