#!/usr/bin/env bash

#

# Author: Makarius

#

# build - build Isabelle/ML

#

# Requires proper Isabelle settings environment.

## diagnostics

function usage()

{

  echo

  echo "Usage: $PRG [OPTIONS] TARGET"

  echo

  echo "  Options are:"

  echo "    -b           build target images"

  echo

  echo "  Build Isabelle/ML TARGET: RAW or Pure"

  echo

  exit 1

}

function fail()

{

  echo "$1" >&2

  exit 2

}

[ -z "$ISABELLE_HOME" ] && fail "Missing Isabelle settings environment"

## process command line

# options

BUILD_IMAGES=false

while getopts "b" OPT

do

  case "$OPT" in

    b)

      BUILD_IMAGES="true"

      ;;

    \?)

      usage

      ;;

  esac

done

shift $(($OPTIND - 1))

# args

TARGET="Pure"

[ "$#" -ge 1 ] && { TARGET="$1"; shift; }

[ "$TARGET" = RAW -o "$TARGET" = Pure ] || fail "Bad target: \"$TARGET\""

[ "$#" -eq 0 ] || usage

## main

# get compatibility file

ML_SYSTEM_BASE=$(echo "$ML_SYSTEM" | cut -f1 -d-)

[ -z "$ML_SYSTEM" ] && fail "Missing ML_SYSTEM settings!"

COMPAT=""

[ -f "ML-Systems/${ML_SYSTEM_BASE}.ML" ] && COMPAT="ML-Systems/${ML_SYSTEM_BASE}.ML"

[ -f "ML-Systems/${ML_SYSTEM}.ML" ] && COMPAT="ML-Systems/${ML_SYSTEM}.ML"

[ -z "$COMPAT" ] && fail "Missing compatibility file for ML system \"$ML_SYSTEM\"!"

# run isabelle

. "$ISABELLE_HOME/lib/scripts/timestart.bash"

if [ "$TARGET" = RAW ]; then

  if [ "$BUILD_IMAGES" = false ]; then

    "$ISABELLE_PROCESS" \

      -e "use\"$COMPAT\" handle _ => OS.Process.exit OS.Process.failure;" \

      -q RAW_ML_SYSTEM

  else

    "$ISABELLE_PROCESS" \

      -e "use\"$COMPAT\" handle _ => OS.Process.exit OS.Process.failure;" \

      -e "structure Isar = struct fun main () = () end;" \

      -e "ml_prompts \"ML> \" \"ML# \";" \

      -q -w RAW_ML_SYSTEM RAW

  fi

else

  if [ "$BUILD_IMAGES" = false ]; then

    "$ISABELLE_PROCESS" \

      -e "(use\"$COMPAT\"; use\"ROOT.ML\") handle _ => OS.Process.exit OS.Process.failure;" \

      -q RAW_ML_SYSTEM

  else

    "$ISABELLE_PROCESS" \

      -e "(use\"$COMPAT\"; use\"ROOT.ML\") handle _ => OS.Process.exit OS.Process.failure;" \

      -e "ml_prompts \"ML> \" \"ML# \";" \

      -f -q -w RAW_ML_SYSTEM Pure

  fi

fi

RC="$?"

. "$ISABELLE_HOME/lib/scripts/timestop.bash"

if [ "$RC" -eq 0 ]; then

  echo "Finished $TARGET ($TIMES_REPORT)" >&2

fi

exit "$RC"