diff options
| author | Kathy Gray | 2013-07-03 14:48:06 +0100 |
|---|---|---|
| committer | Kathy Gray | 2013-07-03 14:48:30 +0100 |
| commit | af1f1e4cb77fa027275f2466cee7c73d0fa3606f (patch) | |
| tree | 8521a7c22c1338cc0c9b4b31d42e687b5bec1732 /language | |
| parent | d4d4a4fcef7398473c1ba85c5c974ca34cb53cef (diff) | |
Clean up some missed _ s in ott file; move the generated ml file to be ast in a source directory; add source directory and generated ast.
Diffstat (limited to 'language')
| -rw-r--r-- | language/Makefile | 3 | ||||
| -rw-r--r-- | language/l2.ott | 14 |
2 files changed, 8 insertions, 9 deletions
diff --git a/language/Makefile b/language/Makefile index f8858e31..f1607d23 100644 --- a/language/Makefile +++ b/language/Makefile @@ -1,4 +1,3 @@ -#OTTLIB=/Users/sowens/ott/hol OTTLIB=$(dir $(shell which ott))../hol all: l2.pdf @@ -11,7 +10,7 @@ l2Theory.uo: l2Script.sml l2.tex ../src/ast.ml l2Script.sml: l2.ott ott -sort false -generate_aux_rules false -o l2.tex -picky_multiple_parses true l2.ott - ott -sort false -generate_aux_rules true -ocaml_include_terminals true -o l2.ml -o l2Script.sml -picky_multiple_parses true l2.ott + ott -sort false -generate_aux_rules true -ocaml_include_terminals true -o ../src/ast.ml -o l2Script.sml -picky_multiple_parses true l2.ott #rm -f ../src/ast.ml # chmod a-w ../src/ast.ml diff --git a/language/l2.ott b/language/l2.ott index 3c186839..d1bf5793 100644 --- a/language/l2.ott +++ b/language/l2.ott @@ -597,7 +597,7 @@ pat :: 'P_' ::= | lit :: :: lit {{ com Literal constant patterns }} -fpat :: 'FP' ::= +fpat :: 'FP_' ::= {{ com Field patterns }} {{ aux _ l }} | id = pat :: :: Fpat @@ -717,17 +717,17 @@ lexp :: 'LEXP_' ::= | lexp . id :: :: field -fexp :: 'FE' ::= +fexp :: 'FE_' ::= {{ com Field-expressions }} {{ aux _ l }} | id = exp :: :: Fexp -fexps :: 'FES' ::= +fexps :: 'FES_' ::= {{ com Field-expression lists }} {{ aux _ l }} | fexp1 ; ... ; fexpn semi_opt :: :: Fexps -pexp :: 'Pat' ::= +pexp :: 'Pat_' ::= {{ com Pattern matches }} {{ aux _ l }} | pat -> exp :: :: exp @@ -809,7 +809,7 @@ c_tannot_opt :: 'C_typ_annot_' ::= | :: :: none | typ_quant typ :: :: some -c_funcl :: 'C_FCL' ::= +c_funcl :: 'C_FCL_' ::= {{ com Function clauses }} {{ aux _ l }} | id pat = exp :: :: Funcl @@ -824,7 +824,7 @@ c_effects_opt :: '' ::= | :: :: pure {{ com sugar for pure }} | effects :: :: nonpure -c_fundef :: 'C_FD' ::= +c_fundef :: 'C_FD_' ::= {{ com Function definition}} {{ aux _ l }} | function c_rec_opt c_tannot_opt c_effects_opt c_funcl1 and ... and c_funcln :: :: function {{ texlong }} {{ com function definition }} @@ -844,7 +844,7 @@ c_letbind :: 'LB_' ::= {{ com value binding with implicit type }} -val_spec :: 'VS' ::= +val_spec :: 'VS_' ::= {{ com Value type specifications }} {{ aux _ l }} | val typschm id :: :: val_spec |