; An applicative-order term rewriting system for code generation,
; and its termination analysis
;
; Our code generator is an instance of a term re-writing system. The
; re-writing process however is more structured due to the explicit
; marking of redexes and an applicative order of applying them.
;
; 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.

; $Id: PostL.scm,v 2.20 2003/07/04 23:10:23 oleg Exp oleg $

(include "lib/myenv.scm")
(include "lib/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)))))
(run-test
 (assert (not (M-term? '(a b c))))
 (assert (not (M-term? "abc")))
 (assert (not (M-term? '(a (b) (c () d)))))
 (assert (M-term? '(M a)))
 (assert (M-term? '(M a 1)))
 (assert (M-term? '(a (M a 1))))
 (assert (M-term? '(a b (c () (M a 1)))))
)

; 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 "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)))))

(define polynomial-rules
  '(
    ( (M polynomial _x (seq _c (seq-empty)))
      => _c )
    ( (M polynomial _x (seq _c _r))
      =>
      (M add _c (M mult _x (M polynomial _x _r))))


    ( (M mult _x (imm 0)) => (imm 0) )
    ( (M mult (imm 0) _x) => (imm 0) )
    ( (M mult _x (imm 1)) => _x )
    ( (M mult (imm 1) _x) => _x )

    ( (M mult _x  _y) => (mult _x _y) )
    
    ( (M add _x (imm 0)) => _x )
    ( (M add (imm 0) _x) => _x )
    ( (M add _x _y) => (add _x _y) )

))


(run-test
 (assert (equal? '(add (imm 1) (mult (var "x") (imm 2)))
    (reduce '(M polynomial (var "x") (seq (imm 1) (seq (imm 2) (seq-empty))))
	    polynomial-rules)
    ))
 (assert (equal? '(add (imm 1) (mult (var "x") (mult (var "x") (imm 2))))
   (reduce '(M polynomial (var "x") 
	      (seq (imm 1) (seq (imm 0) (seq (imm 2) (seq-empty)))))
	   polynomial-rules)
  )))


(define (gen-mat-code term)
  (define (emit term) (display term) (newline))
  (let* ((env (list (cons '_result_var (gensym))))
	 (rules
	  `(((mat _x) . ,(lambda (env) (substitute-vars '(mat _x) env)))
	    ((imm _x) . ,(lambda (env) (substitute-vars '(imm _x) env)))
	    ((add (mat _x) (imm _c)) . 
	     ,(lambda (env) (emit 
			   (substitute-vars '(mat_add_mc _x _c _result_var)
					    env))
		    (substitute-vars '(mat _result_var) env)))
	    ((add (imm _c) (mat _x)) . 
	     ,(lambda (env) (emit 
			   (substitute-vars '(mat_add_mc _x _c _result_var)
					    env))
		    (substitute-vars '(mat _result_var) env)))
	    ((add (mat _x) (mat _y)) . 
	     ,(lambda (env) (emit 
			   (substitute-vars '(mat_add_mm _x _y _result_var)
					    env))
		    (substitute-vars '(mat _result_var) env)))
	    ((mult (mat _x) (imm _c)) .
	     ,(lambda (env) (emit 
			   (substitute-vars '(mat_mult_mc _x _c _result_var)
					    env))
		    (substitute-vars '(mat _result_var) env)))
	    ((mult (mat _x) (mat _y)) .
	     ,(lambda (env) (emit 
			   (substitute-vars '(mat_mult_mm _x _y _result_var)
					    env))
		    (substitute-vars '(mat _result_var) env)))
	    ((_op _x _y) . 
	   ,(lambda (env)
	      (let ((env-new
		     (cons 
		      (cons '_x_res 
			    (gen-mat-code (substitute-vars '_x env)))
		      (cons
		       (cons '_y_res
			     (gen-mat-code (substitute-vars '_y env)))
		       env))))
		(gen-mat-code (substitute-vars '(_op _x_res _y_res) env-new)))))
	  )))
    (let loop ((rules rules))
      (cond
       ((null? rules) (error "unmatched term: " term))
       ((match-tree (caar rules) term env) =>
	(cdar rules))
       (else (loop (cdr rules)))))))


;========================================================================
;			Termination analysis
;
; A ruleset represents the subset of code we generate.  We may want to
; prove the following properties of the ruleset: *Any* subject M-term
; will be reduced, in a finite number of steps, to a V-term or an
; error.
;
;
; We consider a ruleset as a mapping from terms to terms.
; We want to prove that the mapping is contractive.
;	<ruleset> |- <ruleset> contractive
;
;	all r in <ruleset>: <ruleset> |- r contractive
; ==> <ruleset> |- <ruleset> contractive
;
; The analysis proceeds by repeatedly applying various strategies to
; the rules. A strategy tries to soundly remove a rule from the
; ruleset by preserving or weakining ruleset's termination
; properties. If we managed to remove all the rules, then the original
; ruleset terminates. The prover is strongly normalizing: The
; strategies are applied until they can no longer be applied. If there
; are some rules left, they have to be analyzed by hand or with some
; new strategies.


; Sample rulesets to analyze for termination...

; Arithmetics on numerals

; Transform the natural number n to the "term numeral"
; (succ ... (zero))
(define (make-numeral n)
  (assert (not (negative? n)))
  (if (zero? n) '(zero)
      (list 'succ (make-numeral (- n 1)))))

; Transform the term numeral back to the natural number.
; The inverse of the make-numeral above
(define (eval-numeral num)
  (cond
   ((equal? num '(zero)) 0)
   ((and (pair? num) (eq? 'succ (car num))) (+ 1 (eval-numeral (cadr num))))
   (else (error "Wrong numeral " num))))

(define rule-arithm
  '(
    ( (M mult (zero) _x) => (zero) )
    ( (M mult _x (zero)) => (zero) )
    ( (M mult (succ _x) _y) => (M add _y (M mult _x _y)) )
    ( (M add (zero) _x) => _x )
    ( (M add _x (zero)) => _x )
    ( (M add (succ _x) _y) => (succ (M add _x _y)))

    ( (M min (zero) _) => (zero) )
    ( (M min _ (zero) ) => (zero) )
    ( (M min (succ _x) (succ _y)) => (succ (M min _x _y)))

    ( (M max (zero) _x) => _x )
    ( (M max _x (zero) ) => _x )
    ( (M max (succ _x) (succ _y)) => (succ (M max _x _y)))


    ))

(run-test
 (assert (equal? (make-numeral 0)
		 (reduce `(M min 
			     ,(make-numeral 0)
			     ,(make-numeral 0)
			     ) rule-arithm)))
 (assert (equal? (make-numeral 0)
		 (reduce `(M min 
			     ,(make-numeral 5)
			     ,(make-numeral 0)
			     ) rule-arithm)))

 (assert (equal? (make-numeral 5)
		 (reduce `(M min 
			     ,(make-numeral 5)
			     ,(make-numeral 5)
			     ) rule-arithm)))

 (assert (equal? (make-numeral 5)
		 (reduce `(M min 
			     ,(make-numeral 7)
			     ,(make-numeral 5)
			     ) rule-arithm)))

 (assert (equal? (make-numeral 5)
		 (reduce `(M min 
			     ,(make-numeral 5)
			     ,(make-numeral 7)
			     ) rule-arithm)))

 (assert (equal? (make-numeral 0)
		 (reduce `(M max 
			     ,(make-numeral 0)
			     ,(make-numeral 0)
			     ) rule-arithm)))
 (assert (equal? (make-numeral 5)
		 (reduce `(M max
			     ,(make-numeral 5)
			     ,(make-numeral 0)
			     ) rule-arithm)))

 (assert (equal? (make-numeral 5)
		 (reduce `(M max 
			     ,(make-numeral 5)
			     ,(make-numeral 5)
			     ) rule-arithm)))

 (assert (equal? (make-numeral 7)
		 (reduce `(M max 
			     ,(make-numeral 7)
			     ,(make-numeral 5)
			     ) rule-arithm)))

 (assert (equal? (make-numeral 7)
		 (reduce `(M max 
			     ,(make-numeral 5)
			     ,(make-numeral 7)
			     ) rule-arithm)))
)

(define rule-fact
  `(
    ( (M fact (zero)) => (succ (zero)) )
    ( (M fact (succ _x)) => 
      (M mult (succ _x) (M fact _x)) )
    ,@rule-arithm
))

(define rule-fact-bad		; A ruleset with an intentional error
  '(				; that prevents termination
    ( (M fact (zero)) => (succ (zero)) )
    ( (M fact (succ _x)) => 
      (M mult (succ _x) (M fact (succ _x))) )

    ( (M mult (zero) _x) => (zero) )
    ( (M mult _x (zero)) => (zero) )
    ( (M mult (succ _x) _y) => (M add _y (M mult _x _y)) )
    ( (M add (zero) _x) => _x )
    ( (M add _x (zero)) => _x )
    ( (M add (succ _x) _y) => (succ (M add _x _y)))
))

(run-test
 (assert (equal? (make-numeral 1)
		 (reduce `(M fact ,(make-numeral 0)) rule-fact)))
 (assert (equal? (make-numeral 1)
		 (reduce `(M fact ,(make-numeral 1)) rule-fact)))
 (assert (equal? (make-numeral 2)
		 (reduce `(M fact ,(make-numeral 2)) rule-fact)))
 (assert (equal? (make-numeral 6)
		 (reduce `(M fact ,(make-numeral 3)) rule-fact)))
 (assert (equal? (make-numeral 24)
		 (reduce `(M fact ,(make-numeral 4)) rule-fact)))
 (assert (equal? (make-numeral 120)
		 (reduce `(M fact ,(make-numeral 5)) rule-fact)))
 )


(define rule-evenp
  '(
    ( (M even (seq-empty)) => (yes) )
    ( (M even (seq _c _r)) => (M odd _r) )
    ( (M odd (seq-empty)) => (no)  )
    ( (M odd (seq _c _r)) => (M even _r) )
))

(define rule-evenp-noneff	; Another ruleset with an intentional error
  '(				; that does not prevent termination
    ( (M even (seq-empty)) => (yes) )
    ( (M even (seq _c _r)) => (M odd _r) )
    ( (M odd (seq-empty)) => (no)  )
    ( (M odd (seq _c _r)) => (M even (seq _r _r)) )
))

(define rule-evenp-bad		; Another ruleset with an intentional error
  '(				; that does prevent termination
    ( (M even (seq-empty)) => (yes) )
    ( (M even (seq _c _r)) => (M odd _r) )
    ( (M odd (seq-empty)) => (no)  )
    ( (M odd (seq _c _r)) => (M even (seq _c (seq _c  _r))) )
))


(run-test
 (assert (equal? '(yes) 
		 (reduce '(M even (seq 1 (seq 2 (seq-empty)))) rule-evenp)))
 (assert (equal? '(no) 
		 (reduce '(M odd (seq 1 (seq 2 (seq-empty)))) rule-evenp)))
 (assert (equal? '(yes) 
		 (reduce '(M odd (seq 1 (seq 2 (seq 3 (seq-empty))))) 
			 rule-evenp)))
)

	; modified Ackermann function
(define rule-Ackermann
  '(
    ( (M Ack (zero) _n) => (succ _n) )
    ( (M Ack (succ _m) (zero)) => (M Ack _m (succ (zero))) )
    ( (M Ack (succ _m) (succ _n)) => (M Ack _m (M Ack (succ _m) _n)) )

    ( (M mult (zero) _x) => (zero) )
    ( (M mult _x (zero)) => (zero) )
    ( (M mult (succ _x) _y) => (M add _y (M mult _x _y)) )
    ( (M add (zero) _x) => _x )
    ( (M add _x (zero)) => _x )
    ( (M add (succ _x) _y) => (succ (M add _x _y)))
))

(run-test
 (assert (= 3
   (eval-numeral (reduce '(M Ack (succ (zero)) (succ (zero))) rule-Ackermann)
 )))
 (assert (= 4
   (eval-numeral (reduce '(M Ack (succ (zero)) (succ (succ (zero))))
		       rule-Ackermann))))
 (assert (= 7
 (eval-numeral (reduce '(M Ack (succ (succ (zero))) (succ (succ (zero))))
		       rule-Ackermann))))
 (assert (= 9
 (eval-numeral
   (reduce '(M Ack (succ (succ (zero))) (succ (succ (succ (zero))))) 
	 rule-Ackermann))))
 (assert (= 61
 (eval-numeral
  (reduce '(M Ack (succ (succ (succ (zero)))) (succ (succ (succ (zero))))) 
	 rule-Ackermann))))
)


      

; Given an expression of the form
; exp = var | (Lam var exp) | (exp exp)
; a variable var and an expression e1, replace all free occurrences
; of var in the expression for e1
(define rule-subst
  '(
    ( (M replace (Lam _x _body) _x _) => (Lam _x _body) )
    ( (M replace (Lam _x _body) _y _e1) => (Lam _x (M replace _body _y _e1)))
    ( (M replace (_eh _et) _y _e1) =>
      ((M replace _eh _y _e1) (M replace _et _y _e1)))
    ( (M replace _x _x _e1) => _e1 )
    ( (M replace _x _y _) => _x )
    ))

(run-test
 (assert (equal? '((Lam x (x y)) (Lam y (z y)))
	 (reduce '(M replace ((Lam x (x y)) (Lam y (x y))) x z) rule-subst)))
 (assert (equal? '((Lam x (x z)) (Lam y (x y)))
	 (reduce '(M replace ((Lam x (x y)) (Lam y (x y))) y z) rule-subst)))
)


(include "median-filt.scm")
;(exit 0)


; The following set of patterns exhibits an insidious mutual recursive
; behavior. One mutual recursive loop is of size 3 (an odd length).

(define rule-odd-length-rec
  '(
    ( (M a (zero) _y) => (done _y) ) 
    ( (M a _x _y) => (M b _x _y) )
    ( (M b _x _y) => (M c _x _y) )
    ( (M c (succ _x) (zero)) => (M a _x (succ _x)) )
    ( (M c _x (succ _y)) => (M b _x _y) )
    ( (M d _x _y) => (M a _x _y))
))

(run-test
 (assert (equal? '(done (succ (zero)))
  (reduce '(M d (succ (succ (zero))) (succ (zero))) rule-odd-length-rec)))
)

; Another complex set of mutually-recursive rules

(define rule-complex-mr-bad
  '(
    ( (M a (succ _n) _m _r) => (M a _n _m (succ (succ _r))) )
    ( (M a (zero) (succ _m) _r) => (M a (zero) _m (succ (succ _r))) )
    ( (M a (zero) (zero) (succ _r)) => (M x _r) )
    ( (M x (succ _r)) => (M y _r _r (succ (zero))) )
    ( (M y (succ _r) (succ _r) (succ (zero))) => (M a _r _r (zero)) )
))

; Another complex set of mutually-recursive rules
; Each rule is contractive, rule1 * rule2 is contractive, but
; rule1*rule1*rule2 is not contractive!
(define rule-complex2-mr-bad
  '(
    ( (M a _x (succ _y)) => (M a (succ _x) _y))
    ( (M a (succ (succ _x)) _y) => (M a _x (succ (succ _y))))
   ))



; Indirect recursion: Example 2 from C.S.Lee, CPSE 2002 (LNCS 2487), p. 220
(define indirect-rec
  '(
     ( (M mult _m _n) => (M loop1 _m (zero) _n (zero)) )
     ( (M loop1 (zero) _j1 _n1 _a1) => _a1 )
     ( (M loop1 (succ _i1) _j1 _n1 _a1) => (M loop2 _i1 _n1 _n1 _a1) )
     ( (M loop2 _i2 (zero) _n2 _a2) => (M loop1 _i2 (zero) _n2 _a2) )
     ( (M loop2 _i2 (succ _j2) _n2 _a2)
       => (M loop2 _i2 _j2 _n2 (succ _a2)) )
     ))

; Nested calls: Example 3 from C.S.Lee, CPSE 2002 (LNCS 2487), p. 220
; Deciding termination requires a size-change analysis:
; figuring that the result of (M sub a b), b>0 is always less than a
(define nested-calls
  '(
     ( (M quot _m (zero)) => false)
     ( (M quot _m _n) => (M quot1 _m _n (M less? _m _n)) )

     ( (M quot1 _m _n true) => (zero) )
     ( (M quot1 _m _n false) => (succ (M quot (M sub _m _n) _n)) )

     ( (M less? (zero) (succ _)) => true )
     ( (M less? _      (zero)) => false )
     ( (M less? (succ _x) (succ _y)) => (M less? _x _y) )

     ( (M sub _a (zero)) => _a )
     ( (M sub (succ _a) (succ _b)) => (M sub _a _b) )
   ))

; Complex descent: Descent in a sum of parameter sizes.
; Example 4b from C.S.Lee, CPSE 2002 (LNCS 2487), p. 220
; The number sizeof(x) + sizeof(y) + sizeof(z) decreases on every
; program state transition.
; Pluemer identifies this as an important form of descent.
(define complex-descent-on-sum
  '(
     ( (M p _x _y (seq-empty)) => _x )
     ( (M p _x (seq-empty) (seq _ _z)) => (M p _x _z (seq-empty)) )
     ( (M p _x (seq _ _y) _z) => (M p _z _y _x) )
     ))

; Complex descent: Descent in the maximum over parameter sizes.
; Example 4c from C.S.Lee, CPSE 2002 (LNCS 2487), p. 221
; The number max(sizeof(x), sizeof(y)) decreases on every
; program state transition.
; C.S.Lee says that this descent has been observed in a type inference
; algorithm.
(define complex-descent-on-max
  '(
     ( (M q (seq (seq true _) _) _) => true )
     ( (M q _ (seq (seq true _) _)) => true )
     ( (M q _x _y) => (M and 
			(M q (M hd (M tl _x)) (M tl (M tl _x)))
			(M q (M hd (M tl _y)) (M tl (M tl _y))) ))
     ( (M and true true) => true )
     ( (M and _ _) => false )
     ( (M hd (seq _x _)) => _x )
     ( (M tl (seq _ _xr)) => _xr )
     ))


; Complex descent: Combining different complex descents
; Example 4d from C.S.Lee, CPSE 2002 (LNCS 2487), p. 221.
; C.S.Lee says that this descent is not expected in practice
(define complex-descent-complex
  '(
     ( (M r _x _y _z (seq-empty)) => _x )
     ( (M r _x (seq-empty) _z (seq _ _w)) => 
       (M r _x _x (seq one _z) _w) )
     ( (M r _x _y (seq-empty) (seq _ _w)) => 
       (M r _x _x (seq one (seq-empty)) _w) )
     ( (M r _x (seq _y1 _y) (seq _ _z) _w) =>
       (M r _y (seq _y1 _y) _z (seq one _w)) )
     ))


; The contraction prover considers every rule (<pattern> => <conseq>)
; in turn. If it can prove the rule contracting, it is removed from
; the ruleset. Oftentimes it is possible to reduce the proof of the
; original rule with contractiveness proof of the set of rules
;	((<pattern> => <conseq1>) ...)
; In that case, the original rule is removed from the list and replaced
; with the set of subgoals (subproofs).
; The proof is finished if it ends in an empty ruleset list.


; Given the ruleset ((<pattern> => <conseq>) ...)
; apply a procedure pruner to every rule.
; The procedure should have the following interface:
;	pruner ruleset pattern conseq
; The procedure should return:
;	#f - the pruner failed to do anything with the 'conseq' 
;	     and it should be left alone
;	(c1 c2 ...) - the pruner reduced the conseq to the list of
;	     other consequents. The original rule is replaced with the
;	     list ( (<pattern> => c1) (<pattern> => c2) ...)
;	     and the pruner is re-applied.
;	() - the pruner proved that the consequent is contractive, so
;	     the rule should be removed
; The prune procedure returns the updated ruleset, or #f if no changes
; were made.

(define (prune pruner ruleset)
	; return #f, () or an updated rule
  (define (prune-rule pattern conseq-symb conseq)
    (assert (eq? '=> conseq-symb))
    (let ((pruner-result (pruner ruleset pattern conseq)))
      (and pruner-result
	   (map (lambda (new-conseq) (list pattern '=> new-conseq))
		pruner-result))))

  (let loop ((ruleset ruleset) (new-rset '()) (changed? #f))
    (cond
     ((null? ruleset) (and changed? new-rset))
     ((apply prune-rule (car ruleset)) =>
      (lambda (new-rules)
	(if (null? new-rules)	; the old rule is to be deleted
	    (loop (cdr ruleset) new-rset #t)
				; splice in the new rules and
				; reapply the pruner
	    (loop (append new-rules (cdr ruleset)) new-rset #t))))
     (else (loop (cdr ruleset) (cons (car ruleset) new-rset) changed?)))
))

; Trivial termination judgements
; The following are trivial contractiveness judgements:
;	<ruleset> |- (<pattern> => <conseq>) : rule; 
;       <conseq> is not an M-term
; ==> <ruleset> |- (<pattern> => <conseq>) contractive
;
; That is, if the consequent of a rule cannot be further reduced,
; removing the rule does not affect the termination of the ruleset.
; The strategy is sound even if the consequent contains variables:
; Because of an applicative order of evaluation, a variable
; can never be matched against an M-term. Thus there is no substitution
; during the reduction that may turn a V-term into an M-term.

; Take the list of the above form (the original ruleset works as well)
; and remove all the consequents that are obviously less than the
; originating patterns. Return the pruned list
; if the <conseq> is of the form (symbol <term>*)
; we replace the <conseq> with the list of <term>s, which we will
; scan again

(define (prune-immed ruleset)
  (cout "prune-immed...\n")
  (prune 
   (lambda (ruleset pattern conseq)
     (cond
      ((not (M-term? conseq)) '())	; conseq is contracting
      ((and (pair? conseq) (not (M-term-immed? conseq)))
       conseq)
      (else #f)))
   ruleset))

(run-test
  (cout "testing prune-immed..." nl)
  (pp (prune-immed polynomial-rules))
  (pp (prune-immed rule-evenp))
  (pp (prune-immed rule-fact))
  (pp (prune-immed rule-Ackermann))
)

; Given two M-terms, find out if they can possibly match
; In the future, make a stronger statement: 
; (= (length m-term1) (length m-term2))
(define (M-term-could-match? m-term1 m-term2)
  (assert (and (M-term-immed? m-term1) (M-term-immed? m-term2)))
  (eq? (cadr m-term1) (cadr m-term2)))
	  


; Apply an inference rule about a contractive ruleset: non-occurence
;	and immed-recursion
;
; Non-occurrence: there exists a rule whose consequent is an M-immediate
; term that cannot be unified with a pattern of any existing rule.
; If this rule is activated, it would clearly produce a term that
; can't be re-written further.
; <ruleset> |- (<pattern> => <conseq>) rule
; all r: <ruleset> |- r rule, not( pattern(r) `unify` <conseq> )
; all i: <ruleset> |- (<pattern> => field(<conseq>,i)) contractive
; ==> <ruleset> |- (<pattern> => <conseq>) contractive
;
; Note that <conseq> may contain nested <M-term-simple>s. All such
; components are replaced with _ before we attempt to unify the <conseq>
; with the pattern of any rule. Also we have to make all variables in the
; <conseq> are unique before the unification. We
; use unify-trees procedure to unify the terms.
; Here by `unify` me mean an _acyclic_ unification: clearly
; a consequent (M foo _v _v) does not unify with the pattern
; (M foo (succ _y) _y).
;
; Immediate recursion: there exists a rule whose consequent can unify
; _only_ its own pattern. 
; <ruleset> |- r1 as (<pattern> => <conseq>) rule
; all r: <ruleset> |- r rule, r != r1, not( pattern(r) `unify` <conseq> )
; pattern(r1) `unify` <conseq>
; exists i: field(<pattern>,i) < field(<conseq>,i)
; all i: <ruleset> |- (<pattern> => field(<conseq>,i)) contractive
; ==> <ruleset> |- r1 contractive
;
; We define the '<' relationship between two terms (fields of the pattern
; and the consequent) as a containment.
; Justification: if there exists a rule whose consequent matches only
; its own pattern (simple recursion) and the result of matching
; causes some subterm to shrink, the entire rule is terminating
; provided all embedded M-terms are contractive as well.
;
; Note that the test
;	pattern(r1) `unify` <conseq>
; should have used a cyclic unification: a singleton rule
; (M foo (succ _y)) => (M foo _y)
; is directly recursive (and yet its pattern can be unified with the
; consequent only by a cyclic recursion). However, in the algorithm
; below, we alpha convert the variables in the consequent before
; matching with patterns. Therefore, the acyclic unification is sufficient.


	; given a complex term, replace all embedded occurrences of
	; <M-term-simple> with _.
(define (anonymize-embedded-M term)
  (define (anonymize-M term)
    (cond
     ((not (pair? term)) term)
     ((M-term-immed? term) '_)
     (else (map anonymize-M term))))
  (map anonymize-M term))

	; given a ruleset: ((<pat1> => <conseq1>) ...)
	; and a <conseq>, return all such <pati> that
	; <pati> `unify` <conseq>
	; <conseq> must be an M-term-immed?, otherwise the return result
	; is '(), obviously
(define (all-patterns-that-unify ruleset conseq)
  (if (not (M-term-immed? conseq)) '()
      (let ((M-flattened-conseq (alfa-convert (anonymize-embedded-M conseq))))
	(let loop ((ruleset ruleset) (result '()))
	  (cond
	   ((null? ruleset) result)
	   ((unify-simple? (caar ruleset) M-flattened-conseq)
	    (loop (cdr ruleset) (cons (caar ruleset) result)))
	   (else
	    (loop (cdr ruleset) result)))))))

	; Decide if term1 < term2 in the sense of embedding
(define (term<? term1 term2)
  (and (pair? term2)
    (any? (lambda (term) (or (equal? term1 term) (term<? term1 term))) term2)))

(define (prune-simple-recursion ruleset)

  (cout "prune simple-recursion and non-occurence...\n")
  (prune 
   (lambda (ruleset pattern conseq)
     (let ((possibly-matching-patterns
	    (all-patterns-that-unify ruleset conseq)))
       (cond
	((null? possibly-matching-patterns)
	 (cout "Rule " pattern " => " conseq " is non-occuring\n")
	 (if (pair? conseq) conseq '()))
	((pair? (cdr possibly-matching-patterns))
	 #f)			; More than one matching pattern
	((not (equal? (car possibly-matching-patterns) pattern))
	 #f)			; Not a simple recursion
	((any?
	  (lambda (pattern-cons)
	    (term<? (cdr pattern-cons) (car pattern-cons)))
	  (map cons pattern conseq))
	 (cout "Rule " pattern " => " conseq " is recursively contractive\n")
	 (cddr conseq))
	(else #f))))
   ruleset)
)

(run-test
  (cout "testing prune-simple-recursion..." nl)
  (assert (equal? '() (prune-simple-recursion (prune-immed polynomial-rules))))
  ; can't reduce mutually-recursive rules with prune-simple-recursion
  (assert (not (prune-simple-recursion (prune-immed rule-evenp))))
  (assert (equal? '()
 	    (prune-simple-recursion
 	     '( ((M foo (succ _y)) => (M foo _y))) )))
  (assert (equal? '()
	   (prune-simple-recursion
	     (prune-simple-recursion
		'( ((M foo (succ _y) (succ _y)) => (M foo _y _y)) 
		   ((M foo _y (succ _y)) => (M foo _y _y)) ) ))))
  (assert
    (equal?
      '(((M fact (succ _x)) => (M mult (succ _x) (M fact _x)))
	 ((M mult (succ _x) _y) => (M add _y (M mult _x _y))))
      (prune-simple-recursion (prune-immed rule-fact))))
)

; Converting the ruleset to the M-simple-normal form
; 
; Example: given a rule
;    (M foo _x) => (M bar (succ _x) (M baz _x _x))
; we replace it with two rules
;    (M foo _x) => (M bar (succ _x) _uniq)
;    (M foo _x) => (M baz _x _x)
; where _uniq is a fresh variable. In the new ruleset, the consequent
; of each rule is a M-simple-term (that is, a term with no embedded M-terms)
; Rationale: if the M-simple-normalized ruleset terminates for each input,
; so does the original ruleset. The reason is that
;    (M foo _x) => (M bar (succ _x) _uniq)
; is universally quantified over _uniq. If such a universally
; quantified ruleset terminates, so would the original ruleset (where
; _uniq is replaced with a particular value (M baz _x _x)).
;
; The M-simple-normalization is definitely the weakening: it is sound
; but not complete. So, for some rulesets, we would not be able to
; prove their termination after we performed normalization. And yet,
; the normalization simplifies our analyses and thus beneficial.

; Take a ruleset and return the normalized ruleset
; We assume that each consequent is an M-term-immed
(define (normalize-to-M-simple ruleset)
  ; given a term, normalize it and return the
  ; normalized term and the env: the list of bindings
  ; of unique variables to embedded M-terms.
  ; The embedded terms are replaced with variables
  ; We do a bottom-up traversal
  (define (norm-term term env)
    (if (not (pair? term)) (values term env)
      ; fold over the subterms
      (let loop ((subterms term) (env env) (transformed '()))
	(cond
	  ((null? subterms)
	    (let ((new-term (reverse transformed)))
	      (if (M-term-immed? new-term)
		(let ((var (genvar)))
		  (values var (cons (cons var new-term) env)))
		(values new-term env))))
	  (else
	    (let*-values
	      (((new-subterm env) (norm-term (car subterms) env)))
	      (loop (cdr subterms) env (cons new-subterm transformed))))
	  ))))
  (let loop ((ruleset ruleset) (new-ruleset '()))
    (if (null? ruleset) new-ruleset
      (let*-values
	(((pattern conseq-symb conseq) (apply values (car ruleset)))
	 ((new-conseq env) (norm-term conseq '())))
	(assert (pattern-var? new-conseq)) ; conseq should've been M-immed
	(for-each
	  (lambda (binding)
	    (if (not (eq? (car binding) new-conseq))
	      (cout "normalization: " (car binding) " -> " 
		(cdr binding) nl)))
	  env)
	(let fold ((env env) (new-ruleset new-ruleset))
	  (if (null? env) (loop (cdr ruleset) new-ruleset)
	    (fold (cdr env)
	      (cons
		(list pattern '=> (cdar env))
		new-ruleset))))
	))))

(run-test
  (cout "normalize-to-M-simple" nl)
  (assert
    (match-tree
      '(((M foo _x) => (M baz _x _x)) ((M foo _x) => (M bar (succ _x) _uniq)))
      (normalize-to-M-simple
	'(((M foo _x) => (M bar (succ _x) (M baz _x _x)))))
      '()))
  (assert (equal? '(((M foo _x) => (M bar (succ _x) _z)))
	    (normalize-to-M-simple
	      '(((M foo _x) => (M bar (succ _x) _z))))))
  (assert
    (match-tree
      '(((M var _x _y) => (M x))
	 ((M var _x _y) => (M y _y))
	 ((M var _x _y) => (M bar _g275 _g276))
	 ((M foo _x _y) => (M foo _x _x))
	 ((M foo _x _y) => (M bar (succ _x) _g273)))
      (normalize-to-M-simple
	'(((M foo _x _y) => (M bar (succ _x) (M foo _x _x)))
	   ((M var _x _y) => (M bar (M x) (M y _y)))))
      '()))
)


; Removing rules that are indirectly irrecursive
; A rule is indirectly irrecursive if it is not directly recursive
; and if its pattern does not unify consequents of any reachable
; rules
; We assume all rules have been M-simple-normalized
; This approach doesn't seem to be working out: hardly any rules
; are removed this way.
(define (prune-indirectly-irrecursive ruleset)

  ; pattern and conseq are alpha converted
  (define (indirectly-recursive? pattern conseqs ruleset)
    (cout "pattern: " pattern " conseqs: " conseqs " ruleset: " ruleset nl)
    (and (not (null? ruleset)) (not (null? conseqs))
      (let ((conseq (car conseqs)))
	(let loop ((ruleset ruleset) (examined '()) (conseqs (cdr conseqs)))
	  (cond
	    ((null? ruleset) 
	      (indirectly-recursive? pattern conseqs examined))
	    ((not (unify-simple? conseq (pattern-of (car ruleset))))
	      (loop (cdr ruleset) (cons (car ruleset) examined) conseqs))
	    ((unify-simple? (conseq-of (car ruleset)) pattern)
	      #t)
	    (else
	      (loop (cdr ruleset) examined
		(cons (alfa-convert (conseq-of (car ruleset))) conseqs))))
	  ))))

  (cout "prune indirectly irrecursive rules...\n")

  (let loop ((ruleset ruleset) (examined '()) (changed? #f))
    (if (null? ruleset) (and changed? examined)
      (let* ((rule (car ruleset))
	     (pattern (alfa-convert (pattern-of rule)))
	     (conseq  (alfa-convert (conseq-of rule))))
       (if (unify-simple? pattern conseq) ; directly recursive
	 (loop (cdr ruleset) (cons (car ruleset) examined) changed?)
	 (let ((result
		 (indirectly-recursive? pattern (list conseq)
		   (append (cdr ruleset) examined)))) ; remove the rule itself
	   (if result
	     (loop (cdr ruleset) (cons (car ruleset) examined) changed?)
	     (begin
	       (cout "rule: " rule " indirectly irrecursive" nl)
	       (loop (cdr ruleset) examined #t))))))))
)

(run-test
  (cout nl "prune-indirectly-irrecursive..." nl)
  (pp
    (prune-indirectly-irrecursive
      '( ((M a _x _y) => (M a _x _y))
	 ((M a _x c1) => (M a _x c2)))))
)

; SRFI-1:
; partition pred list -> [list list] 
; Partitions the elements of list with predicate pred, and returns two
; values: the list of in-elements and the list of out-elements. The
; list is not disordered -- elements occur in the result lists in the
; same order as they occur in the argument list. The dynamic order in
; which the various applications of pred are made is not
; specified. One of the returned lists may share a common tail with
; the argument list.

; one of the result lists may share a tail with the original list
(define (partition pred? lst)
  (let down ((lst lst) (k (lambda (in out) (values in out))))
    (cond
     ((null? lst) (k '() '()))
     ((pred? (car lst))
      (down (cdr lst)
	    (lambda (in out)
	      (k (if (null? out) lst (cons (car lst) in)) out))))
     (else
      (down (cdr lst)
	    (lambda (in out)
	      (k in (if (null? in) lst (cons (car lst) out)))))))))

(run-test
 (let*-values (((in out) (partition symbol? '(one 2 3 four five 6))))
    (assert (and (equal? in '(one four five))
		 (equal? out '(2 3 6)))))
)

; Returns the union of the lists, using comparator?  for the 
; element-equality procedure. 
; Adding to lst1 those elements from lst1 that are not already there

(define (lset-union comparator? lst1 lst2)
  (if (eq? comparator? equal?)
      (let loop ((result lst1) (lst lst2))
	(cond
	 ((null? lst) result)
	 ((member (car lst) result) (loop result (cdr lst)))
	 (else (loop (cons (car lst) result) (cdr lst)))))
      (error "Not implemented yet")))

(run-test
 (assert (equal? '(u o i a b c d e)
		 (lset-union equal? '(a b c d e) '(a e i o u))))
 (assert (equal? '(x a a c)
		 (lset-union equal? '(a a c) '(x a x))))
)

; The purpose of roll-one is to eliminate a rule in a ruleset by
; symbolically expanding all other rules with it.
; Given a ruleset, we choose a rule which is not directly recursive
; and non-overlapping (defined below) 
; We then symbolically expand all other rules with the chosen rule,
; add the expansions to the ruleset and eliminate the chosen rule.
; We claim that if the resulting ruleset is terminating for all
; source terms, so is the original one. The claim rests on the
; fact the chosen rule is not directly recursive (that is,
; its consequent does not (cyclically) unify with its own pattern).
; Indeed, let C be the chosen rule, and let T be a V-term.
; If T does not match the pattern of C, then the presence or the absence
; of C is of no importance. If T can be re-written with C, the re-writing
; result will not match C again, so removing C will not affect the
; termination property of the ruleset. It may happen that T matches
; some other rule whose result matches C. However, we added to the ruleset
; an expansion of that rule with C (unfolding of that rule with C).
; So again the termination property will not be affected.
;
; The eventual result of the process is that all cycles of mutual
; recursion become regular recursion or become clusterized (see
; analyze-clusters, below).
; Note that the process of roll-one is converging.
;
; A rule is called directly recursive if its consequent
; unifies its alpha-converted pattern. E.g., the following rules
;   (M foo _x) => (M foo (zero))
;   (M foo _x) => (M foo (succ _x))
;   (M foo (succ _x)) => (M foo _x)
;   (M foo (succ _x) _x) => (M foo _x (zero))
; are directly recursive.
;
; A rule C is called overlapping if there exists a rule A in the ruleset
; (different from C) so that a pattern of C acyclically unifies with
; the pattern of A. That is, the rule C can be considered an "instance"
; of rule A. For example, the rules with the following patterns
;   (M foo (zero)) and (M foo _x)
;   (M foo c _x)  and  (M foo _y c)
;   (M foo _x _y) and (M foo _x _x) ; The second does not match first
; are all overlapping. The last example shows that we really need an
; acyclic unification to decide overlapping rather than a simple
; matching. If rule A overlaps with C, then the expansion of A with C
; may give C again. If no rule overlaps with C, then the expanded
; ruleset will not have a rule that has the same pattern as
; C. Therefore, if we only chose rules that are not directly recursive
; and not overlapping, the expansion process terminates.
;
; Here we assume that the ruleset has been M-simple-normalizied, that is,
; all consequents are M-simple-terms.


; A simpler version of expansion, of historical interest.
; Given a rule and a ruleset, apply the rule to each rule in the ruleset,
; and return the result.
; If in the expansion failed, return #f.
; For each rule in the ruleset, we check if any of atomic M-term-simple
; match the unfolding-rule. If so, they are expanded out. Otherwise,
; the rule is left as it is. We expand out only M-term-simple terms
; (that is, M-terms that do not contain M-terms).
; The internal procedure unfold-term is essentially a one-step
; "abstract" normalization!

(define (expand-with-rule-simple unfolding-rule ruleset)
  (let* ((unfolding-rule (alfa-convert unfolding-rule))
	 (pattern (pattern-of unfolding-rule))
	 (conseq (conseq-of unfolding-rule)))

    ; Unfold all M-term-simple (sub)terms of a term against the unfolding-rule
    ; Return either a term (which can be either equal? to the original
    ; or not, if unfolding succeeded), or #f. The latter indicates
    ; that the input term is a V-term
    (define (unfold-term term)
      (and (pair? term)
	(let loop ((subterms term) (complex? #f) (transformed '()))
	  (cond
	    ((null? subterms)
	      (cond
		(complex? (reverse transformed))
		((not (M-term-immed? term)) #f) ; it's a V-term
	        ; It's a M-term-immed whose subterms are V-terms
	        ; That is, we have a M-simple-term
		; term may contain variables -- but they "don't count"
		; (i.e., they are considered constants)
		((match-tree pattern term '()) =>
		  (lambda (env)
		    ;(cout "matched: " env nl)
		    (substitute-vars conseq env)))
		(else term)		; M-simple-term that doesn't match
	      ))
	    ((unfold-term (car subterms)) => ; a complex subterm
	      (lambda (new-subterm)
		(loop (cdr subterms) #t (cons new-subterm transformed))))
	    (else				; a simple subterm
	      (loop (cdr subterms) complex? 
		(cons (car subterms) transformed)))))
      ))

    (let ((new-ruleset
	    (map (lambda (rule)
		   (cond
		     ((unfold-term (conseq-of rule)) =>
		       (lambda (new-conseq) 
			 (list (pattern-of rule) '=> new-conseq)))
		     (else rule)))
	      ruleset)))
      (and (not (equal? new-ruleset ruleset)) new-ruleset)
    )))

; (run-test
;   (cout nl "Expand-with-rule" nl)
;   (assert
;     (equal? '(((M odd (seq _c _r)) => (res _r _r _r)))
;       (expand-with-rule '( (M even (seq _c _r)) => (res _r _c _r) )
; 	'( ( (M odd (seq _c _r)) => (M even (seq _r _r)) ) ))))
;   (assert
;     (equal?
;       '(((M odd (seq _c _r)) =>
; 	  (M even
; 	    (seq (res _r _r _r) (foo) (res (seq _c _r) _c (seq _c _r)))
; 	    (foo (bar)))))
;       (expand-with-rule '( (M even (seq _c _r)) => (res _r _c _r) )
; 	'( ( (M odd (seq _c _r)) => (M even (seq
; 					      (M even (seq _r _r))
; 					      (foo)
; 					      (M even (seq _c (seq _c  _r))))
; 				      (foo (bar))))))))
;   (assert
;     (equal?
;       '(((M bar _x) => (M foo (succ _x) _x)) ((M bar _x) => (succ _x)))
;       (expand-with-rule '((M foo _x _x) => _x)
; 	'( ((M bar _x) => (M foo (succ _x) _x))
; 	   ((M bar _x) => (M foo (succ _x) (succ _x))) ))))
;   (assert (not
; 	    (expand-with-rule '( (M b _y (f _y)) => (c _y) )
; 	      '( ((M a _x) => (M b _x _x)) ))))
; )

; Given a rule and a ruleset, apply the chosen rule to each rule
; in the ruleset, and add the result to the ruleset.
; Return the expanded ruleset.
; An application of a rule to another rule is their composition:
; we try to re-write the consequent of the latter rule using the
; former rule. This process is essentially a reduction but
; with an abstract (universally quantified) subject term.
(define (expand-with-rule unfolding-rule ruleset)
  (let* ((unfolding-rule (alfa-convert unfolding-rule))
	 (pattern (pattern-of unfolding-rule))
	 (conseq (conseq-of unfolding-rule)))

    ; Return a normalized env
    (define (acyclic-unify-trees tree1 tree2)
      (and-let* ((env (unify-trees tree1 tree2 '()))
		 (env (normalize-subst env #f)))
	env))
	  
    (let loop ((ruleset ruleset) (new-ruleset ruleset))
      (cond
	((null? ruleset) new-ruleset)
	((acyclic-unify-trees (conseq-of (car ruleset)) pattern) =>
	 (lambda (env)
	   (loop (cdr ruleset)
	     (cons
	       (substitute-vars-open 
		 (list (pattern-of (car ruleset)) '=> conseq) env)
	       new-ruleset))))
	(else (loop (cdr ruleset) new-ruleset))))
    ))
	
(run-test
  (cout nl "Expand-with-rule" nl)
  (assert
    (match-tree
      '(((M odd (seq _c _r1)) => (res _r1 _r1 _r1))
	 ( (M odd (seq _c _r)) => (M even (seq _r _r)) )) 
      (expand-with-rule '( (M even (seq _c _r)) => (res _r _c _r) )
	'( ( (M odd (seq _c _r)) => (M even (seq _r _r)) ) ))
      '()))
  (assert
    (equal?
      '( ((M bar _x) => (succ _x))
	 ((M bar _x) => (M foo (succ _x) _x))
	 ((M bar _x) => (M foo (succ _x) (succ _x))) )
      (expand-with-rule '((M foo _x _x) => _x)
	'( ((M bar _x) => (M foo (succ _x) _x))
	   ((M bar _x) => (M foo (succ _x) (succ _x))) ))))
  (assert (equal? '( ((M a _x) => (M b _x _x)) ) ; the original ruleset
	    (expand-with-rule '( (M b _y (f _y)) => (c _y) )
	      '( ((M a _x) => (M b _x _x)) ))))
)


; Given a ruleset, chose a rule and expand the ruleset with it.
; Return the updated ruleset, or #f if the rollout was unsuccessful.
(define (roll-one ruleset)
  (define (recursive? rule)
    (let ((pattern (pattern-of rule))
	  (conseq  (conseq-of rule)))
      (if (not (M-term-immed? conseq))
	(error "conseq " conseq 
	  " is not M-term-immed?. Should've been eliminated earlier"))
      (unify-simple? pattern (alfa-convert conseq))))

  (define (overlapping? chosen-rule)
    (let ((pattern (alfa-convert (pattern-of chosen-rule))))
      (any?
	(lambda (rule) 
	  (and (not (eq? rule chosen-rule))
	    (unify-simple? pattern (pattern-of rule))))
	ruleset)))

  (let loop ((ruleset ruleset) (examined '()))
    (if (null? ruleset) #f  ; failed to pick the rule to expand with
      (let ((rule-to-expand-with (car ruleset)))
	(and (recursive? rule-to-expand-with)
	  (cout "recursive! " rule-to-expand-with nl))
	(and (overlapping? rule-to-expand-with)
	  (cout "overlapping! " rule-to-expand-with nl))
						
	(if (or (recursive? rule-to-expand-with)
	        (overlapping? rule-to-expand-with))
	  (loop (cdr ruleset) (cons rule-to-expand-with examined))
	  (begin
	    (cout "expanding with the rule: " rule-to-expand-with nl)
	    (expand-with-rule rule-to-expand-with
	    ; the ruleset to expand with does not include rule-to-expand-with
	    (append (cdr ruleset) examined))))))
    ))

(run-test
 (cout "Testing roll-one" nl)
 (let ((ruleset '(((M odd (seq _c _r)) => (M even _r)) 
		   ((M even (seq _c _r)) => (M odd _r)))))
   (pp (roll-one ruleset)))
 
 (assert (equal?
	   '(((M foo (succ (zero)) (zero)) => (M foo (succ (zero)) (zero)))
	     ((M foo (succ _x) _x) => (M foo _x (zero))))
	   (roll-one
	     '( ((M foo (succ _x) _x) => (M foo _x (zero))) ; recursive!
		((M foo _u _u) => (M foo (succ _u) (zero)))))))
 (assert (not
	  (roll-one '(((M fact (succ _x)) => (M mult (succ _x) _u))
		      ((M fact (succ _x)) => (M fact _x))
		      ((M mult (succ _x) _y) => (M mult _x _y))))))
 (assert (not
	  (roll-one '(((M a (succ _n) _m _r) => (M a _n _m (succ (succ _r))))
	      ((M a (zero) (succ _m) _r) => (M a (zero) _m (succ (succ _r))))
	      ((M a _ (zero) (succ _r)) => (M x _r))
	      ))))
(assert (equal? '(((M a _u) => (M foo _u _u)))
	  (roll-one '(((M foo (succ _u) _u) => (M z _u))
	      ((M a _u) => (M foo _u _u))))))
)


; Untagling of mutually recursive rules [obsolete: see analyze-clusters]
; The idea is an equivalence transformation
;	ruleset ==> ruleset^n
; where operation * is a rollout operation (see below).
;
; The idea is that given a rule, rule * ruleset is either '(), becomes
; recursive, or can be expanded further. If a rule can be expanded longer
; for more than |ruleset| steps, the rule can be disregarded: we must've
; seen the loop with other rules. The idea is that the longest loop
; in the ruleset can't have more than |ruleset|-1 hops.
;
; First we partition the ruleset into three disjoint sets
;  set-R0: (filter recursive? ruleset)
;  set-NR0: (set-of (r in ruleset) 
;		(and (r1 in set-PR0) (not (unifies (conseq r1) (pattern r)))))
;  set-PR0: (diff ruleset set-R0 set-NR0), or
;           (set-of (r in ruleset)
;		    (and (r1 in set-PR0)
;			 (not (unifies (conseq r) (pattern r)))
;			 (unifies (conseq r1) (pattern r))))
; Note the mutual recursion in definitions of set-PR and set-NR, which
; requires an iterative algorithm.
;
; predicate (recursive? rule) is defined as
;	(unifies (conseq rule) (pattern rule))
;
; We then compute 
; set-R_i+1 = (filter recursive? (* set-PR_i set-PR0))
; set-NR_i+1 = (union 
;		(set-of (r in set-PR_i)
;                 (and (r1 in set-PR0) (not (* r r1))))
;		(set-of (r in set-PR_i+1)
;		 (and (r1 in set-PR_i+1)
;		    (not (unifies (conseq r1) (pattern r)))))
;		(set-of (r in set-PR_i+1)
;		 (and (r1 in set-PR_i+1)
;		    (not (unifies (conseq r) (pattern r1))))) )
; set-PR_i+1 = (diff (* set-PR_i set-PR0) set-R_i+1 set-NR_i+1)
;
; Set set-NR_i+1 is an "untangled" set: rules that no longer exhibit
; mutual recursion
;
; we repeat the procedure for i=0..n-1, where n=(length set-PR0)
; After n steps of rollout, we can disregard set-PRn (it's looping)
; and we return
; (union set-Ri set-NRi)
;
; Operation * is a rollout operation: rollout(rule1,rule2):
;    (<pattern> => <conseq>): rule1  (<pattern1> => <conseq1>): rule2
;    <conseq> `unify` <pattern1> in env1
;    <conseq> is <M-term-simple>
;    ==>
;    (<pattern> => <conseq1>) with appropriate substitution
;    of variables as specified by env.
; rollout-0 and rollout that used to be here are eliminated: they are obsolete
; see analyze-clusters for a better algorithm


;--------------------------------------------------
; Analyzing a cluster of self- and mutually- recursive rules
; A cluster is a maximal set of rules
;     pattern_i => conseq_i
; such that pattern_i `unifies` conseq_j, j /= i and 
;	    conseq_i `unifies` pattern_k (k may be equal to i)
;

; Given a ruleset, split it into clusters and get a function
; process-cluster to try to reduce a cluster.
; The function process-cluster takes a cluster of rules and returns
; '() (if the cluster is proven terminating and should be removed),
; a new set of rules to replace the original cluster, or #f on
; failure to prove anything about the cluster.
; The function identify-clusters returns a new ruleset, or
; #f if no changes to any of the clusters were made.
; The function identify-clusters is thus similar to the function 'prune'
; The former applies to a cluster of rules rather than to individual
; rules.

(define (identify-clusters ruleset process-cluster)

	; Decide if a rule r belongs to a cluster of rules:
	; exists r' in cluster: pattern(r) `unify` conseq(r') and
	; exists r'' in cluster U r: pattern(r'') `unify` conseq(r)   
	; All rules in question are represented as 
	; (rule . (pi...)) where pi are all patterns that unify the
	; conseq(rule)
  (define (belongs-to-cluster? cluster rule.pattern)
    (let 
	((r1 
	  (any? 
	   (lambda (crule.patterns)	; in cluster
	     (member (pattern-of (car rule.pattern)) (cdr crule.patterns)))
	   cluster))
	 (r2
	  (any?
	   (lambda (crule.patterns)	; in cluster
	     (member (pattern-of (car crule.patterns)) (cdr rule.pattern)))
	   cluster))
	 (rself (member (pattern-of (car rule.pattern)) (cdr rule.pattern)))
	 )
      (and r1 (or r2 rself))))

  (let new-cluster-search
      ((lst		     ; ((rule . (pi...)) ...)
	(map (lambda (rule) ; where pi = pattern(ri), ri unifies conseq(rule)
	       (cons rule
		     (all-patterns-that-unify ruleset (conseq-of rule))))
	     ruleset)) 
       (result '())
       (changed? #f))
    ;(cout "\nnew-cls: " (lambda () (pp lst))  nl (lambda () (pp result)))
    (if (null? lst)
	(and changed? result)
	; Take the first element of lst as the seed for the new cluster,
	; and add as many elements from the rest of lst as possible.
	; We add a rule r to the cluster if belongs-to-cluster?
	; predicate says it belongs to
	(let clusterize ((cluster (list (car lst)))
			 (lst (cdr lst)))
	  (let*-values
	   (((add-to-cluster lst-rest)
	     (partition
	      (lambda (rules.patterns)
		(belongs-to-cluster? cluster rules.patterns))
	     lst)))
	   (if (null? add-to-cluster)	; nothing more to add
	       (let* ((full-cluster (map car cluster))
		      (new-cluster (process-cluster full-cluster)))
		 (if new-cluster
		     (new-cluster-search lst-rest 
					 (append new-cluster result) #t)
		     (new-cluster-search lst-rest 
					 (append full-cluster result)
					 changed?)))
	       (clusterize		; otherwise, repeat the iteration
		(append add-to-cluster cluster) lst-rest))
	   )))
    ))

(run-test
 (assert
  (equal? (identify-clusters rule-Ackermann (lambda (cluster) cluster))
	  (reverse rule-Ackermann)))

 (let ((rules '(
		((M c _g16891 (succ _g16890)) => (M c _g16891 _g16890))
		((M b _g16897 (succ _y)) => (M b _g16897 _y))
		((M a (succ _g16977) (zero)) => (M b _g16977 (succ _g16977)))
		((M a _g16982 (succ _g16981)) => (M c _g16982 _g16981))
		((M c (succ _g16942) (zero)) => (M c _g16942 (succ _g16942)))
		((M b (succ _g16946) (zero)) => (M b _g16946 (succ _g16946)))
		((M d _x _y) => (M a _x _y))))
       (clusters
	'( (((M c (succ _g16942) (zero)) => (M c _g16942 (succ _g16942)))
	    ((M c _g16891 (succ _g16890)) => (M c _g16891 _g16890)))
	   
	   (((M b (succ _g16946) (zero)) => (M b _g16946 (succ _g16946)))
	    ((M b _g16897 (succ _y)) => (M b _g16897 _y)))

	   (((M a (succ _g16977) (zero)) => (M b _g16977 (succ _g16977))))
	   (((M a _g16982 (succ _g16981)) => (M c _g16982 _g16981)))
	   (((M d _x _y) => (M a _x _y))) )))

   (assert 
    (= 7 (length
	    (identify-clusters rules
			       (let ((exp-clusters clusters))
				 (lambda (cluster)
				   (assert (pair? exp-clusters))
				   (assert (equal? cluster 
						   (car exp-clusters)))
				   (set! exp-clusters (cdr exp-clusters))
				   cluster))))))
   
    (not
     (identify-clusters rules
			(let ((exp-clusters clusters))
			  (lambda (cluster)
			    (assert (pair? exp-clusters))
			    (assert (equal? cluster 
					    (car exp-clusters)))
			    (set! exp-clusters (cdr exp-clusters))
			    #f))))
   )
 )


; Given a cluster of rules, try to prove it contractive.
; Return a new set of rules, or #f if proof was unsuccessful.
;
; A contraction inference rule for a cluster is a generalization of the
; corresponding rule for a simple mutual recursion:
; <ruleset> |- <rules> a cluster
; <rules> |- <fieldset> contractive
; all i: <ruleset> |- (<pattern> => field(<conseq>,i)) contractive
; ==> <ruleset> |- <rules> contractive
;
; where
; <ruleset> |- <pattern_n> => <conseq_n> a cluster
; all k. field(<conseq_k>,i)  < field(<pattern_k>,i)
; ==> <pattern_n> => <conseq_n> |- {i} contractive
;
; <ruleset> |- <pattern_n> => <conseq_n> a cluster
; exists k. field(<conseq_k>,i)  < field(<pattern_k>,i)
; all p. ( field(<conseq_p>,i) <= field(<pattern_p>,i) )
; {<pattern_p> => <conseq_p>, p /= k} |- <fieldset> contractive
; ==> <pattern_n> => <conseq_n> |- {i} U <fieldset> contractive

; Justification: if there exists a set of fields whose set of values
; always contacts for any sequence of reductions in a cluster,
; the cluster is contractive, provided all embedded M-terms are
; contractive as well.
; The preceeding inference rule is in fact the definition of 
; the lexicographic ordering on the sequence of rules. Lexicographic
; ordering of bounded sequences is well-formed, meaning that any 
; strictly decreasing sequence is finite (thus terminating).


; The following checker of clusters applies when the cluster contains
; more than one rule, that the conseq of every rule is an
; M-term-immed?, and that the number of fields in patterns and
; consequents of all rules is the same.
;
; For every rule, we compute a signature: a sequence 
; sig[i] = '< if field(conseq(rule),i) < field(pattern(rule),i)
;          '= if field(conseq(rule),i) = field(pattern(rule),i)
;          #f otherwise
;
; A cluster exhibits a lexicographic ordering (posesses a contractive set of
; fields) if:
; exists i.  
;   all rule in cluster. sig(rule,i) = '< or sig(rule,i) = '=
;   exists rule in cluster. sig(rule,i) = '<
;   set-of( rule | sig(rule,i) /= '< ) exhibits a lexicographic
;    ordering.
;
; If the cluster is proven contractive, every rule is replaced by a set
; pattern(rule) => field(conseq(rule),i)
; So the other provers can verify that separate fields (embedded M terms)
; are contractive as well.

; There is a faster algorithm to identify a lexicographic ordering
; (which we should implement in the future). Given a set of rules with
; their signatures, compute the signature of the entire set by
; reducing the signatures of all the rules in a cluster by the following
; commutative and associative reduction operation:
;      #f * x --> #f    '= * x ---> x    '< * '< --> '<
; A necessary condition for a cluster being contractive is cluster's
; signature containing at least one '<. Thus if the cluster signature has no
; '<, we report a failure. If we found at least one '<, we remove all the
; rules that have '< in the same position as in the cluster signature.
; We then repeat the process of computing and analyzing signature
; of thus reduced cluster.
;

(define (check-cluster cluster)

  ; compute a signature of a rule, or #f if it can't be computed
  ; A signature is a vector
  (define (rule-signature rule)
    (let ((pattern (pattern-of rule))
	  (conseq (conseq-of rule)))
      (and (M-term-immed? conseq)
	   (= (length pattern) (length conseq))
	   (list->vector 
	    (map (lambda (field-p field-c)
		   (cond
		     
		    ((equal? field-p field-c) '=)
		    ((term<? field-c field-p) '<)
;                   The analyze-bridge function relies on the fact that '=
;                   means identity!
; 		    ((or (and (not (pair? field-c))
; 			   (not (pattern-var? field-c)))
; 		       (and (pair? field-c)
; 			 (null? (cdr field-c)) (not (pair? (car field-c)))
; 			 (not (pattern-var? (car field-c)))))
; 		      '=) ; !!!
		    (else #f)))
		pattern conseq)))))

  ; The procedure implements the lexicograpic ordering test shown in the
  ; comments above
  ; Given a set of signatures and a field index, test to see
  ; if the set of signatures makes lexicographic order with 'i
  ; being the major index
  (define (contractive? signatures i)
    (cond
     ((null? signatures) #t)
     ((>= i (vector-length (car signatures))) #f)
			; if the field is increasing in some signatures
			; try another field
     ((not (every? (lambda (sig) (vector-ref sig i)) signatures))
      (contractive? signatures (++ i)))
     (else		; partition the set of signatures in two subsets
      (let*-values	; depending if sig(i) = '< or '=
       (((decreasing constant)
	 (partition
	  (lambda (sig) (eq? (vector-ref sig i) '<))
	  signatures)))
       (if (null? decreasing)
	  (contractive? signatures (++ i))
	  (contractive? constant 0))))))  ; recursively check the subset

  ; Reduce the list of signatures to one. To be used in the future
  ; algorithm described in the comments.
  (define (reduce-signature signature-l)
    (let loop ((accum (car signature-l)) (lst (cdr signature-l)))
      (cond 
       ((null? lst) accum)
       ((not (= (length (car lst)) (length accum))) #f)
       (else
	(loop
	 (map (lambda (x y)
		(case x
		  ((#f) #f)
		  ((=) y)
		  ((<) (and y '<))))
	      accum (car lst))
	 (cdr lst))))))

  (and-let*
   ( ((pair? cluster))		; at least two rules in a cluster
     ((pair? (cdr cluster)))
     ((begin (display "\nchecking cluster: ") (pp cluster) #t))
     (signatures (map rule-signature cluster))
     ((begin (display "\nSignature: ") (pp signatures) #t))
     ((every? (lambda (x) x) signatures))	; no bad signatures
     ((every? (lambda (s) (eq? '= (vector-ref s 1))) signatures)))
    (cond
      ((contractive? signatures 0)
	(cout "cluster proven contractive\n")
	'() ; If all the rules M-simple-normalized, the cluster is eliminated
	)
      (else (analyze-bridge cluster signatures)))
    ))


; Checking for and removing bridge rules in a cluster
; Given a cluster of rules as defined above, a set of bridge rules
; has the following property:
; exists field i so that:
;   all r (not bridge). field(pattern-of(r),i) = field(conseq-of(r),i)
;   all r1,r2 (bridge). field(pattern-of(r1),i)
;                            `not-unify` field(conseq-of(r2),i)
; Then removing the bridge rules should not affect the termination property
; of the cluster.
; Indeed, let br is a set of bridge rules and cl is the set of the other
; rules in a cluster. The set br is not mutually recursive (field i will
; never match). Furthermore, br(cl)* is not mutually recursive either.
; Suppose cl terminates, and suppose br+cl has an infinite chain of the rules.
; (br+cl)* = br* + (cl*br*cl*)* + cl*
; Because cl terminates, cl* is limited. Because br is not mutually
; recursive, br* can be at most br. Furthermore, because br(cl*) is not
; mutually recursive, in any chain br may appear at most once. Thus
; no infinite chain in (br+cl) is possible.
;
; The equality property on the bridge field in the non-bridge rules
; is important. The equality condition cannot be replaced with
; a decreasing condition. Consider a ruleset:
; A:  (M foo _x (zero)) => (M foo (succ _x) (succ (zero)))
; B:  (M foo (succ _x) _y)  => (M foo _x _y)
; Rule A is a bridge rule: its consequent cannot unify its pattern:
; (succ (zero)) cannot match (zero).
; Rule B is a non-bridge rule. We know that AB* is still non-recursive.
; However, suppose B were the following:
; C:  (M foo (succ _x) (succ _y)) => (M foo _x _y)
; We can no longer claim that AC* is not recursive. In fact, AC is recursive.
; and the cluster {A,C} is non-terminating, whereas {A,B} is terminating.
; Although the rule C is "more contracting", {A,C} is diverging!


; The function analyze-bridge takes a ruleset that must be a cluster,
; and tries to detect a bridge. If it finds the bridge, it removes it
; and returns the remaining rules. If no bridge has been identified,
; the function returns #f.

(define (analyze-bridge ruleset signatures)

  ; test the signatures to see if field i can be a bridge field
  ; return (values non-bridge bridge)
  ; where bridge is the set of rules (whose i-th signature is #f)
  ; and non-bridge is a set of rules whose i-th signature is '=
  ; On failure, return (values ruleset '())
  (define (identify-bridge-field i)
    (let loop ((ruleset ruleset) (signatures signatures)
	       (bridge '()) (non-bridge '()))
      (cond
	((null? ruleset) (values non-bridge bridge))
	((eq? '= (vector-ref (car signatures) i))
	 (loop (cdr ruleset) (cdr signatures)
	   bridge (cons (car ruleset) non-bridge)))
	((eq? #f (vector-ref (car signatures) i))
	 (loop (cdr ruleset) (cdr signatures)
	  (cons (car ruleset) bridge) non-bridge))
	(else (values ruleset '())))))


  ; check to see that the i-th field of the patterns in the bridge
  ; set does not match the i-th field in any of the consequents
  (define (check-bridge-property bridge i)
    (let ((pattern-fields
	    (map (lambda (rule)
		   (list-ref (pattern-of rule) i)) bridge))
	  (conseq-fields
	    (map (lambda (rule)
		   (alfa-convert
		     (list-ref (conseq-of rule) i))) bridge)))
      (every?
	(lambda (pf)
	  (every? (lambda (cf) (not (unify-simple? pf cf))) conseq-fields))
	pattern-fields)))
	
  (let ((n (vector-length (car signatures))))
    (let loop ((i 2))
      (if (>= i n) #f
	(let*-values (((non-bridge bridge) (identify-bridge-field i)))
	  (cond
	    ((null? bridge) (loop (++ i)))
	    ((check-bridge-property bridge i)
	     (cout "Found a bridge on field " i nl)
	     (pp bridge) (cout nl)
	     non-bridge)
	    (else (loop (++ i))))))))
)
	    
(run-test
 (assert (check-cluster 
	   '(((M c (succ _x) (zero)) => (M c _x (succ _x)))
	    ((M c _x (succ _y)) => (M c _x _y)))))
 (pp (check-cluster 
	   '(((M c (succ _x) (zero)) => (M c _x (succ _x)))
	    ((M c _x (succ _y)) => (M c _x (succ _y))))))
 (assert (not (check-cluster 
	   '(((M c (succ _x) (zero)) => (M c _x (succ _x)))
	    ((M c _x (succ _y)) => (M c _x _x))))))
 (assert
 (check-cluster '(((M c (succ _g16942) (zero)) => (M c _g16942 (zero)))
	    ((M c _g16891 (succ _g16890)) => (M c _g16891 _g16890)))))

 (assert
 (check-cluster 
  '(((M merge-two (seq _x _s1) (seq _y _s2) _t _ur _ut _n _c)
     =>
     (M merge-two (seq _x _s1) _s2 (seq _y _t) _ur _ut _n _c))
    ((M merge-two (seq _x _s1) (seq _y _s2) _t _ur _ut _n _c)
     =>
     (M merge-two _s1 (seq _y _s2) (seq _x _t) _ur _ut _n _c)))))
)


(define (analyze-clusters ruleset)
  (cout "\nAnalyzing clusters\n")
  (identify-clusters ruleset check-cluster))

;--------------------------------------------------

(define (prove-termination ruleset)

  ; Take the ruleset and apply a set of pruners in sequence
  ; If some non-trivial pruner returns an updated ruleset, apply it again
  ; until no more transformations are possible.
  ; Return the updated ruleset

  (define reductions-simple (list prune-immed prune-simple-recursion))
  ; The following reductions can assume on a normalized ruleset
  (define reductions (list prune-immed prune-simple-recursion 
		       roll-one))

  (define (transf-step ruleset reductions)
    (let loop ((curr-reds reductions) (ruleset ruleset) (changed? #f))
      (cond
       ((null? curr-reds) 
	(if changed?		; some changes were made
	    (loop reductions ruleset #f)   ; start anew
	    ruleset))
       (((car curr-reds) ruleset) =>
	(lambda (ruleset)		; transformation was successful
	  (cout "The ruleset was reduced to:\n")
	  (pp ruleset)
	  (newline)
	  (if (null? ruleset) ruleset	; It was reduced completely
	      (loop (cdr curr-reds) ruleset #t))))
       (else
	(loop (cdr curr-reds) ruleset changed?)))))



  ; main driver
  (let loop ((step 0) (ruleset ruleset) (maxsteps (length ruleset)))
    (cout nl "===> Big reduction step " step
	  "\nruleset upon entry: ")
    (pp ruleset)
    (newline)
    (let ((ruleset (transf-step ruleset
		     (if (zero? step) reductions-simple reductions))))
      (cond
       ((null? ruleset)
	(cout "The ruleset has been proven contractive" nl nl )
	ruleset)
       ((zero? step)
	 (loop (++ step) (normalize-to-M-simple ruleset) maxsteps))
       ((>= step (min 3 maxsteps)) ; (>= step maxsteps)
        (cout "Too many steps. Can't prove the ruleset contractive" nl nl)
	ruleset)
       (else
	(let ((clustered (analyze-clusters ruleset)))
	  (if (not clustered)
	      (loop maxsteps ruleset maxsteps)
	      (loop (++ step) clustered maxsteps)))))))
)

;(run-test)
(assert (null? (prove-termination polynomial-rules)))
(assert (null? (prove-termination rule-evenp)))
(assert (null? (prove-termination rule-fact)))
(assert
  (equal? '(((M fact (succ _x)) => (M fact (succ _x))))
    (prove-termination rule-fact-bad)))
(assert (null? (prove-termination rule-evenp-noneff)))
(assert (match-tree
	  '(((M odd (seq _g808 _r)) => (M odd (seq _g808 _r))))
	  (prove-termination rule-evenp-bad)
	  '()))
(assert (null? (prove-termination rule-Ackermann)))
(assert (not (null? (prove-termination rule-complex2-mr-bad))))
(prove-termination indirect-rec)
; (prove-termination nested-calls)
; (prove-termination rule-odd-length-rec)
; (prove-termination rule-complex-mr-bad)
(prove-termination complex-descent-on-sum)
(prove-termination '(
  ((M foo (succ _x) _c) => (M foo _x _c))
  ((M foo (zero) c1) => (M foo _y c2))
))
;(exit 0)
;(prove-termination complex-descent-on-max)
;(exit 0)
; complex-descent-complex
;(time (prove-termination rule-median))
;(exit 0)

(let ((rset
	'(((M merge-median-check
     (seq _ (seq-empty))
     (seq _ (seq _g110089 _g110089))
     (succ (zero))
     _g110088
     _g110087
     _g110086)
  =>
  (M merge-median-gen _g110087 _g110088 _g110086 _g110085 _g110084))
 ((M merge-median _seq1 _seq2 _m)
  =>
  (M merge-median-check _seq1 _seq2 _m _seq1 _seq2 _m))
 ((M merge-median-check (seq _ _s1) (seq _ _s2) (succ _m1) _seq1 _seq2 _m)
  =>
  (M merge-median-check _s1 _s2 _m1 _seq1 _seq2 _m))
 ((M merge-median-check
     (seq _ (seq _g108125 _g108125))
     (seq _ (seq-empty))
     (succ (zero))
     _g108124
     _g108123
     _g108122)
  =>
  (M merge-median-gen _g108124 _g108123 _g108122 _g108121 _g108120))
 ((M merge-median-check
     (seq _ (seq _g106233 _g106233))
     (seq _ (seq _g106233 _g106233))
     (succ (zero))
     _g106232
     _g106231
     _g106230)
  =>
  (M merge-median-gen _g106232 _g106231 _g106230 _g106229 _g106228))
 ((M merge-median-gen _seq1 _seq2 _m (succ _km1) odd)
  =>
  (M merge-median _g94126 _g94127 (succ _km1)))
 ((M merge-median-gen _seq1 _seq2 _m _k even)
  =>
  (M merge-median _g94129 _g94130 _k))
 ((M merge-median (seq-empty) (seq _g110089 _g110089) (zero))
  =>
  (M merge-median-gen
     (seq _g110089 _g110089)
     (seq-empty)
     (zero)
     _g110085
     _g110084))
 ((M merge-median (seq _g108125 _g108125) (seq-empty) (zero))
  =>
  (M merge-median-gen
     (seq _g108125 _g108125)
     (seq-empty)
     (zero)
     _g108121
     _g108120))
 ((M merge-median (seq _g106233 _g106233) (seq _g106233 _g106233) (zero))
  =>
  (M merge-median-gen
     (seq _g106233 _g106233)
     (seq _g106233 _g106233)
     (zero)
     _g106229
     _g106228))
 ((M merge-median-gen _seq1 _seq2 _m (succ _km1) odd)
  =>
  (M merge-median _g94123 _g94124 _km1))
 ((M merge-median (seq _x _xr) (seq _y _yr) (succ (zero)))
  =>
  (M merge-median _yr (seq _x _xr) (zero)))
 ((M merge-median (seq _x _xr) (seq _y _yr) (succ (zero)))
  =>
  (M merge-median _xr (seq _y _yr) (zero)))
 ((M merge-median-gen _seq1 _seq2 _m _k even)
  =>
  (M merge-median _g94132 _g94133 _k)))))
 (time (prove-termination rset))
 (time (prove-termination (append rset rset)))
 (time (prove-termination (append rset rset rset)))
)
(exit 0)

(prove-termination
 '(((M merge-median-check
     (seq _ (seq-empty))
     (seq _ (seq _g110089 _g110089))
     (succ (zero))
     _g110088
     _g110087
     _g110086)
  =>
  (M merge-median-gen _g110087 _g110088 _g110086 _g110085 _g110084))
 ((M merge-median _seq1 _seq2 _m)
  =>
  (M merge-median-check _seq1 _seq2 _m _seq1 _seq2 _m))
 ((M merge-median-check (seq _ _s1) (seq _ _s2) (succ _m1) _seq1 _seq2 _m)
  =>
  (M merge-median-check _s1 _s2 _m1 _seq1 _seq2 _m))
 ((M merge-median-check
     (seq _ (seq _g108125 _g108125))
     (seq _ (seq-empty))
     (succ (zero))
     _g108124
     _g108123
     _g108122)
  =>
  (M merge-median-gen _g108124 _g108123 _g108122 _g108121 _g108120))
 ((M merge-median-check
     (seq _ (seq _g106233 _g106233))
     (seq _ (seq _g106233 _g106233))
     (succ (zero))
     _g106232
     _g106231
     _g106230)
  =>
  (M merge-median-gen _g106232 _g106231 _g106230 _g106229 _g106228))
 ((M merge-median-gen _seq1 _seq2 _m (succ _km1) odd)
  =>
  (M merge-median _g94126 _g94127 (succ _km1)))
 ((M merge-median-gen _seq1 _seq2 _m _k even)
  =>
  (M merge-median _g94129 _g94130 _k))
 ((M merge-median (seq-empty) (seq _g110089 _g110089) (zero))
  =>
  (M merge-median-gen
     (seq _g110089 _g110089)
     (seq-empty)
     (zero)
     _g110085
     _g110084))
 ((M merge-median (seq _g108125 _g108125) (seq-empty) (zero))
  =>
  (M merge-median-gen
     (seq _g108125 _g108125)
     (seq-empty)
     (zero)
     _g108121
     _g108120))
 ((M merge-median (seq _g106233 _g106233) (seq _g106233 _g106233) (zero))
  =>
  (M merge-median-gen
     (seq _g106233 _g106233)
     (seq _g106233 _g106233)
     (zero)
     _g106229
     _g106228))
 ((M merge-median-gen _seq1 _seq2 _m (succ _km1) odd)
  =>
  (M merge-median _g94123 _g94124 _km1))
 ((M merge-median (seq _x _xr) (seq _y _yr) (succ (zero)))
  =>
  (M merge-median _yr (seq _x _xr) (zero)))
 ((M merge-median (seq _x _xr) (seq _y _yr) (succ (zero)))
  =>
  (M merge-median _xr (seq _y _yr) (zero)))
 ((M merge-median-gen _seq1 _seq2 _m _k even)
  =>
  (M merge-median _g94132 _g94133 _k))))