diff options
| author | Kathy Gray | 2014-02-21 23:09:09 +0000 |
|---|---|---|
| committer | Kathy Gray | 2014-02-21 23:09:09 +0000 |
| commit | 80628627e3d1bfc3cfca0d1c676f256e5fcba10b (patch) | |
| tree | d1340eaca97771b3f1cd0e2b60db5ef1e9ea5514 /language/Makefile | |
| parent | 53146de4b82f90d1b06e9a09c5ec7c5b458fda53 (diff) | |
Add type annotations to lem grammar, including printing out the annotated ast, and extending the interpreter to expect annotations.
Annotations and locations are still not used by the interpreter.
Diffstat (limited to 'language/Makefile')
| -rw-r--r-- | language/Makefile | 10 |
1 files changed, 3 insertions, 7 deletions
diff --git a/language/Makefile b/language/Makefile index d650f957..2076069c 100644 --- a/language/Makefile +++ b/language/Makefile @@ -9,7 +9,7 @@ all: l2.pdf l2_parse.pdf l2.ml l2_parse.ml l2.lem %Theory.uo: %Script.sml Holmake --qof -I $(OTTLIB) $@ -l2.tex: l2.ott l2_rules.ott +l2.tex: l2.ott l2_typ.ott l2_rules.ott ott -sort false -generate_aux_rules false -o $@ -picky_multiple_parses true $^ %.tex: %.ott @@ -21,12 +21,8 @@ l2.tex: l2.ott l2_rules.ott %Script.sml: %.ott ott -sort false -generate_aux_rules true -o $@ -picky_multiple_parses true $^ -%.lem: %.ott - # work around what is probably a bug in -generate_aux_rules true: when we try to generate Lem code with - # that turned on, we get some surprising-looking parse failures in a - # few rules. Likely we're not doing the proper transform for rules - # generated from inductive relation syntax. - ott -sort false -generate_aux_rules false -o $@ -picky_multiple_parses true $^ +l2.lem: l2.ott l2_typ.ott + ott -sort false -generate_aux_rules true -o $@ -picky_multiple_parses true $^ clean: rm -rf *~ |