diff options
Diffstat (limited to 'language/l2.ott')
| -rw-r--r-- | language/l2.ott | 254 |
1 files changed, 131 insertions, 123 deletions
diff --git a/language/l2.ott b/language/l2.ott index 031cfb5a..5002eb2b 100644 --- a/language/l2.ott +++ b/language/l2.ott @@ -138,7 +138,7 @@ metavar x , y , z ::= {{ ocaml terminal * text }} {{ lem terminal * string }} {{ hol string }} - {{ com Variables }} + {{ com identifier }} {{ ocamlvar "[[x]]" }} {{ lemvar "[[x]]" }} @@ -147,7 +147,7 @@ metavar ix ::= {{ ocaml terminal * text }} {{ lem terminal * string }} {{ hol string }} - {{ com Variables }} + {{ com infix identifier }} {{ ocamlvar "[[ix]]" }} {{ lemvar "[[ix]]" }} @@ -159,17 +159,17 @@ l :: '' ::= {{ phantom }} {{ ocaml l }} {{ lem l }} {{ hol unit }} - {{ com Source locations }} + {{ com Source location }} | :: :: Unknown {{ ocaml Unknown }} {{ lem Unknown }} {{ hol () }} id :: '' ::= - {{ com identifiers }} + {{ com Identifier }} {{ aux _ l }} - | x :: :: Id - | ( x ) :: :: DeIId {{ com remove infix status }} + | x :: :: id + | ( x ) :: :: deIid {{ com remove infix status }} %% %% x_l {{ tex \ottnt{x}^{l} }} , y_l {{ tex \ottnt{y}^{l} }} , z_l {{ tex \ottnt{z}^{l} }} , name :: '' ::= @@ -284,36 +284,37 @@ grammar base_kind :: 'BK_' ::= - {{ com base kinds}} + {{ com base kind}} {{ aux _ l }} - | Type :: :: type - | Nat :: :: nat - | Endian :: :: endian - | Effects :: :: effects + | Type :: :: type {{ com kind of types }} + | Nat :: :: nat {{ com kind of natural number size expressions }} + | Endian :: :: endian {{ com kind of endianness specifications }} + | Effects :: :: effects {{ com kind of effect sets }} kind :: 'K_' ::= {{ com kinds}} {{ aux _ l }} - | base_kind1 -> ... -> base_kindn :: :: kind + | base_kind1 -> ... -> base_kindn :: :: kind % we'll never use ...-> Nat nexp :: 'Nexp_' ::= - {{ com expressions of kind Nat, for vector lengths }} + {{ com expression of kind Nat, for vector sizes and origins }} {{ aux _ l }} - | id :: :: var - | num :: :: constant - | nexp1 * nexp2 :: :: times {{ com must be linear after normalisation... except for the type of *, ahem }} - | nexp1 + nexp2 :: :: sum - | 2 ** nexp :: :: exp + | id :: :: id {{ com identifier }} + | num :: :: constant {{ com constant }} + | nexp1 * nexp2 :: :: times {{ com product }} +%{{ com must be linear after normalisation... except for the type of *, ahem }} + | nexp1 + nexp2 :: :: sum {{ com sum }} + | 2 ** nexp :: :: exp {{ com exponential }} | ( nexp ) :: S :: paren {{ icho [[nexp]] }} endian :: 'End_' ::= {{ com endianness specifications}} {{ aux _ l }} - | id :: :: var - | inc :: :: inc - | dec :: :: dec + | id :: :: id {{ com identifier }} + | inc :: :: inc {{ com increasing (little-endian) }} + | dec :: :: dec {{ com decreasing (big-endian) }} | ( endian ) :: S :: paren {{ icho [[endian]] }} effect :: 'Effect_' ::= @@ -339,20 +340,20 @@ effects :: 'Effects_' ::= typ :: 'Typ_' ::= - {{ com Constructors of kind Type }} + {{ com Constructor of kind Type }} | _ :: :: wild {{ com Unspecified type }} | id :: :: var - {{ com Type variables }} + {{ com Type variable }} | typ1 -> typ2 effects :: :: fn - {{ com Function types -- first-order only}} + {{ com Function type (first-order only in user code) }} % TODO: build first-order restriction into AST or just into type rules? neither - see note % TODO: concrete syntax for effects in a function type? needed only for pp, not in user syntax. | typ1 * .... * typn :: :: tup - {{ com Tuple types }} + {{ com Tuple type }} % TODO union in the other kind grammars? or make a syntax of argument? or glom together the grammars and leave o the typechecker | id typ_arg1 .. typ_argn :: :: app - {{ com type constructor applications }} + {{ com type constructor application }} | ( typ ) :: S :: paren {{ icho [[typ]] }} typ_arg :: 'Typ_arg_' ::= @@ -364,31 +365,31 @@ typ_arg :: 'Typ_arg_' ::= % plus more for l-value/r-value pairs, as introduced by the L3 'compound' declarations ... ref typ -typ_sugar :: 'Typ_sugar_' ::= - {{ com library types and syntactic sugar }} +typ_lib :: 'Typ_lib_' ::= + {{ com library types and syntactic sugar for them }} {{ aux _ l }} % boring base types: - | unit :: :: unit - | bool :: :: bool - | bit :: :: bit {{ com pure bits, not mutable bits! }} + | unit :: :: unit {{ com unit type with value $()$ }} + | bool :: :: bool {{ com booleans $[[true]]$ and $[[false]]$ }} + | bit :: :: bit {{ com pure bit values (not mutable bits) }} % experimentally trying with two distinct types of bool and bit ... - | nat :: :: nat - | string :: :: string + | nat :: :: nat {{ com natural numbers 0,1,2,... }} + | string :: :: string {{ com UTF8 strings }} % finite subranges of nat - | enum nexp1 nexp2 endian :: :: enum {{ com natural numbers from [[nexp2]] to [[nexp2]]+[[nexp1]]-1, ordered by [[endian]] }} + | enum nexp1 nexp2 endian :: :: enum {{ com natural numbers [[nexp2]] .. [[nexp2]]+[[nexp1]]-1, ordered by [[endian]] }} | [ nexp ] :: :: enum1 {{ com sugar for \texttt{enum nexp 0 inc} }} | [ nexp '..' nexp' ] :: :: enum2 {{ com sugar for \texttt{enum (nexp'-nexp+1) nexp inc} or \texttt{enum (nexp-nexp'+1) nexp' dec} }} % use .. not - to avoid ambiguity with nexp - % total maps and vectors indexed by finite subranges of nat - | vector nexp1 nexp2 endian typ :: :: vector + | vector nexp1 nexp2 endian typ :: :: vector {{ com vector of [[typ]], indexed by natural range }} % probably some sugar for vector types, using [ ] similarly to enums: % (but with .. not : in the former, to avoid confusion...) - | typ [ nexp ] :: :: vector2 - | typ [ nexp : nexp' ] :: :: vector3 + | typ [ nexp ] :: :: vector2 {{ com sugar for vector indexed by [ [[nexp]] ] }} + | typ [ nexp : nexp' ] :: :: vector3 {{ com sugar for vector indexed by [ [[nexp]]:[[nexp']] ] }} % ...so bit [ nexp ] etc is just an instance of that - | list typ :: :: list - | set typ :: :: set - | reg typ :: :: reg {{ com type of mutable register components }} + | list typ :: :: list {{ com list of [[typ]] }} + | set typ :: :: set {{ com finite set of [[typ]] }} + | reg typ :: :: reg {{ com mutable register components holding [[typ]] }} % "reg t" is basically the ML "t ref" % not sure how first-class it should be, though % use "reg word32" etc for the types of vanilla registers @@ -404,7 +405,7 @@ Typ_fn <= Typ_tup grammar nexp_constraint :: 'NC_' ::= - {{ com contraints over kind Nat }} + {{ com contraint over kind Nat }} {{ aux _ l }} | nexp = nexp' :: :: fixed | nexp >= nexp' :: :: bounded_ge @@ -416,8 +417,8 @@ nexp_constraint :: 'NC_' ::= kinded_id :: 'KOpt_' ::= {{ com optionally kind-annotated identifier }} - | id :: :: none - | kind id :: :: kind + | id :: :: none {{ com identifier }} + | kind id :: :: kind {{ com kind-annotated variable }} | ( kinded_id ) :: S :: paren {{ icho [[kinded_id]] }} typquant :: 'TypQ_' ::= @@ -442,14 +443,14 @@ typschm :: 'TypSchm_' ::= grammar ctor_def :: 'CT_' ::= - {{ com Datatype definition clauses }} + {{ com Datatype constructor definition clause }} | id : typschm :: :: ct % but we could get away with disallowing constraints in typschm, we % think - if it's useful to do that -enum_opt :: 'EnumOpt_' ::= - | :: :: empty - | enum :: :: enum +%enum_opt :: 'EnumOpt_' ::= +% | :: :: empty +% | enum :: :: enum %% tdefbody :: 'TD_' ::= %% {{ com Type definition bodies }} @@ -478,9 +479,9 @@ enum_opt :: 'EnumOpt_' ::= %%% OR, IN C STYLE tdef :: 'TD_' ::= - {{ com Type definition bodies }} + {{ com Type definition body }} | typedef id naming_scheme_opt = typschm :: :: abbrev - {{ com Type abbreviations }} + {{ com Type abbreviation }} {{ texlong }} | typedef id naming_scheme_opt = const struct typquant { typ1 id1 ; ... ; typn idn semi_opt } :: :: record {{ com Struct type definition }} {{ texlong }} % for specifying constructor result types of nat-indexed GADTs, we can @@ -491,18 +492,18 @@ tdef :: 'TD_' ::= {{ com Union type definition}} {{ texlong }} | typedef id naming_scheme_opt = enum { id1 ; ... ; idn semi_opt } :: :: enum - {{ com enumeration type definition}} + {{ com enumeration type definition}} {{ texlong }} - | typedef id = register bits [ nexp : nexp' ] { bitfield1 : id1 ; ... ; bitfieldn : idn } -:: :: register {{ com register mutable bitfield type }} + | typedef id = register bits [ nexp : nexp' ] { index_range1 : id1 ; ... ; index_rangen : idn } +:: :: register {{ com register mutable bitfield type }} {{ texlong }} % also sugar [ nexp ] -bitfield :: 'BF_' ::= - | num :: :: bit - | num1 '..' num2 :: :: bits - | bitfield1 , bitfield2 :: :: bitfields +index_range :: 'BF_' ::= {{ com index specification, e.g.~for bitfields }} + | num :: :: 'single' {{ com single index }} + | num1 '..' num2 :: :: range {{ com index range }} + | index_range1 , index_range2 :: :: concat {{ com concatenation of index ranges }} % @@ -516,26 +517,25 @@ bitfield :: 'BF_' ::= grammar lit :: 'L_' ::= - {{ com Literal constants }} - | true :: :: true - | false :: :: false - | num :: :: num - | hex :: :: hex - {{ com hex and bin are constant bit vectors, entered as C-style hex or binaries }} - | bin :: :: bin - | string :: :: string - | ( ) :: :: unit + {{ com Literal constant }} + | ( ) :: :: unit {{ com $() : [[unit]]$ }} %Presumably we want to remove bitzero and bitone ? - | bitzero :: :: zero - {{ com bitzero and bitone are constant bits, if commonly used we will consider overloading 0 and 1 }} - | bitone :: :: one + | bitzero :: :: zero {{ com $[[bitzero]] : [[bit]]$ }} + | bitone :: :: one {{ com $[[bitone]] : [[bit]]$ }} + | true :: :: true {{ com $[[true]] : [[bool]]$ }} + | false :: :: false {{ com $[[false]] : [[bool]]$ }} + | num :: :: num {{ com natural number constant }} + | hex :: :: hex {{ com bit vector constant, C-style }} + {{ com hex and bin are constant bit vectors, C-style }} + | bin :: :: bin {{ com bit vector constant, C-style }} + | string :: :: string {{ com string constant }} semi_opt {{ tex \ottnt{;}^{?} }} :: 'semi_' ::= {{ phantom }} {{ ocaml terminal * bool }} {{ lem (terminal * bool) }} {{ hol bool }} - {{ com Optional semi-colons }} - | :: :: no + {{ com Optional semi-colon }} + | :: :: no {{ hol F }} {{ ocaml false }} {{ lem false }} @@ -551,56 +551,61 @@ semi_opt {{ tex \ottnt{;}^{?} }} :: 'semi_' ::= {{ phantom }} pat :: 'P_' ::= - {{ com Patterns }} + {{ com Pattern }} {{ aux _ l }} | _ :: :: wild - {{ com Wildcards }} + {{ com wildcard }} | ( pat as id ) :: :: as - {{ com Named patterns }} + {{ com named pattern }} % ML-style % | ( pat : typ ) :: :: typ % {{ com Typed patterns }} % C-style | ( typ pat ) :: :: typ - {{ com Typed patterns }} + {{ com typed pattern }} + + | id :: :: id + {{ com identifier }} + % | id pat1 .. patn :: :: app - {{ com Single variable and constructor patterns }} + {{ com union constructor pattern }} + % OR? do we invent something ghastly including a union keyword? Perhaps not... % | <| fpat1 ; ... ; fpatn semi_opt |> :: :: record % {{ com Record patterns }} % OR - | struct { fpat1 ; ... ; fpatn semi_opt } :: :: c_record - {{ com C-style struct patterns }} + | { fpat1 ; ... ; fpatn semi_opt } :: :: record + {{ com struct pattern }} %Patterns for vectors %Should these be the same since vector syntax has changed, and lists have also changed? | [ pat1 , .. , patn ] :: :: vector - {{ com Vector patterns }} + {{ com vector pattern }} | [ num1 = pat1 , .. , numn = patn ] :: :: vector_indexed - {{ com Vector patterns }} + {{ com vector pattern (with explicit indices) }} % cf ntoes for this | pat1 : .. : patn :: :: vector_concat - {{ com Concatenated vector patterns }} + {{ com concatenated vector pattern }} | ( pat1 , .... , patn ) :: :: tup - {{ com Tuple patterns }} + {{ com tuple pattern }} | [| pat1 , .. , patn |] :: :: list - {{ com List patterns }} + {{ com list pattern }} | ( pat ) :: :: paren % | pat1 '::' pat2 :: :: cons % {{ com Cons patterns }} % | id '+' num :: :: num_add % {{ com constant addition patterns }} | lit :: :: lit - {{ com Literal constant patterns }} + {{ com literal constant pattern }} fpat :: 'FP_' ::= - {{ com Field patterns }} + {{ com Field pattern }} {{ aux _ l }} | id = pat :: :: Fpat @@ -617,36 +622,36 @@ P_app <= P_as grammar exp :: 'E_' ::= - {{ com Expressions }} + {{ com Expression }} {{ aux _ l }} | ( exp ) :: S :: paren {{ ichlo [[exp]] }} - | { exp1 ; ... ; expn } :: :: block + | { exp1 ; ... ; expn } :: :: block {{ com block (parsing conflict with structs?) }} - | id :: :: ident - {{ com Identifiers }} + | id :: :: id + {{ com identifier }} | lit :: :: lit - {{ com Literal constants }} + {{ com literal constant }} | exp1 exp2 :: :: app - {{ com Function applications }} + {{ com function application }} | exp1 id exp2 :: :: infix - {{ com Infix applications }} + {{ com infix function application }} | ( exp1 , .... , expn ) :: :: tup - {{ com Tuples }} + {{ com tuple }} | if exp1 then exp2 else exp3 :: :: if - {{ com Conditionals }} + {{ com conditional }} % vectors - | [ exp1 , ... , expn ] :: :: vector + | [ exp1 , ... , expn ] :: :: vector {{ com vector (indexed from 0) }} % endianness comes from global command-line option??? - | [ num1 = exp1 , ... , numn = expn ] :: :: vector_indexed + | [ num1 = exp1 , ... , numn = expn ] :: :: vector_indexed {{ com vector (indexed consecutively) }} % num1 .. numn must be a consecutive list of naturals % we pick [ ] not { } for vector literals for consistency with their @@ -658,7 +663,7 @@ exp :: 'E_' ::= {{ com vector access }} | exp [ exp1 : exp2 ] :: :: vector_subrange - {{ com Subvector extraction }} + {{ com subvector extraction }} % do we want to allow a comma-separated list of such thingies? | [ exp with exp1 = exp2 ] :: :: vector_update @@ -673,7 +678,7 @@ exp :: 'E_' ::= | [| exp1 , .. , expn |] :: :: list {{ com list }} | exp1 '::' exp2 :: :: cons - {{ com Cons expressions }} + {{ com cons }} % const unions @@ -682,12 +687,12 @@ exp :: 'E_' ::= % TODO - | <| fexps |> :: :: record - {{ com Records }} - | <| exp with fexps |> :: :: recup - {{ com Functional update for records }} + | { fexps } :: :: record + {{ com struct }} + | { exp with fexps } :: :: recup + {{ com functional update of struct }} | exp . id :: :: field - {{ com Field projection for records }} + {{ com field projection from struct }} %Expressions for creating and accessing vectors @@ -703,36 +708,36 @@ exp :: 'E_' ::= % and maybe with nice syntax | switch exp { case pexp1 ... case pexpn } :: :: case - {{ com Pattern matching expressions }} + {{ com pattern matching }} % | ( typ ) exp :: :: Typed % {{ com Type-annotated expressions }} | letbind in exp :: :: let - {{ com Let expressions }} + {{ com let expression }} | lexp := exp :: :: assign + {{ com imperative assignment }} - -lexp :: 'LEXP_' ::= - | id :: :: ident - {{ com Identifiers }} - | lexp [ exp ] :: :: vector - | lexp [ exp1 : exp2 ] :: :: vector_range +lexp :: 'LEXP_' ::= {{ com lvalue expression }} + | id :: :: id + {{ com identifier }} + | lexp [ exp ] :: :: vector {{ com vector element }} + | lexp [ exp1 : exp2 ] :: :: vector_range {{ com subvector }} % maybe comma-sep such lists too - | lexp . id :: :: field + | lexp . id :: :: field {{ com struct field }} fexp :: 'FE_' ::= - {{ com Field-expressions }} + {{ com field-expression }} {{ aux _ l }} | id = exp :: :: Fexp fexps :: 'FES_' ::= - {{ com Field-expression lists }} + {{ com field-expression list }} {{ aux _ l }} | fexp1 ; ... ; fexpn semi_opt :: :: Fexps pexp :: 'Pat_' ::= - {{ com Pattern matches }} + {{ com pattern match }} {{ aux _ l }} | pat -> exp :: :: exp % apparently could use -> or => for this. @@ -809,12 +814,12 @@ grammar %%%%% C-ish style %%%%%%%%%% tannot_opt :: 'Typ_annot_opt_' ::= - {{ com Optional type annotations }} + {{ com Optional type annotation }} | :: :: none | typ_quant typ :: :: some funcl :: 'FCL_' ::= - {{ com Function clauses }} + {{ com Function clause }} {{ aux _ l }} | id pat = exp :: :: Funcl @@ -825,7 +830,7 @@ rec_opt :: 'Rec_' ::= effects_opt :: 'Effects_opt_' ::= {{ aux _ l }} - | :: :: pure {{ com sugar for pure }} + | :: :: pure {{ com sugar for empty effect set }} | effects :: :: nonpure fundef :: 'FD_' ::= @@ -840,7 +845,7 @@ fundef :: 'FD_' ::= % which is ok for the typ_quant part but not for the typ part letbind :: 'LB_' ::= - {{ com Let bindings }} + {{ com Let binding }} {{ aux _ l }} | typschm id = exp :: :: val_explicit {{ com Value binding }} @@ -849,12 +854,12 @@ letbind :: 'LB_' ::= val_spec :: 'VS_' ::= - {{ com Value type specifications }} + {{ com Value type specification }} {{ aux _ l }} | val typschm id :: :: val_spec default_typing_spec :: 'DT_' ::= - {{ com default kinding and typing assumptions }} + {{ com default kinding and typing assumption }} {{ aux _ l }} | default base_kind regexp :: :: kind | default typschm regexp :: :: typ @@ -870,7 +875,7 @@ default_typing_spec :: 'DT_' ::= %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% def :: 'DEF_' ::= - {{ com Top-level definitions }} + {{ com Top-level definition }} {{ aux _ l }} | type_def :: :: type {{ com Type definition }} @@ -885,13 +890,13 @@ def :: 'DEF_' ::= | register typ id :: :: reg_dec {{ com Register declaration }} - | split function rec_opt tannot_opt effects_opt id :: :: split_function + | split function rec_opt tannot_opt effects_opt id :: :: split_function {{ texlong }} | function clause funcl :: :: split_funcl | end id :: :: split_end - | split typedef id naming_scheme_opt = const union typquant :: :: split_variant + | split typedef id naming_scheme_opt = const union typquant :: :: split_variant {{ texlong }} | union member id = typ id' :: :: split_unioncl @@ -1302,6 +1307,9 @@ defs :: '' ::= grammar terminals :: '' ::= + | ** :: :: starstar + {{ tex \ensuremath{\mathop{\mathord{*}\mathord{*} } } }} + {{ com \texttt{**} }} | >= :: :: geq {{ tex \ensuremath{\geq} }} {{ com \texttt{>=} }} |