prove_goal.el
author oheimb
Fri Jun 02 20:38:28 2000 +0200 (2000-06-02)
changeset 9028 8a1ec8f05f14
parent 0 a5a9c433f639
permissions -rw-r--r--
added HOL/Prolog
clasohm@0
     1
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
clasohm@0
     2
;; special function for Isabelle
clasohm@0
     3
;;
clasohm@0
     4
;;
clasohm@0
     5
; goalify.el
clasohm@0
     6
;
clasohm@0
     7
; Emacs command to change "goal" proofs to "prove_goal" proofs 
clasohm@0
     8
; and reverse IN A REGION.
clasohm@0
     9
;    [would be difficult in "sed" since replacements involve multiple lines]
clasohm@0
    10
;
clasohm@0
    11
;; origin is prove_goalify.el
clasohm@0
    12
;; enhanced by Franz Regensburger
clasohm@0
    13
;;    corrected some errors in regular expressions
clasohm@0
    14
;;    changed name prove_goalify --> goalify
clasohm@0
    15
;;    added inverse functions        ungoalify
clasohm@0
    16
;
clasohm@0
    17
; function goalify:
clasohm@0
    18
; 
clasohm@0
    19
; val PAT = goalARGS;$
clasohm@0
    20
; COMMANDS;$
clasohm@0
    21
; val ID = result();
clasohm@0
    22
; 
clasohm@0
    23
; to
clasohm@0
    24
; 
clasohm@0
    25
; val ID = prove_goalARGS
clasohm@0
    26
;  (fn PAT=>
clasohm@0
    27
;  [
clasohm@0
    28
;  COMMANDS
clasohm@0
    29
;  ]);
clasohm@0
    30
;;
clasohm@0
    31
;; Note: PAT must be an identifier. _ as pattern is not supported.
clasohm@0
    32
;;
clasohm@0
    33
; function ungoalify:
clasohm@0
    34
; 
clasohm@0
    35
; val ID = prove_goalARGS
clasohm@0
    36
;  (fn PAT=>
clasohm@0
    37
;  [
clasohm@0
    38
;  COMMANDS
clasohm@0
    39
;  ]);
clasohm@0
    40
;
clasohm@0
    41
;
clasohm@0
    42
; to 
clasohm@0
    43
; val PAT = goalARGS;$
clasohm@0
    44
; COMMANDS;$
clasohm@0
    45
; val ID = result();
clasohm@0
    46
; 
clasohm@0
    47
clasohm@0
    48
clasohm@0
    49
(defun ungoalify (alpha omega)
clasohm@0
    50
 "Change well-formed prove_goal proofs to goal...result"
clasohm@0
    51
  (interactive "r"
clasohm@0
    52
	       "*") 
clasohm@0
    53
  ; 0: restrict editing to region
clasohm@0
    54
  (narrow-to-region alpha omega)
clasohm@0
    55
clasohm@0
    56
  ; 1: insert delimiter ID 
clasohm@0
    57
  (goto-char (point-min))
clasohm@0
    58
  (replace-regexp  
clasohm@0
    59
  "[ \t]*val[ \t]+\\([^ \t\n=]+\\)[ \t\n=]+prove_goal" "\\1")
clasohm@0
    60
clasohm@0
    61
  ; 2: insertt delimiter ARGS  PAT  and  before first command   
clasohm@0
    62
  (goto-char (point-min))
clasohm@0
    63
  (replace-regexp  
clasohm@0
    64
  "[ \n\t]*(fn[ \t]+\\([^=]+\\)=>[^(]*" "\\1\n")
clasohm@0
    65
clasohm@0
    66
  ; 3: shift  over all commands
clasohm@0
    67
  ; Note: only one line per command
clasohm@0
    68
  (goto-char (point-max))
clasohm@0
    69
  (while (not (equal (point) (point-min)))
clasohm@0
    70
    (goto-char (point-min))
clasohm@0
    71
    (replace-regexp  
clasohm@0
    72
    "[ \t]*\\(.*\\),[ \t]*\n" "by \\1;\n"))
clasohm@0
    73
    
clasohm@0
    74
  ; 4: fix last 
clasohm@0
    75
  (goto-char (point-min))
clasohm@0
    76
  (replace-regexp  
clasohm@0
    77
    "[ \t]*\\(.*\\)[ \t\n]*\][ \t\n]*)[ \t\n]*;" "by \\1;")
clasohm@0
    78
clasohm@0
    79
  ; 5: arange new val Pat = goal .. 
clasohm@0
    80
  (goto-char (point-min))
clasohm@0
    81
  (replace-regexp  
clasohm@0
    82
  "\\([^]*\\)\\([^]*\\)\\([^]*\\)\n\\([^]*\\)"
clasohm@0
    83
  "val \\3= goal\\2;\n\\4\nval \\1 = result();")
clasohm@0
    84
clasohm@0
    85
  ; widen again
clasohm@0
    86
  (widen)
clasohm@0
    87
)
clasohm@0
    88
clasohm@0
    89
clasohm@0
    90
(defun goalify (alpha omega)
clasohm@0
    91
 "Change well-formed goal...result proofs to use prove_goal"
clasohm@0
    92
  (interactive "r"
clasohm@0
    93
               "*") 
clasohm@0
    94
clasohm@0
    95
  ; 0: restrict editing to region
clasohm@0
    96
  (narrow-to-region alpha omega)
clasohm@0
    97
clasohm@0
    98
  ; 1: delimit the identifier in "val ID = result()" using ^Q
clasohm@0
    99
  (goto-char (point-min))
clasohm@0
   100
  (replace-regexp  "val[ \t\n]+\\([^ \t\n=]+\\)[ \t\n=]+result();[ \t]*$"
clasohm@0
   101
   "\\1")
clasohm@0
   102
clasohm@0
   103
  ; 2: replace terminal \";  by  
clasohm@0
   104
  (goto-char (point-min))
clasohm@0
   105
  (replace-regexp  "\";[ \t]*$" "")
clasohm@0
   106
clasohm@0
   107
  ; 3: replace lines "by ...;" with "...,"
clasohm@0
   108
  (goto-char (point-min))
clasohm@0
   109
  (replace-regexp  "by[ \n\t]*\\([^;]*\\)[ \t\n]*;"  "\t\\1,")
clasohm@0
   110
clasohm@0
   111
  ; 4: removing the extra commas, those followed by ^Q
clasohm@0
   112
  (goto-char (point-min))
clasohm@0
   113
  (replace-regexp  ",[ \n\t]*"  "")
clasohm@0
   114
clasohm@0
   115
  ; 5: transforming goal... to prove_goal...
clasohm@0
   116
  (goto-char (point-min))
clasohm@0
   117
  (replace-regexp
clasohm@0
   118
  "val[ \t\n]+\\([^ \n\t=]+\\)[ \t\n=]+goal\\([^]*\\)
clasohm@0
   119
\\([^]*\\)\\([^]*\\)"  
clasohm@0
   120
  "val \\4 = prove_goal\\2\"\n (fn \\1 =>\n\t[\n\\3\n\t]);")
clasohm@0
   121
clasohm@0
   122
  ; 6: widen again
clasohm@0
   123
  (widen)
clasohm@0
   124
)
clasohm@0
   125