;; ---------------------------------------------------------------------------
;;  ~/events/derivation.events
;; ---------------------------------------------------------------------------

;; These are the functions defining a derivation.

(enable-theory sets)
(enable-theory lists)
(enable-theory grammar)
(enable-theory tokens)

;; A Derivation is a list of Derivation Steps.
;; A Derivation Step consists of a left part, a prod and a right part.
;; A Derivation Rule is a list of Labels.

;; There will be some lists with tokens and nonterminals mixed. One needs to
;; pick the token-name out for the tokens and make a list.

(add-shell mk-Derivation-Step Undefined-DS is-derivation-step
  ((sel-left-Derivation-Step (none-of) zero)
   (sel-prod-Derivation-Step (none-of) zero) 
   (sel-right-Derivation-Step (none-of) zero)))

;; The lhs is an atom, so it must be put in a list, or append will ignore it!

(defn step-source (DS)
 (append (sel-left-Derivation-Step DS)
	 (append (list (sel-lhs (sel-prod-Derivation-Step DS)))
		 (sel-right-Derivation-Step DS))))

(defn step-target (DS)
 (append (sel-left-Derivation-Step DS)
	 (append (sel-rhs (sel-prod-Derivation-Step DS))
		 (sel-right-Derivation-Step DS))))

(defn source (Derivation)
 (if (nlistp Derivation)
     nil
     (step-source (car Derivation))))

(defn target (Derivation)
 (if (nlistp Derivation)
     nil
     (step-target (last Derivation))))

(defn deriv-rule (Derivation)
 (if (nlistp Derivation)
     nil
     (append
      (sel-label (sel-prod-Derivation-Step (car Derivation)))
      (deriv-rule (cdr Derivation)))))

(defn productions (Derivation)
 (if (nlistp Derivation)
     nil
     (union (list (sel-prod-Derivation-Step (car Derivation)))
	    (productions (cdr Derivation)))))

; This function would be a witness for a forall construct.

(defn lockstep (Derivation)
  (if (or (nlistp Derivation)
	  (nlistp (cdr Derivation)))
      T
      (and (equal (step-source (cadr Derivation))
		  (step-target (car Derivation)))
	   (lockstep (cdr Derivation)))))

;; This function, too, is for the forall. Since the lockstep checks that 
;; source and target are equal, it should suffice to test just the source here.

(defn all-in-vocab (Derivation v)
  (if (nlistp Derivation)
      T
      (and (is-string-in (step-source (car Derivation)) v)
	   (all-in-vocab (cdr Derivation) v))))

(defn is-Derivation-in (Derivation Grammar)
   (and (subsetp (productions Derivation) (sel-productions Grammar))
	(all-in-vocab Derivation (append (vocab Grammar) (list (end-of-file))))
	(lockstep Derivation)))

(defn all-rights-terminal (Derivation Terminals)
 (if (nlistp Derivation)
     T
     (and (is-string-in 
	   (sel-right-Derivation-Step (car Derivation)) Terminals)
	  (all-rights-terminal (cdr Derivation) Terminals))))

(defn all-lefts-terminal (Derivation Terminals)
 (if (nlistp Derivation)
     T
     (and (is-string-in (sel-left-Derivation-Step (car Derivation)) Terminals)
	  (all-rights-terminal (cdr Derivation) Terminals))))


(defn is-right-derivation-in (Derivation Grammar)
 (and (is-Derivation-in Derivation Grammar)
      (all-rights-terminal 
       Derivation 
       (append (sel-terminals Grammar) (list (end-of-file))))))

(defn is-left-derivation-in (Derivation Grammar)
 (and (is-Derivation-in Derivation Grammar)
      (all-lefts-terminal 
       Derivation 
       (append (sel-terminals Grammar) (list (end-of-file))))))
(deftheory derivations 
 (IS-LEFT-DERIVATION-IN IS-RIGHT-DERIVATION-IN
  ALL-LEFTS-TERMINAL ALL-RIGHTS-TERMINAL IS-DERIVATION-IN ALL-IN-VOCAB
  LOCKSTEP PRODUCTIONS DERIV-RULE TARGET SOURCE STEP-TARGET STEP-SOURCE
  MK-DERIVATION-STEP ))

(disable-theory derivations)