make-rulenames
author paulson
Tue, 23 Jul 2002 15:07:12 +0200
changeset 13409 d4ea094c650e
parent 0 a5a9c433f639
permissions -rwxr-xr-x
Relativization and Separation for the function "nth"
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     1
#!/bin/sh
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     2
#   Title: 	make-rulenames
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     3
#   Author: 	Larry Paulson, Cambridge University Computer Laboratory
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     4
#   Copyright   1990  University of Cambridge
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     5
#
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     6
#shell script for adding signature and val declarations to a rules file
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     7
#  usage:  make-rulenames <directory>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     8
#
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     9
#Input is the file ruleshell.ML, which defines a theory.
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    10
#Output is .rules.ML
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    11
#
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    12
#
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    13
#Rule lines begin with a line containing the word "extend_theory"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    14
#       and end   with a line containing the word "get_axiom"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    15
#
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    16
#Each rule name xyz must appear on a line that begins
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    17
#           <spaces> ("xyz"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    18
# ENSURE THAT THE FIRST RULE LINE DOES NOT CONTAIN A "[" CHARACTER!
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    19
#The file RULESIG gets lines like	val Eq_comp: thm
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    20
#    These are inserted after the line containing the string INSERT-RULESIG
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    21
#
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    22
#The file RULENAMES gets lines like	val Eq_comp = ax"Eq_comp";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    23
#    These are inserted after the line containing the string INSERT-RULENAMES
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    24
#The input file should define the function "ax" above this point.
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    25
#
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    26
set -eu		#terminate if error or unset variable
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    27
if [ ! '(' -d $1 -a -f $1/ruleshell.ML ')' ]; \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    28
           then echo $1 is not a suitable directory; exit 1; \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    29
           fi
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    30
sed -n -e '/extend_theory/,/get_axiom/ s/^ *("\([^"]*\)".*$/  val \1: thm/p' $1/ruleshell.ML > RULESIG
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    31
sed -n -e '/extend_theory/,/get_axiom/ s/^ *("\([^"]*\)".*$/val \1 = ax"\1";/p' $1/ruleshell.ML > RULENAMES
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    32
sed -e '/INSERT-RULESIG/ r RULESIG
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    33
/INSERT-RULENAMES/ r RULENAMES' $1/ruleshell.ML > $1/.rules.ML
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    34
#WARNING: there must be no spaces after the filename in the "r" command!!
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    35
rm RULESIG RULENAMES
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    36