diff options
| -rw-r--r-- | language/l2.ott | 254 | ||||
| -rw-r--r-- | src/ast.ml | 237 |
2 files changed, 247 insertions, 244 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{>=} }} @@ -45,21 +45,21 @@ let combine_lex_skips s1 s2 = type terminal = lex_skips -type x = terminal * text (* Variables *) -type ix = terminal * text (* Variables *) +type x = terminal * text (* identifier *) +type ix = terminal * text (* infix identifier *) type -id_aux = (* identifiers *) +id_aux = (* Identifier *) Id of x - | DeIId of terminal * x * terminal (* remove infix status *) + | DeIid of terminal * x * terminal (* remove infix status *) type -base_kind_aux = (* base kinds *) - BK_type of terminal - | BK_nat of terminal - | BK_endian of terminal - | BK_effects of terminal +base_kind_aux = (* base kind *) + BK_type of terminal (* kind of types *) + | BK_nat of terminal (* kind of natural number size expressions *) + | BK_endian of terminal (* kind of endianness specifications *) + | BK_effects of terminal (* kind of effect sets *) type @@ -84,12 +84,12 @@ effect_aux = (* effect *) type -nexp_aux = (* expressions of kind Nat, for vector lengths *) - Nexp_var of id - | Nexp_constant of terminal * int - | Nexp_times of nexp * terminal * nexp (* must be linear after normalisation... except for the type of *, ahem *) - | Nexp_sum of nexp * terminal * nexp - | Nexp_exp of terminal * terminal * nexp +nexp_aux = (* expression of kind Nat, for vector sizes and origins *) + Nexp_id of id (* identifier *) + | Nexp_constant of terminal * int (* constant *) + | Nexp_times of nexp * terminal * nexp (* product *) + | Nexp_sum of nexp * terminal * nexp (* sum *) + | Nexp_exp of terminal * terminal * nexp (* exponential *) and nexp = Nexp_aux of nexp_aux * l @@ -106,7 +106,7 @@ effect = type -nexp_constraint_aux = (* contraints over kind Nat *) +nexp_constraint_aux = (* contraint over kind Nat *) NC_fixed of nexp * terminal * nexp | NC_bounded_ge of nexp * terminal * nexp | NC_bounded_le of nexp * terminal * nexp @@ -119,37 +119,37 @@ kind = type -endian_aux = (* endianness specifications *) - End_var of id - | End_inc of terminal - | End_dec of terminal - - -type effects_aux = (* effect set *) Effects_var of id | Effects_set of terminal * (effect * terminal) list * terminal (* effect set *) type +endian_aux = (* endianness specifications *) + End_id of id (* identifier *) + | End_inc of terminal (* increasing (little-endian) *) + | End_dec of terminal (* decreasing (big-endian) *) + + +type nexp_constraint = NC_aux of nexp_constraint_aux * l type kinded_id = (* optionally kind-annotated identifier *) - KOpt_none of id - | KOpt_kind of kind * id + KOpt_none of id (* identifier *) + | KOpt_kind of kind * id (* kind-annotated variable *) type -endian = - End_aux of endian_aux * l +effects = + Effects_aux of effects_aux * l type -effects = - Effects_aux of effects_aux * l +endian = + End_aux of endian_aux * l type @@ -160,12 +160,12 @@ typquant_aux = type -typ = (* Constructors of kind Type *) +typ = (* Constructor of kind Type *) Typ_wild of terminal (* Unspecified type *) - | Typ_var of id (* Type variables *) - | Typ_fn of typ * terminal * typ * effects (* Function types -- first-order only *) - | Typ_tup of (typ * terminal) list (* Tuple types *) - | Typ_app of id * (typ_arg) list (* type constructor applications *) + | Typ_var of id (* Type variable *) + | Typ_fn of typ * terminal * typ * effects (* Function type (first-order only in user code) *) + | Typ_tup of (typ * terminal) list (* Tuple type *) + | Typ_app of id * (typ_arg) list (* type constructor application *) and typ_arg = (* Type constructor arguments of all kinds *) Typ_arg_nexp of nexp @@ -185,16 +185,16 @@ typschm_aux = (* Type schemes *) type -lit = (* Literal constants *) - L_true of terminal - | L_false of terminal - | L_num of terminal * int - | L_hex of terminal * string (* hex and bin are constant bit vectors, entered as C-style hex or binaries *) - | L_bin of terminal * string - | L_string of terminal * Ulib.UTF8.t - | L_unit of terminal * terminal - | L_zero of terminal (* bitzero and bitone are constant bits, if commonly used we will consider overloading 0 and 1 *) - | L_one of terminal +lit = (* Literal constant *) + L_unit of terminal * terminal (* $() : _$ *) + | L_zero of terminal (* $_ : _$ *) + | L_one of terminal (* $_ : _$ *) + | L_true of terminal (* $_ : _$ *) + | L_false of terminal (* $_ : _$ *) + | L_num of terminal * int (* natural number constant *) + | L_hex of terminal * string (* bit vector constant, C-style *) + | L_bin of terminal * string (* bit vector constant, C-style *) + | L_string of terminal * Ulib.UTF8.t (* string constant *) type @@ -203,24 +203,25 @@ typschm = type -pat_aux = (* Patterns *) - P_wild of terminal (* Wildcards *) - | P_as of terminal * pat * terminal * id * terminal (* Named patterns *) - | P_typ of terminal * typ * pat * terminal (* Typed patterns *) - | P_app of id * (pat) list (* Single variable and constructor patterns *) - | P_c_record of terminal * terminal * (fpat * terminal) list * terminal * bool * terminal (* C-style struct patterns *) - | P_vector of terminal * (pat * terminal) list * terminal (* Vector patterns *) - | P_vector_indexed of terminal * ((terminal * int * terminal * pat) * terminal) list * terminal (* Vector patterns *) - | P_vector_concat of (pat * terminal) list (* Concatenated vector patterns *) - | P_tup of terminal * (pat * terminal) list * terminal (* Tuple patterns *) - | P_list of terminal * (pat * terminal) list * terminal (* List patterns *) +pat_aux = (* Pattern *) + P_wild of terminal (* wildcard *) + | P_as of terminal * pat * terminal * id * terminal (* named pattern *) + | P_typ of terminal * typ * pat * terminal (* typed pattern *) + | P_id of id (* identifier *) + | P_app of id * (pat) list (* union constructor pattern *) + | P_record of terminal * (fpat * terminal) list * terminal * bool * terminal (* struct pattern *) + | P_vector of terminal * (pat * terminal) list * terminal (* vector pattern *) + | P_vector_indexed of terminal * ((terminal * int * terminal * pat) * terminal) list * terminal (* vector pattern (with explicit indices) *) + | P_vector_concat of (pat * terminal) list (* concatenated vector pattern *) + | P_tup of terminal * (pat * terminal) list * terminal (* tuple pattern *) + | P_list of terminal * (pat * terminal) list * terminal (* list pattern *) | P_paren of terminal * pat * terminal - | P_lit of lit (* Literal constant patterns *) + | P_lit of lit (* literal constant pattern *) and pat = P_aux of pat_aux * l -and fpat_aux = (* Field patterns *) +and fpat_aux = (* Field pattern *) FP_Fpat of id * terminal * pat and fpat = @@ -228,57 +229,57 @@ and fpat = type -exp_aux = (* Expressions *) - E_block of terminal * (exp * terminal) list * terminal - | E_ident of id (* Identifiers *) - | E_lit of lit (* Literal constants *) - | E_app of exp * exp (* Function applications *) - | E_infix of exp * id * exp (* Infix applications *) - | E_tup of terminal * (exp * terminal) list * terminal (* Tuples *) - | E_if of terminal * exp * terminal * exp * terminal * exp (* Conditionals *) - | E_vector of terminal * (exp * terminal) list * terminal - | E_vector_indexed of terminal * ((terminal * int * terminal * exp) * terminal) list * terminal +exp_aux = (* Expression *) + E_block of terminal * (exp * terminal) list * terminal (* block (parsing conflict with structs?) *) + | E_id of id (* identifier *) + | E_lit of lit (* literal constant *) + | E_app of exp * exp (* function application *) + | E_infix of exp * id * exp (* infix function application *) + | E_tup of terminal * (exp * terminal) list * terminal (* tuple *) + | E_if of terminal * exp * terminal * exp * terminal * exp (* conditional *) + | E_vector of terminal * (exp * terminal) list * terminal (* vector (indexed from 0) *) + | E_vector_indexed of terminal * ((terminal * int * terminal * exp) * terminal) list * terminal (* vector (indexed consecutively) *) | E_vector_access of exp * terminal * exp * terminal (* vector access *) - | E_vector_subrange of exp * terminal * exp * terminal * exp * terminal (* Subvector extraction *) + | E_vector_subrange of exp * terminal * exp * terminal * exp * terminal (* subvector extraction *) | E_vector_update of terminal * exp * terminal * exp * terminal * exp * terminal (* vector functional update *) | E_vector_update_range of terminal * exp * terminal * exp * terminal * exp * terminal * exp * terminal (* vector functional subrange update (with another vector) *) | E_list of terminal * (exp * terminal) list * terminal (* list *) - | E_cons of exp * terminal * exp (* Cons expressions *) - | E_record of terminal * fexps * terminal (* Records *) - | E_recup of terminal * exp * terminal * fexps * terminal (* Functional update for records *) - | E_field of exp * terminal * id (* Field projection for records *) - | E_case of terminal * exp * terminal * ((terminal * pexp)) list * terminal (* Pattern matching expressions *) - | E_let of letbind * terminal * exp (* Let expressions *) - | E_assign of lexp * terminal * exp + | E_cons of exp * terminal * exp (* cons *) + | E_record of terminal * fexps * terminal (* struct *) + | E_recup of terminal * exp * terminal * fexps * terminal (* functional update of struct *) + | E_field of exp * terminal * id (* field projection from struct *) + | E_case of terminal * exp * terminal * ((terminal * pexp)) list * terminal (* pattern matching *) + | E_let of letbind * terminal * exp (* let expression *) + | E_assign of lexp * terminal * exp (* imperative assignment *) and exp = E_aux of exp_aux * l -and lexp = - LEXP_ident of id (* Identifiers *) - | LEXP_vector of lexp * terminal * exp * terminal - | LEXP_vector_range of lexp * terminal * exp * terminal * exp * terminal - | LEXP_field of lexp * terminal * id +and lexp = (* lvalue expression *) + LEXP_id of id (* identifier *) + | LEXP_vector of lexp * terminal * exp * terminal (* vector element *) + | LEXP_vector_range of lexp * terminal * exp * terminal * exp * terminal (* subvector *) + | LEXP_field of lexp * terminal * id (* struct field *) -and fexp_aux = (* Field-expressions *) +and fexp_aux = (* field-expression *) FE_Fexp of id * terminal * exp and fexp = FE_aux of fexp_aux * l -and fexps_aux = (* Field-expression lists *) +and fexps_aux = (* field-expression list *) FES_Fexps of (fexp * terminal) list * terminal * bool and fexps = FES_aux of fexps_aux * l -and pexp_aux = (* Pattern matches *) +and pexp_aux = (* pattern match *) Pat_exp of pat * terminal * exp and pexp = Pat_aux of pexp_aux * l -and letbind_aux = (* Let bindings *) +and letbind_aux = (* Let binding *) LB_val_explicit of typschm * id * terminal * exp (* Value binding *) | LB_val_implicit of terminal * id * terminal * exp (* value binding with implicit type *) @@ -287,7 +288,7 @@ and letbind = type -funcl_aux = (* Function clauses *) +funcl_aux = (* Function clause *) FCL_Funcl of id * pat * terminal * exp @@ -299,12 +300,12 @@ rec_opt_aux = type effects_opt_aux = - Effects_opt_pure (* sugar for pure *) + Effects_opt_pure (* sugar for empty effect set *) | Effects_opt_nonpure of effects type -tannot_opt = (* Optional type annotations *) +tannot_opt = (* Optional type annotation *) Typ_annot_opt_none | Typ_annot_opt_some of terminal * typ @@ -330,12 +331,12 @@ fundef_aux = (* Function definition *) type -val_spec_aux = (* Value type specifications *) +val_spec_aux = (* Value type specification *) VS_val_spec of terminal * typschm * id type -default_typing_spec_aux = (* default kinding and typing assumptions *) +default_typing_spec_aux = (* default kinding and typing assumption *) DT_kind of terminal * base_kind * terminal * string | DT_typ of terminal * typschm * terminal * string @@ -356,7 +357,7 @@ default_typing_spec = type -def_aux = (* Top-level definitions *) +def_aux = (* Top-level definition *) DEF_type of terminal (* Type definition *) | DEF_fundef of fundef (* Function definition *) | DEF_val of letbind (* Value definition *) @@ -376,28 +377,28 @@ def = type -typ_sugar_aux = (* library types and syntactic sugar *) - Typ_sugar_unit of terminal - | Typ_sugar_bool of terminal - | Typ_sugar_bit of terminal (* pure bits, not mutable bits! *) - | Typ_sugar_nat of terminal - | Typ_sugar_string of terminal * Ulib.UTF8.t - | Typ_sugar_enum of terminal * nexp * nexp * endian (* natural numbers from nexp to nexp+nexp-1, ordered by endian *) - | Typ_sugar_enum1 of terminal * nexp * terminal (* sugar for \texttt{enum nexp 0 inc} *) - | Typ_sugar_enum2 of terminal * nexp * terminal * nexp * terminal (* sugar for \texttt{enum (nexp'-nexp+1) nexp inc} or \texttt{enum (nexp-nexp'+1) nexp' dec} *) - | Typ_sugar_vector of terminal * nexp * nexp * endian * typ - | Typ_sugar_vector2 of typ * terminal * nexp * terminal - | Typ_sugar_vector3 of typ * terminal * nexp * terminal * nexp * terminal - | Typ_sugar_list of terminal * typ - | Typ_sugar_set of terminal * typ - | Typ_sugar_reg of terminal * typ (* type of mutable register components *) +typ_lib_aux = (* library types and syntactic sugar for them *) + Typ_lib_unit of terminal (* unit type with value $()$ *) + | Typ_lib_bool of terminal (* booleans $_$ and $_$ *) + | Typ_lib_bit of terminal (* pure bit values (not mutable bits) *) + | Typ_lib_nat of terminal (* natural numbers 0,1,2,... *) + | Typ_lib_string of terminal * Ulib.UTF8.t (* UTF8 strings *) + | Typ_lib_enum of terminal * nexp * nexp * endian (* natural numbers nexp .. nexp+nexp-1, ordered by endian *) + | Typ_lib_enum1 of terminal * nexp * terminal (* sugar for \texttt{enum nexp 0 inc} *) + | Typ_lib_enum2 of terminal * nexp * terminal * nexp * terminal (* sugar for \texttt{enum (nexp'-nexp+1) nexp inc} or \texttt{enum (nexp-nexp'+1) nexp' dec} *) + | Typ_lib_vector of terminal * nexp * nexp * endian * typ (* vector of typ, indexed by natural range *) + | Typ_lib_vector2 of typ * terminal * nexp * terminal (* sugar for vector indexed by [ nexp ] *) + | Typ_lib_vector3 of typ * terminal * nexp * terminal * nexp * terminal (* sugar for vector indexed by [ nexp:nexp ] *) + | Typ_lib_list of terminal * typ (* list of typ *) + | Typ_lib_set of terminal * typ (* finite set of typ *) + | Typ_lib_reg of terminal * typ (* mutable register components holding typ *) type -bitfield = - BF_bit of terminal * int - | BF_bits of terminal * int * terminal * terminal * int - | BF_bitfields of bitfield * terminal * bitfield +index_range = (* index specification, e.g.~for bitfields *) + BF_single of terminal * int (* single index *) + | BF_range of terminal * int * terminal * terminal * int (* index range *) + | BF_concat of index_range * terminal * index_range (* concatenation of index ranges *) type @@ -406,28 +407,22 @@ defs_aux = (* Definition sequences *) type -typ_sugar = - Typ_sugar_aux of typ_sugar_aux * l +typ_lib = + Typ_lib_aux of typ_lib_aux * l type -ctor_def = (* Datatype definition clauses *) +ctor_def = (* Datatype constructor definition clause *) CT_ct of id * terminal * typschm type -enum_opt = - EnumOpt_empty - | EnumOpt_enum of terminal - - -type -tdef = (* Type definition bodies *) - TD_abbrev of terminal * id * terminal * terminal * typschm (* Type abbreviations *) +tdef = (* Type definition body *) + TD_abbrev of terminal * id * terminal * terminal * typschm (* Type abbreviation *) | TD_record of terminal * id * terminal * terminal * terminal * terminal * typquant * terminal * ((typ * id) * terminal) list * terminal * bool * terminal (* Struct type definition *) | TD_variant of terminal * id * terminal * terminal * terminal * terminal * typquant * terminal * ((typ * id) * terminal) list * terminal * bool * terminal (* Union type definition *) | TD_enum of terminal * id * terminal * terminal * terminal * terminal * (id * terminal) list * terminal * bool * terminal (* enumeration type definition *) - | TD_register of terminal * id * terminal * terminal * terminal * terminal * nexp * terminal * nexp * terminal * terminal * ((bitfield * terminal * id) * terminal) list * terminal (* register mutable bitfield type *) + | TD_register of terminal * id * terminal * terminal * terminal * terminal * nexp * terminal * nexp * terminal * terminal * ((index_range * terminal * id) * terminal) list * terminal (* register mutable bitfield type *) type |