prove_goal.el

Declares the function exit_use to behave like use but fail if
errors are detected. It can be used in all Makefiles except Pure, which will
write the exception handler explicitly ("exit" will have been declared
already).

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; special function for Isabelle
;;
;;
; goalify.el
;
; Emacs command to change "goal" proofs to "prove_goal" proofs 
; and reverse IN A REGION.
;    [would be difficult in "sed" since replacements involve multiple lines]
;
;; origin is prove_goalify.el
;; enhanced by Franz Regensburger
;;    corrected some errors in regular expressions
;;    changed name prove_goalify --> goalify
;;    added inverse functions        ungoalify
;
; function goalify:
; 
; val PAT = goalARGS;$
; COMMANDS;$
; val ID = result();
; 
; to
; 
; val ID = prove_goalARGS
;  (fn PAT=>
;  [
;  COMMANDS
;  ]);
;;
;; Note: PAT must be an identifier. _ as pattern is not supported.
;;
; function ungoalify:
; 
; val ID = prove_goalARGS
;  (fn PAT=>
;  [
;  COMMANDS
;  ]);
;
;
; to 
; val PAT = goalARGS;$
; COMMANDS;$
; val ID = result();
; 


(defun ungoalify (alpha omega)
 "Change well-formed prove_goal proofs to goal...result"
  (interactive "r"
	       "*") 
  ; 0: restrict editing to region
  (narrow-to-region alpha omega)

  ; 1: insert delimiter ID 
  (goto-char (point-min))
  (replace-regexp  
  "[ \t]*val[ \t]+\\([^ \t\n=]+\\)[ \t\n=]+prove_goal" "\\1")

  ; 2: insertt delimiter ARGS  PAT  and  before first command   
  (goto-char (point-min))
  (replace-regexp  
  "[ \n\t]*(fn[ \t]+\\([^=]+\\)=>[^(]*" "\\1\n")

  ; 3: shift  over all commands
  ; Note: only one line per command
  (goto-char (point-max))
  (while (not (equal (point) (point-min)))
    (goto-char (point-min))
    (replace-regexp  
    "[ \t]*\\(.*\\),[ \t]*\n" "by \\1;\n"))
    
  ; 4: fix last 
  (goto-char (point-min))
  (replace-regexp  
    "[ \t]*\\(.*\\)[ \t\n]*\][ \t\n]*)[ \t\n]*;" "by \\1;")

  ; 5: arange new val Pat = goal .. 
  (goto-char (point-min))
  (replace-regexp  
  "\\([^]*\\)\\([^]*\\)\\([^]*\\)\n\\([^]*\\)"
  "val \\3= goal\\2;\n\\4\nval \\1 = result();")

  ; widen again
  (widen)
)


(defun goalify (alpha omega)
 "Change well-formed goal...result proofs to use prove_goal"
  (interactive "r"
               "*") 

  ; 0: restrict editing to region
  (narrow-to-region alpha omega)

  ; 1: delimit the identifier in "val ID = result()" using ^Q
  (goto-char (point-min))
  (replace-regexp  "val[ \t\n]+\\([^ \t\n=]+\\)[ \t\n=]+result();[ \t]*$"
   "\\1")

  ; 2: replace terminal \";  by  
  (goto-char (point-min))
  (replace-regexp  "\";[ \t]*$" "")

  ; 3: replace lines "by ...;" with "...,"
  (goto-char (point-min))
  (replace-regexp  "by[ \n\t]*\\([^;]*\\)[ \t\n]*;"  "\t\\1,")

  ; 4: removing the extra commas, those followed by ^Q
  (goto-char (point-min))
  (replace-regexp  ",[ \n\t]*"  "")

  ; 5: transforming goal... to prove_goal...
  (goto-char (point-min))
  (replace-regexp
  "val[ \t\n]+\\([^ \n\t=]+\\)[ \t\n=]+goal\\([^]*\\)
\\([^]*\\)\\([^]*\\)"  
  "val \\4 = prove_goal\\2\"\n (fn \\1 =>\n\t[\n\\3\n\t]);")

  ; 6: widen again
  (widen)
)