| 0 |      1 | #!/bin/sh
 | 
|  |      2 | #   Title: 	get-rulenames  (see also make-rulenames)
 | 
|  |      3 | #   Author: 	Larry Paulson, Cambridge University Computer Laboratory
 | 
|  |      4 | #   Copyright   1990  University of Cambridge
 | 
|  |      5 | #
 | 
|  |      6 | #shell script to generate "val" declarations for a theory's axioms 
 | 
|  |      7 | #  also generates a comma-separated list of axiom names
 | 
|  |      8 | #
 | 
|  |      9 | #  usage:  make-rulenames  <file>
 | 
|  |     10 | #
 | 
|  |     11 | #Rule lines begin with a line containing the word "extend_theory"
 | 
|  |     12 | #       and end   with a line containing the word "get_axiom"
 | 
|  |     13 | #Each rule name xyz must appear on a line that begins
 | 
|  |     14 | #        <spaces> ("xyz"
 | 
|  |     15 | #Output lines have the form
 | 
|  |     16 | #        val Eq_comp = ax"Eq_comp";
 | 
|  |     17 | #
 | 
|  |     18 | sed -n -e '/ext[end]*_theory/,/get_axiom/ s/^[ []*("\([^"]*\)".*$/val \1	= ax"\1";/p' $1
 | 
|  |     19 | echo
 | 
|  |     20 | echo `sed -n -e '/ext[end]*_theory/,/get_axiom/ s/^[ []*("\([^"]*\)".*$/\1/p' $1 | tr '\012' ','`
 |