* HOL-Word:
New extensive library and type for generic, fixed size machine
words, with arithemtic, bit-wise, shifting and rotating operations,
reflection into int, nat, and bool lists, automation for linear
arithmetic (by automatic reflection into nat or int), including
lemmas on overflow and monotonicity. Instantiated to all appropriate
arithmetic type classes, supporting automatic simplification of
numerals on all operations. Jointly developed by NICTA, Galois, and
PSU.
* still to do: README.html/document + moving some of the generic lemmas
to appropriate place in distribution
#!/usr/bin/env bash
#
# $Id$
# Author: Florian Haftmann, TUM
#
# DESCRIPTION: issue code generation from shell
## diagnostics
PRG="$(basename "$0")"
function usage()
{
echo
echo "Usage: $PRG IMAGE THY SERI"
echo
echo " Issues code generation using image IMAGE,"
echo " theory THY,"
echo " with Isar command 'code_gen SERI'"
echo
exit 1
}
## process command line
[ "$#" -lt 2 -o "$1" = "-?" ] && usage
IMAGE="$1"; shift
THY="$1"; shift
SERI="$1"
## main
SERI=$(echo $SERI | sed -e 's/\\/\\\\"/g; s/"/\\\"/g')
CMD="Isar.toplevel (fn _ => (use_thy \"$THY\"; CodePackage.codegen_command (theory \"$THY\") \"$SERI\"))"
"$ISABELLE" -q -e "$CMD" "$IMAGE"