;; ---------------------------------------------------------------------------
;;   ~/events/toktrans-5.events
;; ---------------------------------------------------------------------------

(enable-theory tokens)

;; This token transformation function finds and removes continuations from a 
;; token list.
;; From the occam Reference Manual: 
;; "A long statement may be broken immediately after one of the following: 
;; an operator, a comma, a semi-colon, an assignment, or the keywords 
;; IS, FROM or FOR. A statement can be broken over several lines, providing the
;; continuation is indentated at least as much as the first line of the 
;; statement." In this token transformation function, I remove any 
;; indentation that immediately follows the elements from the list 
;; that are contained in PL0R.

(defn is-kw-indentation (x)   
  (equal (token-name x) 'indent))

(defn is-indentation (x)   
  (and (is-kw-indentation x)
       (numberp (token-value x))))

(prove-lemma tokenp-is-kw-indentation (rewrite)
 (implies (is-kw-indentation x)
          (tokenp x)))

;; Since empty lines disturb the proof as well, they are removed.

(defn remove-empty-lines (l)
  (if (nlistp l)
      l
      (if (and (is-kw-indentation (car l))
               (or (nlistp (cdr l))
                   (is-kw-indentation (cadr l))))
          (remove-empty-lines (cdr l))
          (cons (car l) (remove-empty-lines (cdr l))))))

(defn no-empty-lines (l)
 (if (nlistp l)
     t
     (if (and (is-kw-indentation (car l))
              (or (nlistp (cdr l))
                  (is-kw-indentation (cadr l))))
         f
         (no-empty-lines (cdr l)))))

(prove-lemma main-theorem-toktrans-5a (rewrite) 
  (no-empty-lines (remove-empty-lines l)))

(prove-lemma no-empty-lines-meaning (rewrite)
 (implies (and (no-empty-lines toks)
               (is-kw-indentation (car toks)))
          (not (is-kw-indentation (cadr toks)))))

;; This function removes the continuations.

(defn discontinue (toks continue-list)
 (if (nlistp toks)
     toks
     (if (member (token-name (car toks)) continue-list)
         (if (is-kw-indentation (cadr toks))
             (cons (car toks) (discontinue (cddr toks) continue-list))
             (cons (car toks) (discontinue (cdr toks) continue-list)))
         (cons (car toks) (discontinue (cdr toks) continue-list)))))

(defn no-continuations-p (toks continue-list)
  (if (nlistp toks)
      T
      (if (member (token-name (car toks)) continue-list)
          (if (is-kw-indentation (cadr toks))
              F
              (no-continuations-p (cdr toks) continue-list))
          (no-continuations-p (cdr toks) continue-list))))

(prove-lemma discontinue-car (rewrite)
 (implies (listp toks)
          (equal (car (discontinue toks list))
                 (car toks))))

;; The main theorem for toktrans-5b insists on no empty lines.

(prove-lemma main-theorem-toktrans-5b (rewrite)
 (implies (no-empty-lines toks)
          (no-continuations-p (discontinue toks continue-list) continue-list))
          ((disable is-kw-indentation)))

(defn toktrans-5 (toks continue-list)
 (remove-empty-lines 
   (discontinue toks continue-list)))