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