make-rulenames
author nipkow
Tue May 09 22:10:08 1995 +0200 (1995-05-09)
changeset 1114 c8dfb56a7e95
parent 0 a5a9c433f639
permissions -rwxr-xr-x
Prod is now a parent of Lfp.
Added thm induct2 to Lfp.
Changed the way patterns in abstractions are pretty printed.
It has become simpler now but fails if split has more than one argument
because then the ast-translation does not match.
     1 #!/bin/sh
     2 #   Title: 	make-rulenames
     3 #   Author: 	Larry Paulson, Cambridge University Computer Laboratory
     4 #   Copyright   1990  University of Cambridge
     5 #
     6 #shell script for adding signature and val declarations to a rules file
     7 #  usage:  make-rulenames <directory>
     8 #
     9 #Input is the file ruleshell.ML, which defines a theory.
    10 #Output is .rules.ML
    11 #
    12 #
    13 #Rule lines begin with a line containing the word "extend_theory"
    14 #       and end   with a line containing the word "get_axiom"
    15 #
    16 #Each rule name xyz must appear on a line that begins
    17 #           <spaces> ("xyz"
    18 # ENSURE THAT THE FIRST RULE LINE DOES NOT CONTAIN A "[" CHARACTER!
    19 #The file RULESIG gets lines like	val Eq_comp: thm
    20 #    These are inserted after the line containing the string INSERT-RULESIG
    21 #
    22 #The file RULENAMES gets lines like	val Eq_comp = ax"Eq_comp";
    23 #    These are inserted after the line containing the string INSERT-RULENAMES
    24 #The input file should define the function "ax" above this point.
    25 #
    26 set -eu		#terminate if error or unset variable
    27 if [ ! '(' -d $1 -a -f $1/ruleshell.ML ')' ]; \
    28            then echo $1 is not a suitable directory; exit 1; \
    29            fi
    30 sed -n -e '/extend_theory/,/get_axiom/ s/^ *("\([^"]*\)".*$/  val \1: thm/p' $1/ruleshell.ML > RULESIG
    31 sed -n -e '/extend_theory/,/get_axiom/ s/^ *("\([^"]*\)".*$/val \1 = ax"\1";/p' $1/ruleshell.ML > RULENAMES
    32 sed -e '/INSERT-RULESIG/ r RULESIG
    33 /INSERT-RULENAMES/ r RULENAMES' $1/ruleshell.ML > $1/.rules.ML
    34 #WARNING: there must be no spaces after the filename in the "r" command!!
    35 rm RULESIG RULENAMES
    36