patch

#!/bin/sh

if test -z "$HOL2DK_DIR"
then
    echo "HOL2DK_DIR is not set"
    exit 1
fi

if test -z "$HOLLIGHT_DIR"
then
    echo "HOLLIGHT_DIR is not set"
    exit 1
fi

if test $# -ne 0
then
    echo "usage: `basename $0`"
    echo "patch the HOL-Light sources in $HOLLIGHT_DIR"
    exit 1
fi

patch() {
    if test -f $HOLLIGHT_DIR/$1-bak.ml
    then
        echo "$HOLLIGHT_DIR/$1-bak.ml already exists"
        exit 1
    else
        echo "cp $HOLLIGHT_DIR/$1.ml $HOLLIGHT_DIR/$1-bak.ml"
        cp $HOLLIGHT_DIR/$1.ml $HOLLIGHT_DIR/$1-bak.ml
        echo "patch $HOLLIGHT_DIR/$1.ml ..."
        sed -e 's/.*REMOVE.*//' -e 's/open Lib/needs "lib.ml";;/' $HOL2DK_DIR/$1.ml > $HOLLIGHT_DIR/$1.ml
    fi
}

create() {
    if test -f $HOLLIGHT_DIR/$1.ml
    then
        echo "$HOLLIGHT_DIR/$1.ml already exists"
        exit 1
    else
        echo "create $HOLLIGHT_DIR/$1.ml ..."
        sed -e 's/.*REMOVE.*//' -e 's/^open .*//' $HOL2DK_DIR/$1.ml > $HOLLIGHT_DIR/$1.ml
    fi
}

patch fusion
patch bool
patch equal
create xnames