1 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
2 ;; special function for Isabelle
7 ; Emacs command to change "goal" proofs to "prove_goal" proofs
8 ; and reverse IN A REGION.
9 ; [would be difficult in "sed" since replacements involve multiple lines]
11 ;; origin is prove_goalify.el
12 ;; enhanced by Franz Regensburger
13 ;; corrected some errors in regular expressions
14 ;; changed name prove_goalify --> goalify
15 ;; added inverse functions ungoalify
19 ; val PAT = goalARGS;$
25 ; val ID = prove_goalARGS
31 ;; Note: PAT must be an identifier. _ as pattern is not supported.
35 ; val ID = prove_goalARGS
43 ; val PAT = goalARGS;$
49 (defun ungoalify (alpha omega)
50 "Change well-formed prove_goal proofs to goal...result"
53 ; 0: restrict editing to region
54 (narrow-to-region alpha omega)
56 ; 1: insert delimiter ID
57 (goto-char (point-min))
59 "[ \t]*val[ \t]+\\([^ \t\n=]+\\)[ \t\n=]+prove_goal" "\\1")
61 ; 2: insertt delimiter ARGS PAT and before first command
62 (goto-char (point-min))
64 "[ \n\t]*(fn[ \t]+\\([^=]+\\)=>[^(]*" "\\1\n")
66 ; 3: shift over all commands
67 ; Note: only one line per command
68 (goto-char (point-max))
69 (while (not (equal (point) (point-min)))
70 (goto-char (point-min))
72 "[ \t]*\\(.*\\),[ \t]*\n" "by \\1;\n"))
75 (goto-char (point-min))
77 "[ \t]*\\(.*\\)[ \t\n]*\][ \t\n]*)[ \t\n]*;" "by \\1;")
79 ; 5: arange new val Pat = goal ..
80 (goto-char (point-min))
82 "\\([^]*\\)\\([^]*\\)\\([^]*\\)\n\\([^]*\\)"
83 "val \\3= goal\\2;\n\\4\nval \\1 = result();")
90 (defun goalify (alpha omega)
91 "Change well-formed goal...result proofs to use prove_goal"
95 ; 0: restrict editing to region
96 (narrow-to-region alpha omega)
98 ; 1: delimit the identifier in "val ID = result()" using ^Q
99 (goto-char (point-min))
100 (replace-regexp "val[ \t\n]+\\([^ \t\n=]+\\)[ \t\n=]+result();[ \t]*$"
103 ; 2: replace terminal \"; by
104 (goto-char (point-min))
105 (replace-regexp "\";[ \t]*$" "")
107 ; 3: replace lines "by ...;" with "...,"
108 (goto-char (point-min))
109 (replace-regexp "by[ \n\t]*\\([^;]*\\)[ \t\n]*;" "\t\\1,")
111 ; 4: removing the extra commas, those followed by ^Q
112 (goto-char (point-min))
113 (replace-regexp ",[ \n\t]*" "")
115 ; 5: transforming goal... to prove_goal...
116 (goto-char (point-min))
118 "val[ \t\n]+\\([^ \n\t=]+\\)[ \t\n=]+goal\\([^]*\\)
119 \\([^]*\\)\\([^]*\\)"
120 "val \\4 = prove_goal\\2\"\n (fn \\1 =>\n\t[\n\\3\n\t]);")