#
# sample Makefile for Objective Caml
# Copyright (C) 2001 Jean-Christophe FILLIATRE
# 
# This library is free software; you can redistribute it and/or
# modify it under the terms of the GNU Library General Public
# License version 2, as published by the Free Software Foundation.
# 
# This library is distributed in the hope that it will be useful,
# but WITHOUT ANY WARRANTY; without even the implied warranty of
# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.
# 
# See the GNU Library General Public License version 2 for more details
# (enclosed in the file LGPL).

# where to install the binaries
prefix=/usr/local
datarootdir=@datarootdir@
exec_prefix=${prefix}
BINDIR=${exec_prefix}/bin

# where to install the man page
MANDIR=${prefix}/man

# other variables set by ./configure
OCAMLC   = ocamlc.opt
OCAMLOPT = ocamlopt.opt
OCAMLDEP = ocamldep
OCAMLLEX = ocamllex.opt
OCAMLYACC= ocamlyacc
OCAMLLIB = /usr/local/lib/ocaml
OCAMLBEST= opt
OCAMLVERSION = 3.09.2
OCAMLWEB = ocamlweb
OCAMLWIN32 = no
EXT = 

INCLUDES = 
BFLAGS = -dtypes -g $(INCLUDES)
OFLAGS = -dtypes $(INCLUDES)

# main target
#############

NAME = mini_coq
EXE= $(NAME)$(EXT)
ifeq ($(CAMLBEST),byte)
BYTE	= $(EXE)
OPT	= $(NAME).opt$(EXT)
else
BYTE	= $(NAME).byte$(EXT)
OPT	= $(EXE)
endif

all: $(EXE)

# bytecode and native-code compilation
######################################

CMO = parser.cmo lexer.cmo mini_coq.cmo
CMX = $(CMO:.cmo=.cmx)

GENERATED = lexer.ml parser.ml parser.mli

$(BYTE): $(CMO)
	$(OCAMLC) $(BFLAGS) -o $@ $^

$(OPT): $(CMX)
	$(OCAMLOPT) $(OFLAGS) -o $@ $^

test: $(EXE) test.v
	./$(EXE) test.v

tests: $(EXE)
	for f in ../tests/*/*.v; do \
	  ./$(EXE) $$f; \
	done

# generic rules
###############

.SUFFIXES: .mli .ml .cmi .cmo .cmx .mll .mly .tex .dvi .ps .html

.mli.cmi:
	$(OCAMLC) -c $(BFLAGS) $<

.ml.cmo:
	$(OCAMLC) -c $(BFLAGS) $<

.ml.o:
	$(OCAMLOPT) -c $(OFLAGS) $<

.ml.cmx:
	$(OCAMLOPT) -c $(OFLAGS) $<

.mll.ml:
	$(OCAMLLEX) $<

.mly.ml:
	$(OCAMLYACC) -v $<

.mly.mli:
	$(OCAMLYACC) -v $<

.tex.dvi:
	latex $< && latex $<

.dvi.ps:
	dvips $< -o $@ 

.tex.html:
	hevea $<

# Emacs tags
############

tags:
	find . -name "*.ml*" | sort -r | xargs \
	etags "--regex=/let[ \t]+\([^ \t]+\)/\1/" \
	      "--regex=/let[ \t]+rec[ \t]+\([^ \t]+\)/\1/" \
	      "--regex=/and[ \t]+\([^ \t]+\)/\1/" \
	      "--regex=/type[ \t]+\([^ \t]+\)/\1/" \
              "--regex=/exception[ \t]+\([^ \t]+\)/\1/" \
	      "--regex=/val[ \t]+\([^ \t]+\)/\1/" \
	      "--regex=/module[ \t]+\([^ \t]+\)/\1/"

# Makefile is rebuilt whenever Makefile.in or configure.in is modified
######################################################################

Makefile: Makefile.in config.status
	./config.status

config.status: configure
	./config.status --recheck

configure: configure.in
	autoconf 

# clean
#######

clean-test:
	cd tests; \
	  for d in . bad-sem bad-exec exec; do rm -f $$d/*~ $$d/*.vm; done;

clean:: clean-test
	rm -f *.cm[iox] *.o *~ *.annot
	rm -f $(GENERATED) parser.output
	rm -f $(BYTE) $(OPT)
	rm -f *.aux *.log $(NAME).tex $(NAME).dvi $(NAME).ps

dist-clean distclean:: clean
	rm -f Makefile config.cache config.log config.status

# depend
########

.depend depend:: $(GENERATED)
	rm -f .depend
	$(OCAMLDEP) $(INCLUDES) *.ml *.mli > .depend

include .depend