blob: 038b3d00eb627810e1763228d05b4fb93475d86b (
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
|
FILES=\
Datatypes.ml Logic.ml Wf.ml Peano.ml Specif.ml Compare_dec.ml \
Bool.ml List.ml Sumbool.ml BinPos.ml BinNat.ml BinInt.ml \
ZArith_dec.ml Zeven.ml Zmin.ml Zmisc.ml Zbool.ml Zpower.ml Zdiv.ml \
FSetInterface.ml FSetBridge.ml FSetList.ml FSetAVL.ml \
Coqlib.ml Maps.ml Sets.ml union_find.ml AST.ml Integers.ml \
../caml/Camlcoq.ml ../caml/Floataux.ml Floats.ml Values.ml \
Mem.ml Globalenvs.ml \
Op.ml Cminor.ml Cmconstr.ml \
Csharpminor.ml Cminorgen.ml \
Registers.ml RTL.ml \
../caml/RTLgenaux.ml RTLgen.ml \
RTLtyping.ml \
Lattice.ml Kildall.ml \
Constprop.ml CSE.ml \
Locations.ml Conventions.ml LTL.ml \
Ordered.ml InterfGraph.ml ../caml/Coloringaux.ml Coloring.ml \
Parallelmove.ml Allocation.ml \
Tunneling.ml Linear.ml Lineartyping.ml Linearize.ml \
Mach.ml Stacking.ml \
PPC.ml PPCgen.ml \
Main.ml \
../caml/CMparser.ml ../caml/CMlexer.ml \
../caml/PrintPPC.ml ../caml/Main2.ml
EXTRACTEDFILES:=$(filter-out ../caml/%, $(FILES))
GENFILES:=$(EXTRACTEDFILES) $(EXTRACTEDFILES:.ml=.mli)
CAMLINCL=-I ../caml
OCAMLC=ocamlc -g $(CAMLINCL)
OCAMLOPT=ocamlopt $(CAMLINCL)
OCAMLDEP=ocamldep $(CAMLINCL)
COQINCL=-I ../lib -I ../backend
COQEXEC=coqtop $(COQINCL) -batch -load-vernac-source
../ccomp: $(FILES:.ml=.cmo)
$(OCAMLC) -o ../ccomp $(FILES:.ml=.cmo)
../ccomp.opt: Pack.cmx
$(OCAMLOPT) -o ../ccomp.opt Pack.cmx
Pack.cmx: $(FILES:.ml=.cmx)
$(OCAMLOPT) -pack -o Pack.cmx $(FILES:.ml=.cmx)
extraction:
@rm -f $(GENFILES)
$(COQEXEC) extraction.v
@echo "Fixing file names..."
@for i in $(GENFILES); do \
j=`./uncapitalize $$i`; \
test -f $$i || (test -f $$j && mv $$j $$i); \
done
@echo "Patching files..."
@for i in *.patch; do patch < $$i; done
../caml/CMparser.ml ../caml/CMparser.mli: ../caml/CMparser.mly
ocamlyacc -v ../caml/CMparser.mly
beforedepend:: ../caml/CMparser.ml ../caml/CMparser.mli
clean::
rm -f ../caml/CMparser.ml ../caml/CMparser.mli ../caml/CMparser.output
../caml/CMlexer.ml: ../caml/CMlexer.mll
ocamllex ../caml/CMlexer.mll
beforedepend:: ../caml/CMlexer.ml
clean::
rm -f ../caml/CMlexer.ml
.SUFFIXES: .ml .mli .cmo .cmi .cmx
.mli.cmi:
$(OCAMLC) -c $*.mli
.ml.cmo:
$(OCAMLC) -c $*.ml
.ml.cmx:
$(OCAMLOPT) -c $*.ml
clean::
rm -f $(GENFILES)
rm -f *.cm? *.o
cd ../caml && rm -f *.cm? *.o
rm -f ccomp
depend: beforedepend
$(OCAMLDEP) ../caml/*.mli ../caml/*.ml *.mli *.ml > .depend
include .depend
|
