1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
|
BENCH ?= no
ifeq ($(BENCH),yes)
WHY3=../../bin/why3.opt
WHY3SHARE=../../share
else
ifeq ($(BINDIR),)
WHY3=why3
else
WHY3=$(BINDIR)/why3
endif
WHY3SHARE=$(shell $(WHY3) --print-datadir)
endif
include $(WHY3SHARE)/Makefile.config
ifeq ($(BENCH),yes)
INCLUDE += -I ../../lib/why3
endif
MAIN = main
OBJ = defunctionalization
ML = $(addsuffix .ml, $(OBJ))
CMO = $(addsuffix .cmo, $(OBJ))
CMX = $(addsuffix .cmx, $(OBJ))
OCAMLOPT = ocamlopt -noassert -inline 1000
all: $(MAIN).opt
extract: $(ML)
doc:
$(WHY3) doc ../defunctionalization.mlw
$(WHY3) session html ../defunctionalization.mlw
@echo firefox ../defunctionalization.html why3session.html
$(MAIN).byte: $(CMO) $(MAIN).cmo
ocamlc -g $(INCLUDE) zarith.cma -o $@ $^
$(MAIN).opt: $(CMX) $(MAIN).cmx
$(OCAMLOPT) $(INCLUDE) zarith.cmxa -o $@ $^
$(MAIN).cmx: $(CMX)
$(ML): ../defunctionalization.mlw
$(WHY3) extract -D ocaml64 --recursive -L .. -o $@ \
defunctionalization.DirectSem \
defunctionalization.CPS \
defunctionalization.Defunctionalization
%.cmx: %.ml
$(OCAMLOPT) $(INCLUDE) -annot -c $<
%.cmo: %.ml
ocamlc $(INCLUDE) -annot -g -c $<
%.cmi: %.mli
ocamlc $(INCLUDE) -annot -g -c $<
clean::
rm -f $(ML) *.cm[xio] $(MAIN).opt
|
