src/Tools/Metis/make-metis
author wenzelm
Fri, 02 Oct 2009 22:15:08 +0200
changeset 32861 105f40051387
parent 32740 9dd0a2f83429
child 39350 a47de56ae6c2
permissions -rwxr-xr-x
eliminated dead code;
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
#
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
     3
# make-metis - turn original Metis files into Isabelle ML source.
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
     4
#
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
     5
# Structure declarations etc. are made local by wrapping into a
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
     6
# collective structure Metis.  Signature and functor definitions are
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
     7
# global!
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)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    10
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    11
(
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    12
  cat <<EOF
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
(* GENERATED FILE -- DO NOT EDIT -- GENERATED FILE -- DO NOT EDIT *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    15
(* GENERATED FILE -- DO NOT EDIT -- GENERATED FILE -- DO NOT EDIT *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    16
(* GENERATED FILE -- DO NOT EDIT -- GENERATED FILE -- DO NOT EDIT *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    17
(******************************************************************)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    18
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    19
print_depth 0;
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    20
25430
372d6749f00e patching in the latest changes from Hurd
paulson
parents: 23452
diff changeset
    21
structure Metis = struct structure Word = Word structure Array = Array end;
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    22
EOF
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    23
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    24
  for FILE in $(cat "$THIS/src/FILES")
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    25
  do
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    26
    echo
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    27
    echo "(**** Original file: $FILE ****)"
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    28
    echo
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    29
    if [ "$(basename "$FILE" .sig)" != "$FILE" ]
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    30
    then
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    31
      echo -e "$FILE (global)" >&2
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    32
      "$THIS/scripts/mlpp" -c isabelle "src/$FILE" | \
32740
9dd0a2f83429 explicit indication of Unsynchronized.ref;
wenzelm
parents: 30161
diff changeset
    33
      perl -p -e 's/\b([A-Za-z]+\.[A-Za-z]+)/Metis.\1/g;' -e 's/\bfrag\b/Metis.frag/;' | \
9dd0a2f83429 explicit indication of Unsynchronized.ref;
wenzelm
parents: 30161
diff changeset
    34
      perl -p -e 's/\bref\b/Unsynchronized.ref/g;'
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    35
    elif fgrep -q functor "src/$FILE"
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    36
    then
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    37
      "$THIS/scripts/mlpp" -c isabelle "src/$FILE" | \
32740
9dd0a2f83429 explicit indication of Unsynchronized.ref;
wenzelm
parents: 30161
diff changeset
    38
      perl -p -e 's/ union / op union /g;' -e 's/ subset / op subset /g;' | \
9dd0a2f83429 explicit indication of Unsynchronized.ref;
wenzelm
parents: 30161
diff changeset
    39
      perl -p -e 's/\bref\b/Unsynchronized.ref/g;'
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    40
    else
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    41
      echo -e "$FILE (local)" >&2
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    42
      echo "structure Metis = struct open Metis"
23452
95b70054bb3a renamed metis-env.ML to metis_env.ML;
wenzelm
parents: 23448
diff changeset
    43
      cat < "metis_env.ML"
32740
9dd0a2f83429 explicit indication of Unsynchronized.ref;
wenzelm
parents: 30161
diff changeset
    44
      "$THIS/scripts/mlpp" -c isabelle "src/$FILE" | \
9dd0a2f83429 explicit indication of Unsynchronized.ref;
wenzelm
parents: 30161
diff changeset
    45
      perl -p -e 's/\bref\b/Unsynchronized.ref/g;'
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    46
      echo "end;"
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    47
    fi
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    48
  done
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    49
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    50
  echo "print_depth 10;"
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    51
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    52
) > metis.ML