diff options
Diffstat (limited to 'language')
| -rw-r--r-- | language/Makefile | 2 | ||||
| -rw-r--r-- | language/l2.ott | 75 |
2 files changed, 48 insertions, 29 deletions
diff --git a/language/Makefile b/language/Makefile index 595a09e8..dcadaff2 100644 --- a/language/Makefile +++ b/language/Makefile @@ -8,7 +8,7 @@ l2.pdf: l2.tex l2Theory.uo: l2Script.sml Holmake --qof -I $(OTTLIB) l2Theory.uo -l2.tex ../src/ast.ml l2Script.sml: l2.ott ../../../rsem/ott/src/ott +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 ../src/ast.ml -o l2Script.sml -picky_multiple_parses true l2.ott diff --git a/language/l2.ott b/language/l2.ott index 6051051a..3bdfeba8 100644 --- a/language/l2.ott +++ b/language/l2.ott @@ -34,7 +34,7 @@ metavar bin ::= metavar string ::= {{ phantom }} - {{ ocaml terminal * Ulib.UTF8.t }} + {{ ocaml terminal * string }} {{ lem (terminal * string) }} {{ hol string }} {{ com String literals }} @@ -49,22 +49,24 @@ metavar regexp ::= embed {{ ocaml -type text = Ulib.Text.t +type text = string type l = | Unknown | Trans of string * l option | Range of Lexing.position * Lexing.position +type 'a annot = l * 'a + exception Parse_error_locn of l * string type ml_comment = - | Chars of Ulib.Text.t + | Chars of string | Comment of ml_comment list type lex_skip = | Com of ml_comment - | Ws of Ulib.Text.t + | Ws of string | Nl type lex_skips = lex_skip list option @@ -80,7 +82,7 @@ let pp_lex_skips ppf sk = (* TODO: fix? *) Format.fprintf ppf "(**)" | Ws(r) -> - Format.fprintf ppf "%s" (Ulib.Text.to_string r) + Format.fprintf ppf "%s" r (*(Ulib.Text.to_string r)*) | Nl -> Format.fprintf ppf "\\n") sks @@ -165,6 +167,12 @@ l :: '' ::= {{ phantom }} {{ lem Unknown }} {{ hol () }} +annot :: '' ::= + {{ phantom }} + {{ ocaml 'a annot }} + {{ lem annot }} + {{ hol unit }} + id :: '' ::= {{ com Identifier }} {{ aux _ l }} @@ -318,7 +326,7 @@ nexp :: 'Nexp_' ::= order :: 'Ord_' ::= {{ com vector order specifications, of kind $[[Order]]$}} - {{ aux _ l }} + {{ aux _ l }} | id :: :: id {{ com identifier }} | inc :: :: inc {{ com increasing (little-endian) }} | dec :: :: dec {{ com decreasing (big-endian) }} @@ -326,7 +334,7 @@ order :: 'Ord_' ::= effect :: 'Effect_' ::= {{ com effect }} - {{ aux _ l }} + {{ aux _ l }} | rreg :: :: rreg {{ com read register }} | wreg :: :: wreg {{ com write register }} | rmem :: :: rmem {{ com read memory }} @@ -345,9 +353,9 @@ effects :: 'Effects_' ::= % TODO: are we going to need any effect polymorphism? Conceivably for built-in maps and folds. Yes. But we think we don't need any interesting effect-set expressions, eg effectset-variable union {rreg}. - typ :: 'Typ_' ::= {{ com Type expressions, of kind $[[Type]]$ }} + {{ aux _ l }} | _ :: :: wild {{ com Unspecified type }} | id :: :: var @@ -365,6 +373,7 @@ typ :: 'Typ_' ::= typ_arg :: 'Typ_arg_' ::= {{ com Type constructor arguments of all kinds }} + {{ aux _ l }} | nexp :: :: nexp | typ :: :: typ | order :: :: order @@ -374,7 +383,7 @@ typ_arg :: 'Typ_arg_' ::= typ_lib :: 'Typ_lib_' ::= {{ com library types and syntactic sugar for them }} - {{ aux _ l }} + {{ aux _ l }} {{ auxparam 'a }} % boring base types: | unit :: :: unit {{ com unit type with value $()$ }} | bool :: :: bool {{ com booleans $[[true]]$ and $[[false]]$ }} @@ -413,7 +422,7 @@ grammar nexp_constraint :: 'NC_' ::= {{ com constraint over kind $[[Nat]]$ }} - {{ aux _ l }} + {{ aux _ annot }} {{ auxparam 'a }} | nexp = nexp' :: :: fixed | nexp >= nexp' :: :: bounded_ge | nexp '<=' nexp' :: :: bounded_le @@ -424,12 +433,14 @@ nexp_constraint :: 'NC_' ::= kinded_id :: 'KOpt_' ::= {{ com optionally kind-annotated identifier }} + {{ aux _ l }} | id :: :: none {{ com identifier }} | kind id :: :: kind {{ com kind-annotated variable }} | ( kinded_id ) :: S :: paren {{ icho [[kinded_id]] }} typquant :: 'TypQ_' ::= - {{ aux _ l }} {{ com type quantifiers and constraints}} + {{ com type quantifiers and constraints}} + {{ aux _ annot }} {{ auxparam 'a }} | forall kinded_id1 ... kinded_idn . nexp_constraint1 , ... , nexp_constrainti . :: :: tq {{ texlong }} % WHY ARE CONSTRAINTS HERE AND NOT IN THE KIND LANGUAGE @@ -438,8 +449,8 @@ typquant :: 'TypQ_' ::= | :: :: no_forall {{ com sugar, omitting quantifier and constraints }} typschm :: 'TypSchm_' ::= - {{ com type scheme }} - {{ aux _ l }} + {{ com type scheme }} + {{ aux _ annot }} {{ auxparam 'a }} | typquant typ :: :: ts @@ -451,6 +462,7 @@ typschm :: 'TypSchm_' ::= grammar ctor_def :: 'CT_' ::= {{ com Datatype constructor definition clause }} + {{ aux _ annot }} {{ auxparam 'a }} | id : typschm :: :: ct % but we could get away with disallowing constraints in typschm, we % think - if it's useful to do that @@ -470,6 +482,7 @@ ctor_def :: 'CT_' ::= %% naming_scheme_opt :: 'Name_sect_' ::= {{ com Optional variable-naming-scheme specification for variables of defined type }} + {{ aux _ l }} | :: :: none | [ name = regexp ] :: :: some %% @@ -487,6 +500,7 @@ ctor_def :: 'CT_' ::= type_def :: 'TD_' ::= {{ com Type definition body }} + {{ aux _ annot }} {{ auxparam 'a }} | typedef id naming_scheme_opt = typschm :: :: abbrev {{ com type abbreviation }} {{ texlong }} | typedef id naming_scheme_opt = const struct typquant { typ1 id1 ; ... ; typn idn semi_opt } :: :: record @@ -508,6 +522,7 @@ type_def :: 'TD_' ::= index_range :: 'BF_' ::= {{ com index specification, for bitfields in register types}} + {{ aux _ l }} | num :: :: 'single' {{ com single index }} | num1 '..' num2 :: :: range {{ com index range }} | index_range1 , index_range2 :: :: concat {{ com concatenation of index ranges }} @@ -525,6 +540,7 @@ grammar lit :: 'L_' ::= {{ com Literal constant }} + {{ aux _ l }} | ( ) :: :: unit {{ com $() : [[unit]]$ }} %Presumably we want to remove bitzero and bitone ? | bitzero :: :: zero {{ com $[[bitzero]] : [[bit]]$ }} @@ -559,7 +575,7 @@ semi_opt {{ tex \ottnt{;}^{?} }} :: 'semi_' ::= {{ phantom }} pat :: 'P_' ::= {{ com Pattern }} - {{ aux _ l }} + {{ aux _ annot }} {{ auxparam 'a }} | lit :: :: lit {{ com literal constant pattern }} | _ :: :: wild @@ -614,7 +630,7 @@ pat :: 'P_' ::= fpat :: 'FP_' ::= {{ com Field pattern }} - {{ aux _ l }} + {{ aux _ annot }} {{ auxparam 'a }} | id = pat :: :: Fpat parsing @@ -631,7 +647,7 @@ grammar exp :: 'E_' ::= {{ com Expression }} - {{ aux _ l }} + {{ aux _ annot }} {{ auxparam 'a }} | { exp1 ; ... ; expn } :: :: block {{ com block (parsing conflict with structs?) }} % maybe we really should have indentation-sensitive syntax :-) (given that some of the targets do) @@ -736,6 +752,7 @@ exp :: 'E_' ::= lexp :: 'LEXP_' ::= {{ com lvalue expression }} + {{ aux _ annot }} {{ auxparam 'a }} | id :: :: id {{ com identifier }} | lexp [ exp ] :: :: vector {{ com vector element }} @@ -746,17 +763,17 @@ lexp :: 'LEXP_' ::= {{ com lvalue expression }} fexp :: 'FE_' ::= {{ com Field-expression }} - {{ aux _ l }} + {{ aux _ annot }} {{ auxparam 'a }} | id = exp :: :: Fexp fexps :: 'FES_' ::= {{ com Field-expression list }} - {{ aux _ l }} + {{ aux _ annot }} {{ auxparam 'a }} | fexp1 ; ... ; fexpn semi_opt :: :: Fexps pexp :: 'Pat_' ::= {{ com Pattern match }} - {{ aux _ l }} + {{ aux _ annot }} {{ auxparam 'a }} | pat -> exp :: :: exp % apparently could use -> or => for this. @@ -833,29 +850,31 @@ grammar tannot_opt :: 'Typ_annot_opt_' ::= {{ com Optional type annotation for functions}} + {{ aux _ annot }} {{ auxparam 'a }} | :: :: none | typ_quant typ :: :: some rec_opt :: 'Rec_' ::= -% {{ aux _ l }} {{ com Optional recursive annotation for functions }} + {{ aux _ l }} | :: :: nonrec {{ com non-recursive }} | rec :: :: rec {{ com recursive }} effects_opt :: 'Effects_opt_' ::= - {{ aux _ l }} {{ com Optional effect annotation for functions }} + {{ com Optional effect annotation for functions }} + {{ aux _ annot }} {{ auxparam 'a }} | :: :: pure {{ com sugar for empty effect set }} | effects :: :: effects funcl :: 'FCL_' ::= {{ com Function clause }} - {{ aux _ l }} + {{ aux _ annot }} {{ auxparam 'a }} | id pat = exp :: :: Funcl fundef :: 'FD_' ::= {{ com Function definition}} - {{ aux _ l }} + {{ aux _ annot }} {{ auxparam 'a }} | function rec_opt tannot_opt effects_opt funcl1 and ... and funcln :: :: function {{ texlong }} % {{ com function definition }} % TODO note that the typ in the tannot_opt is the *result* type, not @@ -867,7 +886,7 @@ fundef :: 'FD_' ::= letbind :: 'LB_' ::= {{ com Let binding }} - {{ aux _ l }} + {{ aux _ annot }} {{ auxparam 'a }} | typschm pat = exp :: :: val_explicit {{ com value binding, explicit type ([[pat]] must be total)}} | let pat = exp :: :: val_implicit @@ -876,12 +895,12 @@ letbind :: 'LB_' ::= val_spec :: 'VS_' ::= {{ com Value type specification }} - {{ aux _ l }} + {{ aux _ annot }} {{ auxparam 'a }} | val typschm id :: :: val_spec default_typing_spec :: 'DT_' ::= {{ com Default kinding or typing assumption }} - {{ aux _ l }} + {{ aux _ annot }} {{ auxparam 'a }} | default base_kind id :: :: kind | default typschm id :: :: typ % The intended semantics of these is that if an id in binding position @@ -897,7 +916,7 @@ default_typing_spec :: 'DT_' ::= def :: 'DEF_' ::= {{ com Top-level definition }} - {{ aux _ l }} + {{ aux _ annot }} {{ auxparam 'a }} | type_def :: :: type {{ com type definition }} | fundef :: :: fundef @@ -924,7 +943,7 @@ def :: 'DEF_' ::= defs :: '' ::= {{ com Definition sequence }} -% {{ aux _ l }} + {{ auxparam 'a }} | def1 .. defn :: :: Defs |