config

#!/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

usage() {
    cat <<__EOF__
usage: `basename $0` \$hollight_file.ml \$root_path [--mapping \$mapping.lp] [--renaming \$renaming.lp] [rocq_or_lean_file_or_module] ... [\$deps.mk]

arguments:
  \$hollight_file.ml: path to an ml file relative to \$HOLLIGHT_DIR
  \$root_path: name of the generated library
  file_or_module: modules that need to be imported in generated files
  \$deps.mk: dependencies of Rocq files given in arguments

effect in the current directory:
- create a file CONFIG containing the command used to create links
- create a file BASE containing the base name of \$hollight_file.ml
- create a file ROOT_PATH containing \$root_path
- create a file lambdapi.pkg
- create a file _CoqProject
- create a file MAPPING containing \$mapping.lp
- create a file RENAMING containing \$renaming.lp
- create a file REQUIRING containing the list of Rocq module names that need to be imported (in the same order as they are given in the command)
- create a file ROCQFILES containing the list of Rocq files given in argument
- create a file LEANFILES containing the list of Lean files given in argument
- copy \$deps.mk and the Rocq files given in argument
- copy theory_hol.dk and theory_hol.lp from \$HOL2DK_DIR
- add links to Makefile, BIG_FILES, part.mk and spec.mk from \$HOL2DK_DIR
- add links to \$hollight_file.prf, \$hollight_file.nbp, \$hollight_file.sig, \$hollight_file.thm, \$hollight_file.pos, and \$hollight_file.use files in \$HOLLIGHT_DIR
__EOF__
}

error() { echo error: $1; echo; usage; exit 1; }

invalid_arg() { error invalid argument \"$1\"; }

if test $# -eq 0; then usage; exit 0; fi

parse_args() {
    if test $# -ne 0; then
        case $1 in
            --mapping)
                if test -n "$mapping"; then error 'mapping file already set'; fi
                shift
                if test $# -eq 0; then error 'mapping file missing'; fi
                mapping=$1
                shift
                parse_args $*;;
            --renaming)
                if test -n "$renaming"; then error 'renaming file already set'; fi
                shift
                if test $# -eq 0; then error 'renaming file missing'; fi
                renaming=$1
                shift
                parse_args $*;;
            *.ml)
                if test -z "$hollight_file"
                then
                    hollight_file=$1
                    shift
                    parse_args $*
                else
                    error 'too many ml files'
                fi;;
            *.mk)
                if test -z "$mk_file"
                then
                    mk_file=$1
                    shift
                    parse_args $*
                else
                    error 'too many make files'
                fi;;
            *.v)
                if test -z "$root_path"
                then
                    error 'the root_path must be given before'
                else
                    rocqfiles="$rocqfiles $1"
                    base_rocqfiles="$base_rocqfiles `basename $1`"
                    requiring="$requiring $root_path.`basename $1 .v`"
                    shift
                    parse_args $*
                fi;;
            *.lean)
                if test -z "$root_path"
                then
                    error 'the root_path must be given before'
                else
                    leanfiles="$leanfiles $1"
                    base_leanfiles="$base_leanfiles `basename $1`"
                    requiring="$requiring $root_path.`basename $1 .lean`"
                    shift
                    parse_args $*
                fi;;
            *)
                if test -z "$root_path"
                then
                    root_path=$1
                else
                    requiring="$requiring $1"
                fi
                shift
                parse_args $*;;
        esac
    fi
}

parse_args $*
if test -z "$root_path"
then
    error 'missing root_path'
fi

echo create CONFIG ...
echo '#!/bin/sh' > CONFIG
echo hol2dk config $* >> CONFIG
chmod a+x CONFIG

echo create BASE ...
echo `basename $hollight_file .ml` > BASE

echo create ROOT_PATH ...
echo $root_path > ROOT_PATH

echo create lambdapi.pkg ...
echo package_name = $root_path > lambdapi.pkg
echo root_path = $root_path >> lambdapi.pkg

echo create _CoqProject ...
echo "-R . $root_path ." > _CoqProject

echo create MAPPING ...
if test -z "$mapping"
then
    touch mapping.lp
    mapping=mapping.lp
fi
echo $mapping > MAPPING

echo create RENAMING ...
if test -z "$renaming"
then
    touch renaming.lp
    renaming=renaming.lp
fi
echo $renaming > RENAMING

echo create REQUIRING ...
echo $requiring > REQUIRING

echo create ROCQFILES ...
echo $base_rocqfiles > ROCQFILES

echo create LEANFILES ...
echo $base_leanfiles > LEANFILES

if test -z "$mk_file"
then
    echo create deps.mk ...
    rm -f deps.mk
    touch deps.mk
    if test -n "$base_rocqfiles"
    then
        set $base_rocqfiles
        echo -n ${1}o >> deps.mk
        shift
        for f in $*
        do
            echo -n " ${f}o" >> deps.mk
        done
        echo : >> deps.mk
    fi
else
    echo ln -f -s $mk_file deps.mk
    ln -f -s $mk_file deps.mk
fi

for f in theory_hol.dk theory_hol.lp
do
    echo cp -f $HOL2DK_DIR/$f .
    cp -f $HOL2DK_DIR/$f .
done

for f in Makefile BIG_FILES part.mk spec.mk
do
    echo ln -f -s $HOL2DK_DIR/$f
    ln -f -s $HOL2DK_DIR/$f
done

for ext in prf nbp sig thm pos use
do
    echo ln -f -s $HOLLIGHT_DIR/${hollight_file%.ml}.$ext
    ln -f -s $HOLLIGHT_DIR/${hollight_file%.ml}.$ext
done

for f in $rocqfiles
do
    echo cp -f $f .
    cp -f $f .
done

if test -n "$leanfiles"
then
    if test ! -d .lake
    then
       echo lake init $root_path math
       lake init $root_path math
       rm -f $root_path.lean $root_path/Basic.lean
    fi
    for f in $leanfiles
    do
        echo cp -f $f $root_path
        cp -f $f $root_path
    done
fi