minlog 4.0.99.20100221-5.2 / usr / share / minlog / src / psym.scm

; $Id: psym.scm 2359 2009-12-10 17:12:32Z schwicht $
; 5. Predicates
; =============

; To be renamed into pred.scm

; A predicate is
; - a predicate variable
; - a predicate constant
; - an inductively defined predicate constant
; Generalities for all kinds of predicates:

(define (predicate-to-arity predicate)
  (cond ((pvar-form? predicate) (pvar-to-arity predicate))
	((predconst-form? predicate) (predconst-to-arity predicate))
	((idpredconst-form? predicate) (idpredconst-to-arity predicate))
	(else (myerror "predicate-to-arity"  "predicate expected" predicate))))

; Totality matters for the abstracted variables of a cterm, because of
; the inductively defined existential quantifier.  The default is the
; use of partial variables.

(define (predicate-to-cterm predicate)
  (let* ((arity (predicate-to-arity predicate))
	 (types (arity-to-types arity))
	 (vars (map type-to-new-partial-var types))
	 (varterms (map make-term-in-var-form vars))
	 (formula (apply make-predicate-formula (cons predicate varterms))))
      (apply make-cterm (append vars (list formula)))))

(define (predicate-to-cterm-with-total-vars predicate)
  (let* ((arity (predicate-to-arity predicate))
	 (types (arity-to-types arity))
	 (vars (map type-to-new-var types))
	 (varterms (map make-term-in-var-form vars))
	 (formula (apply make-predicate-formula (cons predicate varterms))))
      (apply make-cterm (append vars (list formula)))))

(define (predicate-to-tvars pred)
  (cond ((pvar-form? pred)
	 (let* ((arity (pvar-to-arity pred))
		(types (arity-to-types arity)))
	   (apply union (map type-to-free types))))
	((predconst-form? pred)
	 (let* ((arity (predconst-to-arity pred))
		(types (arity-to-types arity)))
	   (apply union (map type-to-free types))))
	((idpredconst-form? pred)
	 (let* ((types (idpredconst-to-types pred))
		(cterms (idpredconst-to-cterms pred))
		(formulas (map cterm-to-formula cterms)))
	   (apply union (append (map type-to-free types)
				(map formula-to-tvars formulas)))))
	(else (myerror "predicate-to-tvars" "predicate expected" pred))))

(define (predicate-equal? pred1 pred2)
  (cond
   ((pvar-form? pred1)
    (and (pvar-form? pred2) (equal? pred1 pred2)))
   ((predconst-form? pred1)
    (and (predconst-form? pred2)
	 (let ((name1 (predconst-to-name pred1))
	       (arity1 (predconst-to-arity pred1))
	       (index1 (predconst-to-index pred1))
	       (name2 (predconst-to-name pred2))
	       (arity2 (predconst-to-arity pred2))
	       (index2 (predconst-to-index pred2)))
	   (and (string=? name1 name2)
		(equal? arity1 arity2)
		(= index1 index2)))))
;     (and (predconst-form? pred2) (equal? pred1 pred2)))
   ((idpredconst-form? pred1)
    (and (idpredconst-form? pred2)
	 (let ((name1 (idpredconst-to-name pred1))
	       (types1 (idpredconst-to-types pred1))
	       (cterms1 (idpredconst-to-cterms pred1))
	       (name2 (idpredconst-to-name pred2))
	       (types2 (idpredconst-to-types pred2))
	       (cterms2 (idpredconst-to-cterms pred2)))
	   (and (string=? name1 name2)
		(equal? types1 types2)
		(= (length cterms1) (length cterms2))
		(apply and-op (map (lambda (x y) (cterm=? x y))
				   cterms1 cterms2))))))
   (else (myerror "predicate-equal?" "predicate expected" pred1))))	   


; 5-1. Predicate variables
; ========================

; A predicate variable of arity rho_1,..., rho_n is viewed as a
; placeholder for a formula with distinguished (different) variables
; x_1,..., x_n of types rho_1,..., rho_n (a so called comprehension
; term).  

(define (make-arity . x) (cons 'arity x))

(define (arity-to-types arity) (cdr arity))

(define (arity-to-string arity)
  (if (and (list? arity)
           (< 0 (length arity))
           (eq? 'arity (car arity)))
      (let* ((types (arity-to-types arity))
             (strings (map type-to-string types))
             (strings-with-leading-spaces
              (map (lambda (s) (string-append " " s)) strings)))
        (apply string-append
               (append (list "(arity")
                       strings-with-leading-spaces
		       (list ")"))))
      (myerror "arity-to-string" "arity expected" arity)))

(define (d-arity arity)
  (if COMMENT-FLAG (display (arity-to-string arity))))

; Complete test

(define (arity? x)
  (and (list? x)
       (< 0 (length x))
       (eq? 'arity (car x))
       (apply and-op (map type? (arity-to-types x)))))  

(define (arity-to-alg-names arity)
  (apply union (map type-to-alg-names (arity-to-types arity))))

; Predicate variable names are provided in the form of an association
; list, which assigns to the names their arities.  By default we have
; the predicate variable bot of arity (arity), called (logical) falsity.

; For the convenient display of predicate variables, we may provide
; default variable names for certain arities.

(define DEFAULT-PVAR-NAMES '())
(define INITIAL-DEFAULT-PVAR-NAMES DEFAULT-PVAR-NAMES)

(define (default-pvar-name arity)
  (let ((info (assoc arity DEFAULT-PVAR-NAMES)))
    (if info (cadr info) "")))

(define (set-default-pvar-name arity string)
  (set! DEFAULT-PVAR-NAMES (cons (list arity string) DEFAULT-PVAR-NAMES)))

(define PVAR-NAMES (list (list "bot" (make-arity))))
(define INITIAL-PVAR-NAMES PVAR-NAMES)

(define (add-pvar-name . x)
  (if (null? x)
      (myerror "add-pvar-name" "arguments expected")
      (let* ((rev (reverse x))
	     (arity (car rev))
	     (strings (reverse (cdr rev))))
	(if (not (arity? arity))
	    (myerror "add-pvar-name" "arity expected" arity))
	(for-each
	 (lambda (string)
	   (if (and (string? string) (not (string=? string "")))
	       (if (is-used? string arity 'pvar)
		   *the-non-printing-object*
		   (begin
		     (set! PVAR-NAMES
			   (append PVAR-NAMES (list (list string arity))))
		     (add-token string 'pvar-name (cons arity string))
		     (if (string=? "" (default-pvar-name arity))
			 (set-default-pvar-name arity string))
		     (comment
		      "ok, predicate variable " string ": "
		      (arity-to-string arity) " added")))
	       (myerror "add-pvar-name" "string expected" string)))
	 strings))))

(define apv add-pvar-name)

(define (remove-pvar-name . strings)
  (define (rpv1 string)
    (let ((info (assoc string PVAR-NAMES)))
      (if info
	  (let* ((arity (cadr info))
		 (info1 (assoc arity DEFAULT-PVAR-NAMES)))
	    (do ((l PVAR-NAMES (cdr l))
		 (res '() (if (string=? (caar l) string)
			      res
			      (cons (car l) res))))
		((null? l) (set! PVAR-NAMES (reverse res))))
	    (do ((l DEFAULT-PVAR-NAMES (cdr l)) ;added 01-05-24
		 (res '() (if (string=? (cadar l) string)
			      res
			      (cons (car l) res))))
		((null? l) (set! DEFAULT-PVAR-NAMES (reverse res))))
	    (remove-token string)
	    (comment "ok, predicate variable " string " is removed")
	    (if (and info1 (string=? (cadr info1) string))
		(comment
		 "warning: " string " was default pvariable of arity "
		 (arity-to-string arity))))
	  (myerror "remove-pvar-name" "predicate variable name expected"
		   string))))
  (for-each rpv1 strings))

(define rpv remove-pvar-name)

; Predicate variables are implemented as lists ('pvar arity index
; h-deg n-deg name).  If a predicate variable carries no index, we let
; the index be -1.  name is a string (the name of the predicate
; variable), to be used for output.

; To make sure that predicate variables generated by the system are
; different from all user introduced predicate variables, we maintain a
; global counter MAXPVARINDEX.  Whenever the user introduces a
; predicate variable, e.g. p^27, then MAXPVARINDEX is incremented to
; at least 27.

(define MAXPVARINDEX -1)
(define INITIAL-MAXPVARINDEX MAXPVARINDEX)

; Degrees of positivity (Harrop-degree) and negativity.

; Every predicate variable carries a pair h-deg, n-deg.  This
; restricts the admitted comprehension term {x|A} as follows.
; h-deg  n-deg   tau^+(A)    tau^-(A) 
;   0      0     arbitrary   arbitrary 
;   1      0     nulltype    arbitrary 
;   0      1     arbitrary   nulltype
;   1      1     nulltype    nulltype

(define h-deg-zero 0)
(define h-deg-one 1)

(define (h-deg-zero? h-deg)
  (and (integer? h-deg) (zero? h-deg)))

(define (h-deg-one? h-deg)
  (and (integer? h-deg) (positive? h-deg)))

(define (h-deg? x)
  (and (integer? x) (not (negative? x))))

(define n-deg-zero 0)
(define n-deg-one 1)

(define (n-deg-zero? n-deg)
  (and (integer? n-deg) (zero? n-deg)))

(define (n-deg-one? n-deg)
  (and (integer? n-deg) (positive? n-deg)))

(define (n-deg? x)
  (and (integer? x) (not (negative? x))))

; Constructor, accessors and tests for predicate variables:

(define (make-pvar arity index h-deg n-deg name)
  (set! MAXPVARINDEX (max index MAXPVARINDEX))
  (list 'pvar arity index h-deg n-deg name))

(define (pvar-form? x) (and (pair? x) (eq? 'pvar (car x))))

(define pvar-to-arity cadr)
(define pvar-to-index caddr)
(define pvar-to-h-deg cadddr)
(define (pvar-to-n-deg pvar) (car (cddddr pvar)))
(define (pvar-to-name pvar) (cadr (cddddr pvar)))

; Complete test:

(define (pvar? x)
  (and (list? x)
       (= 6 (length x))
       (let ((tag (car x))
	     (arity (cadr x))
	     (index (caddr x))
	     (h-deg (cadddr x))
	     (n-deg (car (cddddr x)))
	     (name (cadr (cddddr x))))
	 (and (eq? 'pvar tag)
	      (arity? arity)
	      (integer? index) (<= -1 index)
	      (h-deg? h-deg)
	      (n-deg? n-deg)
	      (or (string=? "" name)
		  (assoc name PVAR-NAMES))))))

; For convenience we add mk-pvar with options.  Options are index
; (default -1), h-deg (default h-deg-zero), n-deg (default
; n-deg-zero), and name (default given by (default-pvar-name arity)).

(define (mk-pvar arity . options)
  (let ((index -1)
	(h-deg h-deg-zero)
	(n-deg n-deg-zero)
	(name (default-pvar-name arity)))
    (if (pair? options)
	(begin (set! index (car options))
	       (set! options (cdr options))))
    (if (pair? options)
	(begin (set! h-deg (car options))
	       (set! options (cdr options))))
    (if (pair? options)
	(begin (set! n-deg (car options))
	       (set! options (cdr options))))
    (if (pair? options)
	(begin (set! name (car options))
	       (set! options (cdr options))))
    (if (pair? options)
	 (myerror "make-pvar" "unexpected argument" options))
  (cond ((not (and (integer? index) (<= -1 index)))
	 (myerror "make-pvar" "index >= -1 expected" index))
	((not (h-deg? h-deg))
	 (myerror "make-pvar" "h-deg expected" h-deg))
	((not (n-deg? n-deg))
	 (myerror "make-pvar" "n-deg expected" n-deg))
	((not (string? name))
	 (myerror "make-pvar" "string expected" name))
	(else (make-pvar arity index h-deg n-deg name)))))

(define (pvar-with-positive-content? pvar)
  (h-deg-zero? (pvar-to-h-deg pvar)))

(define (pvar-with-negative-content? pvar)
  (n-deg-zero? (pvar-to-n-deg pvar)))

; For display purposes we use

(define (pvar-to-string pvar)
  (let* ((arity (pvar-to-arity pvar))
	 (types (arity-to-types arity))
	 (index (pvar-to-index pvar))
	 (h-deg (pvar-to-h-deg pvar))
	 (n-deg (pvar-to-n-deg pvar))
	 (name (pvar-to-name pvar))
	 (default-pvar-name-with-type-args?
	   (and (string=? "" name) (pair? types)))
	 (proper-name
	  (if (string=? "" name)
	      (let* ((strings (map type-to-string types))
		     (strings-with-leading-spaces
		      (map (lambda (x) (string-append " " x)) strings)))
		(if (null? types)
		    "Pvar"
		    (apply string-append (append (list "(Pvar")
						 strings-with-leading-spaces
						 (list ")")))))
	      name))
	 (modifier
	  (if (h-deg-zero? h-deg)
	      (if (n-deg-zero? n-deg)
		  (if (and (not (= index -1))
			   default-pvar-name-with-type-args?) "_" "") "'")
	      (if (n-deg-zero? n-deg) "^" "^'")))
	 (index-string (if (= index -1) "" (number-to-string index))))
    (string-append proper-name modifier index-string)))

(define (pvar-name? string) (assoc string PVAR-NAMES))

(define (pvar-name-to-arity string)
  (let ((info (assoc string PVAR-NAMES)))
    (if info
	(cadr info)
	(myerror "pvar-name-to-arity" "pvar-name expected"
		 string))))

; For automatic generation of predicate variables we need

(define (numerated-pvar? pvar)
  (and (string=? "" (pvar-to-name pvar))
       (<= 0 (pvar-to-index pvar))))

(define (numerated-pvar-to-index x) (pvar-to-index x))

(define (arity-to-new-pvar arity . rest)
  (if (null? rest)
      (make-pvar arity (+ 1 MAXPVARINDEX) h-deg-one n-deg-one
		 (default-pvar-name arity))
      (make-pvar arity (+ 1 MAXPVARINDEX) 
		 (pvar-to-h-deg (car rest)) (pvar-to-n-deg (car rest))
		 (default-pvar-name arity))))
		
(define (arity-to-new-non-harrop-pvar arity)
  (make-pvar arity (+ 1 MAXPVARINDEX) h-deg-zero n-deg-one
	     (default-pvar-name arity)))

(define (arity-to-new-general-pvar arity)
  (make-pvar arity (+ 1 MAXPVARINDEX) h-deg-zero n-deg-zero
	     (default-pvar-name arity)))

; Occasionally we may want to create a new pvariable with the same name
; (and degree of totality) as a given one.  This is useful e.g. for
; bound renaming.  Therefore we supply

(define (pvar-to-new-pvar pvar)
  (make-pvar
   (pvar-to-arity pvar)
   (+ 1 MAXPVARINDEX)
   (pvar-to-h-deg pvar)
   (pvar-to-n-deg pvar)
   (pvar-to-name pvar)))

(define (compose-p-substitutions psubst1 psubst2)
  (compose-substitutions-wrt
   cterm-substitute equal? pvar-cterm-equal? psubst1 psubst2))


; 5-2. Predicate constants
; ========================

; General reasons for having predicate constants:
; - We need Equal, Total and STotal, which are *not* placeholders for formulas
; - We need predicates to be axiomatized

; General properties of predconsts:
; - They have no computational content.
; - They do not change their name when a tsubst is employed.  Hence from
;   a name one can only read off the uninstantiated type.
; - Their meaning can be fixed by axioms (e.g. for Equal, E and also for
;   Bar(.,.) of arity ('arity tree seq))

; Predicate constant names are provided in the form of an association
; list, which assigns to the names their arities.  By default we have
; the predicate constants Equal of arity (arity alpha alpha) and
; Total, STotal both of arity (arity alpha).

(define PREDCONST-NAMES
  (list
   (list "Equal" (make-arity (make-tvar -1 DEFAULT-TVAR-NAME)
			     (make-tvar -1 DEFAULT-TVAR-NAME)))
   (list "Total" (make-arity (make-tvar -1 DEFAULT-TVAR-NAME)))
   (list "STotal" (make-arity (make-tvar -1 DEFAULT-TVAR-NAME)))))

(define INITIAL-PREDCONST-NAMES PREDCONST-NAMES)

(define (add-predconst-name . x)
  (if (null? x)
      (myerror "add-predconst-name" "arguments expected")
      (let* ((rev (reverse x))
	     (arity (car rev))
	     (strings (reverse (cdr rev))))
	(if (not (arity? arity))
	    (myerror "add-predconst-name" "arity expected" arity))
	(for-each
	 (lambda (string)
	   (if (and (string? string) (not (string=? string "")))
	       (if (is-used? string arity 'predconst)
		   *the-non-printing-object*
		   (begin
		     (set! PREDCONST-NAMES
			   (append PREDCONST-NAMES (list (list string arity))))
		     (add-token
		      string
		      'predconst-name
		      (string-and-arity-to-predconst-parse-function
		       string arity))
		     (comment
		      "ok, predicate constant " string ": "
		      (arity-to-string arity) " added")))
	       (myerror "add-predconst-name" "string expected" string)))
	 strings))))

(define (string-and-arity-and-cterms-to-idpc-parse-function name arity cterms)
  (lambda args
    (let* ((uninst-types (arity-to-types arity))
	   (arg-types
	    (if (= (length uninst-types) (length args))
		(map term-to-type args)
		(apply
		 myerror
		 (append
		  (list "string-and-arity-and-cterms-to-idpc-parse-function"
			"arguments and arity of different lengths"
			name arity)
		  args))))
	   (uninst-type (apply mk-arrow (append uninst-types
						(list (make-alg "boole")))))
	   (type (apply mk-arrow (append arg-types
					 (list (make-alg "boole")))))
	   (tsubst (type-match-modulo-coercion uninst-type type))
	   (tvars (idpredconst-name-to-tvars name)))
      (if tsubst
	  (let ((subst-types
		 (map (lambda (tvar) (let ((info (assoc tvar tsubst)))
				       (if info (cadr info) tvar)))
		      tvars)))
	    (apply make-predicate-formula
		   (cons (make-idpredconst name subst-types cterms) args)))
	  (apply
	   myerror
	   (append
	    (list "string-and-arity-and-cterms-to-idpc-parse-function"
		  "types do not fit for inductively defined predicate constant"
		  name)
	    uninst-types arg-types))))))

(define (string-and-arity-to-predconst-parse-function string arity)
  (lambda (index . args)
    (let* ((uninst-types (arity-to-types arity))
	   (types (map term-to-type args))
	   (uninst-type
	    (apply mk-arrow (append uninst-types (list (make-alg "boole")))))
	   (type (apply mk-arrow (append types (list (make-alg "boole")))))
	   (tsubst (if (= (length uninst-types) (length types))
		       (type-match uninst-type type)
		       #f)))
      (if tsubst
	  (apply
	   make-predicate-formula
	   (cons (make-predconst arity tsubst index string)
		 args))
	  (apply myerror (cons "types do not fit"
			       (cons string
				     (append uninst-types types))))))))

(define apredc add-predconst-name) 

(define (remove-predconst-name . strings)
  (define (rpredc1 string)
    (let ((info (assoc string PREDCONST-NAMES)))
      (if info
	  (begin
	    (do ((l PREDCONST-NAMES (cdr l))
		 (res '() (if (string=? (caar l) string)
			      res
			      (cons (car l) res))))
		((null? l) (set! PREDCONST-NAMES (reverse res))))
	    (remove-token string)
	    (comment "ok, predicate constant " string " is removed"))
	  (myerror "remove-predconst-name" "predicate constant name expected"
		   string))))
  (for-each rpredc1 strings))

(define rpredc remove-predconst-name) 

; Predicate constants are implemented as lists 
; ('predconst uninst-arity tsubst index name).  

; Constructor, accessors and tests for predicate constants:

(define (make-predconst uninst-arity tsubst index name)
  (list 'predconst uninst-arity tsubst index name))

(define (predconst-form? x) (and (pair? x) (eq? 'predconst (car x))))

(define predconst-to-uninst-arity cadr)
(define predconst-to-tsubst caddr)
(define predconst-to-index cadddr)
(define (predconst-to-name predconst) (car (cddddr predconst)))

(define (predconst-to-arity predconst)
  (let* ((uninst-arity (predconst-to-uninst-arity predconst))
	 (tsubst (predconst-to-tsubst predconst))
	 (uninst-types (arity-to-types uninst-arity))
	 (types (map (lambda (x) (type-substitute x tsubst)) uninst-types)))
    (apply make-arity types)))

; (Almost) complete test:

(define (predconst? x)
  (and (list? x)
       (= 5 (length x))
       (let ((tagsymbol (car x))
	     (uninst-arity (cadr x))
	     (tsubst (caddr x))
	     (index (cadddr x))
	     (name (car (cddddr x))))
	 (and (eq? 'predconst tagsymbol)
	      (arity? uninst-arity)
	      (integer? index) (<= -1 index)
	      (tsubst? tsubst)
	      (or (string=? "" name)
		  (assoc name PREDCONST-NAMES))))))

(define (predconst-name? string) (assoc string PREDCONST-NAMES))

(define (predconst-name-to-arity predconst-name)
  (let ((info (assoc string PREDCONST-NAMES)))
    (if info
	(cadr info)
	(myerror "predconst-name-to-arity" "predconst-name expected"
		 predconst-name))))

; To allow for a convenient display, we maintain a global variable
; PREDCONST-DISPLAY consisting of entries (name token-type display-string)

(define PREDCONST-DISPLAY '())
(define INITIAL-PREDCONST-DISPLAY PREDCONST-DISPLAY)

(define (add-predconst-display name token-type display-string)
  (set! PREDCONST-DISPLAY
	(cons (list name token-type display-string) PREDCONST-DISPLAY)))

; For instance, adding for a predconst Less the token type predconst-infix
; and the display string << requires

; (add-token
;  "<<"
;  'predconst-infix
;  (string-and-arity-to-predconst-parse-function
;   "Less" (make-arity (py DEFAULT-TVAR-NAME) (py DEFAULT-TVAR-NAME))))

; (add-predconst-display "Less" 'predconst-infix "<<")

(define (predconst-to-string predconst)
  (let* ((name (predconst-to-name predconst))
	 (index (predconst-to-index predconst))
	 (index-string (if (= index -1) "" (number-to-string index)))
	 (info (assoc name PREDCONST-DISPLAY)))
    (if info
	(string-append (caddr info) index-string)
	(string-append name index-string))))


; 5-3. Inductively defined predicate constants
; ============================================

; Inductively defined predicate constants (idpredconsts) are implemented 
; as lists 

; ('idpredconst name types cterms).

; Constructor, accessors and tests for inductively defined predicate
; constants:

(define (make-idpredconst name types cterms)
  (if
   (and (member name '("ExDT" "ExLT" "ExRT" "ExUT"))
	(not (t-deg-one? (var-to-t-deg (car (cterm-to-vars (car cterms)))))))
   (myerror "make-idpredconst"
	    "comprehension term with total variable expected"
	    (car (cterm-to-vars (car cterms)))))
  (list 'idpredconst name types cterms))

; The following is used in grammar.scm, and involves some tests

(define (idpredconst-name-and-types-and-cterms-to-idpredconst name types
							      cterms)
  (let* ((tvars (idpredconst-name-to-tvars name))
	 (tsubst
	  (if (= (length tvars) (length types))
	      (make-substitution tvars types)
	      (apply
	       myerror
	       (append (list
			"idpredconst-name-and-types-and-cterms-to-idpredconst"
		       "equal lengths of tvars and types expected")
		       tvars types))))
	 (param-pvars (idpredconst-name-to-param-pvars name))
	 (subst-param-pvar-arities
	  (map (lambda (arity)
		 (apply make-arity (map (lambda (type)
					  (type-substitute type tsubst))
					(arity-to-types arity))))
	       (map pvar-to-arity param-pvars)))
	 (cterm-arities
	  (map (lambda (cterm) (apply make-arity
				      (map var-to-type (cterm-to-vars cterm))))
	       cterms)))
    (if (not (equal? subst-param-pvar-arities cterm-arities))
	(apply myerror
	       (append
		(list "idpredconst-name-and-types-and-cterms-to-idpredconst"
		      "equal arities expected")
		subst-param-pvar-arities cterm-arities)))
    (make-idpredconst name types cterms)))

(define (idpredconst-form? x) (and (pair? x) (eq? 'idpredconst (car x))))

(define idpredconst-to-name cadr)
(define idpredconst-to-types caddr)
(define idpredconst-to-cterms cadddr)

(define (idpredconst-to-arity idpc)
  (let* ((name (idpredconst-to-name idpc))
	 (types (idpredconst-to-types idpc))
	 (tsubst (idpredconst-name-and-types-to-tsubst name types))
	 (pvar (idpredconst-name-to-pvar name))
	 (uninst-arity (pvar-to-arity pvar))
	 (uninst-types (arity-to-types uninst-arity))
	 (inst-types
	  (map (lambda (x) (type-substitute x tsubst)) uninst-types)))
    (apply make-arity inst-types)))

; (Almost) complete test:

(define (idpredconst? x)
  (and (list? x)
       (= 4 (length x))
       (let ((tag (car x))
	     (name (cadr x))
	     (types (caddr x))
	     (cterms (cadddr x)))
	 (and (eq? 'idpredconst tag)
	      (assoc name IDS)))))

(define (idpredconst-to-pinst idpc)
  (let* ((name (idpredconst-to-name idpc))
	 (types (idpredconst-to-types idpc))
	 (param-cterms (idpredconst-to-cterms idpc))
	 (idpc-names-with-pvars-and-opt-alg-names
	  (idpredconst-name-to-idpc-names-with-pvars-and-opt-alg-names name))
	 (names (map car idpc-names-with-pvars-and-opt-alg-names))
	 (clauses-with-opt-constr-names
	  (apply append
		 (map idpredconst-name-to-clauses-with-names
		      names)))
	 (clauses (map car clauses-with-opt-constr-names))
	 (param-pvars (idpredconst-name-to-param-pvars name))
	 (clause-tvars-list (map formula-to-tvars clauses))
	 (clause-tvars (apply union clause-tvars-list))
	 (tsubst (if (= (length clause-tvars) (length types))
		     (make-substitution clause-tvars types)
		     (apply
		      myerror
		      (append
		       (list
			"idpredconst-to-pinst:"
			"equal lengths of clause-tvars and types expected")
		       clause-tvars types))))
	 (var-lists (map cterm-to-vars param-cterms))
	 (cterm-arities
	  (map (lambda (x) (apply make-arity (map var-to-type x))) var-lists))
	 (param-pvar-arities (map pvar-to-arity param-pvars))
	 (subst-param-pvar-arities
	  (map (lambda (x) (apply make-arity
				  (map (lambda (y) (type-substitute y tsubst))
				       (arity-to-types x))))
	       param-pvar-arities)))
    (if (equal? cterm-arities subst-param-pvar-arities)
	(make-substitution-wrt pvar-cterm-equal? param-pvars param-cterms)
	(apply myerror (append (list "idpredconst-to-pinst"
				     "equal arities expected")
			       cterm-arities subst-param-pvar-arities)))))

; To allow for a convenient display, we maintain a global variable
; IDPREDCONST-DISPLAY consisting of entries (name token-type display-string)

(define IDPREDCONST-DISPLAY '())
(define INITIAL-IDPREDCONST-DISPLAY IDPREDCONST-DISPLAY)

(define (add-idpredconst-display name token-type display-string)
  (set! IDPREDCONST-DISPLAY
	(cons (list name token-type display-string) IDPREDCONST-DISPLAY)))

; For instance, adding for a idpredconst RatEq the token type
; pred-infix and the display string === requires

; (add-token
;  "==="
;  'pred-infix
;  (lambda (x y)
;    (make-predicate-formula (make-idpredconst "RatEq" '() '()) x y)))

; (add-idpredconst-display "RatEq" 'pred-infix "===")

(define (idpredconst-to-string idpc)
  (let* ((name (idpredconst-to-name idpc))
	 (types (idpredconst-to-types idpc))
	 (param-cterms (idpredconst-to-cterms idpc))
	 (type-strings (map type-to-string types))
	 (cterm-strings (map cterm-to-string param-cterms))
	 (strings (append type-strings cterm-strings))
	 (type-strings-with-leading-spaces
	  (map (lambda (x) (string-append " " x)) type-strings))
	 (cterm-strings-with-leading-spaces
	  (map (lambda (x) (string-append " " x)) cterm-strings)))
    (cond
     ((member name '("ExD" "ExDT"))
      (let* ((cterm (car param-cterms))
	     (var (car (cterm-to-vars cterm)))
	     (kernel (cterm-to-formula cterm))
	     (varstring (var-to-string var))
	     (kernelstring (formula-to-string kernel)))
	(string-append "exd" (separator-string "exd" varstring)
		       varstring (separator-string varstring kernelstring)
		       kernelstring)))
     ((member name '("ExL" "ExLT"))
      (let* ((cterm (car param-cterms))
	     (var (car (cterm-to-vars cterm)))
	     (kernel (cterm-to-formula cterm))
	     (varstring (var-to-string var))
	     (kernelstring (formula-to-string kernel)))
	(string-append "exl" (separator-string "exl" varstring)
		       varstring (separator-string varstring kernelstring)
		       kernelstring)))
     ((member name '("ExR" "ExRT"))
      (let* ((cterm (car param-cterms))
	     (var (car (cterm-to-vars cterm)))
	     (kernel (cterm-to-formula cterm))
	     (varstring (var-to-string var))
	     (kernelstring (formula-to-string kernel)))
	(string-append "exr" (separator-string "exr" varstring)
		       varstring (separator-string varstring kernelstring)
		       kernelstring)))
     ((member name '("ExU" "ExUT"))
      (let* ((cterm (car param-cterms))
	     (var (car (cterm-to-vars cterm)))
	     (kernel (cterm-to-formula cterm))
	     (varstring (var-to-string var))
	     (kernelstring (formula-to-string kernel)))
	(string-append "exu" (separator-string "exu" varstring)
		       varstring (separator-string varstring kernelstring)
		       kernelstring)))
;      ((string=? "ExDT" name)
;       (let* ((cterm (car param-cterms))
; 	     (var (car (cterm-to-vars cterm)))
; 	     (kernel (cterm-to-formula cterm))
; 	     (varstring (var-to-string var))
; 	     (kernelstring (formula-to-string kernel)))
; 	(string-append "exdt" (separator-string "exdt" varstring)
; 		       varstring (separator-string varstring kernelstring)
; 		       kernelstring)))
;      ((string=? "ExLT" name)
;       (let* ((cterm (car param-cterms))
; 	     (var (car (cterm-to-vars cterm)))
; 	     (kernel (cterm-to-formula cterm))
; 	     (varstring (var-to-string var))
; 	     (kernelstring (formula-to-string kernel)))
; 	(string-append "exlt" (separator-string "exlt" varstring)
; 		       varstring (separator-string varstring kernelstring)
; 		       kernelstring)))
;      ((string=? "ExRT" name)
;       (let* ((cterm (car param-cterms))
; 	     (var (car (cterm-to-vars cterm)))
; 	     (kernel (cterm-to-formula cterm))
; 	     (varstring (var-to-string var))
; 	     (kernelstring (formula-to-string kernel)))
; 	(string-append "exrt" (separator-string "exrt" varstring)
; 		       varstring (separator-string varstring kernelstring)
; 		       kernelstring)))
;      ((string=? "ExUT" name)
;       (let* ((cterm (car param-cterms))
; 	     (var (car (cterm-to-vars cterm)))
; 	     (kernel (cterm-to-formula cterm))
; 	     (varstring (var-to-string var))
; 	     (kernelstring (formula-to-string kernel)))
; 	(string-append "exut" (separator-string "exut" varstring)
; 		       varstring (separator-string varstring kernelstring)
; 		       kernelstring)))
     ((string=? "AndD" name)
      (let* ((cterm1 (car param-cterms))
	     (cterm2 (cadr param-cterms))
	     (kernel1 (cterm-to-formula cterm1))
	     (kernel2 (cterm-to-formula cterm2)))
	(string-append (formula-to-string kernel1)
		       " andd " 
		       (formula-to-string kernel2))))
     ((string=? "AndL" name)
      (let* ((cterm1 (car param-cterms))
	     (cterm2 (cadr param-cterms))
	     (kernel1 (cterm-to-formula cterm1))
	     (kernel2 (cterm-to-formula cterm2)))
	(string-append (formula-to-string kernel1)
		       " andl " 
		       (formula-to-string kernel2))))
     ((string=? "AndR" name)
      (let* ((cterm1 (car param-cterms))
	     (cterm2 (cadr param-cterms))
	     (kernel1 (cterm-to-formula cterm1))
	     (kernel2 (cterm-to-formula cterm2)))
	(string-append (formula-to-string kernel1)
		       " andr " 
		       (formula-to-string kernel2))))
     ((string=? "AndU" name)
      (let* ((cterm1 (car param-cterms))
	     (cterm2 (cadr param-cterms))
	     (kernel1 (cterm-to-formula cterm1))
	     (kernel2 (cterm-to-formula cterm2)))
	(string-append (formula-to-string kernel1)
		       " andu " 
		       (formula-to-string kernel2))))
     ((string=? "OrD" name)
      (let* ((cterm1 (car param-cterms))
	     (cterm2 (cadr param-cterms))
	     (kernel1 (cterm-to-formula cterm1))
	     (kernel2 (cterm-to-formula cterm2)))
	(string-append (formula-to-string kernel1)
		       " ord " 
		       (formula-to-string kernel2))))
     ((string=? "OrL" name)
      (let* ((cterm1 (car param-cterms))
	     (cterm2 (cadr param-cterms))
	     (kernel1 (cterm-to-formula cterm1))
	     (kernel2 (cterm-to-formula cterm2)))
	(string-append (formula-to-string kernel1)
		       " orl " 
		       (formula-to-string kernel2))))
     ((string=? "OrR" name)
      (let* ((cterm1 (car param-cterms))
	     (cterm2 (cadr param-cterms))
	     (kernel1 (cterm-to-formula cterm1))
	     (kernel2 (cterm-to-formula cterm2)))
	(string-append (formula-to-string kernel1)
		       " orr " 
		       (formula-to-string kernel2))))
     ((string=? "OrU" name)
      (let* ((cterm1 (car param-cterms))
	     (cterm2 (cadr param-cterms))
	     (kernel1 (cterm-to-formula cterm1))
	     (kernel2 (cterm-to-formula cterm2)))
	(string-append (formula-to-string kernel1)
		       " oru " 
		       (formula-to-string kernel2))))
     ((string=? "EqD" name) "eqd")
     (else
      (let* ((info (assoc name IDPREDCONST-DISPLAY))
	     (new-name (if info (caddr info) name))
	     (tvars-inferable-from-arity?
	      (null? (set-minus
		      (idpredconst-name-to-tvars name)
		      (apply union (map type-to-free
					(arity-to-types
					 (pvar-to-arity
					  (idpredconst-name-to-pvar
					   name)))))))))
	(if tvars-inferable-from-arity?
	    (if (null? param-cterms)
		new-name
		(apply string-append
		       (append (list "(" new-name)
			       cterm-strings-with-leading-spaces
			       (list ")"))))
	    (apply string-append
		   (append (list "(" new-name)
			   type-strings-with-leading-spaces
			   cterm-strings-with-leading-spaces
			   (list ")")))))))))

(define (idpredconst-to-free idpc)
  (let* ((types (idpredconst-to-types idpc))
	 (cterms (idpredconst-to-cterms idpc)))
    (apply union (map cterm-to-free cterms))))

; Inductively defined predicate constant names are provided in the form
; of an association list IDS, which assigns all relevant information to
; the name.

; Format of IDS:

; ((idpredconst-name idpredconst-names-with-pvars-and-opt-alg-names
; 	             (clause1 name1) (clause2 name2)...)
;  ...)

; Here the assigned pvars serve for ease of substitutions when forming
; e.g. an elimination axiom.  The presence of an alg-name indicates that
; this idpredconst is to have computational content.  Then all clauses
; with this idpredconst in the conclusion must provide a constr-name.
; If idpredconst is to have no computational content, then all its
; clauses must be invariant (under realizability, a.k.a. `negative').

; How it works: add Acc^ temporarily as a predicate variable.  Then
; parse the clauses.  Create new pvar X.  Substitute Acc^ by X.  Remove
; pvar Acc^.  Create idpredconst Acc.  Form clauses by substituting Acc
; for X.

(define IDS '())
(define INITIAL-IDS IDS)

(define (idpredconst-name? string) (assoc string IDS))

(define (idpredconst-name-to-pvar name)
  (let* ((info1 (assoc name IDS))
	 (idpredconst-names-with-pvars-and-opt-alg-names
	  (if
	   info1 (cadr info1)
	   (myerror
	    "idpredconst-name-to-pvar-name" "idpredconst name expected" name)))
	 (info2 (assoc name idpredconst-names-with-pvars-and-opt-alg-names)))
    (cadr info2)))

(define (idpredconst-name-to-opt-alg-name name)
  (let* ((info1 (assoc name IDS))
	 (idpredconst-names-with-pvars-and-opt-alg-names
	  (if
	   info1 (cadr info1)
	   (myerror
	    "idpredconst-name-to-opt-alg-name" "idpredconst name expected"
	    name)))
	 (info2 (assoc name idpredconst-names-with-pvars-and-opt-alg-names)))
    (cddr info2)))

(define (idpredconst-name-to-alg-name name)
  (let ((opt-alg-name (idpredconst-name-to-opt-alg-name name)))
    (if (pair? opt-alg-name) (car opt-alg-name)
	(myerror "idpredconst-name-to-alg-name"
		 "alg name expected for" name))))

(define (idpredconst-name-to-nbe-alg-name name)
  (string-append "nbe" name))

(define (idpredconst-name-to-idpc-names-with-pvars-and-opt-alg-names name)
  (let* ((info (assoc name IDS)))
    (if info (cadr info)
	(myerror "idpredconst-name-to-idpc-names-with-pvars-and-opt-alg-names"
		 "idpredconst name expected" name))))

(define (idpredconst-name-to-simidpc-names name)
  (map car (idpredconst-name-to-idpc-names-with-pvars-and-opt-alg-names name)))

(define (idpredconst-name-to-pvars name)
  (map cadr
       (idpredconst-name-to-idpc-names-with-pvars-and-opt-alg-names name)))

(define (idpredconst-name-to-param-pvars name)
  (let* ((idpc-names-with-pvars-and-opt-alg-names
	  (idpredconst-name-to-idpc-names-with-pvars-and-opt-alg-names name))
	 (names (map car idpc-names-with-pvars-and-opt-alg-names))
	 (pvars (map cadr idpc-names-with-pvars-and-opt-alg-names))
	 (clauses-with-names
	  (apply append (map idpredconst-name-to-clauses-with-names names)))
	 (clauses (map car clauses-with-names))
	 (clause-pvars-list (map formula-to-pvars clauses))
	 (clause-pvars (apply union clause-pvars-list)))
    (set-minus clause-pvars pvars)))

(define (idpredconst-name-to-clauses-with-names name)
  (let* ((info (assoc name IDS)))
    (if info (cddr info)
	(myerror "idpredconst-name-to-clauses-with-names"
		 "idpredconst name expected" name))))

(define (idpredconst-name-to-clauses name)
  (map car (idpredconst-name-to-clauses-with-names name)))

(define (idpredconst-name-to-tvars name)
  (let* ((idpredconst-names-with-pvars-and-opt-alg-names
	  (idpredconst-name-to-idpc-names-with-pvars-and-opt-alg-names name))
	 (names (map car idpredconst-names-with-pvars-and-opt-alg-names))
	 (clauses-with-names
	  (apply append
		 (map idpredconst-name-to-clauses-with-names
		      names)))
	 (clauses (map car clauses-with-names))
	 (clause-tvars-list (map formula-to-tvars clauses)))
    (apply union clause-tvars-list)))

(define (idpredconst-name-and-types-to-tsubst name types)
  (let ((tvars (idpredconst-name-to-tvars name)))
    (if (= (length tvars) (length types))
	(make-substitution tvars types)
	(apply myerror (append (list  "idpredconst-name-and-types-to-tsubst"
				      "equal lengths expected")
			       tvars types)))))

; add-ids means add inductively defined predicates.  How it works: We
; are given idpc-names-with-arities-and-opt-alg-names.  For simplicity
; assume that there is only one idpc-name.  We are also given its
; clauses as clause-strings-with-opt-names.  For parsing the
; clause-strings, a new predicate variable is created and (using it)
; clauses-with-new-pvars-and-names are built.  The names of the
; clauses are either given or else created, in the form EvenZero,
; EvenOne etc.  The presence of an alg-name (e.g., algEven) in
; idpc-names-with-arities-and-opt-alg-names indicates that the idpc is
; computationally relevant (c.r.), that is requires witnesses, for
; extraction.  If an alg-name is present, then all clauses with this
; idpredconst as conclusion generate constructors; default-name
; cEvenZero, cEvenOne.  We use nbeEven as alg-name for nbe.

; We also allow computationally irrelevant (c.i.) (or
; non-computational, n.c.) inductively defined predicates.  Then
; idpc-names-with-arities-and-opt-alg-names has no alg-name.
; Important special cases are: (i) For every I its witnessing
; predicate IReal.  It is special in the sense that it just states the
; fact that we do have a realizer for I.  (ii) Leibniz equality EqD,
; and computationally irrelevant versions ExU and AndU (better: ExNC,
; AndNC) of the existential quantifier and of conjunction.  These are
; special in the sense that they are defined by just one clause, which
; contains impnc, allnc only and has no recursive premises.  In all
; other cases the elimination scheme must be (severely) restricted to
; n.c. formulas.  Moreover, all clauses must have non-computational
; invariant (n.c.i.) parameter and premise formulas.  This ensures
; that the soundness theorem continues to hold: all intro and elim
; axioms are invariant, i.e., nullterm mr A is the same as A.

(define (add-ids idpc-names-with-arities-and-opt-alg-names .
		 clause-strings-with-opt-names)
  (if (not (list? idpc-names-with-arities-and-opt-alg-names))
      (myerror
       "add-ids" "list idpc-names-with-arities-and-opt-alg-names expected"
       idpc-names-with-arities-and-opt-alg-names))
  (for-each
   (lambda (x)
     (if
      (not (and (<= 2 (length x))
		(string? (car x))
		(arity? (cadr x))
		(or (= 2 (length x))
		    (and (= 3 (length x)) (string? (caddr x))))))
      (myerror "add-ids" "idpc-name with arity and opt alg-name expected" x)))
   idpc-names-with-arities-and-opt-alg-names)
  (set! OLD-COMMENT-FLAG COMMENT-FLAG)
  (set! COMMENT-FLAG #f)
  (let* ((idpc-names (map car idpc-names-with-arities-and-opt-alg-names))
	 (new-idpc-names-test
	  (if (not (apply and-op (map (lambda (s)
					(and (string? s)
					     (not (is-used? s '()
							    'idpredconst))))
				      idpc-names)))
	      (begin
		(set! COMMENT-FLAG OLD-COMMENT-FLAG)
		(myerror "add-ids" "list of new strings expected"
			 idpc-names))))
	 (clause-strings-with-opt-names-test
	  (for-each
	   (lambda (x)
	     (if (or (not (list? x))
		     (< 2 (length x))
		     (not (string? (car x)))
		     (and (pair? (cdr x)) (not (string? (cadr x)))))
		 (begin
		   (set! COMMENT-FLAG OLD-COMMENT-FLAG)
		   (myerror "add-ids"
			    "list of clause-string and optional name expected"
			    x))))
	   clause-strings-with-opt-names))
	 (all-with-content?
	  (apply and-op (map (lambda (x) (< 2 (length x)))
			     idpc-names-with-arities-and-opt-alg-names)))
	 (all-without-content?
	  (apply and-op (map (lambda (x) (= 2 (length x)))
			     idpc-names-with-arities-and-opt-alg-names)))
	 (all-with-or-all-without-content-test
	  (if
	   (not (or all-with-content? all-without-content?))
	   (begin
	     (set! COMMENT-FLAG OLD-COMMENT-FLAG)
	     (myerror "add-ids" "inductively defined predicate constants"
		      idpc-names
		      "should be either all with or all without content"))))
	 (arities (map cadr idpc-names-with-arities-and-opt-alg-names))
	 (clause-strings (map car clause-strings-with-opt-names))
	 (new-pvars (map arity-to-new-general-pvar arities))
	 (var-lists
	  (map (lambda (arity)
		 (map type-to-new-partial-var (arity-to-types arity)))
	       arities))
	 (atoms (map (lambda (x y)
		       (apply make-predicate-formula
			      (cons x (map make-term-in-var-form y))))
		     new-pvars var-lists))
	 (cterms (map (lambda (x y) (apply make-cterm (append x (list y))))
		      var-lists atoms))
					;now we can parse clause-strings
	 (clauses-with-new-pvars
	  (begin (do ((l1 idpc-names (cdr l1))
		      (l2 arities (cdr l2)))
		     ((null? l1))
		   (add-pvar-name (car l1) (car l2)))
		 (let* ((pvars
			 (map (lambda (x y)
				(make-pvar x -1 h-deg-zero n-deg-zero y))
			      arities idpc-names))
			(psubst (map (lambda (x y) (list x y))
				     pvars cterms)))
		   (map (lambda (x) (formula-substitute (pf x) psubst))
			clause-strings))))
	 (param-pvars (set-minus (apply union (map formula-to-pvars
						   clauses-with-new-pvars))
				 new-pvars))
	 (clause-test
	  (if
	   all-with-content?
	   (for-each
	    (lambda (fla clause-string)
	      (if (not (cr-idpc-clause? fla new-pvars param-pvars))
		  (let ((free (formula-to-free fla)))
		    (set! COMMENT-FLAG OLD-COMMENT-FLAG)
		    (apply remove-var-name idpc-names)
		    (if
		     (pair? free)
		     (apply myerror
			    (append
			     (list "add-ids" "unexpected free variables")
			     free (list "in clause" clause-string))))
		    (myerror
		     "add-ids"
		     "not a clause for a computationally relevant idpc"
		     clause-string))))
	    clauses-with-new-pvars clause-strings)
					;else all without content
	   (for-each
	    (lambda (fla clause-string)
	      (if (not (nc-idpc-clause? fla new-pvars param-pvars))
		  (let ((free (formula-to-free fla)))
		    (set! COMMENT-FLAG OLD-COMMENT-FLAG)
		    (apply remove-var-name idpc-names)
		    (if
		     (pair? free)
		     (apply myerror
			    (append
			     (list "add-ids" "unexpected free variables")
			     free (list "in clause" clause-string))))
		    (myerror
		     "add-ids"
		     "not a clause for a non-computational idpc"
		     clause-string))))
	    clauses-with-new-pvars clause-strings)))
; 	 (clause-test
; 	  (for-each
; 	   (lambda (fla clause-string)
; 	     (if (not (clause? fla new-pvars))
; 		 (let ((free (formula-to-free fla)))
; 		   (set! COMMENT-FLAG OLD-COMMENT-FLAG)
; 		   (apply remove-var-name idpc-names)
; 		   (if
; 		    (pair? free)
; 		    (apply myerror
; 			   (append (list "add-ids" "unexpected free variables")
; 				   free (list "in clause" clause-string))))
; 		   (myerror
; 		    "add-ids"
; 		    "not a clause in the sense of clause?" clause-string))))
; 	   clauses-with-new-pvars clause-strings))
; 	 (uniform-non-recursive-clause-test
; 	  (if
; 	   all-without-content?
; 	   (for-each
; 	    (lambda (fla)
; 	      (if
; 	       (not (apply uniform-non-recursive-clause? (cons fla new-pvars)))
; 	       (begin
; 		 (set! COMMENT-FLAG OLD-COMMENT-FLAG)
; 		 (apply remove-var-name idpc-names)
; 		 (myerror "add-ids" "uniform non-recursive clause expected"
; 			  "for idpc not requiring witnesses" fla))))
; 	    clauses-with-new-pvars)))
	 (clauses-with-new-pvars-and-opt-names
	  (map (lambda (x y) (cons x y))
	       clauses-with-new-pvars
	       (map cdr clause-strings-with-opt-names)))
	 (clauses-with-new-pvars-and-names
	  (do ((l clauses-with-new-pvars-and-opt-names (cdr l))
	       (pvar-counter-alist-and-res
		(list (map (lambda (pvar) (list pvar 0)) new-pvars) '())
		(let* ((pvar-counter-alist (car pvar-counter-alist-and-res))
		       (res (cadr pvar-counter-alist-and-res))
		       (clause-with-new-pvar-and-opt-name (car l))
		       (clause (car clause-with-new-pvar-and-opt-name))
		       (opt-name (cdr clause-with-new-pvar-and-opt-name))
		       (pvar
			(let* ((kernel (all-allnc-form-to-final-kernel clause))
			       (concl
				(imp-impnc-form-to-final-conclusion kernel)))
			  (predicate-form-to-predicate concl)))
		       (idpc-name
			(cadr (assoc pvar (map (lambda (x y) (list x y))
					       new-pvars idpc-names))))
		       (i (cadr (assoc pvar pvar-counter-alist)))
		       (name (if (null? opt-name)
				 (string-append
				  idpc-name
				  (number-to-alphabetic-string i))
				 (car opt-name))))
		  (list (cons (list pvar (+ 1 i))
			      (remove (list pvar i) pvar-counter-alist))
			(cons (list clause name) res)))))
	      ((null? l) (reverse (cadr pvar-counter-alist-and-res)))))
	 (clause-names (map cadr clauses-with-new-pvars-and-names))
	 (idpc-names-and-clauses-with-new-pvars-and-names
	  (map
	   (lambda (idpc-name)
	     (do ((l clauses-with-new-pvars-and-names (cdr l))
		  (res
		   '()
		   (if
		    (let* ((pvar (cadr (assoc idpc-name
					      (map (lambda (x y) (list x y))
						   idpc-names
						   new-pvars))))
			   (kernel (all-allnc-form-to-final-kernel (caar l)))
			   (concl (imp-impnc-form-to-final-conclusion kernel)))
		      (and (predicate-form? concl)
			   (equal? pvar (predicate-form-to-predicate concl))))
		    (cons (car l) res)
		    res)))
		 ((null? l) (cons idpc-name (reverse res)))))
	   idpc-names))
	 (nbe-types (map nbe-formula-to-type clauses-with-new-pvars))
	 (new-tvars (map PVAR-TO-TVAR new-pvars))
	 (new-tvars-cc (if all-with-content?
			   (map PVAR-TO-TVAR new-pvars)
			   '()))
	 (alg-names (if all-with-content?
			(map caddr idpc-names-with-arities-and-opt-alg-names)
			'()))
	 (nbe-alg-names (map idpredconst-name-to-nbe-alg-name idpc-names))
					;for stringtyped-constr-names temp.
					;add nbe-alg-names with token type
					;alg to ALGEBRAS
	 (nbe-tsubst-for-new-tvars
	  (begin 	 
	    (set! OLD-ALGEBRAS ALGEBRAS)
	    (for-each (lambda (x)
			(set! ALGEBRAS
			      (cons (list x nbe-alg-names 'alg) ALGEBRAS)))
		      nbe-alg-names)
	    (map (lambda (x y) (list x (make-alg y)))
		 new-tvars nbe-alg-names)))
	 (nbe-free-tvars-list (map type-to-free nbe-types))
	 (param-pvar-tvars (map PVAR-TO-TVAR param-pvars))
	 (nbe-standard-tvars-list ;alpha1 ... for stringtyped-constr-names
	  (map (lambda (free-tvars)
		 (do ((i 1 (+ 1 i))
		      (res '() (cons (make-tvar i DEFAULT-TVAR-NAME) res)))
		     ((> i (length (union free-tvars param-pvar-tvars)))
		      (reverse res))))
	       nbe-free-tvars-list))
	 (nbe-tsubst-list
	  (map (lambda (free-tvars standard-tvars)
		 (map (lambda (x y) (list x y))
		      (union free-tvars param-pvar-tvars) standard-tvars))
	       nbe-free-tvars-list nbe-standard-tvars-list))
	 (nbe-constr-types
	  (map (lambda (type tsubst)
		 (type-substitute
		  type (append nbe-tsubst-for-new-tvars tsubst)))
	       nbe-types nbe-tsubst-list))
	 (nbe-type-strings (map type-to-string nbe-constr-types))
	 (et-types (if all-without-content? '()
		       (map formula-to-et-type clauses-with-new-pvars)))
	 (et-constr-names
	  (if all-without-content? '()
	      (map (lambda (name) (string-append "c" name)) clause-names)))
	 (et-tvars (set-minus (apply union (map (lambda (x)
						  (type-to-free
						   (formula-to-et-type x)))
						clauses-with-new-pvars))
			      new-tvars))
	 (et-standard-tvars
	  (do ((i 1 (+ 1 i))
	       (res '() (cons (make-tvar i DEFAULT-TVAR-NAME) res)))
	      ((> i (length et-tvars)) (reverse res))))
	 (et-tsubst (map (lambda (x y) (list x y)) et-tvars et-standard-tvars))
	 (tsubst2 ;temporarily add alg-names with token type alg to ALGEBRAS
	  (begin 	 
	    (for-each (lambda (x)
			(set! ALGEBRAS
			      (cons (list x alg-names 'alg) ALGEBRAS)))
		      alg-names)
	    (map (lambda (x y) (list x (make-alg y)))
		 new-tvars-cc alg-names)))
	 (et-constr-types
	  (map (lambda (x) (type-substitute x (append tsubst2 et-tsubst)))
	       et-types))
	 (et-type-strings (map type-to-string et-constr-types))
	 (stringtyped-et-constr-names
	  (map (lambda (x y) (list x y))
	       et-constr-names et-type-strings))
	 (nbe-alg-names-and-number-of-clauses
	  (map (lambda (x y) (list x (length (cdr y))))
	       nbe-alg-names
	       idpc-names-and-clauses-with-new-pvars-and-names))
	 (nbe-constr-names
	  (apply
	   append
	   (map (lambda (nbe-alg-name idpredconst-name)
		  (let ((number-of-clauses
			 (cadr (assoc nbe-alg-name
				      nbe-alg-names-and-number-of-clauses))))
		    (do ((n 0 (+ 1 n))
			 (res '() (cons (string-append
					 (number-to-alphabetic-string n)
					 idpredconst-name)
					res)))
			((= n number-of-clauses) (reverse res)))))
		nbe-alg-names idpc-names)))
	 (stringtyped-nbe-constr-names
	  (map (lambda (x y) (list x y))
	       nbe-constr-names nbe-type-strings))
	 (param-tvars
	  (apply union (map formula-to-tvars clauses-with-new-pvars))))
    (apply remove-pvar-name idpc-names)
    (set! ALGEBRAS OLD-ALGEBRAS)
					;check for nullary clauses (2008-02-24)
    (if (null? clauses-with-new-pvars)
	(begin (set! COMMENT-FLAG OLD-COMMENT-FLAG)
	       (myerror "add-ids" "nullary clause missing")))
    (let
	((remove-safe-clauses
	  (lambda (clauses)
	    (let*
		((concl-pvars
		  (map (lambda (x)
			 (predicate-form-to-predicate
			  (imp-impnc-all-allnc-form-to-final-conclusion x)))
		       clauses))
		 (clauses-wo-rec-calls-to-concl-pvars
		  (list-transform-positive clauses
		    (lambda (clause)
		      (null?
		       (list-transform-positive
			   (imp-form-to-premises
			    (all-allnc-form-to-final-kernel clause))
			 (lambda (x)
			   (let ((concl
				  (imp-impnc-all-allnc-form-to-final-conclusion
				   x)))
			     (and (predicate-form? concl)
				  (member
				   (predicate-form-to-predicate concl)
				   concl-pvars)))))))))
		 (safe-pvars
		  (map (lambda (x)
			 (predicate-form-to-predicate
			  (imp-impnc-all-allnc-form-to-final-conclusion x)))
		       clauses-wo-rec-calls-to-concl-pvars))
		 (safe-clauses
		  (list-transform-positive clauses
		    (lambda (x)
		      (member
		       (predicate-form-to-predicate
			(imp-impnc-all-allnc-form-to-final-conclusion x))
		       safe-pvars)))))
	      (if (null? safe-clauses)
		  (begin
		    (set! COMMENT-FLAG OLD-COMMENT-FLAG)
		    (apply
		     myerror
		     (append
		      (list "add-ids" "nullary clause missing in clauses")
		      clauses))))
	      (set-minus clauses safe-clauses)))))
      (do ((clauses clauses-with-new-pvars (remove-safe-clauses clauses)))
          ((null? clauses))))
    (let ((free (apply union (map type-to-free nbe-constr-types))))
      (if (null? free)
	  (apply add-algs (cons nbe-alg-names stringtyped-nbe-constr-names))
	  (apply add-algebras-with-parameters
		 (append (list nbe-alg-names 'alg-typeop (length free))
			 stringtyped-nbe-constr-names))))
    (if
     (pair? alg-names)
     (let ((et-constr-type-tvars
	    (apply union (map type-to-free et-constr-types))))
       (if (null? et-constr-type-tvars)
	   (apply add-algs (cons alg-names stringtyped-et-constr-names))
	   (apply add-algebras-with-parameters
		  (append
		   (list alg-names 'alg-typeop (length et-constr-type-tvars))
		   stringtyped-et-constr-names)))))
    (for-each ;of idpc-names-and-clauses-with-new-pvars-and-names and arities
     (lambda (x arity)
       (let ((idpc-name (car x))
	     (clauses-with-new-pvars-and-names (cdr x))
	     (idpc-names-with-pvars-and-opt-alg-names
	      (map (lambda (x y) (cons (car x) (cons y (cddr x))))
		   idpc-names-with-arities-and-opt-alg-names
		   new-pvars))
	     (non-inferable-param-tvars
	      (set-minus
	       param-tvars
	       (apply union (map type-to-free (arity-to-types arity))))))
	 (set! COMMENT-FLAG OLD-COMMENT-FLAG)
	 (comment "ok, inductively defined predicate constant "
		  idpc-name " added")
	 (set! IDS (cons (append
			  (list
			   idpc-name
			   idpc-names-with-pvars-and-opt-alg-names)
			  clauses-with-new-pvars-and-names)
			 IDS))
	 (cond
	  ((and (null? param-pvars)
		(null? non-inferable-param-tvars))
	   (add-token ;
	    idpc-name
	    'idpredconst-name
	    (string-and-arity-and-cterms-to-idpc-parse-function
	     idpc-name arity '())))
	  ((and (pair? param-pvars)
		(pair? non-inferable-param-tvars))
	   (add-token ;
	    idpc-name
	    'idpredconstscheme-name
	    idpc-name))
	  ((and (pair? param-pvars)
		(null? non-inferable-param-tvars))
	   (add-token ;
	    idpc-name
	    'idpredconstscheme-name-wit ;wit=with-inferable-types
	    (lambda (cterms)
	      (string-and-arity-and-cterms-to-idpc-parse-function
	       idpc-name arity cterms))))
	  (else
	   (myerror
	    "add-ids"
	    "unexpected idpredconst without cterms whose param-tvars"
	    "cannot be inferred from the arguments" idpc-name)))))
     idpc-names-and-clauses-with-new-pvars-and-names
     arities)
    (for-each ;of idpc-names-and-clauses-with-new-pvars-and-names
     (lambda (x)
       (let ((idpc-name (car x))
	     (clauses-with-new-pvars-and-names (cdr x)))
	 (do ((i 0 (+ 1 i))
	      (names (map cadr clauses-with-new-pvars-and-names) (cdr names)))
	     ((= i (length clauses-with-new-pvars-and-names)))
	   (let* ((cterms
		   (if (member idpc-name '("ExDT" "ExLT" "ExRT" "ExUT"))
		       (map predicate-to-cterm-with-total-vars param-pvars)
		       (map predicate-to-cterm param-pvars)))
		  (aconst (number-and-idpredconst-to-intro-aconst
			   i (make-idpredconst idpc-name param-tvars cterms)))
		  (proof (make-proof-in-aconst-form aconst)))
	     (set! THEOREMS
		   (cons (list (car names) aconst proof) THEOREMS))))))
     idpc-names-and-clauses-with-new-pvars-and-names)))

(define (remove-idpc-name . x)
  (define (rin1 idpc-name)
    (let* ((simidpc-names
	    (idpredconst-name-to-simidpc-names idpc-name))
	   (opt-alg-names
	    (apply union
		   (map (lambda (n) (idpredconst-name-to-opt-alg-name n))
			simidpc-names))))
      (set! OLD-COMMENT-FLAG COMMENT-FLAG)
      (set! COMMENT-FLAG #f)
      (if (pair? opt-alg-names) (remove-alg-name (car opt-alg-names)))
      (remove-alg-name (idpredconst-name-to-nbe-alg-name idpc-name))
      (for-each remove-token simidpc-names)
      (set! COMMENT-FLAG OLD-COMMENT-FLAG)
      (set! IDS (list-transform-positive IDS
		  (lambda (x) (not (member (car x) simidpc-names)))))
      (for-each (lambda (x)
		  (comment
		   "ok, inductively defined predicate constant " x " removed"))
		simidpc-names)))
  (for-each (lambda (idpc-name)
	      (if (not (assoc idpc-name IDS))
		  (myerror "remove-idpc-name" "idpc name expected" idpc-name)))
	    x)
  (for-each rin1 x))

; append-hat appends ^ to every occurrence of name in string, where
; the following character is neither ^ nor alphabetic and the
; preceding character is not alphabetic.

(define (number-to-alphabetic-string i)
  (do ((charlist (reverse (string->list (number-to-string i))) (cdr charlist))
       (res '() (append (let ((char (car charlist)))
			  (cond ((char=? char #\0) (list #\Z #\e #\r #\o))
				((char=? char #\1) (list #\O #\n #\e)) 
				((char=? char #\2) (list #\T #\w #\o)) 
				((char=? char #\3) (list #\T #\h #\r #\e #\e)) 
				((char=? char #\4) (list #\F #\o #\u #\r))
				((char=? char #\5) (list #\F #\i #\v #\e))
				((char=? char #\6) (list #\S #\i #\x))
				((char=? char #\7) (list #\S #\e #\v #\e #\n))
				((char=? char #\8) (list #\E #\i #\g #\h #\t))
				((char=? char #\9) (list #\N #\i #\n #\e))
				(else (myerror "numeric char expected" char))))
			res)))
      ((null? charlist) (list->string res))))

(define (alphabetic-string-to-number string)
  (let ((l (string-length string)))
    (cond
     ((and (<= 4 l) (string=? "Zero" (substring string 0 4))) 0)
     ((and (<= 3 l) (string=? "One" (substring string 0 3))) 1)
     ((and (<= 3 l) (string=? "Two" (substring string 0 3))) 2)
     ((and (<= 5 l) (string=? "Three" (substring string 0 5))) 3)
     ((and (<= 4 l) (string=? "Four" (substring string 0 4))) 4)
     ((and (<= 4 l) (string=? "Five" (substring string 0 4))) 5)
     ((and (<= 3 l) (string=? "Six" (substring string 0 3))) 6)
     ((and (<= 5 l) (string=? "Seven" (substring string 0 5))) 7)
     ((and (<= 5 l) (string=? "Eight" (substring string 0 5))) 8)
     ((and (<= 4 l) (string=? "Nine" (substring string 0 4))) 9)
     (else
      (myerror "alphabetic-string-to-number" "unexpected string" string)))))

(define (strings-and-rest-to-numbers-and-rest string)
  (let ((l (string-length string)))
    (cond
     ((and (<= 4 l) (string=? "Zero" (substring string 0 4)))
      (cons 0 (strings-and-rest-to-numbers-and-rest (substring string 4 l))))
     ((and (<= 3 l) (string=? "One" (substring string 0 3)))
      (cons 1 (strings-and-rest-to-numbers-and-rest (substring string 3 l))))
     ((and (<= 3 l) (string=? "Two" (substring string 0 3)))
      (cons 2 (strings-and-rest-to-numbers-and-rest (substring string 3 l))))
     ((and (<= 5 l) (string=? "Three" (substring string 0 5)))
      (cons 3 (strings-and-rest-to-numbers-and-rest (substring string 5 l))))
     ((and (<= 4 l) (string=? "Four" (substring string 0 4)))
      (cons 4 (strings-and-rest-to-numbers-and-rest (substring string 4 l))))
     ((and (<= 4 l) (string=? "Five" (substring string 0 4)))
      (cons 5 (strings-and-rest-to-numbers-and-rest (substring string 4 l))))
     ((and (<= 3 l) (string=? "Six" (substring string 0 3)))
      (cons 6 (strings-and-rest-to-numbers-and-rest (substring string 3 l))))
     ((and (<= 5 l) (string=? "Seven" (substring string 0 5)))
      (cons 7 (strings-and-rest-to-numbers-and-rest (substring string 5 l))))
     ((and (<= 5 l) (string=? "Eight" (substring string 0 5)))
      (cons 8 (strings-and-rest-to-numbers-and-rest (substring string 5 l))))
     ((and (<= 4 l) (string=? "Nine" (substring string 0 4)))
      (cons 9 (strings-and-rest-to-numbers-and-rest (substring string 4 l))))
     (else (list string)))))

(define (constructor-name-to-i-and-idpredconst-name string)
  (let* ((numbers-and-rest (strings-and-rest-to-numbers-and-rest string))
	 (i (do ((l numbers-and-rest (cdr l))
		 (res 0 (if (integer? (car l))
			    (+ (* 10 res) (car l))
			    (myerror "integer expected" (car l)))))
		((or (string? (car l)) (null? l)) res)))
	 (name (car (last-pair numbers-and-rest))))
    (list i name)))