(synonyms ann string) 

(define pc-atom?
  {A --> boolean}
   P -> (and (symbol? P) (not (== P =>)) (not (== P ~))))

(datatype wff

  if (pc-atom? P)
  ____________
  P : atom;

  P : atom;
  _______
  P : wff;

  P : wff;
  ============
  [~ P] : wff;
  
  P : wff; Q : wff;
  =================
  [P => Q] : wff;)
  
(datatype axiom

   P : wff; Q : wff;
   _________________
   (scheme1 P Q) : axiom; 

   P : wff; Q : wff; R : wff;
   __________________________
   (scheme2 P Q R) : axiom; 

   P : wff; Q : wff;
   _________________
   (scheme3 P Q) : axiom;)

(datatype proof

  ___________
  [] : proof;  
  
  Step : axiom; Proof : proof;
  ____________________________
  (append Proof [Step]) : proof;
  
  M : number; N : number; Proof : proof;
  _______________________________________
  (append Proof [(mp* (nth M Proof) (nth N Proof))]) : proof;

  Proof : (list wff) >> P;
  ________________________
  Proof : proof >> P;)
  
(define scheme1
  {wff --> wff --> wff}
   P Q -> [Q => [P => Q]])
	  
(define scheme2
  {wff --> wff --> wff --> wff}
   P Q R -> [[P => [Q => R]] => [[P => Q] => [P => R]]])
   
(define scheme3
  {wff --> wff --> wff}
   P Q -> [[[~ P] => [~ Q]] => [[[~ P] => Q] => P]])

(define mp*
  {wff --> wff --> wff}
   P [P => Q] -> Q)
   
(define mp
  {number --> number --> proof --> proof}
   M N Proof -> (trap-error (append Proof [(mp* (nth M Proof) (nth N Proof))])
                            (/. E (do (output "mp failure~%") Proof))))   

(define a1
  {wff --> wff --> proof --> proof}
   P Q Proof -> (append Proof [(scheme1 P Q)]))   
   
(define a2
  {wff --> wff --> wff --> proof --> proof} 
   P Q R Proof -> (append Proof [(scheme2 P Q R)]))

(define a3
  {wff --> wff --> proof --> proof} 
   P Q Proof -> (append Proof [(scheme3 P Q)]))    

(define hilbert
  {wff --> (proof * (list ann))}
   P -> (hilbert-loop P [] []))

(define hilbert-loop
  {wff --> proof --> (list ann) --> (proof * (list ann))}
   P Proof Ann -> (@p Proof Ann)		where (end-proof? Proof P) 
   P Proof Ann -> (let NL (nl)
                       Show (print-proof 1 Proof Ann)
                       Ask (ask)
                       It (it)
		                   (if (= It "stop")  
		                      (error "exit~%") 
		                      (hilbert-loop P (Ask Proof) (append Ann [It])))))

(define stop
  {proof --> proof}
   X -> X) 
                        
(define end-proof?
  {(list wff) --> wff --> boolean}
   [P] P -> true
   [_ P | Ps] Q -> (end-proof? [P | Ps] Q)
   _ _ -> false)

(define print-proof
  {number --> (list wff) --> (list ann) --> symbol}
   _ [] [] -> skip
   N [Step | Proof] [Ann | Anns] -> (do (output "~A. ~R   ~A~%" N Step Ann) 
			                (print-proof (+ N 1) Proof Anns)))

(define ask
  {--> (proof --> proof)}
   -> (let Prompt (output "~%> ")
               (trap-error (input+ (proof --> proof)) 
                           (/. E (do (output (error-to-string E))
		           (nl)
		           (ask))))))