clasohm@0: #!/bin/sh
clasohm@0: #   Title: 	make-rulenames
clasohm@0: #   Author: 	Larry Paulson, Cambridge University Computer Laboratory
clasohm@0: #   Copyright   1990  University of Cambridge
clasohm@0: #
clasohm@0: #shell script for adding signature and val declarations to a rules file
clasohm@0: #  usage:  make-rulenames <directory>
clasohm@0: #
clasohm@0: #Input is the file ruleshell.ML, which defines a theory.
clasohm@0: #Output is .rules.ML
clasohm@0: #
clasohm@0: #
clasohm@0: #Rule lines begin with a line containing the word "extend_theory"
clasohm@0: #       and end   with a line containing the word "get_axiom"
clasohm@0: #
clasohm@0: #Each rule name xyz must appear on a line that begins
clasohm@0: #           <spaces> ("xyz"
clasohm@0: # ENSURE THAT THE FIRST RULE LINE DOES NOT CONTAIN A "[" CHARACTER!
clasohm@0: #The file RULESIG gets lines like	val Eq_comp: thm
clasohm@0: #    These are inserted after the line containing the string INSERT-RULESIG
clasohm@0: #
clasohm@0: #The file RULENAMES gets lines like	val Eq_comp = ax"Eq_comp";
clasohm@0: #    These are inserted after the line containing the string INSERT-RULENAMES
clasohm@0: #The input file should define the function "ax" above this point.
clasohm@0: #
clasohm@0: set -eu		#terminate if error or unset variable
clasohm@0: if [ ! '(' -d $1 -a -f $1/ruleshell.ML ')' ]; \
clasohm@0:            then echo $1 is not a suitable directory; exit 1; \
clasohm@0:            fi
clasohm@0: sed -n -e '/extend_theory/,/get_axiom/ s/^ *("\([^"]*\)".*$/  val \1: thm/p' $1/ruleshell.ML > RULESIG
clasohm@0: sed -n -e '/extend_theory/,/get_axiom/ s/^ *("\([^"]*\)".*$/val \1 = ax"\1";/p' $1/ruleshell.ML > RULENAMES
clasohm@0: sed -e '/INSERT-RULESIG/ r RULESIG
clasohm@0: /INSERT-RULENAMES/ r RULENAMES' $1/ruleshell.ML > $1/.rules.ML
clasohm@0: #WARNING: there must be no spaces after the filename in the "r" command!!
clasohm@0: rm RULESIG RULENAMES
clasohm@0: