samth/test-bugs — Issue #87: a defproperty that runs  in Dracula, but won't admit
Author: racket-bug-submit
Created: 2012-03-08 00:49:26+00:00
State: open
Labels: acl2, anon-submit, gnats-migrated, invalid

###### Originally submitted on: Wed Oct 29 18:56:01 -0400 2008
#f
Property definitions usually admit under the ACL2 mode in Dracula, but there seems to be at least one case where a runnable property fails to admit

##### Steps to Reproduce:

(include-book "doublecheck" :dir :teachpacks)
(defun is-prefix (ps xs)
(or (endp ps)
(and (not (endp xs))
(equal (car ps) (car xs))
(is-prefix (cdr ps) (cdr xs)))))
(defun pattern-in (ps xs)
(if (endp xs)
(endp ps)
(or (is-prefix ps xs)
(pattern-in ps (cdr xs)))))

;(match-prefix ps xs) = (qs rs ys)
; where qs = longest sequence prefixing is both ps and xs
; (append qs rs) = ps --ie, rs is what's left of ps
; and (append qs ys) = xs --ie, ys is what's left of xs
(defun match-prefix (ps xs)
(if (or (endp ps) (endp xs)
(not (equal (car ps) (car xs))))
(list nil ps xs)
(let* ((pspsxs (match-prefix (cdr ps) (cdr xs))))
(list (cons (car ps) (car pspsxs))
(cadr pspsxs)
(caddr pspsxs)))))

; (break-at-prefix ps xs) = (before after)
; where (append before ps after) = xs if ps occurs in xs
; and before = xs, after=nil otherwise
(defun break-at-pattern (ps xs)
(if (endp xs)
(list nil nil)
(let* ((pspsxs (match-prefix ps xs)))
(if (null (cadr pspsxs))
(list nil (caddr pspsxs))
(let* ((xsxs (break-at-pattern ps (cdr xs))))
(list (cons (car xs) (car xsxs))
(cadr xsxs)))))))

(defproperty bap-when-pattern-present-tst
(ps :value (random-list-of (random-integer))
xs :value (random-list-of (random-integer)))
(implies (and (true-listp ps)
(true-listp xs)
(pattern-in ps xs))
(equal (append (car (break-at-pattern ps xs))
ps
(cadr (break-at-pattern ps xs)))
xs)))

##### Release:

4.1

##### Environment:

windows "Windows NT 5.1 (Build 2600) Service Pack 3" (win32\i386\3m) (get-display-depth) = 32
Human Language: english
(current-memory-use) 98983816

Collections:
(("C:\\Documents and Settings\\Rex Page\\Application Data\\PLT Scheme\\4.1\\collects" non-existent-path) ("C:\\Program Files\\PLT\\collects" "afm" "algol60" "browser" "combinator-parser" "compiler" "config" "defaults" "drscheme" "dynext" "embedded-gui" "eopl" "errortrace" "ffi" "file" "framework" "frtime" "games" "graphics" "gui-debugger" "help" "hierlist" "htdch" "htdp" "html" "icons" "info-domain" "lang" "launcher" "lazy" "macro-debugger" "make" "mred" "mrlib" "mysterx" "mzcom" "mzlib" "mzscheme" "net" "openssl" "parser-tools" "planet" "plot" "preprocessor" "profj" "r5rs" "r6rs" "readline" "redex" "rnrs" "s-exp" "scheme" "scribble" "scribblings" "setup" "sgl" "slatex" "slideshow" "srfi" "stepper" "string-constants" "swindle" "syntax" "syntax-color" "teachpack" "test-box-recovery" "test-engine" "tex2page" "texpict" "trace" "typed-scheme" "version" "web-server" "wxme" "xml"))
Computer Language: (("Dracula Languages" "Dracula v4.2") (#("C:\\ACL2-3.3\\bin\\acl2.exe" #f) . #(#t write mixed-fraction-e #f #t debug)))

###### This bug was converted from Gnats bug [9876](http://bugs.racket-lang.org/query/?cmd=view&pr=9876).

[anon-submit page AT ou.edu]