|
1 #!/usr/bin/env bash |
|
2 # |
|
3 # make-metis - turn original Metis files into Isabelle ML source. |
|
4 # |
|
5 # Structure declarations etc. are made local by wrapping into a |
|
6 # collective structure Metis. Signature and functor definitions are |
|
7 # global! |
|
8 |
|
9 THIS=$(cd "$(dirname "$0")"; echo $PWD) |
|
10 |
|
11 ( |
|
12 cat <<EOF |
|
13 (* |
|
14 This file was generated by the "make-metis" script. The BSD License is used |
|
15 with Joe Hurd's kind permission. Extract from a September 13, 2010 email |
|
16 written by Joe Hurd: |
|
17 |
|
18 I hereby give permission to the Isabelle team to release Metis as part |
|
19 of Isabelle, with the Metis code covered under the Isabelle BSD |
|
20 license. |
|
21 *) |
|
22 |
|
23 (******************************************************************) |
|
24 (* GENERATED FILE -- DO NOT EDIT -- GENERATED FILE -- DO NOT EDIT *) |
|
25 (* GENERATED FILE -- DO NOT EDIT -- GENERATED FILE -- DO NOT EDIT *) |
|
26 (* GENERATED FILE -- DO NOT EDIT -- GENERATED FILE -- DO NOT EDIT *) |
|
27 (******************************************************************) |
|
28 |
|
29 print_depth 0; |
|
30 |
|
31 EOF |
|
32 |
|
33 for FILE in $(cat "$THIS/FILES") |
|
34 do |
|
35 echo |
|
36 echo "(**** Original file: $FILE ****)" |
|
37 echo |
|
38 echo -e "$FILE" >&2 |
|
39 "$THIS/scripts/mlpp" -c polyml "src/$FILE" | \ |
|
40 perl -p -e \ |
|
41 's/type name$/type name = string/;'\ |
|
42 's/\bref\b/Unsynchronized.ref/g;'\ |
|
43 's/\bPolyML.pointerEq\b/pointer_eq/g;'\ |
|
44 's/(?<!\.)\bexplode\b/String.explode/g;'\ |
|
45 's/(?<!\.)\bimplode\b/String.implode/g;'\ |
|
46 's/(?<!\.)\bprint\b/TextIO.print/g;'\ |
|
47 's/\bRL\b/Metis_RL/g;'\ |
|
48 "`grep "^\(signature\|structure\|functor\)" src/*.{sig,sml} | \ |
|
49 sed "s/[^:]*:[a-z]* \([A-Za-z0-9_]*\).*/\1/" | \ |
|
50 tr " " "\n" | \ |
|
51 sort | \ |
|
52 uniq | \ |
|
53 sed 's/\(.*\)/s\/\\\\b\1\\\\b\/Metis_\1\/g;/'`" |
|
54 done |
|
55 |
|
56 cat <<EOF |
|
57 ; |
|
58 print_depth 10; |
|
59 EOF |
|
60 |
|
61 ) > metis.ML |