get-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: 	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' ','`