clasohm@0: #!/bin/sh
clasohm@0: #   Title: 	get-rulenames  (see also make-rulenames)
clasohm@0: #   Author: 	Larry Paulson, Cambridge University Computer Laboratory
clasohm@0: #   Copyright   1990  University of Cambridge
clasohm@0: #
clasohm@0: #shell script to generate "val" declarations for a theory's axioms 
clasohm@0: #  also generates a comma-separated list of axiom names
clasohm@0: #
clasohm@0: #  usage:  make-rulenames  <file>
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: #Each rule name xyz must appear on a line that begins
clasohm@0: #        <spaces> ("xyz"
clasohm@0: #Output lines have the form
clasohm@0: #        val Eq_comp = ax"Eq_comp";
clasohm@0: #
clasohm@0: sed -n -e '/ext[end]*_theory/,/get_axiom/ s/^[ []*("\([^"]*\)".*$/val \1	= ax"\1";/p' $1
clasohm@0: echo
clasohm@0: echo `sed -n -e '/ext[end]*_theory/,/get_axiom/ s/^[ []*("\([^"]*\)".*$/\1/p' $1 | tr '\012' ','`