#|

Copyright © 2022 by Pete Manolios 

Author: Pete Manolios
Date:   9/20/2022

Code used in lecture 4 of Computer-Aided Reasoning.  

|#

(in-package "ACL2S")

"BEGIN DEMO ROTATE LEFT

"

#|

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
  (match (list l n)
    ((:or (& 0) (nil &)) l)
    (((f . r) &) (Rotate-Left (app r (list f)) (1- n)))))

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

" What is the (worst-time) complexity of Rotate-Left? "

(time$ (Rotate-Left '(1 2 3 4 5) (expt 10 6)))
(time$ (Rotate-Left '(1 2 3 4 5) (expt 10 7)))
(time$ (Rotate-Left '(1 2 3 4 5) (expt 10 8)))

" Exponential in the size of its input.
  Adding a 0 to the end of n increased running time by a factor of 10!
"

" Define an efficient version "

(definec eRotate-Left (l :tl n :nat) :tl
  (match l
    (nil nil)
    (& (Rotate-Left l (mod n (len l))))))

" What is the (worst-time) complexity of eRotate-Left? "

(time$ (eRotate-Left '(1 2 3 4 5) (expt 10 6)))
(time$ (eRotate-Left '(1 2 3 4 5) (expt 10 7)))
(time$ (eRotate-Left '(1 2 3 4 5) (expt 10 8)))

(property (l :tl n :nat)
  :proofs? nil
  (== (eRotate-Left l n)
      (Rotate-Left l n)))

(ubt! 1)

"END DEMO ROTATE LEFT

"