diff options
| -rw-r--r-- | language/Makefile | 6 | ||||
| -rw-r--r-- | language/l2.ott | 58 | ||||
| -rw-r--r-- | language/l2_terminals_non_tt.ott | 31 | ||||
| -rw-r--r-- | language/l2_terminals_tt.ott | 31 |
4 files changed, 94 insertions, 32 deletions
diff --git a/language/Makefile b/language/Makefile index c297829c..bbccf6a5 100644 --- a/language/Makefile +++ b/language/Makefile @@ -1,6 +1,6 @@ #OTT=../../../rsem/ott/bin/ott # this is the binary that gets rebuilt by make in ott/src: -OTT=../../../github/ott/src/ott +OTT=../../../github/ott/src/ott -merge true OTTLIB=$(dir $(shell which ott))../hol .PHONY: all @@ -18,10 +18,10 @@ type_system.pdf: doc_in.tex type_system.tex pdflatex type_system.tex pdflatex type_system.tex -l2.tex: l2.ott l2_typ.ott l2_rules.ott +l2.tex: l2.ott l2_terminals_non_tt.ott l2_typ.ott l2_rules.ott $(OTT) -sort false -generate_aux_rules false -o $@ -picky_multiple_parses true $^ -doc_in.tex: l2.ott primitive_doc.ott l2_typ.ott l2_rules.ott +doc_in.tex: l2.ott primitive_doc.ott l2_terminals_tt.ott l2_typ.ott l2_rules.ott $(OTT) -sort false -generate_aux_rules false -tex_wrap false -o $@ -picky_multiple_parses true $^ %.tex: %.ott diff --git a/language/l2.ott b/language/l2.ott index fdeaf743..599e89bf 100644 --- a/language/l2.ott +++ b/language/l2.ott @@ -950,21 +950,21 @@ terminals :: '' ::= | ** :: :: starstar {{ tex \ensuremath{\mathop{\mathord{*}\mathord{*} } } }} {{ com \texttt{**} }} - | >= :: :: geq -% {{ tex \ensuremath{\geq} }} - {{ tex \ottsym{\textgreater=} }} - {{ com \texttt{>=} }} - | '<=' :: :: leq -% {{ tex \ensuremath{\leq} }} - {{ tex \ottsym{\textless=} }} - {{ com \texttt{<=} }} - | -> :: :: arrow -% {{ tex \ensuremath{\rightarrow} }} - {{ tex \ottsym{-\textgreater} }} - {{ com \texttt{->} }} - | ==> :: :: Longrightarrow - {{ tex \ensuremath{\Longrightarrow} }} - {{ com \texttt{==>} }} +% | >= :: :: geq +% % {{ tex \ensuremath{\geq} }} +% {{ tex \ottsym{\textgreater=} }} +% {{ com \texttt{>=} }} +% | '<=' :: :: leq +% % {{ tex \ensuremath{\leq} }} +% {{ tex \ottsym{\textless=} }} +% {{ com \texttt{<=} }} +% | -> :: :: arrow +% % {{ tex \ensuremath{\rightarrow} }} +% {{ tex \ottsym{-\textgreater} }} +% {{ com \texttt{->} }} + | ==> :: :: Longrightarrow + {{ tex \ensuremath{\Longrightarrow} }} + {{ com \texttt{==>} }} % | <| :: :: startrec % {{ tex \ensuremath{\langle|} }} % {{ com \texttt{<|} }} @@ -985,12 +985,12 @@ terminals :: '' ::= {{ tex \ensuremath{\not=} }} | emptyset :: :: emptyset {{ tex \ensuremath{\emptyset} }} - | < :: :: lt -% {{ tex \ensuremath{\langle} }} - {{ tex \ottsym{<} }} - | > :: :: gt -% {{ tex \ensuremath{\rangle} }} - {{ tex \ottsym{>} }} +% | < :: :: lt +% % {{ tex \ensuremath{\langle} }} +% {{ tex \ottsym{<} }} +% | > :: :: gt +% % {{ tex \ensuremath{\rangle} }} +% {{ tex \ottsym{>} }} | lt :: :: mathlt {{ tex < }} | gt :: :: mathgt @@ -1035,13 +1035,13 @@ terminals :: '' ::= {{ tex \ottkw{consistent\_decrease}~ }} | == :: :: equiv {{ tex \equiv }} - | [| :: :: range_start - {{ tex \mbox{$\ottsym{[\textbar}$} }} - | |] :: :: range_end - {{ tex \mbox{$\ottsym{\textbar]}$} }} - | [|| :: :: list_start - {{ tex \mbox{$\ottsym{[\textbar\textbar}$} }} - | ||] :: :: list_end - {{ tex \mbox{$\ottsym{\textbar\textbar]}$} }} +% | [| :: :: range_start +% {{ tex \mbox{$\ottsym{[\textbar}$} }} +% | |] :: :: range_end +% {{ tex \mbox{$\ottsym{\textbar]}$} }} +% | [|| :: :: list_start +% {{ tex \mbox{$\ottsym{[\textbar\textbar}$} }} +% | ||] :: :: list_end +% {{ tex \mbox{$\ottsym{\textbar\textbar]}$} }} diff --git a/language/l2_terminals_non_tt.ott b/language/l2_terminals_non_tt.ott new file mode 100644 index 00000000..2c466b8b --- /dev/null +++ b/language/l2_terminals_non_tt.ott @@ -0,0 +1,31 @@ +grammar +terminals :: '' ::= + | < :: :: lt + {{ tex \ensuremath{\langle} }} +% {{ tex \ottsym{<} }} + | > :: :: gt + {{ tex \ensuremath{\rangle} }} +% {{ tex \ottsym{>} }} + +% | [| :: :: range_start +% {{ tex \mbox{$\ottsym{[\textbar}$} }} +% | |] :: :: range_end +% {{ tex \mbox{$\ottsym{\textbar]}$} }} +% | [|| :: :: list_start +% {{ tex \mbox{$\ottsym{[\textbar\textbar}$} }} +% | ||] :: :: list_end +% {{ tex \mbox{$\ottsym{\textbar\textbar]}$} }} + + | -> :: :: arrow + {{ tex \ensuremath{\rightarrow} }} +% {{ tex \ottsym{-\textgreater} }} + {{ com \texttt{->} }} + + | >= :: :: geq + {{ tex \ensuremath{\geq} }} +% {{ tex \ottsym{\textgreater=} }} + {{ com \texttt{>=} }} + | '<=' :: :: leq + {{ tex \ensuremath{\leq} }} +% {{ tex \ottsym{\textless=} }} + {{ com \texttt{<=} }} diff --git a/language/l2_terminals_tt.ott b/language/l2_terminals_tt.ott new file mode 100644 index 00000000..c6bc8d34 --- /dev/null +++ b/language/l2_terminals_tt.ott @@ -0,0 +1,31 @@ +grammar +terminals :: '' ::= + | < :: :: lt +% {{ tex \ensuremath{\langle} }} + {{ tex \ottsym{<} }} + | > :: :: gt +% {{ tex \ensuremath{\rangle} }} + {{ tex \ottsym{>} }} + + | [| :: :: range_start + {{ tex \mbox{$\ottsym{[\textbar}$} }} + | |] :: :: range_end + {{ tex \mbox{$\ottsym{\textbar]}$} }} + | [|| :: :: list_start + {{ tex \mbox{$\ottsym{[\textbar\textbar}$} }} + | ||] :: :: list_end + {{ tex \mbox{$\ottsym{\textbar\textbar]}$} }} + + | -> :: :: arrow +% {{ tex \ensuremath{\rightarrow} }} + {{ tex \ottsym{-\textgreater} }} + {{ com \texttt{->} }} + + | >= :: :: geq +% {{ tex \ensuremath{\geq} }} + {{ tex \ottsym{\textgreater=} }} + {{ com \texttt{>=} }} + | '<=' :: :: leq +% {{ tex \ensuremath{\leq} }} + {{ tex \ottsym{\textless=} }} + {{ com \texttt{<=} }} |