src/Tools/Metis/make_metis
author wenzelm
Sat, 09 Jul 2011 21:53:27 +0200
changeset 43721 fad8634cee62
parent 43268 c0eaa8b9bff5
child 56281 03c3d1a7c3b8
permissions -rwxr-xr-x
echo prover input via raw_messages, for improved protocol tracing;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
     1
#!/usr/bin/env bash
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
     2
#
39413
blanchet
parents: 39412
diff changeset
     3
# make_metis - turn original Metis files into Isabelle ML source.
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
     4
#
39427
a28be69dcb68 update comment
blanchet
parents: 39415
diff changeset
     5
# Signatures, structures, and functors are renamed to have a "Metis_" prefix.
a28be69dcb68 update comment
blanchet
parents: 39415
diff changeset
     6
# A few other ad hoc transformations are performed to ensure that the sources
a28be69dcb68 update comment
blanchet
parents: 39415
diff changeset
     7
# compile within Isabelle on Poly/ML and SML/NJ.
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
     8
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
     9
THIS=$(cd "$(dirname "$0")"; echo $PWD)
39433
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES";
blanchet
parents: 39427
diff changeset
    10
make -f Makefile.FILES refresh_FILES
39448
64639ff50fcd streamlined "make_metis"
blanchet
parents: 39433
diff changeset
    11
FILES=$(cat "$THIS/FILES")
39433
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES";
blanchet
parents: 39427
diff changeset
    12
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    13
(
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    14
  cat <<EOF
39411
ec989bd98fc8 use "Metis_" prefix rather than "Metis" structure;
blanchet
parents: 39350
diff changeset
    15
(*
39413
blanchet
parents: 39412
diff changeset
    16
   This file was generated by the "make_metis" script. The BSD License is used
39411
ec989bd98fc8 use "Metis_" prefix rather than "Metis" structure;
blanchet
parents: 39350
diff changeset
    17
   with Joe Hurd's kind permission. Extract from a September 13, 2010 email
ec989bd98fc8 use "Metis_" prefix rather than "Metis" structure;
blanchet
parents: 39350
diff changeset
    18
   written by Joe Hurd:
ec989bd98fc8 use "Metis_" prefix rather than "Metis" structure;
blanchet
parents: 39350
diff changeset
    19
ec989bd98fc8 use "Metis_" prefix rather than "Metis" structure;
blanchet
parents: 39350
diff changeset
    20
       I hereby give permission to the Isabelle team to release Metis as part
ec989bd98fc8 use "Metis_" prefix rather than "Metis" structure;
blanchet
parents: 39350
diff changeset
    21
       of Isabelle, with the Metis code covered under the Isabelle BSD
ec989bd98fc8 use "Metis_" prefix rather than "Metis" structure;
blanchet
parents: 39350
diff changeset
    22
       license.
ec989bd98fc8 use "Metis_" prefix rather than "Metis" structure;
blanchet
parents: 39350
diff changeset
    23
*)
ec989bd98fc8 use "Metis_" prefix rather than "Metis" structure;
blanchet
parents: 39350
diff changeset
    24
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    25
(******************************************************************)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    26
(* GENERATED FILE -- DO NOT EDIT -- GENERATED FILE -- DO NOT EDIT *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    27
(* GENERATED FILE -- DO NOT EDIT -- GENERATED FILE -- DO NOT EDIT *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    28
(* GENERATED FILE -- DO NOT EDIT -- GENERATED FILE -- DO NOT EDIT *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    29
(******************************************************************)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    30
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    31
print_depth 0;
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    32
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    33
EOF
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    34
39448
64639ff50fcd streamlined "make_metis"
blanchet
parents: 39433
diff changeset
    35
  for FILE in $FILES
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    36
  do
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    37
    echo
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    38
    echo "(**** Original file: $FILE ****)"
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    39
    echo
39411
ec989bd98fc8 use "Metis_" prefix rather than "Metis" structure;
blanchet
parents: 39350
diff changeset
    40
    echo -e "$FILE" >&2
39448
64639ff50fcd streamlined "make_metis"
blanchet
parents: 39433
diff changeset
    41
    "$THIS/scripts/mlpp" -c polyml "$FILE" | \
39411
ec989bd98fc8 use "Metis_" prefix rather than "Metis" structure;
blanchet
parents: 39350
diff changeset
    42
    perl -p -e \
ec989bd98fc8 use "Metis_" prefix rather than "Metis" structure;
blanchet
parents: 39350
diff changeset
    43
's/\bref\b/Unsynchronized.ref/g;'\
39448
64639ff50fcd streamlined "make_metis"
blanchet
parents: 39433
diff changeset
    44
"`grep "^\(signature\|structure\|functor\)" $FILES | \
39411
ec989bd98fc8 use "Metis_" prefix rather than "Metis" structure;
blanchet
parents: 39350
diff changeset
    45
  sed "s/[^:]*:[a-z]* \([A-Za-z0-9_]*\).*/\1/" | \
ec989bd98fc8 use "Metis_" prefix rather than "Metis" structure;
blanchet
parents: 39350
diff changeset
    46
  tr " " "\n" | \
ec989bd98fc8 use "Metis_" prefix rather than "Metis" structure;
blanchet
parents: 39350
diff changeset
    47
  sort | \
ec989bd98fc8 use "Metis_" prefix rather than "Metis" structure;
blanchet
parents: 39350
diff changeset
    48
  uniq | \
ec989bd98fc8 use "Metis_" prefix rather than "Metis" structure;
blanchet
parents: 39350
diff changeset
    49
  sed 's/\(.*\)/s\/\\\\b\1\\\\b\/Metis_\1\/g;/'`"
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    50
  done
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    51
39411
ec989bd98fc8 use "Metis_" prefix rather than "Metis" structure;
blanchet
parents: 39350
diff changeset
    52
  cat <<EOF
ec989bd98fc8 use "Metis_" prefix rather than "Metis" structure;
blanchet
parents: 39350
diff changeset
    53
;
ec989bd98fc8 use "Metis_" prefix rather than "Metis" structure;
blanchet
parents: 39350
diff changeset
    54
print_depth 10;
ec989bd98fc8 use "Metis_" prefix rather than "Metis" structure;
blanchet
parents: 39350
diff changeset
    55
EOF
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    56
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    57
) > metis.ML