Filtering...

match-testing

books/acl2s/match-testing
other
(in-package "ACL2S")
other
(include-book "acl2s/custom" :dir :system :ttags :all)
other
(set-termination-method :ccg)
other
(definec int-class
  (x :int)
  :pos (match x (:pos 1) (:even 2) (:neg 3)))
other
(definec int-class2
  (x :int)
  :pos (match x
    (:pos (:even 1) (:odd 2))
    (:neg (:even 3) (:odd 4))
    (0 5)))
other
(definec int-class3
  (x :int)
  :pos (match x
    (:pos (:even 1) (& 2))
    (:neg (:even 3) (& 4))
    (& 5)))
other
(property (x :int)
  (== (int-class2 x)
    (int-class3 x)))
other
(must-fail (definec int-class4
    (x :int)
    :pos (match x
      (:pos (:even 1) (& 2))
      (:neg (:even 3) (:nat 4))
      (& 5))))
other
(definec fact
  (n :nat)
  :pos (match n
    (0 1)
    (& (* n (fact (1- n))))))
other
(definec fact1
  (n :nat)
  :pos (match n
    ((:t (< n 2)) 1)
    (& (* n (fact1 (1- n))))))
other
(property (n :nat)
  (== (fact1 n) (fact n)))
other
(definec fib
  (n :nat)
  :pos :skip-tests t
  (match n
    ((:or 0 1) 1)
    (& (+ (fib (1- n)) (fib (- n 2))))))
other
(definec fib2
  (n :nat)
  :pos :skip-tests t
  (match n
    (0 1)
    (1 1)
    (& (+ (fib2 (1- n)) (fib2 (- n 2))))))
other
(definec fib3
  (n :nat)
  :pos :skip-tests t
  (match n
    ((:t (< n 2)) 1)
    (& (+ (fib3 (1- n)) (fib3 (- n 2))))))
other
(property (n :nat)
  :testing? nil
  (and (== (fib3 n) (fib n))
    (== (fib2 n) (fib n))))
other
(definec pascal
  (i :nat j :nat)
  :pos :skip-tests t
  (match (list i j)
    ((:or (0 &) (& 0) (& !i)) 1)
    (& (+ (pascal (1- i) (1- j))
        (pascal (1- i) j)))))
other
(definec pascal2
  (i :nat j :nat)
  :pos :skip-tests t
  (match (list i j)
    ((0 &) 1)
    ((& 0) 1)
    ((!i !i) 1)
    (& (+ (pascal2 (1- i) (1- j))
        (pascal2 (1- i) j)))))
other
(property (i :nat j :nat)
  :testing? nil
  (== (pascal i j)
    (pascal2 i j)))
other
(definec mem
  (e :all x :tl)
  :bool (match x
    (nil nil)
    ((!e . &) t)
    ((& . r) (mem e r))))
other
(definec subset
  (x :tl y :tl)
  :bool (match x
    (nil t)
    ((f . r) (and (mem f y)
        (subset r y)))))
other
(definec acl2-count2
  (x :all)
  :nat (match x
    ((a . b) (+ 1
        (acl2-count2 a)
        (acl2-count2 b)))
    (:rational (:integer (integer-abs x))
      (& (+ (integer-abs (numerator x))
          (denominator x))))
    ((:r complex/complex-rationalp) (+ 1
        (acl2-count2 (realpart x))
        (acl2-count2 (imagpart x))))
    (:string (length x))
    (& 0)))
other
(property (x :all)
  (== (acl2-count2 x)
    (acl2-count x)))
other
(definec acl2s-size2
  (x :all)
  :nat (match x
    ((a . b) (+ 1
        (acl2s-size2 a)
        (acl2s-size2 b)))
    (:rational (integer-abs (numerator x)))
    ((:r stringp) (length x))
    (& 0)))
other
(property (x :all)
  (== (acl2s-size2 x)
    (acl2s-size x)))
other
(defdata foo
  (record (x . nat)))
other
(defdata bar
  (record (y . nat)))
other
(definec baz
  (a :all)
  :boolean (match a ((:or :foo :bar) t) (& nil)))
other
(property (a :foo) (baz a))
other
(property (a :bar) (baz a))
other
(property (a :int)
  (! (baz a)))
other
(property (a :all)
  (iff (baz a)
    (or (foop a) (barp a))))
other
(definec nested
  (x :all)
  :all (match x
    ((:int :int) 1)
    (((:int :nat) :int) 2)
    ((:or ((:bool :bool)) :bool) 3)
    (& 4)))
other
(check= (nested '(1 2)) 1)
other
(check= (nested '((1 2) 3)) 2)
other
(check= (nested t) 3)
other
(check= (nested '((t nil))) 3)
other
(check= (nested '(t nil)) 4)