src/Tools/Metis/make-metis
author wenzelm
Tue Sep 29 16:24:36 2009 +0200 (2009-09-29)
changeset 32740 9dd0a2f83429
parent 30161 c26e515f1c29
child 39350 a47de56ae6c2
permissions -rwxr-xr-x
explicit indication of Unsynchronized.ref;
wenzelm@23442
     1
#!/usr/bin/env bash
wenzelm@23442
     2
#
wenzelm@23442
     3
# make-metis - turn original Metis files into Isabelle ML source.
wenzelm@23442
     4
#
wenzelm@23442
     5
# Structure declarations etc. are made local by wrapping into a
wenzelm@23442
     6
# collective structure Metis.  Signature and functor definitions are
wenzelm@23442
     7
# global!
wenzelm@23442
     8
wenzelm@23442
     9
THIS=$(cd "$(dirname "$0")"; echo $PWD)
wenzelm@23442
    10
wenzelm@23442
    11
(
wenzelm@23442
    12
  cat <<EOF
wenzelm@23442
    13
(******************************************************************)
wenzelm@23442
    14
(* GENERATED FILE -- DO NOT EDIT -- GENERATED FILE -- DO NOT EDIT *)
wenzelm@23442
    15
(* GENERATED FILE -- DO NOT EDIT -- GENERATED FILE -- DO NOT EDIT *)
wenzelm@23442
    16
(* GENERATED FILE -- DO NOT EDIT -- GENERATED FILE -- DO NOT EDIT *)
wenzelm@23442
    17
(******************************************************************)
wenzelm@23442
    18
wenzelm@23442
    19
print_depth 0;
wenzelm@23442
    20
paulson@25430
    21
structure Metis = struct structure Word = Word structure Array = Array end;
wenzelm@23442
    22
EOF
wenzelm@23442
    23
wenzelm@23442
    24
  for FILE in $(cat "$THIS/src/FILES")
wenzelm@23442
    25
  do
wenzelm@23442
    26
    echo
wenzelm@23442
    27
    echo "(**** Original file: $FILE ****)"
wenzelm@23442
    28
    echo
wenzelm@23442
    29
    if [ "$(basename "$FILE" .sig)" != "$FILE" ]
wenzelm@23442
    30
    then
wenzelm@23442
    31
      echo -e "$FILE (global)" >&2
wenzelm@23442
    32
      "$THIS/scripts/mlpp" -c isabelle "src/$FILE" | \
wenzelm@32740
    33
      perl -p -e 's/\b([A-Za-z]+\.[A-Za-z]+)/Metis.\1/g;' -e 's/\bfrag\b/Metis.frag/;' | \
wenzelm@32740
    34
      perl -p -e 's/\bref\b/Unsynchronized.ref/g;'
wenzelm@23442
    35
    elif fgrep -q functor "src/$FILE"
wenzelm@23442
    36
    then
wenzelm@23442
    37
      "$THIS/scripts/mlpp" -c isabelle "src/$FILE" | \
wenzelm@32740
    38
      perl -p -e 's/ union / op union /g;' -e 's/ subset / op subset /g;' | \
wenzelm@32740
    39
      perl -p -e 's/\bref\b/Unsynchronized.ref/g;'
wenzelm@23442
    40
    else
wenzelm@23442
    41
      echo -e "$FILE (local)" >&2
wenzelm@23442
    42
      echo "structure Metis = struct open Metis"
wenzelm@23452
    43
      cat < "metis_env.ML"
wenzelm@32740
    44
      "$THIS/scripts/mlpp" -c isabelle "src/$FILE" | \
wenzelm@32740
    45
      perl -p -e 's/\bref\b/Unsynchronized.ref/g;'
wenzelm@23442
    46
      echo "end;"
wenzelm@23442
    47
    fi
wenzelm@23442
    48
  done
wenzelm@23442
    49
wenzelm@23442
    50
  echo "print_depth 10;"
wenzelm@23442
    51
wenzelm@23442
    52
) > metis.ML