New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add sequence support. #394

Merged
merged 2 commits into from Jun 16, 2018

Conversation

Projects
None yet
2 participants
@joelburget
Copy link
Collaborator

joelburget commented Jun 14, 2018

This is mostly working, but has four issues that I know of.

  1. I haven't implemented C compilation. I don't know a lot about this feature and in particular aren't sure how we should format sequences.

  2. z3 returns sequences with let-bound variables in them. Example:

(let ((a!1 (seq.++ (seq.unit 42)
                   (seq.++ (seq.unit 44) (seq.++ (seq.unit 46) (seq.unit 29))))))
(let ((a!2 (seq.++ (seq.unit 36)
                   (seq.++ (seq.unit 38) (seq.++ (seq.unit 40) a!1)))))
  (seq.++ (seq.unit 28) (seq.++ (seq.unit 32) (seq.++ (seq.unit 34) a!2))))))

(this is [28, 32, 34, 36, 38, 40, 42, 44, 46, 29])

To parse these back into sbv, we need to evaluate them. This is doable, but its really surprising to me that sbv has to do this. I would expect normalized results back from z3. Also the representation is ridiculous (this is the best way they could think to represent lists in a lisp?). Perhaps I'm just doing something wrong.

  1. There are still a few failing tests (and one that hangs) when run on my computer.

  2. Sequence docstrings need some work. The examples haven't actually been run due to issue 2.

@joelburget

This comment has been minimized.

Copy link
Collaborator Author

joelburget commented Jun 14, 2018

Also, the fibonacci example works fine (modulo reading the result back from z3), but is not very compelling. Suggestions welcome for better examples.

@LeventErkok

This comment has been minimized.

Copy link
Owner

LeventErkok commented Jun 14, 2018

Can you rebase this first? So we can see if it at least passes the current test suite.

Also, I'm a bit concerned that we have Strings and Sequences and there's quite a bit of duplication in between those two. Would be nice to unify them somehow I think; to have one interface to rule them all. (A String then can simply be a Sequence of characters.) Have you considered that kind of a design?

@joelburget joelburget force-pushed the joelburget:sequences branch from d9e2789 to 4c4dcda Jun 14, 2018

@joelburget

This comment has been minimized.

Copy link
Collaborator Author

joelburget commented Jun 14, 2018

Would be nice to unify them somehow

I agree, and I started with more of a unified design: no newtype Sequence. However, there's a bit of a problem -- we end up with overlapping instances for HasKind and SymWord.

instance {-# overlaps #-} HasKind String  where kindOf _ = KString
instance {-# overlappable #-} HasKind a => HasKind [a] where
  kindOf _ = KSequence (kindOf (undefined :: a))

instance {-# overlaps #-} SymWord String where
instance {-# overlappable #-} SymWord a => SymWord [a] where

Now, OverlappingInstances is not so bad, but I find myself needing to use this instance when a has not been instantiated monomorphically, which requires IncoherentInstances. So I decided to be a bit more conservative and add the Sequence newtype. However it's possible this approach could be made to work if I take a longer look.

I later added a typeclass both strings and sequences are instances of.

class SymWord a => SymbolicSequence as a | as -> a where
  elemAt        :: SBV as -> SInteger             -> SBV a
  concat        :: SBV as -> SBV as               -> SBV as
  length        :: SBV as                         -> SInteger
  null          :: SBV as                         -> SBool
  head          :: SBV as                         -> SBV a
  tail          :: SBV as                         -> SBV as
  fromElem      :: SBV a                          -> SBV as
  implode       :: [SBV a]                        -> SBV as
  isInfixOf     :: SBV as -> SBV as               -> SBool
  isSuffixOf    :: SBV as -> SBV as               -> SBool
  isPrefixOf    :: SBV as -> SBV as               -> SBool
  take          :: SInteger -> SBV as             -> SBV as
  drop          :: SInteger -> SBV as             -> SBV as
  subSeq        :: SBV as -> SInteger -> SInteger -> SBV as
  replace       :: SBV as -> SBV as -> SBV as     -> SBV as
  indexOf       :: SBV as -> SBV as               -> SInteger
  offsetIndexOf :: SBV as -> SBV as -> SInteger   -> SInteger

infixr 5 .++
(.++) :: SymbolicSequence as a => SBV as -> SBV as -> SBV as
(.++) = concat

-- | Short cut for 'elemAt'
(.!!) :: SymbolicSequence as a => SBV as -> SInteger -> SBV a
(.!!) = elemAt

However, I found that this class provided no benefit, but sometimes caused typeclass resolution to fail. It also provided very little benefit in terms of code reuse, so I dropped it.

It's also not obvious to me how to share more of the current implementations, since there is newtype wrapping and unwrapping all over for sequences, even though the implementations for Sequence were copy-pasted then modified.

@joelburget

This comment has been minimized.

Copy link
Collaborator Author

joelburget commented Jun 14, 2018

hlint fixed. Unfortunately doctest is going to continue to fail until we can read back z3 sequences.

@LeventErkok

This comment has been minimized.

Copy link
Owner

LeventErkok commented Jun 15, 2018

Thanks! This sort of analysis really helps with the design choices.

I'm about to make a release (for overflow detection functionality) on the master branch. Once that is out I'll merge this into a branch and take it from there.

@LeventErkok LeventErkok changed the base branch from master to sequences Jun 16, 2018

@LeventErkok LeventErkok merged commit e6f2b6c into LeventErkok:sequences Jun 16, 2018

2 checks passed

continuous-integration/appveyor/pr AppVeyor build succeeded
Details
continuous-integration/travis-ci/pr The Travis CI build passed
Details
@joelburget

This comment has been minimized.

Copy link
Collaborator Author

joelburget commented Jun 17, 2018

An update on the design: I tried out an idea to remove the newtype Sequence. Following the same trick that the prelude uses to avoid overlapping instances in Show, I added literalList / unliteralList to SymWord:

joelburget@5447c39#diff-8fbdad1f4b859360c19c404e5d7a2996R386

We also remove the SymWord String and SymWord [a] instances. Now every literalList / unliteralList, except the instance for Char builds deals with sequences. The instance for Char deals with Strings.

This seems to work, at least as far as I implemented in this sketch. It's not fully complete but I don't forsee any problems.

The downside to this approach is some extra duplication. Any time you might be dealing with a symbolic list is going to require an extra function. Eg:

symbolicList  :: String -> Symbolic (SBV [a])
symbolicLists :: [String] -> Symbolic [SBV [a]]
freeList      :: String -> Symbolic (SBV [a])
freeList_     :: Symbolic (SBV [a])
forallList    :: String -> Symbolic (SBV [a])
forallList_   :: Symbolic (SBV [a])
existsList    :: String -> Symbolic (SBV [a])
existsList_   :: Symbolic (SBV [a])

Additionally, I had to duplicate ite to make a list version, which I called iteL:

ite :: Mergeable a => SBool -> a -> a -> a
iteL :: SymWord a => SBool -> SBV [a] -> SBV [a] -> SBV [a]

So, I'm not sure whether this route is better or worse. Thoughts?

@LeventErkok

This comment has been minimized.

Copy link
Owner

LeventErkok commented Jun 17, 2018

Just like SString is not [SChar], I think we'll have to let go of the notion that SSequence a is [SBV a]. I think the right design is not to expose the underlying list in any way, but rather keep it as an abstract type completely. Is that what you were thinking?

@joelburget

This comment has been minimized.

Copy link
Collaborator Author

joelburget commented Jun 18, 2018

Absolutely agreed. I think that this work is everywhere consistent with that philosophy. The type parameter is phantom.

@LeventErkok LeventErkok referenced this pull request Jul 6, 2018

Closed

Add support for lists #406

@LeventErkok

This comment has been minimized.

Copy link
Owner

LeventErkok commented Sep 7, 2018

@joelburget

Hi Joel,

This is now merged to master, with some changes. Some comments; addressing the questions you raised:

  • Instead of SSequence I used SList, which is more in the Haskell spirit
  • C compilation is indeed tricky. I think this is best postponed till someone actually needs/asks for it. (There are issues regarding allocation/deallocation, and it isn't clear how to do those things in C: Use a linked list, or an STL Vector? Nested lists are a whole another story.)
  • z3 examples with let-bound variables: There's an option you can pass to z3 (pp.max_depth) that practically takes care of this problem. So, not an issue.
  • I've written a bunch of tests and all seem to be passing right now. (There are two failing doctests but they have to do with z3 timing out on them, and not related to lists.)
  • I like the Fibonacci example; simple to understand and fun. I added a very simple nested-list example as well. Though indeed would be nice to have some more compelling examples.
  • I agree that the SymbolicSequence class is a seemingly nice idea, but it doesn't really pay off. I agree that going with qualified imports is the simpler/cleaner solution here.
  • The whole overlapping instance issue due to conflation of SString and SList [a] is unfortunate. However, I was able to get rid of the newtype Sequence by doing a bit of type-trickery, while also avoiding symbolicList etc. The trick here is that the internal representation is essentially typeless (well, phantom types), and we can be careful about KString by doing a dynamic cast. This avoids the need of the extra wrapper, and works well in practice. (The Sequence construct was espeically heavy and unsightly when modeling nested symbolic lists.) I think it all works, but some extra testing is always welcome.

I think this addresses all the concerns regarding support for symbolic lists. If you can do some testing on your side, and give it a spin and maybe contribute another example; it'd be ready for release.

Thanks for the nice contribution! It was a great starting point charting out the different design points; really helped me in getting it integrated. Much appreciated.

@joelburget joelburget deleted the joelburget:sequences branch Sep 7, 2018

@joelburget

This comment has been minimized.

Copy link
Collaborator Author

joelburget commented Sep 7, 2018

Thanks for merging this in! I'm really happy to see it in master. @bts and I were just talking about using this yesterday so the timing is perfect.

@LeventErkok

This comment has been minimized.

Copy link
Owner

LeventErkok commented Sep 8, 2018

@joelburget @bts

Great! Would be good to have this running in some real project to make sure all the kinks are ironed out.

Let me know when you're done giving it a spin and I'll make a hackage release; hopefully in the next week or so?

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment