;
; A tree rewriting system.
;
; Based on PostL.scm by Oleg Kiselyov.
;
; Adapted to Chicken Scheme by Ivan Raikov.
;
; As usual \Sigma is a set of function symbols and constants, and \V
; is a set of variables. The members of both sets are Scheme symbols;
; variable names are distinguished by a leading underscore. Constants
; can also be strings and numbers. Like in Prolog, a sole underscore
; is the anonymous variable.  We partition the set of function symbols
; of arity at least 1 into two disjoint subsets, of V- and M-function
; symbols. Terms over V-function symbols, constants, and variables are
; called V-terms. A simple M-term is an application of an M-function
; symbol to V-terms; a term with M symbols is an M-term. In Scheme, we
; represent V- and M- functional terms as S-expressions of the form
; (symbol term ...)  or (M symbol term ...)  correspondingly.
;
; <V-term> ::= number | string | symbol | var | (symbol <V-term>*)
; var ::= a symbol beginning with $ or simply an _
; <M-term-simple> ::= (M symbol <V-term>*)
; <M-term> ::= (M symbol (<V-term>|<M-term>)* ) | 
;	       (symbol <V-term>* <M-term> (<V-term>|<M-term>)* )
;
; Only M-terms are subject to re-writing rules.
; <re-writing-rule> ::= <pattern> => <consequent>
; <pattern> ::= <M-term-simple> 
; <consequent> ::= <M-term> | <V-term>
; 
; When a subject M-term is matched against a rule, variables
; in the pattern are bound to the corresponding pieces in the matching
; term. If the matching succeeds, the <consequent> replaces the subject
; M-term with the variables substituted by the results of matching 
; of the <pattern>. The resulting term should have no variables.
; It's an error if the subject M-term didn't match any rule.

; The evaluator of the system takes an M-term without variables -- the
; subject term -- and a set of re-writing rules. The evaluator scans the
; rules in order, trying to match the redex of the term, which is by
; necessity a simple M-term, against the pattern of a rule. It is an
; error if the redex did not match any rule. If the subject M-term has
; several redexes, the leftmost innermost is reduced first. If the
; re-written redex is not a V-term, it will be reduced again.
;
; The explicit marking of redexes (as M-terms) and the
; applicative order of reductions make it easy to write and analyze
; rules. In particular, the applicative order guarantees composability
; of the rules.
;
; Note the reduction machine is very similar to Refal. '(M' ... ')'
; are equivalent to Refal's configuration braces.
;
; It's possible to write a rule like the following:
;	(M invoke $x $arg) => (M $x $arg)
; However we never use such second-order rules. We use our language as a
; first-order one. So far, it sufficed.


; As the rules represent the infinite set of code we generate, we want
; to analyze the rules rather than analyzing the code. For example,
; we can associate a set of exceptions with each particular V-term.
; Then we can ask which exceptions can possibly be thrown by the code
; generated by the rules.

(module tree-rewrite

	(match-tree unify-trees 
	 reduce 
	 rewrite-map-tree 
	 rewrite-fold-tree 
	 rewrite-fold-tree-partial 
	 substitute-vars substitute-vars-open)

(import scheme chicken)
(require-library srfi-1)
(import (only srfi-1 any fold delete-duplicates))

(include "tree-unif.scm")

; Test if x is an immediate M-term, that is, of the form
; <M symbol <term> ...)
(define (M-term-immed? x)
  (and (pair? x) (eq? 'M (car x)) (pair? (cdr x))))

; Check if a term is subject to substitutions
(define (M-term? term)
  (and (pair? term)
       (or (eq? 'M (car term))
	   (any M-term? (cdr term)))))


; Deconstructors of a rule
(define pattern-of car)
(define conseq-of caddr)



;------------------------------------------------------------------------
;			Reduction machinery
; Note, m-term does not contain variables!

(define (reduce m-term rules)
  (let reduce ((m-term m-term))
    (cond
     ((not (pair? m-term)) m-term)
     ((not (pair? (cdr m-term))) m-term)
     ((eq? 'M (car m-term))
      (let* ((reduced-term 
	      (cons (car m-term)
		    (map reduce (cdr m-term))))
	     (result (do-match reduced-term rules)))
	(if (not result) 
	    (error 'reduce "failed to reduce the term " reduced-term))
	(reduce result)))
     (else
      (map reduce m-term)))))


; At present, go with the first matching rule
(define (do-match term rules)
  (and (pair? rules)
       (or (match-one-rule term (car rules) '())
	   (do-match term (cdr rules)))))


(define (match-one-rule term rule env)
  (assert (and (pair? rule) (pair? (cdr rule))))
  (if (eq? '=> (car rule))
      (substitute-vars (cadr rule) env)
      (let ((new-env (match-tree (car rule) term env)))
	(and new-env (match-one-rule term (cdr rule) new-env)))))

;;
;; TODO: add special cases *default* and *text*
;;

(define (rewrite-map-tree rules)
  (let ((tags (delete-duplicates (map cadar rules))))
    (lambda (term)
      (let recur ((term term))
	(cond ((pair? term) 
	       (if (member (car term) tags)
		   (reduce `(M . ,term) rules)
		   (cons (car term) (map recur (cdr term)))))
	      (else term))))
    ))


(define (rewrite-fold-tree rules f ax)
  (let ((tags (delete-duplicates (map cadar rules))))
    (lambda (term)
      (let recur ((term term) (ax ax))
	(cond ((pair? term) 
	       (if (member (car term) tags)
		   (f (reduce `(M . ,term) rules) ax)
		   (cons (car term) (fold recur ax (cdr term)))))
	      (else (f term ax))))
      )))


(define (rewrite-fold-tree-partial rules f ax)
  (let ((tags (delete-duplicates (map cadar rules))))
    (lambda (term)
      (let recur ((term term) (ax ax))
	(cond ((pair? term) 
	       (if (member (car term) tags)
		   (f (reduce `(M . ,term) rules) ax)
		   (fold recur ax (cdr term))))
	      (else ax)))
      )))


)