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