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