#!/bin/bash

COMP="c"
EXT="o"
EXTA=""
[[ "$1" = "-o" ]] && {
    COMP="opt"
    EXT="x"
    EXTA="x"
}

rm -f *.cm? *.o
ocaml$COMP -c fol.ml &&
ocaml$COMP -c simpl.ml &&
ocaml$COMP -c tptp.ml &&
ocaml$COMP -c spass.ml &&
ocamlyacc -v alloyparse.mly &&
ocaml$COMP -c alloyparse.mli alloyparse.ml &&
ocamllex alloylex.mll &&
ocaml$COMP -c alloylex.ml &&
ocaml$COMP -c alloy.ml &&
ocaml$COMP -c entrypoint.ml &&
ocaml$COMP -c entrypoint_spass.ml &&
ocaml$COMP -c folocaml.ml &&
ocaml$COMP -c entrypoint_ocaml.ml &&
echo "Compilation succeeded. About to link." &&
 ocaml$COMP -o alloy2tptp fol.cm$EXT simpl.cm$EXT tptp.cm$EXT alloyparse.cm$EXT str.cm$EXTA''a alloylex.cm$EXT alloy.cm$EXT entrypoint.cm$EXT &&
ocaml$COMP -o alloy2spass fol.cm$EXT simpl.cm$EXT spass.cm$EXT tptp.cm$EXT alloyparse.cm$EXT str.cm$EXTA''a alloylex.cm$EXT alloy.cm$EXT entrypoint_spass.cm$EXT &&
 ocaml$COMP -o alloy2ocaml fol.cm$EXT simpl.cm$EXT tptp.cm$EXT alloyparse.cm$EXT str.cm$EXTA''a alloylex.cm$EXT alloy.cm$EXT folocaml.cm$EXT entrypoint_ocaml.cm$EXT &&
[[ "$1" = "test" ]] &&
rm -f *.tp && # *.spass
for i in ath bopc copc rab rbc 
do
  ./alloy2tptp < $i.als | ./separer.pl hyp_$i
#  ./alloy2spass < $i.als
done