;; ---------------------------------------------------------------------------
;; ~/events/grammar.events
;; ---------------------------------------------------------------------------

;; This the implementation of the grammar data type.

(enable-theory sets)
(enable-theory lists)

(add-shell mk-grammar Empty-Grammar is-Grammar
  ((sel-Nonterminals (none-of) zero)
   (sel-Terminals    (none-of) zero)
   (sel-Productions  (none-of) zero)
   (sel-Axiom        (none-of) zero)))

;; Using a shell for mk-prod keeps it from opening up.

(add-shell mk-prod Empty-Prod is-production
  ((sel-label (one-of numberp) Zero)
   (sel-lhs   (none-of)        Zero)
   (sel-rhs   (none-of)        Zero)))

(defn vocab (grammar)
 (union (sel-nonterminals grammar) (sel-terminals grammar)))

;; One needs to be able to access the production labelled label.

(defn prod-nr (prods label)
  (if (nlistp prods)
      nil
      (if (equal (sel-label (car prods)) label)
	  (car prods)
	  (prod-nr (cdr prods) label))))

;; These are the explicit fresh tokens.

(defn end-of-file () 'ef)

(defn dot () 'dot)

(defn left-hand-sides (prods)
 (if (nlistp prods)
     nil
     (union (sel-lhs (car prods)) (left-hand-sides (cdr prods)))))

(defn right-hand-sides (prods)
 (if (nlistp prods)
     nil
     (union (sel-rhs (car prods)) (right-hand-sides (cdr prods)))))

(defn all-but-axiom (prods axiom)
 (if (nlistp prods)
      prods
      (if (equal (sel-label (car prods)) axiom)
	  (cdr prods)
	  (cons (car prods) (all-but-axiom (cdr prods) axiom)))))

(defn no-unused-productions (prods axiom)
    (subsetp (left-hand-sides (all-but-axiom prods axiom))
             (right-hand-sides prods)))

(defn labels (prods)
  (if (nlistp prods)
      nil
      (append (list (sel-label (car prods))) (labels (cdr prods)))))

;; This function finds the label number for a production mk-prod (_,lhs, rhs).

(defn find-label (lhs rhs prods)
 (if (nlistp prods)
     'no-such-label
     (if (and (equal lhs (sel-lhs (car prods)))
	      (equal rhs (sel-rhs (car prods))))
	 (sel-label (car prods))
	 (find-label lhs rhs (cdr prods)))))

(defn is-wf-grammar (grammar)
 (let ((prods (sel-productions grammar))
       (nonts (sel-nonterminals grammar))
       (terms (sel-terminals grammar))
       (axiom (sel-axiom grammar)))
   (let ((vocab (union nonts terms))
	 (labs  (labels prods)))
     (and (is-grammar grammar)
          (no-unused-productions prods axiom)
	  (equal (card labs) 
		 (length prods))
          (member axiom labs)
          (equal (intersection  nonts terms) nil )
          (not (member (end-of-file) vocab))
          (not (member (dot) vocab))
          (subsetp (right-hand-sides prods) vocab)))))

#|
(r-loop)
;; The functions can be tested with the expression grammar.

(setq grammar-expr
 (mk-grammar
  '(e t f s)
  '(plus times open close a)
    (list (mk-prod 0 's '(e))
          (mk-prod 1 'e '(e plus t))
	  (mk-prod 2 'e '(t))
	  (mk-prod 3 't '(t times f))
	  (mk-prod 4 't '(f))
	  (mk-prod 5 'f '(open e close))
	  (mk-prod 6 'f '(a)))
  0 ))

(is-wf-grammar grammar)
|#

(deftheory grammar
 (IS-WF-GRAMMAR LABELS NO-UNUSED-PRODUCTIONS ALL-BUT-AXIOM
  RIGHT-HAND-SIDES LEFT-HAND-SIDES DOT END-OF-FILE PROD-NR find-label VOCAB
  MK-PROD MK-GRAMMAR))
(disable-theory grammar)
(disable-theory lists)
(disable-theory sets)