;; ---------------------------------------------------------------------------
;; ~/events/toktrans-7.events 
;; ---------------------------------------------------------------------------

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

;; These definitions and theorems are from an old lists library.

(defn firstn (n l)
  (if (not (listp l))
      nil
      (if (zerop n)
          nil
          (cons (car l) (firstn (sub1 n) (cdr l))))))

(defn nthcdr (n l)
  (if (not (listp l))
      l
      (if (zerop n)
          l
          (nthcdr (sub1 n) (cdr l)))))

(prove-lemma listp-append (rewrite)
  (equal (listp (append a b))
         (or (listp a)
             (listp b))))

(prove-lemma nthcdr-append (rewrite)
  (equal (nthcdr n (append a b))
         (if (leq n (length a))
             (append (nthcdr n a) b)
             (nthcdr (difference n (length a)) b))))

(prove-lemma append-firstn-nthcdr (rewrite)
  (equal (append (firstn i l) (nthcdr i l))
         l))

;; The specification function diff-cycle states the relationship between 
;; absolute and relative indentations using a proper difference function.

(defn pdiff (i j)
  (if (lessp (fix i) (fix j))
      (minus (difference j i))
      (if (equal (fix i) (fix j))
          0
          (difference i j))))

(defn diff-cycle1 (l orig prev)
  (if (nlistp l)
      (list (pdiff orig prev))
      (cons (pdiff (car l) prev)
            (diff-cycle1 (cdr l) orig (car l)))))

(prove-lemma diff-cycle1-nlistp (rewrite)
             (implies (nlistp l)
                      (equal (diff-cycle1 l orig prev)
                             (list (pdiff orig prev)))))

(prove-lemma diff-cycle1-listp (rewrite)
             (implies (listp l)
                      (equal (diff-cycle1 l orig prev)
                             (cons (pdiff (car l) prev)
                                   (diff-cycle1 (cdr l) orig (car l))))))

(defn diff-cycle (l old)
  (diff-cycle1 l old old))


; First determine the magnitude and sign of the indentation. Use a
; fresh token name, 'relative, for this kind of token.
; This means that the resulting list remains a token-listp, which will
; go easy on the induction proof.

(defn is-relative (tok)
  (and (tokenp tok)
       (equal (token-name tok) 'relative)
       (or (numberp (token-value tok))
           (and (negativep (token-value tok))
                (not (equal (negative-guts (token-value tok)) 0))))))

(defn emit-relative (i j)
  (if (lessp (fix i) (fix j))
      (mk-token 'relative (minus (difference j i)))
      (if (equal (fix i) (fix j))
          (mk-token 'relative 0)
          (mk-token 'relative (difference i j)))))

;; Unfortunately, emit1 has to watch out for indentations which are not.
;; well formed. I will ignore such indentations.

(defn emit1 (l orig prev)
  (if (nlistp l)
      (list (emit-relative orig prev))
      (if (is-kw-indentation (car l))
          (if (is-indentation (car l))
              (cons (emit-relative (token-value (car l)) prev)
                    (emit1 (cdr l) orig (token-value (car l))))
              ; should be an error
              (emit1 (cdr l) orig prev))
          (cons (car l) (emit1 (cdr l) orig prev)))))

(defn emit (l old)
  (emit1 l old old))

;; This is the meaning function for the relative indentations.

(defn relative-meaning (l)
  (if (nlistp l)
      nil
      (if (is-relative (car l))
          (cons (token-value (car l))
                (relative-meaning (cdr l)))
          (relative-meaning (cdr l)))))

;; There are no 'relative tokens left in the list.

(defn relative-free (l)  
  (if (nlistp l)
      T
      (if (tokenp (car l))
          (and (not (equal (token-name (car l)) 'relative))
               (relative-free (cdr l)))
          F)))

(prove-lemma diff-cycle1-not-numberp (rewrite)
             (implies  (not (numberp v))
                       (equal (diff-cycle1 z orig v)
                              (diff-cycle1 z orig 0))))

(prove-lemma emit1-theorem (rewrite)
             (implies (and (relative-free l)
                           (token-listp l))
                      (equal (relative-meaning (emit1 l orig prev))
                             (diff-cycle1 (collect-indents l) orig prev))))

(prove-lemma emit-theorem (rewrite)
             (implies (and (relative-free l)
                           (token-listp l))
                      (equal (relative-meaning (emit l old))
                             (diff-cycle (collect-indents l) old)))
             ((do-not-induct T)))

;; This makes a list which contains n copies of v.

(defn my-make-list (v n)
  (if (or (zerop n)
          (not (numberp n)))
      nil
      (cons v (my-make-list v (sub1 n)))))

(prove-lemma length-my-make-list (rewrite)
             (equal (length (my-make-list v n))
                    (fix n)))

(prove-lemma not-numberp-my-make-list (rewrite)
             (implies (not (numberp n))
                      (equal (my-make-list x n) nil)))

(prove-lemma listp-my-make-list (rewrite)
             (implies (lessp 0 (fix n))
                      (listp (my-make-list x n))))

(prove-lemma my-make-list-zero (rewrite)
             (implies (equal n 0)
                      (equal (my-make-list x n) nil)))

(prove-lemma plist-my-make-list (rewrite)
             (equal (plist (my-make-list v n))
                    (my-make-list v n)))

;; Now all I have to do is go through and expand the 'relative tokens
;; to the ni, si, and bi stuff the grammar needs.

(defn ni-si-bis (n)
  (if (equal n 0)
      (my-make-list (mk-token 'si nil) 1)
      (if (lessp 0 n)
          (my-make-list (mk-token 'ni nil) n)
          (my-make-list (mk-token 'bi nil) (negative-guts n)))))

(defn relative-to-ni-si-bi (toks)
  (if (nlistp toks)
      toks
      (if (is-relative (car toks))
          (append (ni-si-bis (token-value (car toks)))
                  (relative-to-ni-si-bi (cdr toks)))
          (cons (car toks) (relative-to-ni-si-bi (cdr toks))))))

;; The specification is more complex than that of the implementation. The 
;; function matches cdrs down the toks, seeing if it matches the 
;; relative value.

(defn matches (n toks)
  (if (nlistp toks)
      F
      (if (equal n 0)
          (equal (car toks) (mk-token 'si nil))
          (if (lessp 0 n)
              (equal (firstn n toks) (my-make-list (mk-token 'ni nil) n))
              (equal (firstn (negative-guts n) toks) 
                     (my-make-list (mk-token 'bi nil) (negative-guts n)))))))

(defn how-much (n)
  (if (equal n 0)
      1
      (if (lessp 0 n)
          (fix n)
          (negative-guts n))))

(defn relative-conversion-ok (pre post)
  (if (nlistp pre)
      ;; There should be just a number of bi tokens on the end.
      (if (nlistp post)
          T
          (and (equal (token-name (car post)) 'bi)
               (relative-conversion-ok pre (cdr post))))
      (if (is-relative (car pre))
          (and (matches (token-value (car pre)) post)
               (relative-conversion-ok 
                (cdr pre)
                (nthcdr (how-much (token-value (car pre))) post)))
          (and (equal (car pre) (car post))
               (relative-conversion-ok (cdr pre) (cdr post)))))
  ((ord-lessp (cons (add1 (length pre)) (length post)))))

;; If it has the name 'relative, it had better be well formed.

(defn all-relative-tokens-good (toks)
  (if (nlistp toks)
      T
      (if (equal (token-name (car toks)) 'relative)
          (and (is-relative (car toks))
               (all-relative-tokens-good (cdr toks)))
          (all-relative-tokens-good (cdr toks)))))

(prove-lemma firstn-my-make-list (rewrite)
 (implies (numberp x)
          (equal (firstn x (my-make-list l x))
                 (my-make-list l  x))))

(prove-lemma nthcdr-my-make-list (rewrite)
 (implies (numberp x)
          (equal (nthcdr x (my-make-list l x))
                 nil)))

(prove-lemma firstn-append-my-make-list (rewrite)
 (implies (numberp x)
          (equal (firstn x (append (my-make-list z x) foo))
                 (my-make-list z x))))
                         

(prove-lemma relative-theorem (rewrite)
 (implies (and (token-listp toks)
               (all-relative-tokens-good toks))
          (relative-conversion-ok toks
                                  (relative-to-ni-si-bi toks)))
 ((do-not-generalize t)))


;; Now I try proving some glue so I can feel good about combining the
;; passes. If toks is a token list and free of relative tokens, emit1 will
;; have the properties so that the relative conversion will go okay.

(prove-lemma glue1 (rewrite)
             (implies (and (token-listp toks)
                           (relative-free toks))
                      (all-relative-tokens-good (emit1 toks n m))))

(prove-lemma glue2 (rewrite)
 (implies (token-listp toks)
          (token-listp (emit1 toks n m))))

;; This is the indentator function.

(defn indentator (l)
 (relative-to-ni-si-bi (emit1 l 0 0)))

;; The result is free of indentation tokens

(defn indent-free (l)
 (if (nlistp l)
     (not (is-kw-indentation l))
     (if (is-kw-indentation (car l))
         F
         (indent-free (cdr l)))))

(prove-lemma indent-free-cons (rewrite)
 (implies (and (indent-free a)
               (not (is-kw-indentation b)))
          (indent-free (cons b a))))

(prove-lemma indent-free-append (rewrite)
 (implies (and (indent-free a)
               (indent-free b))
          (indent-free (append a b)))
 ((disable is-kw-indentation)))

(prove-lemma indent-free-my-make-list (rewrite)
 (implies (indent-free a) 
          (indent-free (my-make-list a n)))))

(prove-lemma indent-free-realtive-to-ni-si-bi (rewrite)
 (implies (and (token-listp x)
               (indent-free x))
          (indent-free (relative-to-ni-si-bi x))))


(prove-lemma non-wf-indentations-removed (rewrite)
 (implies (and (not (nlistp z))
               (is-kw-indentation (car z))
               (not (is-indentation (car z)))
               (numberp n))
         (equal (emit1 z m n)
                (emit1 (cdr z) m n))))

(prove-lemma indent-free-emit1 (rewrite)
 (implies (numberp n)
          (indent-free (emit1 z 0 n))))

(prove-lemma indent-free-indentator (rewrite)
 (implies (token-listp l)
          (indent-free (indentator l))))

(deftheory toktrans 
 (INDENT-FREE INDENTATOR ALL-RELATIVE-TOKENS-GOOD
  RELATIVE-CONVERSION-OK HOW-MUCH MATCHES RELATIVE-TO-NI-SI-BI NI-SI-BIS
  MY-MAKE-LIST RELATIVE-FREE RELATIVE-MEANING EMIT EMIT1 EMIT-RELATIVE
  IS-RELATIVE DIFF-CYCLE DIFF-CYCLE1 PDIFF NTHCDR FIRSTN OK-TOKTRANS-6
  TOKTRANS-6 HALVED-LISTP COLLECT-INDENTS INDENT-POSITIONS-PRESERVED HALVE
  HALF OK-INDENTATION-VALUE PREPARE-INDENTATIONS TOKTRANS-5 NO-CONTINUATIONS-P
  DISCONTINUE NO-EMPTY-LINES REMOVE-EMPTY-LINES IS-INDENTATION
  IS-KW-INDENTATION INTEGER-TOKENS-WELL-FORMED WELL-FORMED-PN NO-LEADING-ZEROS
  LASTDIGIT CONVERT-BACK VALID-ASCII-DIGITS-P DIGITS-TO-ASCII DIGIT-TO-ASCII
  NAT-TO-PN INTEGER-CONVERT ASCII-TO-DIGITS VALID-ASCII-DIGIT-P ASCII-TO-DIGIT
  PN-TO-NAT JUST-DIGITS-LESS-THAN-B IS-INTEGER-TOKEN BASE DIGIT-NINE
  DIGIT-ZERO ASCII-NINE ASCII-ZERO KEY-WORDS-STEP DETERMINE-KEY-WORDS
  MAKE-KEY-WORDS REPLACE-STEP REPLACE MAKE-REPLACE TOKEN-LISTP VALUE
  NO-DISCARDS-LEFT NON-DISCARDS-UNDISTURBED DISCARD ))

(disable-theory toktrans)

(deftheory toktrans-proofs
 (INDENT-FREE-INDENTATOR INDENT-FREE-EMIT1 NON-WF-INDENTATIONS-REMOVED
  INDENT-FREE-REALTIVE-TO-NI-SI-BI INDENT-FREE-MY-MAKE-LIST INDENT-FREE-APPEND
  INDENT-FREE-CONS 
  GLUE2 GLUE1 RELATIVE-THEOREM
  NTHCDR-MY-MAKE-LIST FIRSTN-MY-MAKE-LIST PLIST-MY-MAKE-LIST MY-MAKE-LIST-ZERO
  LISTP-MY-MAKE-LIST NOT-NUMBERP-MY-MAKE-LIST LENGTH-MY-MAKE-LIST EMIT-THEOREM
  EMIT1-THEOREM DIFF-CYCLE1-NOT-NUMBERP DIFF-CYCLE1-LISTP DIFF-CYCLE1-NLISTP
  APPEND-FIRSTN-NTHCDR NTHCDR-APPEND LISTP-APPEND 
  MAIN-THEOREM-TOKTRANS-6 INDENTS-HALVED COLLECT-INDENTS-NLISTP
  INDENT-POSITIONS-PRESERVED-HALVE TOKTRANS-6A-MAIN-THEOREM
  MAIN-THEOREM-TOKTRANS-5B DISCONTINUE-CAR NO-EMPTY-LINES-MEANING
  MAIN-THEOREM-TOKTRANS-5A TOKENP-IS-KW-INDENTATION TOKTRANS-4-MAIN-THEOREM
  VALID-ASCII-DIGITS-P-REVERSE VALID-ASCII-DIGITS-P-APPEND
  REVERSE-ASCII-TO-DIGITS ASCII-TO-DIGITS-APPEND TOKTRANS-4-HELP3
  TOKTRANS-4-HELP2 TOKTRANS-4-HELP1 INVERSE2 INVERSE1 D-A-INVERSE-2
  PLISTP-ASCII-TO-DIGITS REMAINDER-TIMES1-INSTANCE QUOTIENT-TIMES-INSTANCE
  QUOTIENT-PLUS REMAINDER-PLUS QUOTIENT-LESSP-ARG1 COMMUTATIVITY-OF-TIMES
  LESSP-QUOTIENT PLUS-REMAINDER-TIMES-QUOTIENT TIMES-ADD1 EQUAL-TIMES-0
  TIMES-ZERO PLUS-ZERO-ARG2 EQUAL-PLUS-0 COMMUTATIVITY-OF-PLUS
  FIRSTN-APPEND-MY-MAKE-LIST
  TOKTRANS-3-MAIN-THEOREM TOKTRANS-2-MAIN-THEOREM TOKTRANS-1-MAIN-THEOREM
  DISCARD-DOES-NOT-DISTURB-NON-DISCARDS ))

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