SRC = \
	AssemblyInfo.n \
        Pruner.n \
        ArithProofs.n \
        ProvingGrinder.n \
        ProofGen.n \
        Trew.n \
        Grinder.n \
        SmtDumper.n \
	Rational.n \
	PatriciaTree.n \
	Clause.n \
	SimpleSolver.n \
	Core.n \
	QAtom.n \
        PAtom.n \
	Atom.n \
	Parser.n \
	FatalError.n \
	Term.n \
	Command.n \
	Theory.n \
	FreeFunTheory.n \
	LinearTheory.n \
	TcTheory.n \
	Literal.n \
	Proof.n \
	Driver.n \
	Term.SubTrigger.n \
	Term.Matcher.n \
	Term.Pool.n \
	Term.SubstLite.n \
	CSV.n \
	Rule.n \

MACROS_SRC = UtilMacros.n
CSC = gmcs

NFLAGS = -g
SELFCHECKS = -o:SelfChecks=1
SOFILE = $(shell if [ `uname` = Darwin ] ; then echo librdtsc.dylib ; else echo librdtsc.so ; fi)


all: fx7.exe $(SOFILE)

fx7.exe: $(SRC) Fx7.Macros.dll Fx7.BigInteger.dll
	ncc -bar+ -i $(NFLAGS) -o $@ $(SRC) -r:Fx7.Macros.dll -r:Fx7.BigInteger.dll

Fx7.BigInteger.dll: BigInteger.cs
	$(CSC) /t:library /out:$@ $^

Fx7.Macros.dll: $(MACROS_SRC)
	ncc -bar+ -t:library -r:Nemerle.Compiler -i $(NFLAGS) -o $@ $(MACROS_SRC)

clean:
	rm -f  fx7.exe Fx7.Macros.dll *.mdb *.pdb Fx7.BigInteger.dll

.PHONY: tests

librdtsc.dylib: rdtsc.c
	gcc -dynamiclib -o $@ -fPIC -O3 -W -Wall $^

librdtsc.so: rdtsc.c
	gcc -shared -o $@ -fPIC -O3 -W -Wall $^

t0: all
	time $(MAKE) do-t0

do-t0:
	./run $(SELFCHECKS)   -n                               tests/custom
	./run $(SELFCHECKS) -s -n                      -valid   tests/OrdersTest.sx
	./run $(SELFCHECKS) -s -n -ax:tests/escv1.ax   -invalid tests/Examples.esc.invalid
	./run $(SELFCHECKS) -s -n                      -valid   tests/PredTest.esc.valid
	./run $(SELFCHECKS) -s -n                      -invalid tests/PredTest.esc.invalid
	./run $(SELFCHECKS) -s -n -ax:tests/escv3.ax   -valid   tests/Examples.esc3.valid
	./run $(SELFCHECKS) -s -n -ax:tests/necula1.ax -valid   tests/necula1.sx
	./run $(SELFCHECKS) -s -n -ax:tests/saxe1.ax   -invalid tests/saxe1.input
	./run $(SELFCHECKS) -s -n -ax:tests/escv1.ax   -valid   tests/Examples.esc.valid
	./run $(SELFCHECKS) -s -n -ax:tests/def.ax     -valid   tests/Examples.valid
	./run $(SELFCHECKS) -s -n -ax:tests/escv2.ax   -invalid tests/Examples.esc2.invalid
	./run $(SELFCHECKS) -s -n -ax:tests/def.ax     -invalid tests/Examples.invalid

t1: all
	./run benchmarks/01_*

t2: all
	./run benchmarks/0[12]_*

t3: all
	./run benchmarks/0[123]_*

t4: all
	./run benchmarks/0[1234]_*

t5: all
	./run benchmarks/0[12345]_*

t6: all
	./run -t:600 benchmarks/0[123456]_*

t7: all
	./run -t:2500 benchmarks/0[1234567]_*

t9: all
	./run -t:2500 benchmarks/09_*

toq1: all
	./runesc -t:60 esc/q1/*

toq3: all
	./runesc -t:60 esc/q{1,2,3}/*

tq1: all
	./runesc -t:60 esc/qf1/* esc/q1/*

tq2: all
	./runesc -t:60 esc/qf1/* esc/q{1,2}/*

tq3: all
	./runesc -t:60 esc/qf1/* esc/q{1,2,3}/*

tql1: all
	./runesc -t:60 esc/ql1/*

tql2: all
	./runesc -t:60 esc/ql[12]/*

tql3: all
	./runesc -t:60 esc/ql[123]/*


t: all t0 t1