make-rulenames
author nipkow
Tue, 09 May 1995 22:10:08 +0200
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.
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