#|

Copyright © 2022 by Pete Manolios 

Author: Pete Manolios
Date:   9/16/2022

Code used in lecture 3 of Computer-Aided Reasoning.  

|#

(in-package "ACL2S")

"BEGIN DEMO 1

"

"Dotted pairs"
(cons 1 2)

"*, +, append are macros"

(+ 1 2 3 4)
(+)
(*)
(* 1 2 3)
(append '(1 2) '(3 4))
(append '(1 2) '(3 4) '(5 6))

(listp '(1 2))
(listp (cons 1 2))

(tlp '(1 2))
(tlp (cons 1 2))

(car '(1 . 2))
(cdr '(1 . 2))
(cadr '(1 2 . 3))
(cddr '(1 2 . 3))

(in-package "ACL2")
:pe +
:pe *
:pe append
:pe listp
:pe true-listp
:pe acl2s::tlp
:pe tlp
:pe cadr
:trans1 (* 1 2 3)
:trans1 (*)
:trans1 (cadr '(1 2 . 3))
:trans1 (append '(1 2) '(3 4) '(5 6))
(in-package "ACL2S")

#|

Rotate buffer to the left begin.

An example of how contracts are used to help students learn how
to program and specify contracts.

|#


"
Define a function that given a buffer, l, (a true list) and a natural
number, n, rotates the buffer to the left n times.

(Rotate-Left '(1 2 3 4 5) 2) = '(3 4 5 1 2)

"

(definec Rotate-Left (l :tl n :nat) :tl
  (cond ((= n 0) l)
        (t (Rotate-left (app (tail l) (head l))
                        (1- n)))))

(definec Rotate-Left (l :tl n :nat) :tl
  (cond ((= n 0) l)
        ((endp l) nil)
        (t (Rotate-Left (app (tail l) (head l))
                        (1- n)))))

(definec Rotate-Left (l :tl n :nat) :tl
  (cond ((= n 0) l)
        ((endp l) nil)
        (t (Rotate-Left (app (tail l) (list (head l)))
                               (1- n)))))
  
(check= (Rotate-Left '(1 2 3 4 5) 2) '(3 4 5 1 2))

(definec Rotate-Left2 (l :tl n :nat) :tl
  (match (list l n)
    ((:or (& 0) (nil &)) l)
    (((f . r) &) (Rotate-Left2 (app r (list f)) (1- n)))))

(property (l :tl n :nat)
  (== (Rotate-Left2 l n)
      (Rotate-Left l n)))