clasohm@0: ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
clasohm@0: ;; special function for Isabelle
clasohm@0: ;;
clasohm@0: ;;
clasohm@0: ; goalify.el
clasohm@0: ;
clasohm@0: ; Emacs command to change "goal" proofs to "prove_goal" proofs 
clasohm@0: ; and reverse IN A REGION.
clasohm@0: ;    [would be difficult in "sed" since replacements involve multiple lines]
clasohm@0: ;
clasohm@0: ;; origin is prove_goalify.el
clasohm@0: ;; enhanced by Franz Regensburger
clasohm@0: ;;    corrected some errors in regular expressions
clasohm@0: ;;    changed name prove_goalify --> goalify
clasohm@0: ;;    added inverse functions        ungoalify
clasohm@0: ;
clasohm@0: ; function goalify:
clasohm@0: ; 
clasohm@0: ; val PAT = goalARGS;$
clasohm@0: ; COMMANDS;$
clasohm@0: ; val ID = result();
clasohm@0: ; 
clasohm@0: ; to
clasohm@0: ; 
clasohm@0: ; val ID = prove_goalARGS
clasohm@0: ;  (fn PAT=>
clasohm@0: ;  [
clasohm@0: ;  COMMANDS
clasohm@0: ;  ]);
clasohm@0: ;;
clasohm@0: ;; Note: PAT must be an identifier. _ as pattern is not supported.
clasohm@0: ;;
clasohm@0: ; function ungoalify:
clasohm@0: ; 
clasohm@0: ; val ID = prove_goalARGS
clasohm@0: ;  (fn PAT=>
clasohm@0: ;  [
clasohm@0: ;  COMMANDS
clasohm@0: ;  ]);
clasohm@0: ;
clasohm@0: ;
clasohm@0: ; to 
clasohm@0: ; val PAT = goalARGS;$
clasohm@0: ; COMMANDS;$
clasohm@0: ; val ID = result();
clasohm@0: ; 
clasohm@0: 
clasohm@0: 
clasohm@0: (defun ungoalify (alpha omega)
clasohm@0:  "Change well-formed prove_goal proofs to goal...result"
clasohm@0:   (interactive "r"
clasohm@0: 	       "*") 
clasohm@0:   ; 0: restrict editing to region
clasohm@0:   (narrow-to-region alpha omega)
clasohm@0: 
clasohm@0:   ; 1: insert delimiter ID 
clasohm@0:   (goto-char (point-min))
clasohm@0:   (replace-regexp  
clasohm@0:   "[ \t]*val[ \t]+\\([^ \t\n=]+\\)[ \t\n=]+prove_goal" "\\1")
clasohm@0: 
clasohm@0:   ; 2: insertt delimiter ARGS  PAT  and  before first command   
clasohm@0:   (goto-char (point-min))
clasohm@0:   (replace-regexp  
clasohm@0:   "[ \n\t]*(fn[ \t]+\\([^=]+\\)=>[^(]*" "\\1\n")
clasohm@0: 
clasohm@0:   ; 3: shift  over all commands
clasohm@0:   ; Note: only one line per command
clasohm@0:   (goto-char (point-max))
clasohm@0:   (while (not (equal (point) (point-min)))
clasohm@0:     (goto-char (point-min))
clasohm@0:     (replace-regexp  
clasohm@0:     "[ \t]*\\(.*\\),[ \t]*\n" "by \\1;\n"))
clasohm@0:     
clasohm@0:   ; 4: fix last 
clasohm@0:   (goto-char (point-min))
clasohm@0:   (replace-regexp  
clasohm@0:     "[ \t]*\\(.*\\)[ \t\n]*\][ \t\n]*)[ \t\n]*;" "by \\1;")
clasohm@0: 
clasohm@0:   ; 5: arange new val Pat = goal .. 
clasohm@0:   (goto-char (point-min))
clasohm@0:   (replace-regexp  
clasohm@0:   "\\([^]*\\)\\([^]*\\)\\([^]*\\)\n\\([^]*\\)"
clasohm@0:   "val \\3= goal\\2;\n\\4\nval \\1 = result();")
clasohm@0: 
clasohm@0:   ; widen again
clasohm@0:   (widen)
clasohm@0: )
clasohm@0: 
clasohm@0: 
clasohm@0: (defun goalify (alpha omega)
clasohm@0:  "Change well-formed goal...result proofs to use prove_goal"
clasohm@0:   (interactive "r"
clasohm@0:                "*") 
clasohm@0: 
clasohm@0:   ; 0: restrict editing to region
clasohm@0:   (narrow-to-region alpha omega)
clasohm@0: 
clasohm@0:   ; 1: delimit the identifier in "val ID = result()" using ^Q
clasohm@0:   (goto-char (point-min))
clasohm@0:   (replace-regexp  "val[ \t\n]+\\([^ \t\n=]+\\)[ \t\n=]+result();[ \t]*$"
clasohm@0:    "\\1")
clasohm@0: 
clasohm@0:   ; 2: replace terminal \";  by  
clasohm@0:   (goto-char (point-min))
clasohm@0:   (replace-regexp  "\";[ \t]*$" "")
clasohm@0: 
clasohm@0:   ; 3: replace lines "by ...;" with "...,"
clasohm@0:   (goto-char (point-min))
clasohm@0:   (replace-regexp  "by[ \n\t]*\\([^;]*\\)[ \t\n]*;"  "\t\\1,")
clasohm@0: 
clasohm@0:   ; 4: removing the extra commas, those followed by ^Q
clasohm@0:   (goto-char (point-min))
clasohm@0:   (replace-regexp  ",[ \n\t]*"  "")
clasohm@0: 
clasohm@0:   ; 5: transforming goal... to prove_goal...
clasohm@0:   (goto-char (point-min))
clasohm@0:   (replace-regexp
clasohm@0:   "val[ \t\n]+\\([^ \n\t=]+\\)[ \t\n=]+goal\\([^]*\\)
clasohm@0: \\([^]*\\)\\([^]*\\)"  
clasohm@0:   "val \\4 = prove_goal\\2\"\n (fn \\1 =>\n\t[\n\\3\n\t]);")
clasohm@0: 
clasohm@0:   ; 6: widen again
clasohm@0:   (widen)
clasohm@0: )
clasohm@0: