get-rulenames
changeset 0 a5a9c433f639
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/get-rulenames	Thu Sep 16 12:20:38 1993 +0200
     1.3 @@ -0,0 +1,20 @@
     1.4 +#!/bin/sh
     1.5 +#   Title: 	get-rulenames  (see also make-rulenames)
     1.6 +#   Author: 	Larry Paulson, Cambridge University Computer Laboratory
     1.7 +#   Copyright   1990  University of Cambridge
     1.8 +#
     1.9 +#shell script to generate "val" declarations for a theory's axioms 
    1.10 +#  also generates a comma-separated list of axiom names
    1.11 +#
    1.12 +#  usage:  make-rulenames  <file>
    1.13 +#
    1.14 +#Rule lines begin with a line containing the word "extend_theory"
    1.15 +#       and end   with a line containing the word "get_axiom"
    1.16 +#Each rule name xyz must appear on a line that begins
    1.17 +#        <spaces> ("xyz"
    1.18 +#Output lines have the form
    1.19 +#        val Eq_comp = ax"Eq_comp";
    1.20 +#
    1.21 +sed -n -e '/ext[end]*_theory/,/get_axiom/ s/^[ []*("\([^"]*\)".*$/val \1	= ax"\1";/p' $1
    1.22 +echo
    1.23 +echo `sed -n -e '/ext[end]*_theory/,/get_axiom/ s/^[ []*("\([^"]*\)".*$/\1/p' $1 | tr '\012' ','`