0

1 
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;


2 
;; special function for Isabelle


3 
;;


4 
;;


5 
; goalify.el


6 
;


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]


10 
;


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


16 
;


17 
; function goalify:


18 
;


19 
; val PAT = goalARGS;$


20 
; COMMANDS;$


21 
; val ID = result();


22 
;


23 
; to


24 
;


25 
; val ID = prove_goalARGS


26 
; (fn PAT=>


27 
; [


28 
; COMMANDS


29 
; ]);


30 
;;


31 
;; Note: PAT must be an identifier. _ as pattern is not supported.


32 
;;


33 
; function ungoalify:


34 
;


35 
; val ID = prove_goalARGS


36 
; (fn PAT=>


37 
; [


38 
; COMMANDS


39 
; ]);


40 
;


41 
;


42 
; to


43 
; val PAT = goalARGS;$


44 
; COMMANDS;$


45 
; val ID = result();


46 
;


47 


48 


49 
(defun ungoalify (alpha omega)


50 
"Change wellformed prove_goal proofs to goal...result"


51 
(interactive "r"


52 
"*")


53 
; 0: restrict editing to region


54 
(narrowtoregion alpha omega)


55 


56 
; 1: insert delimiter ID


57 
(gotochar (pointmin))


58 
(replaceregexp


59 
"[ \t]*val[ \t]+\\([^ \t\n=]+\\)[ \t\n=]+prove_goal" "\\1")


60 


61 
; 2: insertt delimiter ARGS PAT and before first command


62 
(gotochar (pointmin))


63 
(replaceregexp


64 
"[ \n\t]*(fn[ \t]+\\([^=]+\\)=>[^(]*" "\\1\n")


65 


66 
; 3: shift over all commands


67 
; Note: only one line per command


68 
(gotochar (pointmax))


69 
(while (not (equal (point) (pointmin)))


70 
(gotochar (pointmin))


71 
(replaceregexp


72 
"[ \t]*\\(.*\\),[ \t]*\n" "by \\1;\n"))


73 


74 
; 4: fix last


75 
(gotochar (pointmin))


76 
(replaceregexp


77 
"[ \t]*\\(.*\\)[ \t\n]*\][ \t\n]*)[ \t\n]*;" "by \\1;")


78 


79 
; 5: arange new val Pat = goal ..


80 
(gotochar (pointmin))


81 
(replaceregexp


82 
"\\([^]*\\)\\([^]*\\)\\([^]*\\)\n\\([^]*\\)"


83 
"val \\3= goal\\2;\n\\4\nval \\1 = result();")


84 


85 
; widen again


86 
(widen)


87 
)


88 


89 


90 
(defun goalify (alpha omega)


91 
"Change wellformed goal...result proofs to use prove_goal"


92 
(interactive "r"


93 
"*")


94 


95 
; 0: restrict editing to region


96 
(narrowtoregion alpha omega)


97 


98 
; 1: delimit the identifier in "val ID = result()" using ^Q


99 
(gotochar (pointmin))


100 
(replaceregexp "val[ \t\n]+\\([^ \t\n=]+\\)[ \t\n=]+result();[ \t]*$"


101 
"\\1")


102 


103 
; 2: replace terminal \"; by


104 
(gotochar (pointmin))


105 
(replaceregexp "\";[ \t]*$" "")


106 


107 
; 3: replace lines "by ...;" with "...,"


108 
(gotochar (pointmin))


109 
(replaceregexp "by[ \n\t]*\\([^;]*\\)[ \t\n]*;" "\t\\1,")


110 


111 
; 4: removing the extra commas, those followed by ^Q


112 
(gotochar (pointmin))


113 
(replaceregexp ",[ \n\t]*" "")


114 


115 
; 5: transforming goal... to prove_goal...


116 
(gotochar (pointmin))


117 
(replaceregexp


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


121 


122 
; 6: widen again


123 
(widen)


124 
)


125 
