From 80628627e3d1bfc3cfca0d1c676f256e5fcba10b Mon Sep 17 00:00:00 2001
From: Kathy Gray
Date: Fri, 21 Feb 2014 23:09:09 +0000
Subject: 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.
---
 language/Makefile | 10 +++-------
 1 file changed, 3 insertions(+), 7 deletions(-)

(limited to 'language/Makefile')

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 *~
-- 
cgit v1.2.3