; MINLOG: germanise.scm

; Dummywörter:

(define : "42")
(define fuer "42")
(define gegeben_also "42")
(define mit "42")
(define und_nenne_es "42")
(define wie_in "42")


(define (zeige_Hilfssätze)
  (display-global-assumptions "Hilfssatz1" "Hilfssatz2"))


(define (assume . x-list)
  (let* ((num-goals (pproof-state-to-num-goals))
	 (proof (pproof-state-to-proof))
	 (maxgoal (pproof-state-to-maxgoal)))
    (set! PPROOF-STATE (apply assume-intern
			      (append (list num-goals proof maxgoal) x-list)))
    (pproof-state-history-push PPROOF-STATE)
;    (display-comment "ok, we now have the new goal ")
    (if COMMENT-FLAG (newline))
    (display-num-goal (car (pproof-state-to-num-goals)))))

(define (by-assume-with exhyp var kernel)
  (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 (by-assume-with-intern
			num-goals proof maxgoal exhyp var kernel))
    (pproof-state-history-push PPROOF-STATE)
;    (display-comment "ok, we now have the new goal ")
    (if COMMENT-FLAG (newline))
    (display-num-goal (car (pproof-state-to-num-goals)))))

(define (drop . x-list)
  (let* ((num-goals (pproof-state-to-num-goals))
	 (proof (pproof-state-to-proof))
	 (maxgoal (pproof-state-to-maxgoal)))
    (set! PPROOF-STATE (apply drop-intern
			      (append (list num-goals proof maxgoal) x-list)))
    (pproof-state-history-push PPROOF-STATE)
;    (display-comment "ok, we now have the new goal ")
    (if COMMENT-FLAG (newline))
    (display-num-goal (car (pproof-state-to-num-goals)))))

(define (inst-with-to x . x-list-and-name)
  (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
		  (apply inst-with-to-intern
				 (append (list num-goals proof maxgoal x) x-list-and-name)))
    (pproof-state-history-push PPROOF-STATE)
;    (display-comment "ok, " DEFAULT-GOAL-NAME "_" (number-to-string number)
;					 " can be obtained from")
    (if COMMENT-FLAG (newline))
    (display-num-goal (car (pproof-state-to-num-goals)))))

(define (split)
  (let* ((num-goals (pproof-state-to-num-goals))
	 (proof (pproof-state-to-proof))
	 (maxgoal (pproof-state-to-maxgoal)))
    (set! PPROOF-STATE (split-intern num-goals proof maxgoal))
    (pproof-state-history-push PPROOF-STATE)
;    (display-comment "ok, we now have the new goals ")
    (if COMMENT-FLAG (newline))
    (display-num-goal (cadr (pproof-state-to-num-goals)))
    (if COMMENT-FLAG (newline))
    (display-num-goal (car (pproof-state-to-num-goals)))))


(define (display-new-goals num-goals number)
  (if COMMENT-FLAG
      (let* ((l1 (length num-goals))
	     (l2 (length (pproof-state-to-num-goals)))
	     (new-num-goals
	      (list-head (pproof-state-to-num-goals)
			 (- (+ l2 1) l1))))
	(if (pair? new-num-goals)
	    (begin
	      (for-each (lambda (g)
			  (newline)
			  (display-num-goal g))
			(reverse new-num-goals)))
	    (begin
	      (if (null? (pproof-state-to-num-goals))
		  (begin (newline) (display-comment "QED"))
		  (begin (display-num-goal
			  (car (pproof-state-to-num-goals))))))))))


(define (display-num-goal-aux num-goal f)
  (if
   COMMENT-FLAG
   (let* ((number (num-goal-to-number num-goal))
	  (goal (num-goal-to-goal num-goal))
	  (drop-info (num-goal-to-drop-info num-goal))
	  (hypname-info (num-goal-to-hypname-info num-goal))
	  (indices (hypname-info-to-indices hypname-info))
	  (context (goal-to-context goal))
	  (ncvars (goal-to-ncvars goal))
	  (formula (goal-to-formula goal))
	  (prefix "ZU ZEIGEN: "))
; 	  (goal-name (string-append DEFAULT-GOAL-NAME "_"
; 				    (number-to-string number)))
; 	  (prefix (string-append goal-name ": ")))
     (if (not COQ-GOAL-DISPLAY)
	 (begin
	   (newline)
	   (display-comment
	    prefix (string #\newline)
	    (pretty-print-string 0
				 (- pp-width (string-length COMMENT-STRING)) 
				 (f formula)))
; 	   (display-comment
; 	    prefix
; 	    (pretty-print-string (string-length prefix) 
; 				 (- pp-width (string-length COMMENT-STRING)) 
; 				 (f formula)))
	   (if (not (null? context))
	       (begin (newline)		      
		      (display-comment "WOBEI GEGEBEN IST")))	   
; 	       (display " from"))		   
	   (newline)))
     (do ((c context (cdr c))
	  (i 1 (if (avar? (car c)) (+ 1 i) i))
	  (line "" line))
	 ((null? c) (if (> (string-length line) 0) 
			(begin (display-comment line) (newline))))
       (if (avar? (car c))
	   (if (not (member i drop-info))
	       (let* ((info (member i indices))
		      (string
		       (if info
			   (index-and-hypname-info-to-name
			    i hypname-info)
			   (number-to-string i))))
		 (set! line (string-append line "  " string ":"))
		 (if (> (* 3 (string-length line)) pp-width)
		     (begin
		       (display-comment line)
		       (newline)
		       (set! line "    ")))
		 (set! line (string-append 
			     line 
			     (pretty-print-string
			      (string-length line)
			      (- pp-width (string-length COMMENT-STRING))
			      (f (avar-to-formula (car c))))))
		 (if (pair? (cdr c))
		     (begin (display-comment line) (newline)
			    (set! line "")))))
	   (let* ((var (car c))
		  (varstring (var-to-string var))
		  (cv? (not (member var ncvars)))
		  (mod-varstring
		   (if cv?
		       varstring
		       (string-append "{" varstring "}"))))
	     (set! line (string-append line "  " mod-varstring)))))
     (if COQ-GOAL-DISPLAY
	 (begin
	   (display-comment
	    "--------------------------------------------------")
	   (newline)
	   (display-comment
	    (pretty-print-string 0
				 (- pp-width (string-length COMMENT-STRING)) 
				 (f formula)))
	   (newline))))))





; Beweisstrategien ohne dummies

(define Behauptung_folgt_aus use)

(define benutze use)

(define (benutze_linke_Seite string)
  (use-with string 'left))

(define (benutze_rechte_Seite string)
  (use-with string 'right))

(define (Fallunterscheidung string)
  (cases(pt string)))

(define fix assume)

(define suche_einfachen_Beweis search)
; (define klar auto)

(define nicht_mehr_gebraucht drop)

(define nimm_an assume)

(define (nimm_das string)
  (ex-intro (pt string)))

(define (vereinfache)
  (ng #t))

(define zerlege_Behauptung split)

(define (zuzeigen string)
  (set-goal(pf string)))



; Beweisstrategien mit dummies

(define (kombiniere string0 string1 string2 string3 string4)
  (inst-with-to string0 string2 string4))

(define (nimm_ein string0 string1 string2 string3 string4)
  (by-assume-with string2 string0 string4))

(define (insbesondere_gilt string0 string1 string2)
  (assert (pf string2))
  (prop)
  (assume string0))

(define (verwende_gegebenes string0 string1 string2 string3 string4)
  (inst-with-to string0 (pt string2) string4))