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;
     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 (* GENERATED FILE -- DO NOT EDIT -- GENERATED FILE -- DO NOT EDIT *)
    15 (* GENERATED FILE -- DO NOT EDIT -- GENERATED FILE -- DO NOT EDIT *)
    16 (* GENERATED FILE -- DO NOT EDIT -- GENERATED FILE -- DO NOT EDIT *)
    17 (******************************************************************)
    18 
    19 print_depth 0;
    20 
    21 structure Metis = struct structure Word = Word structure Array = Array end;
    22 EOF
    23 
    24   for FILE in $(cat "$THIS/src/FILES")
    25   do
    26     echo
    27     echo "(**** Original file: $FILE ****)"
    28     echo
    29     if [ "$(basename "$FILE" .sig)" != "$FILE" ]
    30     then
    31       echo -e "$FILE (global)" >&2
    32       "$THIS/scripts/mlpp" -c isabelle "src/$FILE" | \
    33       perl -p -e 's/\b([A-Za-z]+\.[A-Za-z]+)/Metis.\1/g;' -e 's/\bfrag\b/Metis.frag/;' | \
    34       perl -p -e 's/\bref\b/Unsynchronized.ref/g;'
    35     elif fgrep -q functor "src/$FILE"
    36     then
    37       "$THIS/scripts/mlpp" -c isabelle "src/$FILE" | \
    38       perl -p -e 's/ union / op union /g;' -e 's/ subset / op subset /g;' | \
    39       perl -p -e 's/\bref\b/Unsynchronized.ref/g;'
    40     else
    41       echo -e "$FILE (local)" >&2
    42       echo "structure Metis = struct open Metis"
    43       cat < "metis_env.ML"
    44       "$THIS/scripts/mlpp" -c isabelle "src/$FILE" | \
    45       perl -p -e 's/\bref\b/Unsynchronized.ref/g;'
    46       echo "end;"
    47     fi
    48   done
    49 
    50   echo "print_depth 10;"
    51 
    52 ) > metis.ML