equal
deleted
inserted
replaced
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' ','` |
|