;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; 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)
)