prove_goal.el

New bounded quantifier syntax: !x<i. P etc

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