;; ---------------------------------------------------------------------------
;; ~/events/toktrans-4.events
;; ---------------------------------------------------------------------------

(enable-theory tokens)
(enable-theory lists)

;; This is a token transformation function for converting lists of digit 
;; characters which are contained in token values to decimal integers. The 
;; function is called integer-convert.
;; It only works on the INTEGER tokens, and leaves all other tokens intact.
;; It is modelled on Bill Bevier's positional number etude.
;; The digits must first be converted from ASCII values to digits.

(defn ascii-zero () 48)
(defn ascii-nine () 57)

(defn digit-zero () 0)
(defn digit-nine () 9)

(defn base () 10)

;; This is the predicate for finding the tokens that toktrans-4 will work on.

(defn is-integer-token (tok)
 (equal (token-name tok) 'INTEGER))

;; This function checks that the list consists of digits less than b.

(defn just-digits-less-than-b (l b) 
 (if (listp l)
     (and (numberp (car l))
          (lessp (car l) b) ; Each digit must be less than the base
          (just-digits-less-than-b (cdr l) b))
     (equal l nil)))

;; This is the Horner method for computing a natural number from
;; a positional number representation l and a base b.
;; This means the list l must be in the reverse digit form - but that 
;; saves worrying about exponents and such.

(defn pn-to-nat (l b)
  (if (listp l) 
      (plus (car l)
            (times (pn-to-nat (cdr l) b) b))
      (digit-zero)))  

;; This is the conversion function that returns the digit for an ASCII code.
;; This function coerces all non-digital digits to 0, 

(defn ascii-to-digit (ascii)
 (if (or (lessp ascii (ascii-zero))
         (lessp (ascii-nine) ascii))
     (digit-zero)
     (difference ascii (ascii-zero))))

(defn valid-ascii-digit-p (ascii)
 (and (numberp ascii)
      (not (or (lessp ascii (ascii-zero))
               (lessp (ascii-nine) ascii)))))

(defn ascii-to-digits (l)
 (if (nlistp l)
     l
     (cons (ascii-to-digit (car l))
           (ascii-to-digits (cdr l)))))

(prove-lemma plistp-ascii-to-digits (rewrite)
 (equal (plistp (ascii-to-digits w))
        (plistp w)))

;; This is the token transformation function toktrans-4.

(defn integer-convert (toks)
 (if (nlistp toks)
     toks
     (if (is-integer-token (car toks))
         (let ((value (ascii-to-digits (token-value (car toks)))))
           (if (just-digits-less-than-b value (base))
               (cons (mk-token (token-name (car toks))
                            (pn-to-nat (reverse value) (base)))
                     (integer-convert (cdr toks)))
               'token-error))
         (cons (car toks) (integer-convert (cdr toks))))))

;; This is the retrieve function for one number, it converts a natural 
;; number to a positional number with digits of base b.

(defn nat-to-pn (n b)   
 (if (lessp 1 b)
     (if (zerop n)
         nil
         (cons (remainder n b)
               (nat-to-pn (quotient n b) b )))
     nil))

;; There have to be inverse functions for ascii-to-digits as well.

(defn digit-to-ascii (digit)
 (plus digit (ascii-zero))))

(defn digits-to-ascii (digits)
 (if (nlistp digits)
     digits
     (cons (digit-to-ascii (car digits))
           (digits-to-ascii (cdr digits)))))

;; When does a list consist of valid ascii digits?

(defn valid-ascii-digits-p (l)  
 (if (nlistp l)
     T
     (and (valid-ascii-digit-p (car l))
          (valid-ascii-digits-p (cdr l)))))

(prove-lemma d-a-inverse-1 (rewrite)
 (implies (and (listp value)
               (valid-ascii-digits-p value))
          (equal (digits-to-ascii (ascii-to-digits value))
                 (cons (digit-to-ascii (ascii-to-digit (car value)))
                       (digits-to-ascii (ascii-to-digits (cdr value)))))))
                 
(prove-lemma d-a-inverse-2 (rewrite)
 (implies (and (listp value)
               (valid-ascii-digits-p value))
          (equal (digits-to-ascii (ascii-to-digits value))
                 value))
 ((induct (length value))))

;; This is the retrieve function for a list. Note that I have to reverse 
;; the result before constructing the token.

(defn convert-back (toks)
 (if (nlistp toks)
     toks
     (if (is-integer-token (car toks))
           (cons (mk-token 
                  (token-name (car toks)) 
                  (reverse (digits-to-ascii 
                            (nat-to-pn (token-value (car toks)) 
                                       (base)))))
                 (convert-back (cdr toks)))
         (cons (car toks) (convert-back (cdr toks))))))


;; This lemma is to show that this direction is an inverse.

(prove-lemma inverse1 (rewrite)
 (implies (and (lessp 1 b)
               (numberp n)
               (numberp b))
          (equal (pn-to-nat (nat-to-pn n b) b)
                 n)))

;; One has to know if the positional notation lists are well-formed. 
;; Leading zeros are not acceptable.

(defn lastdigit (l)
     (if (listp l) 
         (if (not (equal (cdr l) nil))
             (lastdigit (cdr l))
             (car l))
         F))

(defn no-leading-zeros (l)
     (not (equal (lastdigit l) (digit-zero))))

(defn well-formed-pn (l b)
     (and (lessp 1 b)
              (plistp l)
              (numberp b)
              (no-leading-zeros l)
              (just-digits-less-than-b l b)))

;; This is the interesting inverse function.

(prove-lemma inverse2 (rewrite)
 (implies (well-formed-pn l b)
          (equal (nat-to-pn (pn-to-nat l b) b)
                 l)))

;; These are the lemmata needed for the proof of the main theorem.

;; If x is a just-digits-less-than-b, reversing it preserves 
;; just-digits-less-than-b-ness

(prove-lemma toktrans-4-help1 (rewrite)
  (implies (just-digits-less-than-b x b)
          (just-digits-less-than-b (reverse x) b)))

(prove-lemma toktrans-4-help2 (Rewrite)
 (implies (and (plistp x)
               (just-digits-less-than-b (reverse x) b))
          (just-digits-less-than-b x b))
 ((use (toktrans-4-help1 (x (reverse x)) (b b)))))

;; I need to know that all the integer token values are well formed.

(defn integer-tokens-well-formed (toks)
 (if (nlistp toks)
     T
     (if (is-integer-token (car toks))
         (and (no-leading-zeros 
               (reverse (ascii-to-digits (token-value (car toks)))))
              (valid-ascii-digits-p (token-value (car toks)))         
              (just-digits-less-than-b 
               (reverse (ascii-to-digits (token-value (car toks)))) (base))
              (plistp (ascii-to-digits (token-value (car toks))))
              (integer-tokens-well-formed (cdr toks)))
         (integer-tokens-well-formed (cdr toks)))))

(prove-lemma toktrans-4-help3 (rewrite)
 (implies (and (not (just-digits-less-than-b 
                     (ascii-to-digits (token-value (car z))) (base)))
               (is-integer-token (car z))
               (listp z))
          (not (integer-tokens-well-formed z))))

(prove-lemma ascii-to-digits-append (rewrite)
 (equal (ascii-to-digits (append a b))
        (append (ascii-to-digits a) (ascii-to-digits b))))

(prove-lemma reverse-ascii-to-digits (rewrite)
 (implies (valid-ascii-digits-p l)
          (equal (reverse (ascii-to-digits l))
                 (ascii-to-digits (reverse l)))))

(prove-lemma valid-ascii-digits-p-append (rewrite)
 (equal (valid-ascii-digits-p (append a b))
        (and (valid-ascii-digits-p a) (valid-ascii-digits-p b))))
        
(prove-lemma valid-ascii-digits-p-reverse (rewrite)
 (equal (valid-ascii-digits-p (reverse w))
        (valid-ascii-digits-p w)))

(prove-lemma reverse-d-a-reverse (rewrite)
 (implies (and (not (equal (lastdigit (ascii-to-digits (reverse w))) 0))
                    (valid-ascii-digits-p w)
                    (just-digits-less-than-b (ascii-to-digits (reverse w))
                                             10)
                    (plistp w))
               (equal (reverse (digits-to-ascii (ascii-to-digits (reverse w))))
                      w))
 ((use (d-a-inverse-2 (value (reverse w)))
       (reverse-reverse (l w)))))

; -----------------------------------------------------
;      Main theorem for toktrans-4
; -----------------------------------------------------

(prove-lemma toktrans-4-main-theorem (rewrite)
 (implies (and (token-listp toks)
               (integer-tokens-well-formed toks)
               (listp toks))
          (equal (convert-back (integer-convert toks))
                 toks))
 ((do-not-generalize T)))