Fixtype of lists of strings fails

[acoglio]

This page shows, at the very end, a form to create a fixing function for the existing STRING-LISTP predicate. However, the following fails (starting in a fresh ACL2 session):

(include-book "centaur/fty/top" :dir :system)
(fty::deflist string-list :pred string-listp :elt-type stringp)

(I'm assigning this issue based on the author indicated in centaur/fty/deftypes.lisp.)

[solswords]

The following form works (somewhat to my surprise):
(fty::deflist string-list :pred string-listp :elt-type stringp :true-listp
t)

I'm not sure how well fty's type-defining events deal with functions that
it would normally generate but that already exist. I believe it will only
work at all with predicates that already exist, not fixing functions or
constructors/accessors/etc., and it's not a feature that's very well tested
for predicates either. As the above example shows, the setting of
:true-listp has to match the existing predicate for lists and alists, and
there may well be other gotchas.

• Sol

On Thu, Oct 13, 2016 at 11:47 AM, Alessandro Coglio <
notifications@github.com> wrote:

Assigned #654 #654 to @solswords
https://github.com/solswords.

—
You are receiving this because you were mentioned.
Reply to this email directly, view it on GitHub
#654 (comment), or mute the
thread
https://github.com/notifications/unsubscribe-auth/AFKzKd36kHwdZf1ybEbVBTq4XBGL18Svks5qzmCPgaJpZM4KWHSy
.

[acoglio]

Thanks for the quick reply.

It seems that the success of the form depends on the included books.

The following fails for me:
(include-book "centaur/fty/top" :dir :system)
(fty::deflist string-list :pred string-listp :elt-type stringp :true-listp t)

The following succeeds:
(include-book "centaur/fty/deftypes" :dir :system)
(include-book "centaur/fty/basetypes" :dir :system)
(fty::deflist string-list :pred string-listp :elt-type stringp :true-listp t)

The following succeeds as well:
(include-book "centaur/fty/deftypes" :dir :system)
(include-book "centaur/fty/basetypes" :dir :system)
(fty::deflist string-list :pred string-listp :elt-type stringp) ; no :true-listp

[ragerdl]

Just reflecting upon what you already know: As you've ascertained, the form
works when less books are included. That's probably because that smaller
set of books doesn't define CAR-OF-STRING-LIST-FIX-X-UNDER-STREQV. Since
the top book transitively includes that (different) definition, the form
fails. That is, unless the :true-listp flag is added so that the
definition trying to be added matches what's already there. Most of ACL2's
built-in list types require true-listp's, so this is probably a common
occurrence for built-in types.

On Fri, Oct 14, 2016 at 8:37 AM, Alessandro Coglio <notifications@github.com

wrote:

Thanks for the quick reply.

It seems that the success of the form depends on the included books.

The following fails for me:
(include-book "centaur/fty/top" :dir :system)
(fty::deflist string-list :pred string-listp :elt-type stringp :true-listp
t)

The following succeeds:
(include-book "centaur/fty/deftypes" :dir :system)
(include-book "centaur/fty/basetypes" :dir :system)
(fty::deflist string-list :pred string-listp :elt-type stringp :true-listp
t)

The following succeeds as well:
(include-book "centaur/fty/deftypes" :dir :system)
(include-book "centaur/fty/basetypes" :dir :system)
(fty::deflist string-list :pred string-listp :elt-type stringp) ; no
:true-listp

—
You are receiving this because you are subscribed to this thread.
Reply to this email directly, view it on GitHub
#654 (comment), or mute
the thread
https://github.com/notifications/unsubscribe-auth/ACJE_lZsVnVP6rGqRgzDMzrGqroVHRNtks5qz4WHgaJpZM4KWHSy
.

[acoglio]

Right, but even with :true-listp t, I get a failure if I include fty/top, while it works if I include only fty/deftypes and fty/basetypes.

Perhaps we should look into making fty/top and the form (with :true-listp t) compatible with each other? When using FTY, it seems reasonable to include fty/top as a starting point.

[solswords]

1. I wouldn't generally expect it to work without the :true-listp t. We
   could perhaps fix it so that it determines true-listp automatically when
   the predicate is already defined (check (not (type-listp 'foo)) to
   determine the value of true-listp).
2. fty/baselists includes std/strings/eqv which defines its own fixing
   function for string-listp, str::string-list-fix. If we specify that as our
   fixing function, it still doesn't work because they are defined slightly
   differently and thus aren't redundant (the fty version gives a measure
   explicitly and is inline). If we fix that, more problems come up and I
   haven't gone further. I suppose we can include fty/deftypes in
   std/strings/eqv and make deflists for string-listp and character-listp
   there instead of doing it manually. I can try doing that at some point,
   but if anyone else wants to do it for me I won't mind.

On Fri, Oct 14, 2016 at 9:59 AM, Alessandro Coglio <notifications@github.com

wrote:

Right, but even with :true-listp t, I get a failure if I include fty/top,
while it works if I include only fty/deftypes and fty/basetypes.

Perhaps we should look into making fty/top and the form (with :true-listp
t) compatible with each other? When using FTY, it seems reasonable to
include fty/top as a starting point.

—
You are receiving this because you were mentioned.
Reply to this email directly, view it on GitHub
#654 (comment), or mute
the thread
https://github.com/notifications/unsubscribe-auth/AFKzKbtnqy5wcfBZdTpGAO9YQANHoYoHks5qz5jCgaJpZM4KWHSy
.

[acoglio]

I gave your suggested fix a shot (it's in my acl2 clone, branch string-list-fix), but when I try building I get an error that might have to do with circular dependencies. For instance, doing make clean (just to be sure) and then cert.pl std/strings/eqv.lisp hangs at the following line (after building a number of other certificates):

Making /Users/AC/Kestrel/ACL2/acl2/books/std/strings/../../xdoc/str.acl2x on 19-Oct-2016 17:49:51

I'm not sure what an .acl2x file is, and I would have to study the STD and FTY code a bit to understand where the error arises and how to break the circular dependency (if that's the problem).

[solswords]

xdoc/str is an awful sort of book (other examples being std/strings/defs-program and std/strings/pretty-program) which exists to provide program mode definitions of various useful functions without depending on the full dependencies of the books where they're defined. These books get certified in two passes, the first of which produces an .acl2x file instead of a regular certificate. The acl2x file is read as part of the second pass and tells ACL2 how make-events expand, so basically it determines the actual contents of the book. This is sound because in the second pass ACL2 checks these events just as it would any others, and these will be the events that get loaded when the certified book is included. So it's basically OK to do whatever we want in the first pass, including modifying the expansions that are written to the acl2x file.

So in xdoc/str, in the first pass we include a bunch of (possibly uncertified) books from std/strings and, in program mode, redundantly replicate their definitions. We arrange (using the acl2x-replace utility) that the acl2x file doesn't contain those include-books, just the program mode definitions.

So probably what's happening is that you've added a dependency in std/strings/eqv on xdoc/str (presumably because some fty books depend on it). xdoc/str doesn't exactly have a dependency on std/strings/eqv, but it probably includes it uncertified in its first pass. So when you try and include it, it also tries to include the book you're certifying, which tries to include it again, which doesn't work out too well.

This is a tricky problem and I'm not sure what to suggest. Basically, we want to use nice string functions to generate documentation for fty types, but we want to use fty to define some of those nice string functions (namely, string-list-fix). We could try to remove the dependency on xdoc/str from fty; not sure how many functions we're using from there.

@jaredcdavis might want to weigh in or just read this and be amused.