;;;; -*- Scheme -*-
;;;; $Id: atr.scm,v 1.3 1992/01/26 13:48:04 bevan Exp $

;;;+file-overivew
;;;
;;; An interpreter for an augmented term rewriting system.
;;; The interpreter is not meant to be used as a production
;;; interpreter since it was written for clarity rather than speed.
;;; Note only pure Scheme is used.
;;;
;;; The code is taken from Appendix C of :-
;;;
;;;   Constraint Programming Languages - Their Specification and Generation
;;;   Wm Leler
;;;   Addison Wesley ISBN 0-201-06243-7
;;;
;;; Most of the comments in the code is the text in the appendix.
;;;
;;; Stephen J. Bevan <bevan@cs.man.ac.uk> 910518
;;;
;;;-file-overivew


;;; The following shows the relation between the syntax used in the
;;; operational semantics and that used in the executable semantics
;;; (scheme code).  The operational syntax is similar to that of the
;;; language Bertrand.
;;;
;;; Expression Type                 Operational      Executable
;;;
;;; variable                        name             (var name)
;;; compound variable               n1.n2.n3         (var n1 n2 n3)
;;; compound variable with first
;;; element a parameter             p1.p2.p3         (parameter p1 p2 p3)
;;; parameter (with guard)          pname'type       (typed pname type)
;;; parameter (multiple guards)     -N/A-            (typed name t1 t2 t3)
;;; numeric constant                123              (constant . 123)
;;; term                            op(args)         (term (:) op args)
;;; labeled term                    label: op(arg)   (term (label) op arg)
;;; compound labeled term           l1.l2: op(arg)   (term (l1 l2) op arg)
;;; "is" expression                 is(expr1, expr2) (is expr1 expr2)

;;; A very simple error handler for systems that don't have one.
;(define error
;  (lambda (error-message argument)
;    (display error-message)
;    (display " ")
;    (display argument)
;    (let loop () (loop))))
;;;-

;;; A number of help functions for detecting the different kinds of
;;; expressions 

(define constant? (lambda (x) (and (pair? x) (eq? (car x) 'constant))))
(define parameter? (lambda (x) (and (pair? x) (eq? (car x) 'parameter))))
(define typed? (lambda (x) (and (pair? x) (eq? (car x) 'typed))))
(define var? (lambda (x) (and (pair? x) (eq? (car x) 'var))))
(define term? (lambda (x) (and (pair? x) (eq? (car x) 'term))))
(define isis? (lambda (x) (and (pair? x) (eq? (car x) 'is))))



;;; The program uses two data types (rule and state), both represented
;;; as vectors.

;;; A `rule' is a vector containing a head expression, a body 
;;; expression, and an optional tag.  These three elements of a rule are
;;; eccessed using the functions below.  If a rule does not contain a tag
;;; then #f is returned.

(define head (lambda (x) (vector-ref x 0)))
(define body (lambda (x) (vector-ref x 1)))
(define tag
  (lambda (x)
    (if (= (vector-length x) 3)
	(vector-ref x 2)
	#f)))



;;; A `state' is a four-tuple, containing a subject expression, a global 
;;; name space, a global type space, and an integer.  The integer is used for
;;; generating label names for the unlabled redexes.

(define make-state (lambda (s g t n) (vector s g t n)))
(define subject (lambda (x) (vector-ref x 0)))
(define globals (lambda (x) (vector-ref x 1)))
(define typesp (lambda (x) (vector-ref x 2)))
(define newname (lambda (x) (vector-ref x 3)))



;;; The following four functions take a state and return a new state with
;;; one of the elements updated.
(define replace-s
  (lambda (state new-subject)
    (vector new-subject (globals state) (typesp state) (newname state))))
(define replace-g
  (lambda (state new-globals)
    (vector (subject state) new-globals (typesp state) (newname state))))
(define replace-t
  (lambda (state new-typesp)
    (vector (subject state) (globals state) new-typesp (newname state))))
(define incr-n
  (lambda (state)
    (vector (subject state)
	    (globals state)
	    (typesp state)
	    (+ 1 (newname state)))))



;;; The main function of the augmented term rewriter takes a subject
;;; expression and a list of rules, constructs a state, and passes the
;;; initial state and the rules ot the rewriter.

(define augmented-term-rewriter
  (lambda (subject-exp rules)
    (rewrite
     (make-state
      subject-exp			; subject expression
      init-phi				; initial global name space
      init-phi				; initial type space
      0)				; initial generated label name
     rules)))

(define init-phi '((*reserved* . *reserved*)))

;;; This function returns a state, which was returned by the function
;;; `rewrite'.  Name spaces (and type spaces) are represented as a list of 
;;; name-value pairs.  The variable `init-phi' represents the empty name
;;; space



;;; The function `rewrite' takes a state and a list of rules, and returns a 
;;; new state containing the completely rewritten subject expression,
;;; a global name space containing all of the bound variables and
;;; their values, a type space containing all the typed variables and
;;; their types, and an integer that indicates whoe many label names
;;; were generated.

(define rewrite
  (lambda (state rules)
    (let ((bound-variable-state (rewrite-globals state)))
      (if bound-variable-state
	  (rewrite bound-variable-state rules)
	  (let ((new-state (rewrite-exp state rules rules)))
	    (if new-state
		(rewrite new-state rules)
		state))))))

;;; `rewrite' first calls the function `rewrite-globals' which
;;; replaces bound variables by their value.  If a bound variable was
;;; found, `rewrite-globals' returns a new state, otherwise it returns
;;; #f.  If a bound variable was found, the `rewrite' calls itself
;;; recursively.  Otherwise, `rewrite-exp' is called which rewrites
;;; subexpressions of the subject expression that match one of the
;;; rules, and also rewrites `is' expressions.  The reason for having
;;; a separate rewriter for bound variables, rather than combining it
;;; into `rewrite-exp' is because of the requirement that all bound
;;; variables be replaced by their values before any more binding
;;; is performed.  If no redexes are found by either `rewrite-globals'
;;; or `rewrite-exp' (they both return #f) the `rewrite' terminates
;;; and returns the state.



;;; `rewrite-exp' is passed two copies of the rules.  If first
;;; attempts to match the outermost term of the subject expression
;;; against the first rule in the rules (by calling `try-rule').  If
;;; this fails, it recurively calls itself, removing the head of the
;;; list of rules

(define rewrite-exp
  (lambda (state rules-left-to-try rules)
    (if (null? rules-left-to-try)
	(rewrite-subexpressions state rules)
	(let ((new-state (try-rule state (car rules-left-to-try))))
	  (if new-state
	      new-state
	      (rewrite-exp state (cdr rules-left-to-try) rules))))))



;;; when the list of rules is empty, then the outermost term has
;;; failed to match any rule in the rules, so `rewrite-subexpressions'
;;; is called with the original set of rules.
(define rewrite-subexpressions
  (lambda (state rules)
    (let ((expr (subject state)))
      (cond ((constant? expr) #f)
	    ((var? expr) #f)
	    ((term? expr)
	     (rewrite-args (first3 expr) (cdddr expr) state rules))
	    ((isis? expr) (rewrite-is state))
	    (else (error "Invalid subject expression:" expr))))))



(define rewrite-args
  (lambda (previous-terms terms-to-try state rules)
    (if (null? terms-to-try)
	#f
	(let ((new-state
	       (rewrite-exp (replace-s state (car terms-to-try)) rules rules)))
	  (if new-state
	      (replace-s new-state
			 (append previous-terms
				 (cons (subject new-state) (cdr terms-to-try))))
	      (rewrite-args (append previous-terms
				    (list (car terms-to-try)))
			    (cdr terms-to-try)
			    state
			    rules))))))

(define first3			; return the first 3 elements of a list
  (lambda (alist)
    (list (car alist) (cadr alist) (caddr alist))))



;;; If the outermost term is an operator with arguments, then
;;; `rewrite' is called recursivlely on each of the arguments (by
;;; `rewrite-args').  If any argument was a redex then that
;;; transformed argument is reinserted into the subject expression in
;;; the state.  The `first3' function is used to skip over the first
;;; three elements of a list representing an expression (the symbol
;;; 'term, the lable, and the operator) when calling `rewrite-args'



;;; If the outermost term is an `is' expression, then
;;; `rewrite-subexpressions' calls the function `rewrite-is'

(define rewrite-is
  (lambda (state)
    (let ((expr (subject state))
	  (space (globals state)))
      (if (and (pair? (cdr expr))	; two args?
	       (var? (cadr expr))	; first is var?
	       (pair? (cddr expr))	; second is expr?
	       (not (lookup (cdadr expr) space)) ; var not bound?
	       (not (rewrite-globals	; var not in expr?
		     (make-state (caddr expr)
				 (bind (cdadr expr '() init-phi))
				 init-phi
				 0))))
	  (replace-g (replace-s state true-expr)
		     (bind (cdadr expr) (caddr expr) space))
	  (error "invalid is expression:" expr)))))

(define true-expr '(expr (:) true))

;;; `rewrite-is' checks to make sure the `is' expression is well
;;; formed, that the variable is not already bound, and that the
;;; value does not contain an instance of the variable.  If everything
;;; is in order, then a new state with a new subject expression and a
;;; new global name space is returned.  The new global name space is
;;; the old global name space with the addition of a new name/value
;;; pair for th new bound variable.  The new subject expressin is the
;;; nullary operator (constant) `true'.



;;; The `try-rule' fucntion (which was called by `rewrite-exp') takes
;;; a state and a single rule, and tries to match the head of the rule
;;; against the subject expression in the state.
(define try-rule
  (lambda (state rule)
    (let ((phi (match state (head rule) init-phi)))
      (if phi
	  (let ((label (get-label (subject state) (newname state))))
	    (replace-s
	     (bind-type
	      (if (eq? (last label) (newname state))
		  (incr-n state)
		  state)
	      rule
	      label)
	     (transform (body rule) phi label)))
	  #f))))



;;; `match' returns #f if there is no match, otherwise it returns a
;;; name space that gives the bindings for all the parameter variables
;;; in the head of the rule.  If a match was found the `get-label'
;;; returns the label of the matched subexpression, or generates a
;;; label.  `try-rule' returns a new state, with a new subject
;;; expression, possibly a new type space (if the rule was typed), and
;;; possibly an incremented newname (if the label was generated).  The
;;; new subject expression is the transformed body of the rule.


;;; `match' takes a state (containing a subject expression) a pattern
;;; (head of a rule) and an initial parameter name space, and builds
;;; the parameter name space.

(define match
  (lambda (state pattern phi)
    (let ((expr (subject state)))
      (cond
       ((parameter? pattern) (bind (cadr pattern) expr phi))
       ((and (typed? pattern) (var? expr))
	(let ((var-type (lookup (cdr expr) (typesp state))))
	  (if (and var-type (memq var-type (cddr pattern)))
	      (bind (cadr pattern) expr phi)
	      #f)))
       ((and (typed? pattern)
	     (constant? expr)
	     (eq? (caddr pattern) 'constant))
	(bind (cadr pattern) expr phi))
       ((and (constant? pattern)
	     (constant? expr)
	     (= (cdr pattern) (cdr expr)))
	phi)
       ((and (term? pattern)
	     (term? expr)
	     (eq? (caddr pattern) (caddr expr)))
	(match-args (replace-s state (cdddr expr))
		    (cdddr pattern)
		    phi))
       ((var? pattern)
	(error "Local variable in head of rule" #f))
       (else #f)))))

(define match-args
  (lambda (state patterns phi)
    (let ((args (subject state)))
      (cond ((and (null? args) (null? patterns)) phi)
	    ((null? args) #f)
	    ((null? patterns) #f)
	    (else
	     (let ((new-phi (match (replace-s state (car args))
				   (car patterns)
				   phi)))
	       (if new-phi
		   (match-args (replace-s state (cdr args))
			       (cdr patterns)
			       new-phi)
		   #f)))))))



;;; `get-label' check to see if the last element of the label of the
;;; matched expression is a colon, and if so replaces it with a
;;; generated name, which is simply a number (the user is not allowed
;;; to use numbers for labels, so there can be no conflict from
;;; generated labels)

(define get-label
  (lambda (expr lgen)
    (if (eq? (last (cadr expr)) ':)
	(replace-last (cadr expr) lgen)
	(cadr expr))))



(define last		; return the last element of a proper list
  (lambda (lst)
    (if (pair? lst)
	(if (null? (cdr lst))
	    (car lst)
	    (last (cdr lst)))
	(error "Cannot return last element of atom:" lst))))



(define replace-last	; replace the last element of a list
  (lambda (lst val)
    (if (and (pair? lst) (null? (cdr lst)))
	(list val)
	(cons (car lst) (replace-last (cdr lst) val)))))



;;; `bind-type' (called by `try-rule' if a match was found) binds a
;;; type to the label in the type space if the rule was tagged (even
;;; if the labe was generated):

(define bind-type
  (lambda (state rule label)
    (let ((rule-tag (tag rule)))
      (if rule-tag
	  (replace-t state (bind label rule-tag (typesp state)))
	  state))))



;;; The function `transform' takes a body of the matched rule, a
;;; paramter name space, and a label, and returns a transformed
;;; expression:


(define transform
  (lambda (rule-body phi label)
    (cond
     ((parameter? rule-body_)
      (let ((param-val (lookup (cadr rule-body) phi)))
	(if param-val
	    (if (= (length (cdr rule-body)) 1)
		param-val		; not qualified parameter
		(if (var? param-val)
		    (cons (car param-val) (append (cdr param-val)
						  (cddr rule-body)))
		    (error "A qualified parameter matched a non-variable"
			   param-val)))
	    (error "Parameter in body that is not head:" rule-body))))
     ((var? rule-body)
      (cons (car rule-body) (append label (cdr rule-body))))
     ((constant? rule-body) rule-body)
     ((term? rule-body)
      (append (list
	       (car rule-body)		; 'term
	       (append label (cadr rule-body))
	       (caddr rule-body))
	      (transform-args (cdddr rule-body) phi label)))
     ((isis? rule-body)
      (cons (car rule-body) (transform-args (cdr rule-body) phi label)))
     (else (error "Invalid body of rule:" rule-body)))))


(define transform-args
  (lambda (args phi label)
    (if (null? args)
	'()
	(cons (transform (car args) phi label)
	      (transform-args (cdr args) phi label)))))



;;; We still need to define the functions for dealing with the name
;;; spaces (including parameter and global name spaces, and type
;;; spaces)


(define bind
  (lambda (var val name-space)
    (cons (cons var val) name-space)))


(define lookup
  (lambda (var name-space)
    (let ((entry (assoc var name-space)))
      (if entry
	  (cdr entry)
	  #f))))

;;; `bind' constructs a name-value pair, and adds it onto the
;;; beginning of the name space list.  `lookup' searches the list for
;;; the specified name.  They are quite simple (and, of course, quite
;;; inefficient)



(define rewrite-globals
  (lambda (state)
    (let ((expr (subject state))
	  (space (globals state)))
      (cond
       ((var? expr)
	(let ((val (lookup (cdr expr) (globals state))))
	  (if val			; variable is bound
	      (replace-s state val)	; replace by value
	      #f)))
       ((constant? expr) #f)
       ((term? expr) (rewrite-g-args (first3 expr) (cdddr expr) state))
       ((isis? expr) (rewrite-g-args (list (car expr)) (cdr expr) state))
       (else (error "invalid subject expression:" expr))))))

(define rewrite-g-args
  (lambda (previous-terms terms state)
    (if (null? terms)
	#f
	(let ((new-state (rewrite-globals (replace-s state (car terms)))))
	  (if new-state
	      (replace-s new-state
			 (append previous-terms
				 (cons (subject new-state)
				       (cdr terms))))
	      (rewrite-g-args
	       (append previous-terms (list (car terms)))
	       (cdr terms)
	       state))))))