get-rulenames
author paulson
Fri, 29 Nov 1996 18:03:21 +0100
changeset 2284 80ebd1a213fd
parent 0 a5a9c433f639
permissions -rwxr-xr-x
Swapped arguments of Crypt (for clarity and because it is conventional)
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: 	get-rulenames  (see also 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 to generate "val" declarations for a theory's axioms 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     7
#  also generates a comma-separated list of axiom names
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     8
#
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     9
#  usage:  make-rulenames  <file>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    10
#
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    11
#Rule lines begin with a line containing the word "extend_theory"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    12
#       and end   with a line containing the word "get_axiom"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    13
#Each rule name xyz must appear on a line that begins
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    14
#        <spaces> ("xyz"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    15
#Output lines have the form
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    16
#        val Eq_comp = ax"Eq_comp";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    17
#
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    18
sed -n -e '/ext[end]*_theory/,/get_axiom/ s/^[ []*("\([^"]*\)".*$/val \1	= ax"\1";/p' $1
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    19
echo
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    20
echo `sed -n -e '/ext[end]*_theory/,/get_axiom/ s/^[ []*("\([^"]*\)".*$/\1/p' $1 | tr '\012' ','`