blob: c9bb56237cd912ce3a194be3a65a2bd4174ad8b5 (
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
100
101
102
103
104
105
106
107
108
109
|
#
# General variables
#
TOPDIR=../../..
# Files with axioms to be realized: can't be extracted directly
AXIOMSVO:= \
theories/Reals/% \
theories/Num/%
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))
MLI:= $(patsubst %.ml,%.mli,$(ML))
CMO:= $(patsubst %.ml,%.cmo,$(ML))
OSTDLIB:=$(shell (ocamlc -where))
#
# General rules
#
all: v2ml ml $(MLI) $(CMO)
ml: $(ML)
depend: $(ML)
rm -f .depend; ocamldep $(INCL) theories/*/*.ml theories/*/*.mli > .depend
tree:
mkdir -p $(DIRS)
cp $(OSTDLIB)/pervasives.cmi $(OSTDLIB)/obj.cmi $(OSTDLIB)/lazy.cmi theories
#%.mli:%.ml
# ./make_mli $< > $@
%.cmi:%.mli
ocamlc -c $(INCL) -nostdlib $<
%.cmo:%.ml
ocamlc -c $(INCL) -nostdlib $<
$(ML): ml2v
./extract $@
clean:
rm -f theories/*/*.ml* theories/*/*.cm*
#
# Utilities
#
open:
find theories -name "*".ml -exec ./qualify2open \{\} \;
undo_open:
find theories -name "*".ml -exec mv \{\}.orig \{\} \;
ml2v: ml2v.ml
ocamlopt -o $@ $<
v2ml: v2ml.ml
ocamlopt -o $@ $<
$(MAKE)
#
# Extraction of Reals
#
REALSAXIOMSVO:=theories/Reals/Rsyntax.vo
REALSALLVO:=$(shell cd $(TOPDIR); ls -tr theories/Reals/*.vo)
REALSVO:=$(filter-out $(REALSAXIOMSVO),$(REALSALLVO))
REALSML:=$(shell test -x v2ml && ./v2ml $(REALSVO))
REALSCMO:= $(patsubst %.ml,%.cmo,$(REALSML))
reals: all realsml theories/Reals/addReals.cmo $(REALSCMO)
realsml: $(REALSML)
theories/Reals/addReals.ml:
cp -f addReals theories/Reals/addReals.ml
$(REALSML):
./extract $@
#
# The End
#
.PHONY: all tree clean reals realsml depend
include .depend
|
