equal
deleted
inserted
replaced
1 #!/bin/sh |
|
2 # Title: make-rulenames |
|
3 # Author: Larry Paulson, Cambridge University Computer Laboratory |
|
4 # Copyright 1990 University of Cambridge |
|
5 # |
|
6 #shell script for adding signature and val declarations to a rules file |
|
7 # usage: make-rulenames <directory> |
|
8 # |
|
9 #Input is the file ruleshell.ML, which defines a theory. |
|
10 #Output is .rules.ML |
|
11 # |
|
12 # |
|
13 #Rule lines begin with a line containing the word "extend_theory" |
|
14 # and end with a line containing the word "get_axiom" |
|
15 # |
|
16 #Each rule name xyz must appear on a line that begins |
|
17 # <spaces> ("xyz" |
|
18 # ENSURE THAT THE FIRST RULE LINE DOES NOT CONTAIN A "[" CHARACTER! |
|
19 #The file RULESIG gets lines like val Eq_comp: thm |
|
20 # These are inserted after the line containing the string INSERT-RULESIG |
|
21 # |
|
22 #The file RULENAMES gets lines like val Eq_comp = ax"Eq_comp"; |
|
23 # These are inserted after the line containing the string INSERT-RULENAMES |
|
24 #The input file should define the function "ax" above this point. |
|
25 # |
|
26 set -eu #terminate if error or unset variable |
|
27 if [ ! '(' -d $1 -a -f $1/ruleshell.ML ')' ]; \ |
|
28 then echo $1 is not a suitable directory; exit 1; \ |
|
29 fi |
|
30 sed -n -e '/extend_theory/,/get_axiom/ s/^ *("\([^"]*\)".*$/ val \1: thm/p' $1/ruleshell.ML > RULESIG |
|
31 sed -n -e '/extend_theory/,/get_axiom/ s/^ *("\([^"]*\)".*$/val \1 = ax"\1";/p' $1/ruleshell.ML > RULENAMES |
|
32 sed -e '/INSERT-RULESIG/ r RULESIG |
|
33 /INSERT-RULENAMES/ r RULENAMES' $1/ruleshell.ML > $1/.rules.ML |
|
34 #WARNING: there must be no spaces after the filename in the "r" command!! |
|
35 rm RULESIG RULENAMES |
|
36 |
|