lib/scripts/run-poplogml

rudimentary class target implementation

#!/usr/bin/env bash
#
# $Id$
# Author: Makarius
#
# Poplog/PML startup script (version 15.6/2.1).

export -n INFILE OUTFILE COPYDB COMPRESS MLTEXT TERMINATE NOWRITE


## diagnostics

function fail_out()
{
  echo "Unable to create output heap file: \"$OUTFILE\"" >&2
  exit 2
}

function check_mlhome_file()
{
  if [ ! -f "$1" ]; then
    echo "Unable to locate $1" >&2
    echo "Please check your ML_HOME setting!" >&2
    exit 2
  fi
}

function check_heap_file()
{
  if [ ! -f "$1" ]; then
    echo "Expected to find ML heap file $1" >&2
    return 1
  else
    return 0
  fi
}


## prepare databases

if [ -z "$INFILE" ]; then
  EXIT="fun exit (i: int) = OS.execve \"/bin/sh\" [\"sh\", \"-c\", \"exit \" ^ makestring i] (OS.envlist());"
  USE='pop11
section $-ml;

ml_exception Use of string;

ml_val use : string -> unit =
procedure(name) with_props use;
        lvars name, path;
        lconstant UseExn = exception("Use");

        define dlocal pop_exception_handler(n, msg, idstring, severity);
                returnunless(severity == `E` or severity == `R`)(false);
                erasenum(n);
                raise(UseExn(name));
        enddefine;

        unless sourcefile(name) ->> path then raise(UseExn(name)) endunless;
        ml_load(path);
        ml_unit;
endprocedure;

ml_val use_string : string -> unit =
procedure(str) with_props use_string;
        lvars str;
        lconstant UseExn = exception("Use");

        define dlocal pop_exception_handler(n, msg, idstring, severity);
                [n ^n msg ^msg  idstring ^idstring severity ^severity] ==>
                returnunless(severity == `E` or severity == `R`)(false);
                erasenum(n);
                raise(UseExn(str));
        enddefine;

        ml_compile(stringin(str));
        ml_unit;
endprocedure;

endsection;
ml'
  DB=""
else
  EXIT=""
  USE=""
  DB="+$INFILE"
fi

if [ -z "$OUTFILE" ]; then
  COMMIT='fun commit () = (StdIO.output (StdIO.std_err, "Error - Database is not opened for writing.\n"); false);'
else
  ML_OPTIONS="$ML_OPTIONS -nort"
  if [ -z "$NOWRITE" ]; then
    COMMIT="fun commit () = if System.make {image =\"$OUTFILE\", lock = false, share = false, banner = false, init = false} then System.restart() else true;"
  else
    COMMIT="fun commit () = if System.make {image =\"$OUTFILE\", lock = true, share = true, banner = false, init = false} then System.restart() else true;"
  fi
  [ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; }
fi


## run it!

POPLOG="$ML_HOME/poplog"
check_mlhome_file "$POPLOG"

INIT="$ISABELLE_TMP/init.ml"
echo 'pop11
section $-ml;
false -> ml_quiet;
endsection;
ml' > "$INIT"

echo "$EXIT $USE $COMMIT $MLTEXT" >> "$INIT"

if [ -n "$TERMINATE" ]; then
  ML_OPTIONS="$ML_OPTIONS -nostdin"
  echo "commit();" >> "$INIT"
fi

"$POPLOG" pml "$DB" $ML_OPTIONS -load "$INIT" 2>&1
RC="$?"

rm -f "$INIT"

if [ -n "$OUTFILE" ] && check_heap_file "$OUTFILE"; then
  [ -n "$NOWRITE" ] && chmod -w "$OUTFILE"
  rm -f "$OUTFILE-"
fi

exit "$RC"