diff options
| author | Brian Campbell | 2017-10-18 15:07:24 +0100 |
|---|---|---|
| committer | Brian Campbell | 2017-10-18 15:07:24 +0100 |
| commit | bd9cabab3e20b92a705f37f0a1974033a869bde0 (patch) | |
| tree | c73e3e47b4ce0578c9b79ca3ebd3ad74db93ffa4 /language/Makefile | |
| parent | 79043c19238559a7daea7b495e604ef00a6b2a8c (diff) | |
| parent | 4043f496ff8dae7fa2bc2b4da4e02d2d9942e66d (diff) | |
Merge branch 'experiments' of Peter_Sewell/sail into mono-experiments
(and fix up monomorphisation)
Diffstat (limited to 'language/Makefile')
| -rw-r--r-- | language/Makefile | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/language/Makefile b/language/Makefile index 9167d65f..77aa5607 100644 --- a/language/Makefile +++ b/language/Makefile @@ -4,7 +4,7 @@ OTT=../../../github/ott/src/ott OTTLIB=$(dir $(shell which ott))../hol .PHONY: all -all: l2.ml l2_parse.ml l2.lem +all: l2.ml l2_parse.ml l2.lem l2_parse2.ml l2_parse2_parser.mly docs: l2.pdf l2_parse.pdf @@ -36,6 +36,12 @@ doc_in.tex: l2.ott primitive_doc.ott l2_terminals_tt.ott l2_typ.ott l2_rules.ott l2.lem: l2.ott $(OTT) -sort false -generate_aux_rules true -o $@ -picky_multiple_parses true $^ +ROOT=l2_parse2 +# generate the ocaml AST type, ocamllex lexer, menhir parser, and ocaml pretty printers for the AST, all from the Ott soruce +$(ROOT)_ast.ml $(ROOT)_lexer.mll $(ROOT)_parser.mly $(ROOT)_parser_pp.ml $(ROOT)_ast.tex : $(ROOT).ott Makefile + $(OTT) -quotient_rules false -generate_aux_rules false -i $(ROOT).ott -o $(ROOT)_parser.mly -o $(ROOT)_lexer.mll -o $(ROOT)_ast.ml -o $(ROOT).tex + + clean: rm -rf *~ rm -rf *.uo *.ui *.sig *.sml .HOLMK |