make-rulenames
author wenzelm
Fri Mar 07 15:30:23 1997 +0100 (1997-03-07)
changeset 2768 bc6d915b8019
parent 0 a5a9c433f639
permissions -rwxr-xr-x
renamed SYSTEM to RAW_ML_SYSTEM;
     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