minlog 4.0.99.20100221-6 / usr / share / doc / minlog / examples / reflection.scm

; $Id: reflection.scm 2156 2008-01-25 13:25:12Z schimans $

; 2005-08-21 Reflection

; Goal: recursively define an evaluation function for linear terms.
; Write tactic natlin to prove equations like "1+n+m+m=m+n+m+1".

; (load "~/minlog/init.scm")

(set! COMMENT-FLAG #f)
(libload "nat.scm")
(libload "list.scm")
(set! COMMENT-FLAG #t)

(add-algs (list "expr")
	  '("Zer" "expr")
	  '("Suc" "expr=>expr")
	  '("Var" "nat=>expr")
	  '("Add" "expr=>nat=>expr"))

; (pp (pt "Add(Suc(Var 1))2"))

(add-program-constant "Eval" (py "expr=>list nat=>nat") 1)

(add-var-name "ns" (py "list nat"))

(add-computation-rule (pt "Eval Zer ns") (pt "0")) 
(add-computation-rule (pt "Eval(Suc expr)ns") (pt "Succ(Eval expr ns)"))
(add-computation-rule (pt "Eval(Var n)(Nil nat)") (pt "0")) 
(add-computation-rule (pt "Eval(Var 0)(m::ns)") (pt "m"))
(add-computation-rule (pt "Eval(Var(Succ n))(m::ns)") (pt "Eval(Var n)ns"))
(add-computation-rule (pt "Eval(Add expr n)ns")
		      (pt "(Eval expr ns)+(Eval(Var n)ns)"))

; Let term be of type nat, with possible with Zero, Succ and NatPlus.
; All other parts of the term are considered unknown and put in the
; environment.

(define (term-and-env-to-linarith-expr-and-env term env)
  (if (not (equal? (py "nat") (term-to-type term)))
      (myerror "term-and-env-to-linarith-expr-and-env"
	       "term of type nat expected" term))
  (cond
   ((and (term-in-const-form? term)
	 (string=? "Zero" (const-to-name (term-in-const-form-to-const term))))
    (list (pt "Zer") env))
   ((and (term-in-app-form? term)
	 (term-in-const-form? (term-in-app-form-to-op term))
	 (string=? "Succ" (const-to-name (term-in-const-form-to-const
					  (term-in-app-form-to-op term)))))
    (let* ((prev (term-and-env-to-linarith-expr-and-env
		  (term-in-app-form-to-arg term) env))
	   (expr1 (car prev))
	   (env1 (cadr prev)))						       
      (list (make-term-in-app-form (pt "Suc") expr1) env1)))
   ((and (term-in-app-form? term)
	 (term-in-const-form? (term-in-app-form-to-final-op term))
	 (string=? "NatPlus" (const-to-name
			      (term-in-const-form-to-const
			       (term-in-app-form-to-final-op term))))
	 (= 2 (length (term-in-app-form-to-args term))))
    (let* ((args (term-in-app-form-to-args term))
	   (arg1 (car args))
	   (arg2 (cadr args))
	   (prev1 (term-and-env-to-linarith-expr-and-env arg1 env))
	   (expr1 (car prev1))
	   (env1 (cadr prev1))
	   (info (assoc-wrt term=? arg2 env1)))
      (if info
	  (list (mk-term-in-app-form
		 (pt "Add") expr1 (make-numeric-term (cadr info)))
		env1)
	  (let* ((i (length env1))
		 (add-expr
		  (mk-term-in-app-form
		   (pt "Add") expr1 (make-numeric-term i))))
	    (list add-expr (append env1 (list (list arg2 i))))))))
   (else
    (let ((info (assoc-wrt term=? term env)))
      (if info
	  (list (make-term-in-app-form
		 (pt "Var") (make-numeric-term (cadr info)))
		env)
					;else extend env
	  (let* ((i (length env))
		 (var-expr
		  (make-term-in-app-form (pt "Var") (make-numeric-term i))))
	    (list var-expr (append env (list (list term i))))))))))

(define (term-to-linarith-expr-and-env term)
  (term-and-env-to-linarith-expr-and-env term '()))

; (pp (car (term-to-linarith-expr-and-env (nt (pt "n*m+1+2*(n+n)")))))

; (define term (nt (pt "n*m+1+2*(n+n)")))
; (define expr-and-env  (term-to-linarith-expr-and-env term))
; (define expr (car expr-and-env))
; (define env (cadr expr-and-env))

(define (terms-to-list-term terms)
  (if (null? terms)
      (pt "(Nil nat)")
      (mk-term-in-app-form
       (make-term-in-const-form
	(let* ((constr (constr-name-to-constr "Cons"))
	       (tvars (const-to-tvars constr))
	       (subst (make-substitution tvars (list (py "nat")))))
	  (const-substitute constr subst #f)))
       (car terms)
       (terms-to-list-term (cdr terms)))))

; (pp (terms-to-list-term (map car env)))
; n*m::n:     

; (define list-term (terms-to-list-term (map car env)))
; (pp (nt (mk-term-in-app-form (pt "Eval") expr list-term)))
; (pp term)
; Both give Succ(n*m+n+n+n+n)

; Insertion sort for expressions

(add-program-constant "Last" (py "expr=>nat") 1)

(add-computation-rule (pt "Last Zer") (pt "0"))
(add-computation-rule (pt "Last(Suc expr)") (pt "Last expr"))
(add-computation-rule (pt "Last(Var n)") (pt "n"))
(add-computation-rule (pt "Last(Add expr n)") (pt "n"))

; (pp (nt (pt "Last(Suc(Add(Add(Add(Add(Var 0)1)1)1)1))")))

(add-program-constant "Sorted" (py "expr=>boole") 1)

(add-computation-rule (pt "Sorted Zer") (pt "True"))
(add-computation-rule (pt "Sorted(Suc expr)") (pt "Sorted expr"))
(add-computation-rule (pt "Sorted(Var n)") (pt "True"))
(add-computation-rule (pt "Sorted(Add expr n)")
		      (pt "Sorted expr and Last expr<=n"))

; (pp (nt (pt "Sorted(Suc(Add(Add(Add(Add(Var 0)1)1)1)1))")))
		      
(add-program-constant "ExprInsert" (py "expr=>nat=>expr") 1)

(add-computation-rule (pt "ExprInsert Zer m") (pt "Var m"))
(add-computation-rule (pt "ExprInsert(Suc expr)m")
		      (pt "Suc(ExprInsert expr m)"))
(add-computation-rule (pt "ExprInsert(Var n)m")
		      (pt "[if (m<=n) (Add(Var m)n) (Add(Var n)m)]"))
(add-computation-rule (pt "ExprInsert(Add expr n)m")
		      (pt "[if (m<=n)
                               (Add(ExprInsert expr m)n)
                               (Add(Add expr n)m)]"))

; (pp (nt (pt "ExprInsert(Add(Add(Var 0)3)5)2")))

; "LastExprInsert"
(set-goal
 (pf "all expr,m.Last(ExprInsert expr m)=[if (m<=Last expr) (Last expr) m]"))
(ind)
(assume "m")
(ng)
(cases (pt "m"))
(prop)
(strip)
(prop)

(assume "expr" "IH" "m")
(ng)
(use "IH")

(assume "n" "m")
(ng)
(cases (pt "m<=n"))
(prop)
(prop)

(assume "expr" "n" "IH" "m")
(ng)
(cases (pt "m<=n"))
(prop)
(prop)
(save "LastExprInsert")

; "LeLastExprInsert"
(set-goal
 (pf "all expr,m,n.Last expr<=n -> m<=n -> Last(ExprInsert expr m)<=n"))
(strip)
(simp "LastExprInsert")
(cases (pt "m<=Last expr"))
(ng)
(prop)
(ng)
(prop)
(save "LeLastExprInsert")

; "SortedExprInsert"
(set-goal (pf "all expr,n.Sorted expr -> Sorted(ExprInsert expr n)"))
(ind)
(assume "n")
(prop)
(search)
(assume "n" "m" "Triv")
(cases (pt "m<=n"))
(ng)
(assume "m<=n")
(simp "m<=n")
(ng)
(prop)
(assume "m<=n -> F")
(ng)
(simp "m<=n -> F")
(ng)
(add-global-assumption
 "SortedExprInsertAux1" (pf "all n,m.(m<=n -> F) -> n<=m"))
(use "SortedExprInsertAux1")
(use "m<=n -> F")

(assume "expr" "n" "IH" "m" "H1")
(ng)
(cases (pt "m<=n"))
(assume "m<=n")
(ng)
(split)
(use "IH")
(use-with "H1" 'left)
(use "LeLastExprInsert")
(use-with "H1" 'right)
(use "m<=n")
(assume "m<=n -> F")
(ng)
(split)
(use "H1")
(use "SortedExprInsertAux1")
(use "m<=n -> F")
(save "SortedExprInsert")

; "EvalInsert"
(set-goal
 (pf "all m,ns,expr.
      Eval(ExprInsert expr m)ns=(Eval expr ns)+(Eval(Var m)ns)"))
(assume "m" "ns")
(ind)
(auto)
(assume "n")
(ng)
(cases (pt "m<=n"))
(ng)
(assume "m<n")
(add-global-assumption "NatPlusCom" (pf "all nat1,nat2.nat1+nat2=nat2+nat1"))
(use "NatPlusCom")
(ng)
(prop)

(assume "expr" "n" "IH")
(ng)
(cases (pt "m<=n"))
(assume "m<=n")
(ng)
(simp "IH")
(add-global-assumption
 "EvalInsertAux1" (pf "all nat1,nat2,nat3.nat2+nat3=nat3+nat2 ->
                                          nat1+nat2+nat3=nat1+nat3+nat2"))
; better from nat2=nat3 -> nat1+nat2=nat1+nat3
(use "EvalInsertAux1")
(use "NatPlusCom")
(assume "m<n -> F")
(ng)
(prop)
(save "EvalInsert")

(add-program-constant "ExprInsSort" (py "expr=>expr") 1)

(add-computation-rule (pt "ExprInsSort Zer") (pt "Zer"))
(add-computation-rule (pt "ExprInsSort(Suc expr)")
		      (pt "Suc(ExprInsSort expr)"))
(add-computation-rule (pt "ExprInsSort(Var n)") (pt "Var n"))
(add-computation-rule (pt "ExprInsSort(Add expr n)")
		      (pt "ExprInsert(ExprInsSort expr) n"))

; (pp (nt (pt "ExprInsSort(Add(Add(Var 5)0)2)")))

; "EvalSort"
(set-goal (pf "all ns,expr Eval(ExprInsSort expr)ns=Eval expr ns"))
(assume "ns")
(ind)
(use "Truth-Axiom")

(assume "expr" "IH")
(use "IH")

(assume "n")
(use "Truth-Axiom")

(assume "expr" "n" "IH")
(ng)
(simp "EvalInsert")
(simp "IH")
(prop)
(save "EvalSort")

; Now for the proof generation

; "NatEqSym"
(set-goal (pf "all nat1,nat2.nat1=nat2 -> nat2=nat1"))
(ind)
(cases)
(prop)
(strip)
(prop)
(assume "nat1" "IH")
(cases)
(prop)
(use "IH")
(save "NatEqSym")


; "NatEqTrans"
(set-goal (pf "all nat1,nat2,nat3.nat1=nat2 -> nat2 =nat3 -> nat1=nat3"))
(ind)
(cases)
(strip)
(prop)
(strip)
(prop)
(assume "nat1" "IH1")
(cases)
(strip)
(prop)
(assume "nat2")
(cases)
(prop)
(use "IH1")
(save "NatEqTrans")

(define (natlin-intern num-goals proof maxgoal)
  (let* ((num-goal (car num-goals))
	 (goal (num-goal-to-goal num-goal))
	 (goal-formula (goal-to-formula goal)))
    (if (not (and (atom-form? goal-formula)
		  (let* ((kernel (atom-form-to-kernel goal-formula))
			 (op (term-in-app-form-to-final-op kernel))
			 (args (term-in-app-form-to-args kernel)))
		    (and (term-in-const-form? op)
			 (equal? (py "nat=>nat=>boole") (term-to-type op))
			 (string=? "=" (const-to-name
					(term-in-const-form-to-const op)))))))
	(myerror "natlin-intern" "equality between nat-terms expected"))
    (let* ((kernel (atom-form-to-kernel goal-formula))
	   (args (term-in-app-form-to-args kernel))
	   (arg1 (car args))
	   (arg2 (cadr args))
	   (r1 (nt arg1))
	   (r2 (nt arg2))
	   (e1-and-env1 (term-to-linarith-expr-and-env r1))
	   (e1 (car e1-and-env1))
	   (env1 (cadr e1-and-env1))
	   (e2-and-env2 (term-and-env-to-linarith-expr-and-env r2 env1))
	   (e2 (car e2-and-env2))
	   (env2 (cadr e2-and-env2))
	   (terms (map car env2))
	   (ns (terms-to-list-term terms))
	   (se1 (nt (make-term-in-app-form (pt "ExprInsSort") e1)))
	   (se2 (nt (make-term-in-app-form (pt "ExprInsSort") e2))))
      (if (not (term=? se1 se2))
	  (myerror "natlin-intern" "unprovable equality"))
      (let* ((ve1 (nt (mk-term-in-app-form (pt "Eval") e1 ns)))
	     (ve2 (nt (mk-term-in-app-form (pt "Eval") e2 ns)))
	     (vse1 (nt (mk-term-in-app-form (pt "Eval") se1 ns)))
	     (vse2 (nt (mk-term-in-app-form (pt "Eval") se2 ns)))
	     (new-proof
	      (mk-proof-in-elim-form
	       (make-proof-in-aconst-form
		(theorem-name-to-aconst "NatEqTrans"))
	       ve1 vse1 ve2
	       (mk-proof-in-elim-form
		(make-proof-in-aconst-form
		 (theorem-name-to-aconst "NatEqSym"))
		vse1 ve1 (mk-proof-in-elim-form
			  (make-proof-in-aconst-form
			   (theorem-name-to-aconst "EvalSort")) ns e1))
	       (mk-proof-in-elim-form
		(make-proof-in-aconst-form
		 (theorem-name-to-aconst "EvalSort")) ns e2))))
	(make-pproof-state
	 (cdr num-goals)
	 (goal-subst proof goal new-proof)
	 maxgoal)))))

(define (natlin)
  (let* ((num-goals (pproof-state-to-num-goals))
	 (proof (pproof-state-to-proof))
	 (maxgoal (pproof-state-to-maxgoal))
	 (number (num-goal-to-number (car num-goals))))
    (set! PPROOF-STATE (natlin-intern num-goals proof maxgoal))
    (pproof-state-history-push PPROOF-STATE)
    (if
     COMMENT-FLAG
     (begin (display-comment "ok, " DEFAULT-GOAL-NAME "_"
			     (number-to-string number) " is proved.")
	    (if (null? (pproof-state-to-num-goals))
		(begin (display "  Proof finished.") (newline))
		(begin (display "  The active goal now is") (newline)
		       (display-num-goal
			(car (pproof-state-to-num-goals)))))))))

(set-goal (pf "1+n+m+m=m+n+m+1"))
(strip)
(natlin)

(dpe)

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Outdated stuff:
(add-algs (list "expr")
	  '("Var" "nat=>expr")
	  '("Num" "nat=>expr")
	  '("Mul" "nat=>expr=>expr")
	  '("Add" "expr=>expr=>expr"))

(pp (pt "Add(Var 1)(Mul 7(Var 2))"))

(add-program-constant "Eval" (py "expr=>list nat=>nat") 1)

(add-var-name "ns" (py "list nat"))

(add-computation-rule (pt "Eval(Var n)(Nil nat)") (pt "0")) 
(add-computation-rule (pt "Eval(Var 0)(m::ns)") (pt "m"))
(add-computation-rule (pt "Eval(Var(Succ n))(m::ns)") (pt "Eval(Var n)ns"))
(add-computation-rule (pt "Eval(Num n)ns") (pt "n"))
(add-computation-rule (pt "Eval(Mul n expr)ns") (pt "n*Eval expr ns"))
(add-computation-rule (pt "Eval(Add expr1 expr2)ns")
		      (pt "(Eval expr1 ns)+(Eval expr2 ns)"))

(define (term-and-env-to-linarith-expr-and-env term env)
  (if (not (equal? (py "nat") (term-to-type term)))
      (myerror "term-and-env-to-linarith-expr-and-env"
	       "term of type nat expected" term))
  (cond
   ((is-numeric-term? term)
    (list (make-term-in-app-form (pt "Num") term) env))
   ((and (term-in-app-form? term)
	 (term-in-const-form? (term-in-app-form-to-final-op term))
	 (= 2 (length (term-in-app-form-to-args term)))
	 (let* ((args (term-in-app-form-to-args term))
		(arg1 (car args))
		(name (const-to-name (term-in-const-form-to-const
				      (term-in-app-form-to-final-op term)))))
	   (or (string=? name "NatPlus")
	       (and (string=? name "NatTimes") (is-numeric-term? arg1)))))
    (let* ((op (term-in-app-form-to-final-op term))
	   (args (term-in-app-form-to-args term))
	   (arg1 (car args))
	   (arg2 (cadr args))
	   (name (const-to-name (term-in-const-form-to-const op))))
      (if
       (string=? "NatTimes" name)
       (let* ((prev2 (term-and-env-to-linarith-expr-and-env arg2 env))
	      (expr2 (car prev2))
	      (env1 (cadr prev2)))
	 (list (apply mk-term-in-app-form (list (pt "Mul") arg1 expr2))
	       env1))
       (let* ((prev1 (term-and-env-to-linarith-expr-and-env arg1 env))
	      (expr1 (car prev1))
	      (env1 (cadr prev1))
	      (prev2 (term-and-env-to-linarith-expr-and-env arg2 env1))
	      (expr2 (car prev2))
	      (env2 (cadr prev2)))
	 (list (apply mk-term-in-app-form (list (pt "Add") expr1 expr2))
	       env2)))))
   (else
    (let* ((info (assoc-wrt term=? term env)))
      (if
       info
       (list (make-term-in-app-form
	      (pt "Var") (make-numeric-term (cadr info)))
	     env)
					;else extend env
       (let* ((i (length env))
	      (var-expr
	       (make-term-in-app-form (pt "Var") (make-numeric-term i))))
	 (list var-expr (append env (list (list term i))))))))))

(define (term-to-linarith-expr-and-env term)
  (term-and-env-to-linarith-expr-and-env term '()))

(pp (car (term-to-linarith-expr-and-env (pt "n*m+5+3*(n+n)"))))

(define term (pt "n*m+5+3*(n+n)"))
(define expr-and-env  (term-to-linarith-expr-and-env (pt "n*m+5+3*(n+n)")))
(define expr (car expr-and-env))
(define env (cadr expr-and-env))

(define (terms-to-list-term terms)
  (if (null? terms)
      (pt "(Nil nat)")
      (mk-term-in-app-form
       (make-term-in-const-form
	(let* ((constr (constr-name-to-constr "Cons"))
	       (tvars (const-to-tvars constr))
	       (subst (make-substitution tvars (list (py "nat")))))
	  (const-substitute constr subst #f)))
       (car terms)
       (terms-to-list-term (cdr terms)))))

(pp (terms-to-list-term (map car env)))       

(pp (nt (apply mk-term-in-app-form
	       (list (pt "Eval") expr (terms-to-list-term (map car env))))))
(pp (nt (pt "n*m+5+3*(n+n)")))

; Changed: (1) environments are taken as lists of naturals (not
; functions) (2) To define term-to-linarith-expr-and-env we employ an
; auxiliary function term-to-linarith-expr-and-env-aux

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(define (term-to-linarith-expr term)
  (if (not (equal? (py "nat") (term-to-type term)))
      (myerror "term-to-linarith-expr" "term of type nat expected" term))
  (cond
   ((is-numeric-term? term)
    (make-term-in-app-form (pt "Num") term))
   ((and (term-in-app-form? term)
	 (term-in-const-form? (term-in-app-form-to-final-op term))
	 (= 2 (length (term-in-app-form-to-args term)))
	 (let* ((args (term-in-app-form-to-args term))
		(arg1 (car args))
		(name (const-to-name (term-in-const-form-to-const
				      (term-in-app-form-to-final-op term)))))
	   (or (string=? name "NatPlus")
	       (and (string=? name "NatTimes") (is-numeric-term? arg1)))))
    (let* ((args (term-in-app-form-to-args term))
	   (name (const-to-name (term-in-const-form-to-const
				 (term-in-app-form-to-final-op term)))))
      (if (string=? name "NatPlus")
	  (apply mk-term-in-app-form		  
		  (list (pt "Add")
			(term-to-linarith-expr (car args))
			(term-to-linarith-expr (cadr args))))
	  (apply mk-term-in-app-form		  
		 (list (pt "Mul")
		       (car args)
		       (term-to-linarith-expr (cadr args)))))))
   (else
    (let* ((count ...))))))

; To do: add environment to the result.  Update it if an unknown term
; is encountered.  Carry along counter for the newly introduced free
; variables is the term

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

; Working version, but still problem with the environment

(define (term-to-linarith-expr term)
  (if (not (equal? (py "nat") (term-to-type term)))
      (myerror "term-to-linarith-expr" "term of type nat expected" term))
  (if
   (is-numeric-term? term)
   (make-term-in-app-form (pt "Num") term)
   (case (tag term)
     ((term-in-var-form)
      (let* ((var (term-in-var-form-to-var term))
	     (index (var-to-index var))
	     (i (+ 1 index))) ;to make up for the index -1
	(if (string=? "n" (var-to-name var))
	    (make-term-in-app-form (pt "Var") (make-numeric-term i))
	    (myerror "term-to-linarith-expr"
		     "n is the only variable name allowed"
		     (var-to-name var)))))
     ((term-in-const-form)     
      (myerror "term-to-linarith-expr" "numeric term expected" term))
     ((term-in-app-form)
      (if
       (term-in-const-form? (term-in-app-form-to-final-op term))
       (let* ((op (term-in-app-form-to-final-op term))
	      (args (term-in-app-form-to-args term))
	      (const (term-in-const-form-to-const op))
	      (name (const-to-name const)))
	 (cond
	  ((not (= 2 (length args)))
	   (myerror "term-to-linarith-expr" "two arguments expected" term))
	  ((and (member name (list "NatTimes"))
		(is-numeric-term? (car args)))
	   (apply mk-term-in-app-form		  
		  (list (pt "Mul")
			(car args)
			(term-to-linarith-expr (cadr args)))))
	  ((member name (list "NatPlus"))
	   (apply mk-term-in-app-form		  
		  (list (pt "Add")
			(term-to-linarith-expr (car args))
			(term-to-linarith-expr (cadr args)))))
	  (else
	   (myerror "term-to-linarith-expr" "unexpected argument" term))))
       (myerror "term-to-linarith-expr" "unexpected argument" term)))
     (else (myerror "term-to-linarith-expr" "unexpected argument" term)))))

(pp (term-to-linarith-expr (pt "n0")))
(pp (term-to-linarith-expr (pt "3*n1")))
(pp (term-to-linarith-expr (pt "n0+n1")))
(pp (term-to-linarith-expr (pt "7*(n0+n1)+n3")))





;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

; Previous try: exprM and exprA

(add-algs (list "exprM" "exprA")
	  '("Var" "nat=>exprM")
	  '("Num" "nat=>exprM")
	  '("Mul" "nat=>exprM=>exprM")
	  '("InM" "exprA=>exprM")
	  '("InA" "exprM=>exprA")
	  '("Add" "exprM=>exprA=>exprA"))

(pp (pt "Add(Var 1)(InA(Mul 7(Var 2)))"))

(add-program-constant "EvalM" (py "exprM=>(nat=>nat)=>nat") 1)
(add-program-constant "EvalA" (py "exprA=>(nat=>nat)=>nat") 1)

(add-var-name "M" (py "exprM"))
(add-var-name "A" (py "exprA"))
(add-var-name "env" (py "nat=>nat"))

(add-computation-rule (pt "EvalM(Var n)env") (pt "env n"))
(add-computation-rule (pt "EvalM(Num n)env") (pt "n"))
(add-computation-rule (pt "EvalM(Mul n M)env") (pt "n*EvalM M env"))
(add-computation-rule (pt "EvalM(InM A)env") (pt "EvalA A env"))
(add-computation-rule (pt "EvalA(InA M)env") (pt "EvalM M env"))
(add-computation-rule (pt "EvalA(Add M A)env")
		      (pt "(EvalM M env)+(EvalA A env)"))

(pp (nt (pt "EvalA(Add(Var 1)(InA(Mul 7(Var 2))))([n]n)")))
(pp (nt (pt "EvalA(Add(Var 1)(InA(Mul 7(Var 2))))([n]n*n)")))
(pp (nt (pt "EvalA(Add(Var 1)(InA(Mul 7(Var 2))))env")))

(define (term-to-exprM term)
  (if (not (equal? (py "nat") (term-to-type term)))
      (myerror "term-to-exprM" "term of type nat expected" term))
  (if
   (is-numeric-term? term)
   (make-term-in-app-form (pt "Num") term)
   (case (tag term)
     ((term-in-var-form)
      (let* ((var (term-in-var-form-to-var term))
	     (index (var-to-index var))
	     (i (+ 1 index))) ;to make up for the index -1
	(make-term-in-app-form (pt "Var") (make-numeric-term i))))
     ((term-in-const-form)     
      (myerror "term-to-exprM" "numeric term expected" term))
     ((term-in-const-form? (term-in-app-form-to-final-op term))
       (let* ((op (term-in-app-form-to-final-op term))
	      (args (term-in-app-form-to-args term))
	      (const (term-in-const-form-to-const op))
	      (name (const-to-name const))
	      (l (length args))
	      (prev1 (term-to-expr (car args)))
	      (prev2 (if (< 1 l) (term-to-expr (cadr args)) 0)))
	 (cond
	  ((and (member name (list "RatPlus" "IntPlus" "PosPlus" "NatPlus"))
		(= l 2))
	   (list '+ prev1 prev2))
	  (else
	   (myerror "term-to-exprM" "unexpected argument" term)))))
     (else (myerror "term-to-exprM" "unexpected argument" term)))))

(pp (term-to-exprM (pt "n7")))