1###############################################################################
2# METIS MAKEFILE
3# Copyright (c) 2001 Joe Hurd, distributed under the BSD License
4###############################################################################
5
6.SUFFIXES:
7
8###############################################################################
9# The default action.
10###############################################################################
11
12.PHONY: default
13default: mosml
14
15###############################################################################
16# Cleaning temporary files.
17###############################################################################
18
19TEMP = \
20  $(MOSML_TARGETS) \
21  bin/mosml/*.sml bin/mosml/*.ui bin/mosml/*.uo bin/mosml/a.out \
22  $(MLTON_TARGETS) \
23  bin/mlton/*.sml bin/mlton/*.mlb \
24  $(POLYML_TARGETS) \
25  bin/polyml/*.sml bin/polyml/*.log bin/polyml/*.o
26
27.PHONY: clean
28clean:
29	@echo
30	@echo '********************'
31	@echo '* Clean everything *'
32	@echo '********************'
33	@echo
34	rm -f $(TEMP)
35	$(MAKE) -C test $@
36
37###############################################################################
38# Testing.
39###############################################################################
40
41.PHONY: test
42test:
43	$(MAKE) -C test
44
45###############################################################################
46# Source files.
47###############################################################################
48
49SRC = \
50  src/Useful.sig src/Useful.sml \
51  src/Lazy.sig src/Lazy.sml \
52  src/Ordered.sig src/Ordered.sml \
53  src/Map.sig src/Map.sml \
54  src/KeyMap.sig src/KeyMap.sml \
55  src/Set.sig src/Set.sml \
56  src/ElementSet.sig src/ElementSet.sml \
57  src/Sharing.sig src/Sharing.sml \
58  src/Stream.sig src/Stream.sml \
59  src/Heap.sig src/Heap.sml \
60  src/Print.sig src/Print.sml \
61  src/Parse.sig src/Parse.sml \
62  src/Name.sig src/Name.sml \
63  src/NameArity.sig src/NameArity.sml \
64  src/Term.sig src/Term.sml \
65  src/Subst.sig src/Subst.sml \
66  src/Atom.sig src/Atom.sml \
67  src/Formula.sig src/Formula.sml \
68  src/Literal.sig src/Literal.sml \
69  src/Thm.sig src/Thm.sml \
70  src/Proof.sig src/Proof.sml \
71  src/Rule.sig src/Rule.sml \
72  src/Normalize.sig src/Normalize.sml \
73  src/Model.sig src/Model.sml \
74  src/Problem.sig src/Problem.sml \
75  src/TermNet.sig src/TermNet.sml \
76  src/AtomNet.sig src/AtomNet.sml \
77  src/LiteralNet.sig src/LiteralNet.sml \
78  src/Subsume.sig src/Subsume.sml \
79  src/KnuthBendixOrder.sig src/KnuthBendixOrder.sml \
80  src/Rewrite.sig src/Rewrite.sml \
81  src/Units.sig src/Units.sml \
82  src/Clause.sig src/Clause.sml \
83  src/Active.sig src/Active.sml \
84  src/Waiting.sig src/Waiting.sml \
85  src/Resolution.sig src/Resolution.sml \
86  src/Tptp.sig src/Tptp.sml \
87  src/Options.sig src/Options.sml
88
89EXTRA_SRC = \
90  src/problems.sml
91
92###############################################################################
93# The ML preprocessor.
94###############################################################################
95
96MLPP = scripts/mlpp
97
98MLPP_OPTS =
99
100###############################################################################
101# Building using Moscow ML.
102###############################################################################
103
104MOSMLC = mosmlc -toplevel -q
105
106MOSML_SRC = \
107  src/Portable.sig src/PortableMosml.sml \
108  $(SRC)
109
110MOSML_TARGETS = \
111  bin/mosml/problems2tptp \
112  bin/mosml/metis
113
114include bin/mosml/Makefile.src
115
116.PHONY: mosml-info
117mosml-info:
118	@echo
119	@echo '*****************************************'
120	@echo '* Build and test the Moscow ML programs *'
121	@echo '*****************************************'
122	@echo
123
124.PHONY: mosml
125mosml: mosml-info $(MOSML_OBJ) $(MOSML_TARGETS) test
126
127###############################################################################
128# Building using MLton.
129###############################################################################
130
131MLTON = mlton
132
133MLTON_OPTS = -runtime 'ram-slop 0.4'
134
135MLTON_SRC = \
136  src/Portable.sig src/PortableMlton.sml \
137  $(SRC)
138
139METIS = bin/mlton/metis
140
141PROBLEMS2TPTP = bin/mlton/problems2tptp
142
143MLTON_TARGETS = \
144  bin/mlton/selftest \
145  $(METIS) \
146  $(PROBLEMS2TPTP)
147
148bin/mlton/%.sml: $(MLTON_SRC) src/%.sml
149	@$(MLPP) $(MLPP_OPTS) -c mlton $^ > $@
150
151bin/mlton/%.mlb: bin/mlton/%.sml
152	echo '$$(SML_LIB)/basis/basis.mlb $$(SML_LIB)/basis/mlton.mlb $(notdir $<)' > $@
153
154bin/mlton/%: bin/mlton/%.mlb
155	@echo
156	@echo '***************************'
157	@echo '* Compile a MLton program *'
158	@echo '***************************'
159	@echo
160	@echo $@
161	cd bin/mlton ; $(MLTON) $(MLTON_OPTS) $(notdir $<)
162	@echo
163
164.PHONY: mlton-info
165mlton-info:
166	@echo
167	@echo '*************************************'
168	@echo '* Build and test the MLton programs *'
169	@echo '*************************************'
170	@echo
171
172.PHONY: mlton
173mlton: mlton-info $(MLTON_TARGETS)
174	$(MAKE) -C test mlton
175
176###############################################################################
177# Building using Poly/ML.
178###############################################################################
179
180POLYML = poly
181
182POLYML_OPTS =
183
184ifeq ($(shell uname), Darwin)
185  POLYML_LINK_OPTS = -lpolymain -lpolyml -segprot POLY rwx rwx
186else
187  POLYML_LINK_OPTS = -lpolymain -lpolyml
188endif
189
190POLYML_SRC = \
191  src/Random.sig src/Random.sml \
192  src/Portable.sig src/PortablePolyml.sml \
193  $(SRC)
194
195POLYML_TARGETS = \
196  bin/polyml/selftest \
197  bin/polyml/problems2tptp \
198  bin/polyml/metis
199
200bin/polyml/%.sml: src/%.sml $(POLYML_SRC)
201	@$(MLPP) $(MLPP_OPTS) -c polyml $(POLYML_SRC) > $@
202	@echo 'fun main () = let' >> $@
203	@$(MLPP) $(MLPP_OPTS) -c polyml $< >> $@
204	@echo "in () end; PolyML.export(\"$(basename $(notdir $<))\", main);" >> $@
205
206bin/polyml/%.o: bin/polyml/%.sml
207	cd bin/polyml ; echo "use \"$(notdir $<)\";" | $(POLYML) $(POLYML_OPTS) > $(basename $(notdir $<)).log
208	@if test $@ -nt $< ; then echo 'compiled $@' ; else cat bin/polyml/$(basename $(notdir $<)).log ; exit 1 ; fi
209
210bin/polyml/%: bin/polyml/%.o
211	@echo
212	@echo '*****************************'
213	@echo '* Compile a Poly/ML program *'
214	@echo '*****************************'
215	@echo
216	@echo $@
217	cd bin/polyml && $(CC) -o $(notdir $@) $(notdir $<) $(POLYML_LINK_OPTS)
218	@echo
219
220.PHONY: polyml-info
221polyml-info:
222	@echo
223	@echo '***************************************'
224	@echo '* Build and test the Poly/ML programs *'
225	@echo '***************************************'
226	@echo
227
228.PHONY: polyml
229polyml: polyml-info $(POLYML_TARGETS)
230	$(MAKE) -C test polyml
231
232###############################################################################
233# Development.
234##############################################################################
235
236include Makefile.dev
237
238Makefile.dev:
239	echo > $@
240