;; ---------------------------------------------------------------------------
;;     ~/events/toktrans-6.events
;; ---------------------------------------------------------------------------

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

;; This token transformation function prepares for the indentation work to be 
;; done in toktrans-7. It looks for the indentation tokens and replaces the 
;; value, which is a carriage return followed by 0 or more blanks, by the
;; number of blanks found. 
;; The halving of the indentation (2 blanks = 1 level) is done here as well.
;; The function toktrans-6a removes the CR and puts in the number of blanks, 
;; the function toktrans-6b halves.

;; ------------ replace chars by length --------------
;;              toktrans 6a

(defn prepare-indentations (toks)
 (if (nlistp toks)
     toks
     (if (is-kw-indentation (car toks))
         (cons
          (mk-token
           (token-name (car toks))
           (sub1 (length (token-value (car toks)))))
          (prepare-indentations (cdr toks)))
         (cons (car toks) (prepare-indentations (cdr toks))))))

(defn ok-indentation-value (l1 l2)
 (if (nlistp l1)
     (nlistp l2)
     (and (if (is-kw-indentation (car l1))
              (and (equal (token-name (car l1))
                          (token-name (car l2)))
                   (equal (token-value (car l2))
                          (sub1 (length (token-value (car l1))))))
              (equal (car l1) (car l2)))
          (ok-indentation-value (cdr l1) (cdr l2)))))

(prove-lemma toktrans-6a-main-theorem (rewrite)
 (implies (and (token-listp toks)
               (listp toks))
          (ok-indentation-value toks (prepare-indentations toks))))

;; ------------ divide length by 2 --------------
;;              toktrans6b

;; The function half returns half of a number (rounded down).

(defn half (n) (quotient n 2))

;; The function halve is applied to a list, not a token!

(defn halve (l)
  (if (nlistp l)
      l
      (if (is-indentation (car l))
          (cons (mk-token (token-name (car l)) 
                          (half (token-value (car l))))
                (halve (cdr l)))
          (cons (car l)
                (halve (cdr l))))))

(defn indent-positions-preserved (l1 l2)
  (if (nlistp l1)
      (equal l1 l2) 
      (if (is-indentation (car l1))
          (and (is-indentation (car l2))
               (indent-positions-preserved (cdr l1) (cdr l2)))
          (and (equal (car l1) (car l2))
               (indent-positions-preserved (cdr l1) (cdr l2))))))

(prove-lemma indent-positions-preserved-halve (rewrite)
  (indent-positions-preserved l (halve l)))

(defn collect-indents (l)
  (if (nlistp l)
      nil 
      (if (is-indentation (car l))
          (cons (fix (token-value (car l)))
                (collect-indents (cdr l)))
          (collect-indents (cdr l)))))

(prove-lemma collect-indents-nlistp (rewrite)
 (implies (nlistp l)
          (equal (collect-indents l) nil)))

(defn halved-listp (l1 l2)
  (if (nlistp l1)
      (nlistp l2)
      (and (equal (car l2) (half (car l1)))
           (halved-listp (cdr l1) (cdr l2)))))

(prove-lemma indents-halved (rewrite)
  (halved-listp (collect-indents l)
                (collect-indents (halve l))))

;; ----- combine both passes -----

(defn toktrans-6 (toks)
 (halve (prepare-indentations toks)))

(defn ok-toktrans-6 (l1 l2)
 (if (nlistp l1)
     (nlistp l2)
     (and (if (is-kw-indentation (car l1))
              (and (equal (token-name (car l1))
                          (token-name (car l2)))
                   (equal (token-value (car l2))
                          (half (sub1 (length (token-value (car l1)))) )))
              (equal (car l1) (car l2)))
          (ok-toktrans-6 (cdr l1) (cdr l2)))))

(prove-lemma main-theorem-toktrans-6 (rewrite)
  (ok-toktrans-6 toks (toktrans-6 toks)))

(disable-theory tokens)
(disable-theory lists)