;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

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

)