prove_goal.el

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/prove_goal.el	Thu Sep 16 12:20:38 1993 +0200
@@ -0,0 +1,125 @@
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; 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)
+)
+