Merge pull request #757 from harshrc/master

Remove GL backend for fixers for now. Fixed type bug in range types.

books/acl2s/cgen/build-enumcalls.lisp

@@ -169,7 +169,7 @@
 ; is the place-holder for the random-seed or BE arg 
   (if (defdata::possible-constant-value-p type)
       (acl2::make enum-info% :domain-size 1 :min-rec-depth 0 :max-rec-depth 1
-                  :category :singleton :expr type :expr2 `(mv ',type seed.)) 
+                  :category :singleton :expr type :expr2 `(mv ',type seed.))
 ;ALSO HANDLE SINGLETON TYPES DIRECTLY
 
     (let ((entry (assoc-eq type (table-alist 'defdata::type-metadata-table wrld))))
@@ -185,7 +185,7 @@
              (TI.min (cdr (assoc-eq :min-rec-depth al)))
              (TI.max (cdr (assoc-eq :max-rec-depth al)))
 
-             (TI.ndef (cdr (assoc-eq :normalized-def al)))
+             (TI.def (cdr (assoc-eq :def al)))
              ((unless (or (eq 't TI.size)
                          (posp TI.size)))
               (prog2$
@@ -203,18 +203,18 @@
 ; interesting numeric type, like 4divp, primep, arithmetic
 ; progression, etc. But you can use / constructor to define some
 ; interesting types, so I need to think about how to make this more general!! TODO
-             ((when (and (and (eq 'ACL2S::RANGE (car TI.ndef))
+             ((when (and (and (consp TI.def) (eq 'ACL2S::RANGE (car TI.def))
                               (defdata::range-subtype-p
                                 range
-                                (defdata::get-tau-int (cadr TI.ndef) (third TI.ndef))))
+                                (defdata::get-tau-int (cadr TI.def) (third TI.def))))
                          (defdata::subtype-p TI.pred 'integerp wrld)
                          (non-empty-non-universal-interval-p range)))
               (make-range-enum-info% 'acl2s::integer range (list entry)))
 
-             ((when (and (and (eq 'ACL2S::RANGE (car TI.ndef))
+             ((when (and (and (consp TI.def) (eq 'ACL2S::RANGE (car TI.def))
                               (defdata::range-subtype-p
                                 range
-                                (defdata::get-tau-int (cadr TI.ndef) (third TI.ndef))))
+                                (defdata::get-tau-int (cadr TI.def) (third TI.def))))
                          (defdata::subtype-p TI.pred 'acl2-numberp wrld)
                          (non-empty-non-universal-interval-p range)))
               (make-range-enum-info% type range (list entry))))

books/acl2s/cgen/cert.acl2

@@ -1,7 +1,7 @@
-(ld "data-structures/define-u-package.lsp" :dir :system)
-(include-book "coi/symbol-fns/portcullis" :dir :system)
-(include-book "centaur/gl/portcullis" :dir :system)
-(include-book "centaur/satlink/portcullis" :dir :system)
+;; (ld "data-structures/define-u-package.lsp" :dir :system)
+;; (include-book "coi/symbol-fns/portcullis" :dir :system)
+;; (include-book "centaur/gl/portcullis" :dir :system)
+;; (include-book "centaur/satlink/portcullis" :dir :system)
 (ld "../package.lsp")
 
 

books/acl2s/cgen/testing-regression.lsp

@@ -1051,5 +1051,53 @@
 )
 
 
+;; CHeck singleton range types are working correctly.
 
+(DEFDATA DECIMAL_30_TO_30 (RANGE RATIONAL (30 <= _ <= 30)))
+(test? (implies (DECIMAL_30_TO_30P x) (= x 30)))
 
+
+;; Check len support in Cgen.
+(defdata d1 (oneof 'a 'b 'c 'd 'e 'f))
+
+(defdata ld1-aux
+  (listof d1)
+  :min-rec-depth 2
+  :max-rec-depth 201)
+
+(acl2s::defunc ld1p (x)
+  :input-contract t
+  :output-contract (booleanp (ld1p x))
+ (and (ld1-auxp x)
+      (>= (len x) 3)
+      (<= (len x) 200)))
+
+;; (defdata ld1 (listof d1))
+
+(defdata d2 'g)
+
+(defdata ld2-aux
+  (listof d2)
+  :min-rec-depth 0
+  :max-rec-depth 7)
+
+(acl2s::defunc ld2p (x)
+  :input-contract t
+  :output-contract (booleanp (ld2p x))
+  (and (ld2-auxp x)
+       (<= (len x) 6)))
+
+Now, cgen fails to find a counterexample for this.
+(acl2s-defaults :set verbosity-level 3)
+
+(test?
+ (implies (and (ld2p a)
+               (ld1p b)
+               (ld1p c)
+               (integerp x)
+               (<= x (len a))
+               (> x 0)
+               (equal (len a) (len b)))
+
+          (and (consp c)
+               (<= x (len c)))))

books/acl2s/cgen/top.lisp

@@ -469,12 +469,12 @@ information in a human-readable form. </p>
 
 
 ; [2016-04-03 Sun] Add fixers support to Cgen
-(defconst *fixers-enabled* t)
-(make-event
- (if *fixers-enabled*
-     '(progn
-        (include-book "fixers2" :ttags :all)
-        (include-book "cgen-rules")
-        (gl::gl-satlink-mode)
-        )
-   '(value-triple :invisible)))
+(defconst *fixers-enabled* nil)
+;; (make-event
+;;  (if *fixers-enabled*
+;;      '(progn
+;;         (include-book "fixers2" :ttags :all)
+;;         (include-book "cgen-rules")
+;;         (gl::gl-satlink-mode)
+;;         )
+;;    '(value-triple :invisible)))

books/acl2s/mode-acl2s-dependencies.lisp

@@ -30,12 +30,12 @@
 (include-book "acl2s/cgen/top" :dir :system :ttags :all)
 
 ; Added for fixers support. [2016-02-19 Fri]
-(make-event
- (if ACL2S::*fixers-enabled*
-     '(progn
-        (include-book "centaur/gl/gl" :dir :system)
-        (include-book "centaur/satlink/top" :dir :system)
-        (include-book "centaur/gl/bfr-satlink" :dir :system :ttags :all)
-        (include-book "centaur/satlink/check-config" :dir :system))
-   '(value-triple :invisible)))
+;; (make-event
+;;  (if ACL2S::*fixers-enabled*
+;;      '(progn
+;;         (include-book "centaur/gl/gl" :dir :system)
+;;         (include-book "centaur/satlink/top" :dir :system)
+;;         (include-book "centaur/gl/bfr-satlink" :dir :system :ttags :all)
+;;         (include-book "centaur/satlink/check-config" :dir :system))
+;;    '(value-triple :invisible)))