#!/bin/sh

#######################################################################
#                                                                     #
#              The Compcert verified compiler                         #
#                                                                     #
#          Xavier Leroy, INRIA Paris-Rocquencourt                     #
#                                                                     #
#  Copyright Institut National de Recherche en Informatique et en     #
#  Automatique.  All rights reserved.  This file is distributed       #
#  under the terms of the INRIA Non-Commercial License Agreement.     #
#                                                                     #
#######################################################################

cildistrib=cil-1.3.5.tar.gz
prefix=/usr/local
bindir='$(PREFIX)/bin'
libdir='$(PREFIX)/lib/compcert'
target=''

usage='Usage: ./configure [options] <target>

Supported targets:
  macosx           (PowerPC, MacOS X)
  ppc-linux        (PowerPC, Linux)
  ppc-linux-cross  (PowerPC, Linux, cross-compilation)
  arm-linux        (ARM, Linux)
  arm-linux-cross  (ARM, Linux, cross-compilation)

Options:
  -prefix <dir>    Install in <dir>/bin and <dir>/lib/compcert
  -bindir <dir>    Install binaries in <dir>
  -libdir <dir>    Install libraries in <dir>
'

# Parse command-line arguments

while : ; do
  case "$1" in
    "") break;;
    -prefix|--prefix)
        prefix=$2; shift;;
    -bindir|--bindir)
        bindir=$2; shift;;
    -libdir|--libdir)
        libdir=$2; shift;;
    *)
        if test -n "$target"; then echo "$usage" 1>&2; exit 2; fi
        target="$1";;
  esac
  shift
done

if test -z "$target"; then echo "$usage" 1>&2; exit 2; fi

# Per-target configuration

case "$target" in
  macosx)
    arch="powerpc"
    variant="macosx"
    cc="gcc -arch ppc"
    cprepro="gcc -arch ppc -U__GNUC__ -E"
    casm="gcc -arch ppc -c"
    clinker="gcc -arch ppc"
    libmath="";;
  ppc-linux)
    arch="powerpc"
    variant="eabi"
    cc="gcc"
    cprepro="gcc -U__GNUC__ -E"
    casm="gcc -c"
    clinker="gcc"
    libmath="-lm";;
  ppc-linux-cross)
    arch="powerpc"
    variant="eabi"
    cc="ppc-linux-gcc"
    cprepro="ppc-linux-gcc -U__GNUC__ -E"
    casm="ppc-linux-gcc -c"
    clinker="ppc-linux-gcc"
    libmath="-lm";;
  arm-linux)
    arch="arm"
    variant="linux"
    cc="gcc"
    cprepro="gcc -U__GNUC__ -E"
    casm="gcc -c"
    clinker="gcc"
    libmath="-lm";;
  arm-linux-cross)
    arch="arm"
    variant="linux"
    cc="arm-linux-gcc"
    cprepro="arm-linux-gcc -U__GNUC__ -E"
    casm="arm-linux-gcc -c"
    clinker="arm-linux-gcc"
    libmath="-lm";;
  *)
    echo "Unsupported configuration '$target'" 1>&2
    echo "$usage" 1>&2
    exit 2;;
esac

# Generate Makefile.config

rm -f Makefile.config
cat > Makefile.config <<EOF
PREFIX=$prefix
BINDIR=$bindir
LIBDIR=$libdir
ARCH=$arch
VARIANT=$variant
CC=$cc
CPREPRO=$cprepro
CASM=$casm
CLINKER=$clinker
LIBMATH=$libmath
EOF

# Extract and configure Cil

set -e
tar xzf $cildistrib
for i in cil.patch/*; do patch -p1 < $i; done
(cd cil && ./configure)

# Extract 'ARCHOS' info from Cil configuration

grep '^ARCHOS=' cil/config.log >> Makefile.config

# Summarize configuration

cat <<EOF

CompCert configuration:
    Target architecture........... $arch ($variant)
    C compiler.................... $cc
    C preprocessor................ $cprepro
    Assembler..................... $casm
    Linker........................ $clinker
    Math library.................. $libmath

EOF