| Quellcodebibliothek Statistik Leitseite products/sources/formale Sprachen/Isabelle/Tools/Metis/ (Beweissystem Isabelle Version 2025-1©) Datei vom 16.11.2025 mit Größe 1 kB |
|
Quelle make_metis Sprache: Text |
|||||||||
|
#!/usr/bin/env bash
# # make_metis - turn original Metis files into Isabelle ML source. # # Signatures, structures, and functors are renamed to have a "Metis_" prefix. # A few other ad hoc transformations are performed to ensure that the sources # compile within Isabelle on Poly/ML and SML/NJ. unset CDPATH THIS=$(cd "$(dirname "$0")"; echo $PWD) make -f Makefile.FILES refresh_FILES FILES=$(cat "$THIS/FILES") ( cat <<EOF (* This file was generated by the "make_metis" script. The BSD License is used with Joe Leslie-Hurd's kind permission. Extract from a September 13, 2010 email written by him: I hereby give permission to the Isabelle team to release Metis as part of Isabelle, with the Metis code covered under the Isabelle BSD license. *) (******************************************************************) (* GENERATED FILE -- DO NOT EDIT -- GENERATED FILE -- DO NOT EDIT *) (* GENERATED FILE -- DO NOT EDIT -- GENERATED FILE -- DO NOT EDIT *) (* GENERATED FILE -- DO NOT EDIT -- GENERATED FILE -- DO NOT EDIT *) (******************************************************************) EOF for FILE in $FILES do echo echo "(**** Original file: $FILE ****)" echo echo -e "$FILE" >&2 "$THIS/scripts/mlpp" -c polyml "$FILE" | \ perl -p -e \ 's/\bref\b/Unsynchronized.ref/g;'\ "`grep "^\(signature\|structure\|functor\)" $FILES | \ sed "s/[^:]*:[a-z]* \([A-Za-z0-9_]*\).*/\1/" | \ tr " " "\n" | \ sort | \ uniq | \ sed 's/\(.*\)/s\/\\\\b\1\\\\b\/Metis_\1\/g;/'`" done cat <<EOF ; EOF ) > metis.ML ¤ Dauer der Verarbeitung: 0.26 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28