]> matita.cs.unibo.it Git - helm.git/blob - helm/ocaml/cic_disambiguation/Makefile
opt goal fixed
[helm.git] / helm / ocaml / cic_disambiguation / Makefile
1
2 PACKAGE = cic_textual_parser2
3 REQUIRES = ulex pxp helm-tactics helm-logger helm-cic_unification camlp4.gramlib
4 NOTATIONS = logic arit tex
5 INTERFACE_FILES = \
6         disambiguateTypes.mli \
7         disambiguateChoices.mli \
8         cicTextualParser2Pp.mli \
9         macro.mli \
10         cicTextualLexer2.mli \
11         cicTextualParser2.mli \
12         disambiguate.mli
13 IMPLEMENTATION_FILES = \
14         $(patsubst %.mli, %.ml, $(INTERFACE_FILES)) \
15         $(patsubst %,%_notation.ml,$(NOTATIONS))
16
17 ULEXDIR := $(shell ocamlfind query ulex)
18
19 LEXER_P4_OPTS = -I $(ULEXDIR) pa_ulex.cma
20 PARSER_P4_OPTS = pa_extend.cmo ./macro.cmo ./pa_unicode_macro.cmo
21 PA_P4_OPTS = q_MLast.cmo pa_extend.cmo
22
23 all:
24
25 cicTextualLexer2.cmo: cicTextualLexer2.ml
26         $(OCAMLC) -pp "camlp4o $(LEXER_P4_OPTS)" -c $<
27 cicTextualParser2.cmo: cicTextualParser2.ml macro.cmo pa_unicode_macro.cmo
28         $(OCAMLC) -pp "camlp4o $(PARSER_P4_OPTS)" -c $<
29 cicTextualLexer2.cmx: cicTextualLexer2.ml
30         $(OCAMLOPT) -pp "camlp4o $(LEXER_P4_OPTS)" -c $<
31 cicTextualParser2.cmx: cicTextualParser2.ml macro.cmo pa_unicode_macro.cmo
32         $(OCAMLOPT) -pp "camlp4o $(PARSER_P4_OPTS)" -c $<
33
34 %_notation.cmo: %_notation.ml cicTextualParser2.cmo
35         $(OCAMLC) -pp "camlp4o $(PARSER_P4_OPTS)" -c $<
36 %_notation.cmx: %_notation.ml cicTextualParser2.cmx
37         $(OCAMLOPT) -pp "camlp4o $(PARSER_P4_OPTS)" -c $<
38
39 pa_unicode_macro.cmo: pa_unicode_macro.ml macro.cmo
40         $(OCAMLC) -pp "camlp4o $(PA_P4_OPTS)" -c $<
41 pa_unicode_macro.cmx: pa_unicode_macro.ml macro.cmx
42         $(OCAMLOPT) -pp "camlp4o $(PA_P4_OPTS)" -c $<
43
44 LOCAL_LINKOPTS = -linkpkg $(PACKAGE).cma
45 test: test_lexer test_parser
46 test_lexer: test_lexer.ml $(PACKAGE).cma
47         $(OCAMLC) $(LOCAL_LINKOPTS) -o $@ $<
48 test_parser: test_parser.ml $(PACKAGE).cma
49         $(OCAMLC) $(LOCAL_LINKOPTS) -o $@ $<
50 make_table: make_table.ml
51         $(OCAMLC) -linkpkg -o $@ $<
52
53 .PHONY: macro_table.dump
54 macro_table.dump: make_table
55         ./make_table $@
56
57 clean: extra_clean
58 distclean: extra_clean
59         rm -f macro_table.dump
60 extra_clean:
61         rm -f test_lexer test_parser make_table
62
63 include ../Makefile.common
64
65 .PHONY: depend
66 depend: macro.cmi macro.cmo pa_unicode_macro.cmi pa_unicode_macro.cmo
67         $(OCAMLDEP) -pp "camlp4o $(PARSER_P4_OPTS) $(LEXER_P4_OPTS)" $(INTERFACE_FILES) $(IMPLEMENTATION_FILES) > .depend
68
69 disambiguateTypes.cmi: disambiguateTypes.mli
70         $(OCAMLC) -c -rectypes $<
71 disambiguateTypes.cmo: disambiguateTypes.ml disambiguateTypes.cmi
72         $(OCAMLC) -c -rectypes $<
73 disambiguateTypes.cmx: disambiguateTypes.ml disambiguateTypes.cmi
74         $(OCAMLOPT) -c -rectypes $<
75