blob: 957cddcf2e8bbf5f7578f38657521279cd4155a8 (
plain)
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
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
|
#
# General variables
#
TOPDIR=../../..
# Files with axioms to be realized: can't be extracted directly
AXIOMSVO:= \
theories/Arith/Arith.vo \
theories/Lists/List.vo \
theories/Reals/% \
theories/Num/% \
theories/Relations/Rstar.vo \
theories/Sets/Integers.vo \
theories/ZArith/Zsyntax.vo
DIRS:= $(shell (cd $(TOPDIR);find theories -type d ! -name CVS))
INCL:= $(patsubst %,-I %,$(DIRS))
VO:= $(shell (cd $(TOPDIR);find theories -name \*.vo))
VO:= $(filter-out $(AXIOMSVO),$(VO))
ML:= $(shell test -x v2ml && ./v2ml $(VO))
CMO:= $(patsubst %.ml,%.cmo,$(ML))
#
# General rules
#
all: $(ML) depend $(CMO) v2ml
depend: $(ML)
rm -f .depend; ocamldep $(INCL) $(ML) > .depend
tree:
mkdir -p $(DIRS)
%.cmo:%.ml
ocamlc $(INCL) -c -i $<
$(ML): ml2v
./extract `./ml2v $@`
clean:
rm -f theories/*/*.ml theories/*/*.cm*
#
# Extraction of Reals
#
REALSML:= \
theories/Reals/typeSyntax.ml \
theories/Reals/addReals.ml \
theories/Reals/rdefinitions.ml \
theories/Reals/raxioms.ml \
theories/Reals/r_Ifp.ml \
theories/Reals/rbase.ml \
theories/Reals/rbasic_fun.ml \
theories/Reals/rlimit.ml \
theories/Reals/rderiv.ml
REALSCMO:= $(patsubst %.ml,%.cmo,$(REALSML))
reals: all $(REALSML) $(REALSCMO)
realsml:
./extract_reals
cp -f addReals.ml theories/Reals
$(REALSML): realsml
#
# Utilities
#
ml2v: ml2v.ml
ocamlc -o $@ $<
v2ml: v2ml.ml
ocamlc -o $@ $<
$(MAKE)
#
# The End
#
.PHONY: all tree clean reals realsml depend
include .depend
|
