diff options
Diffstat (limited to 'language')
| -rw-r--r-- | language/l2.ott | 99 |
1 files changed, 48 insertions, 51 deletions
diff --git a/language/l2.ott b/language/l2.ott index 1cc9b3fd..6051051a 100644 --- a/language/l2.ott +++ b/language/l2.ott @@ -49,30 +49,26 @@ metavar regexp ::= embed {{ ocaml +type text = Ulib.Text.t - -type text = string (* was Ulib.Text.t *) - -type 'a l = 'a -(* +type l = | Unknown | Trans of string * l option | Range of Lexing.position * Lexing.position -*) -exception Parse_error_locn of string l * string + +exception Parse_error_locn of l * string type ml_comment = - | Chars of text + | Chars of Ulib.Text.t | Comment of ml_comment list type lex_skip = | Com of ml_comment - | Ws of text + | Ws of Ulib.Text.t | Nl type lex_skips = lex_skip list option -(* let pp_lex_skips ppf sk = match sk with | None -> () @@ -93,7 +89,7 @@ let combine_lex_skips s1 s2 = | (None,_) -> s2 | (_,None) -> s1 | (Some(s1),Some(s2)) -> Some(s2@s1) -*) + type terminal = lex_skips }} @@ -160,9 +156,9 @@ metavar ix ::= grammar l :: '' ::= {{ phantom }} - {{ ocaml 'a l }} + {{ ocaml l }} {{ lem l }} - {{ hol unit }} + {{ hol unit }} {{ com Source location }} | :: :: Unknown {{ ocaml Unknown }} @@ -171,7 +167,7 @@ l :: '' ::= {{ phantom }} id :: '' ::= {{ com Identifier }} - {{ aux _ l }} {{ auxparam 'a }} + {{ aux _ l }} | x :: :: id | ( x ) :: :: deIid {{ com remove infix status }} % Note: we have just a single namespace. We don't want the same @@ -228,7 +224,7 @@ grammar % a :: 'A_' ::= -% {{ aux _ l }} {{ auxparam 'a }} +% {{ aux _ l }} % {{ ocaml terminal * text }} % {{ lem terminal * string }} % {{ hol string }} @@ -237,7 +233,7 @@ grammar % {{ ichlo [[x]] }} % % N :: 'N_' ::= -% {{ aux _ l }} {{ auxparam 'a }} +% {{ aux _ l }} % {{ ocaml terminal * text }} % {{ lem terminal * string }} % {{ hol string }} @@ -246,7 +242,7 @@ grammar % {{ ichlo [[x]] }} % % EN :: 'EN_' ::= -% {{ aux _ l }} {{ auxparam 'a }} +% {{ aux _ l }} % {{ ocaml terminal * text }} % {{ lem terminal * string }} % {{ hol string }} @@ -255,7 +251,7 @@ grammar % {{ ichlo [[x]] }} % % EFF :: 'EFF_' ::= -% {{ aux _ l }} {{ auxparam 'a }} +% {{ aux _ l }} % {{ ocaml terminal * text }} % {{ lem terminal * string }} % {{ hol string }} @@ -296,7 +292,7 @@ grammar base_kind :: 'BK_' ::= {{ com base kind}} - {{ aux _ l }} {{ auxparam 'a }} + {{ aux _ l }} | Type :: :: type {{ com kind of types }} | Nat :: :: nat {{ com kind of natural number size expressions }} | Order :: :: order {{ com kind of vector order specifications }} @@ -304,14 +300,14 @@ base_kind :: 'BK_' ::= kind :: 'K_' ::= {{ com kinds}} - {{ aux _ l }} {{ auxparam 'a }} + {{ aux _ l }} | base_kind1 -> ... -> base_kindn :: :: kind % we'll never use ...-> Nat nexp :: 'Nexp_' ::= {{ com expression of kind $[[Nat]]$, for vector sizes and origins }} - {{ aux _ l }} {{ auxparam 'a }} + {{ aux _ l }} | id :: :: id {{ com identifier }} | num :: :: constant {{ com constant }} | nexp1 * nexp2 :: :: times {{ com product }} @@ -322,7 +318,7 @@ nexp :: 'Nexp_' ::= order :: 'Ord_' ::= {{ com vector order specifications, of kind $[[Order]]$}} - {{ aux _ l }} {{ auxparam 'a }} + {{ aux _ l }} | id :: :: id {{ com identifier }} | inc :: :: inc {{ com increasing (little-endian) }} | dec :: :: dec {{ com decreasing (big-endian) }} @@ -330,7 +326,7 @@ order :: 'Ord_' ::= effect :: 'Effect_' ::= {{ com effect }} - {{ aux _ l }} {{ auxparam 'a }} + {{ aux _ l }} | rreg :: :: rreg {{ com read register }} | wreg :: :: wreg {{ com write register }} | rmem :: :: rmem {{ com read memory }} @@ -342,7 +338,7 @@ effect :: 'Effect_' ::= effects :: 'Effects_' ::= {{ com effect set, of kind $[[Effects]]$ }} - {{ aux _ l }} {{ auxparam 'a }} + {{ aux _ l }} | id :: :: var | { effect1 , .. , effectn } :: :: set {{ com effect set }} | pure :: M :: pure {{ com sugar for empty effect set }} {{ icho [] }} @@ -351,7 +347,7 @@ effects :: 'Effects_' ::= typ :: 'Typ_' ::= - {{ com Type expressions, of kind $[[Type]]$ }} {{ aux _ l }} {{ auxparam 'a }} + {{ com Type expressions, of kind $[[Type]]$ }} | _ :: :: wild {{ com Unspecified type }} | id :: :: var @@ -368,7 +364,7 @@ typ :: 'Typ_' ::= | ( typ ) :: S :: paren {{ icho [[typ]] }} typ_arg :: 'Typ_arg_' ::= - {{ com Type constructor arguments of all kinds }} {{ aux _ l}} + {{ com Type constructor arguments of all kinds }} | nexp :: :: nexp | typ :: :: typ | order :: :: order @@ -378,7 +374,7 @@ typ_arg :: 'Typ_arg_' ::= typ_lib :: 'Typ_lib_' ::= {{ com library types and syntactic sugar for them }} - {{ aux _ l }} {{ auxparam 'a }} + {{ aux _ l }} % boring base types: | unit :: :: unit {{ com unit type with value $()$ }} | bool :: :: bool {{ com booleans $[[true]]$ and $[[false]]$ }} @@ -417,7 +413,7 @@ grammar nexp_constraint :: 'NC_' ::= {{ com constraint over kind $[[Nat]]$ }} - {{ aux _ l }} {{ auxparam 'a }} + {{ aux _ l }} | nexp = nexp' :: :: fixed | nexp >= nexp' :: :: bounded_ge | nexp '<=' nexp' :: :: bounded_le @@ -427,13 +423,13 @@ nexp_constraint :: 'NC_' ::= % finite-set-bound, as we don't think we need anything more kinded_id :: 'KOpt_' ::= - {{ com optionally kind-annotated identifier }} {{ aux _ l }} {{ auxparam 'a }} + {{ com optionally kind-annotated identifier }} | id :: :: none {{ com identifier }} | kind id :: :: kind {{ com kind-annotated variable }} | ( kinded_id ) :: S :: paren {{ icho [[kinded_id]] }} typquant :: 'TypQ_' ::= - {{ aux _ l }} {{ auxparam 'a }} {{ com type quantifiers and constraints}} + {{ aux _ l }} {{ com type quantifiers and constraints}} | forall kinded_id1 ... kinded_idn . nexp_constraint1 , ... , nexp_constrainti . :: :: tq {{ texlong }} % WHY ARE CONSTRAINTS HERE AND NOT IN THE KIND LANGUAGE @@ -443,7 +439,7 @@ typquant :: 'TypQ_' ::= typschm :: 'TypSchm_' ::= {{ com type scheme }} - {{ aux _ l }} {{ auxparam 'a }} + {{ aux _ l }} | typquant typ :: :: ts @@ -563,7 +559,7 @@ semi_opt {{ tex \ottnt{;}^{?} }} :: 'semi_' ::= {{ phantom }} pat :: 'P_' ::= {{ com Pattern }} - {{ aux _ l }} {{ auxparam 'a }} + {{ aux _ l }} | lit :: :: lit {{ com literal constant pattern }} | _ :: :: wild @@ -618,7 +614,7 @@ pat :: 'P_' ::= fpat :: 'FP_' ::= {{ com Field pattern }} - {{ aux _ l }} {{ auxparam 'a }} + {{ aux _ l }} | id = pat :: :: Fpat parsing @@ -635,7 +631,7 @@ grammar exp :: 'E_' ::= {{ com Expression }} - {{ aux _ l }} {{ auxparam 'a }} + {{ aux _ l }} | { exp1 ; ... ; expn } :: :: block {{ com block (parsing conflict with structs?) }} % maybe we really should have indentation-sensitive syntax :-) (given that some of the targets do) @@ -750,23 +746,23 @@ lexp :: 'LEXP_' ::= {{ com lvalue expression }} fexp :: 'FE_' ::= {{ com Field-expression }} - {{ aux _ l }} {{ auxparam 'a }} + {{ aux _ l }} | id = exp :: :: Fexp fexps :: 'FES_' ::= {{ com Field-expression list }} - {{ aux _ l }} {{ auxparam 'a }} + {{ aux _ l }} | fexp1 ; ... ; fexpn semi_opt :: :: Fexps pexp :: 'Pat_' ::= {{ com Pattern match }} - {{ aux _ l }} {{ auxparam 'a }} + {{ aux _ l }} | pat -> exp :: :: exp % apparently could use -> or => for this. %% % psexp :: 'Pats' ::= %% % {{ com Multi-pattern matches }} -%% % {{ aux _ l }} {{ auxparam 'a }} +%% % {{ aux _ l }} %% % | pat1 ... patn -> exp :: :: exp @@ -807,12 +803,12 @@ grammar %% % %% % lem_funcl :: 'LEM_FCL' ::= %% % {{ com Function clauses }} -%% % {{ aux _ l }} {{ auxparam 'a }} +%% % {{ aux _ l }} %% % | id pat1 ... patn tannot_opt = exp :: :: Funcl %% % %% % lem_letbind :: 'LEM_LB_' ::= %% % {{ com Let bindings }} -%% % {{ aux _ l }} {{ auxparam 'a }} +%% % {{ aux _ l }} %% % | pat tannot_opt = exp :: :: Let_val %% % {{ com Value bindings }} %% % | lem_funcl :: :: Let_fun @@ -822,7 +818,7 @@ grammar %% % grammar %% % lem_val_def :: 'LEM_VD' ::= %% % {{ com Value definitions }} -%% % {{ aux _ l }} {{ auxparam 'a }} +%% % {{ aux _ l }} %% % | let lem_letbind :: :: Let_def %% % {{ com Non-recursive value definitions }} %% % | let rec lem_funcl1 and ... and lem_funcln :: :: Let_rec @@ -830,7 +826,7 @@ grammar %% % %% % lem_val_spec :: 'LEM_VS' ::= %% % {{ com Value type specifications }} -%% % {{ aux _ l }} {{ auxparam 'a }} +%% % {{ aux _ l }} %% % | val x_l : typschm :: :: Val_spec %%%%% C-ish style %%%%%%%%%% @@ -841,24 +837,25 @@ tannot_opt :: 'Typ_annot_opt_' ::= | typ_quant typ :: :: some rec_opt :: 'Rec_' ::= - {{ aux _ l }} {{ auxparam 'a }} {{ com Optional recursive annotation for functions }} +% {{ aux _ l }} + {{ com Optional recursive annotation for functions }} | :: :: nonrec {{ com non-recursive }} | rec :: :: rec {{ com recursive }} effects_opt :: 'Effects_opt_' ::= - {{ aux _ l }} {{ auxparam 'a }} {{ com Optional effect annotation for functions }} + {{ aux _ l }} {{ com Optional effect annotation for functions }} | :: :: pure {{ com sugar for empty effect set }} | effects :: :: effects funcl :: 'FCL_' ::= {{ com Function clause }} - {{ aux _ l }} {{ auxparam 'a }} + {{ aux _ l }} | id pat = exp :: :: Funcl fundef :: 'FD_' ::= {{ com Function definition}} - {{ aux _ l }} {{ auxparam 'a }} + {{ aux _ l }} | 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 @@ -870,7 +867,7 @@ fundef :: 'FD_' ::= letbind :: 'LB_' ::= {{ com Let binding }} - {{ aux _ l }} {{ auxparam 'a }} + {{ aux _ l }} | typschm pat = exp :: :: val_explicit {{ com value binding, explicit type ([[pat]] must be total)}} | let pat = exp :: :: val_implicit @@ -879,12 +876,12 @@ letbind :: 'LB_' ::= val_spec :: 'VS_' ::= {{ com Value type specification }} - {{ aux _ l }} {{ auxparam 'a }} + {{ aux _ l }} | val typschm id :: :: val_spec default_typing_spec :: 'DT_' ::= {{ com Default kinding or typing assumption }} - {{ aux _ l }} {{ auxparam 'a }} + {{ aux _ l }} | default base_kind id :: :: kind | default typschm id :: :: typ % The intended semantics of these is that if an id in binding position @@ -900,7 +897,7 @@ default_typing_spec :: 'DT_' ::= def :: 'DEF_' ::= {{ com Top-level definition }} - {{ aux _ l }} {{ auxparam 'a }} + {{ aux _ l }} | type_def :: :: type {{ com type definition }} | fundef :: :: fundef @@ -927,7 +924,7 @@ def :: 'DEF_' ::= defs :: '' ::= {{ com Definition sequence }} -% {{ aux _ l }} {{ auxparam 'a }} +% {{ aux _ l }} | def1 .. defn :: :: Defs |