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