diff options
Diffstat (limited to 'language/l2.ott')
| -rw-r--r-- | language/l2.ott | 177 |
1 files changed, 95 insertions, 82 deletions
diff --git a/language/l2.ott b/language/l2.ott index d1bf5793..031cfb5a 100644 --- a/language/l2.ott +++ b/language/l2.ott @@ -291,7 +291,7 @@ base_kind :: 'BK_' ::= | Endian :: :: endian | Effects :: :: effects -kind :: '' ::= +kind :: 'K_' ::= {{ com kinds}} {{ aux _ l }} | base_kind1 -> ... -> base_kindn :: :: kind @@ -305,7 +305,7 @@ nexp :: 'Nexp_' ::= | num :: :: constant | nexp1 * nexp2 :: :: times {{ com must be linear after normalisation... except for the type of *, ahem }} | nexp1 + nexp2 :: :: sum - | 2 ^ nexp :: :: exp + | 2 ** nexp :: :: exp | ( nexp ) :: S :: paren {{ icho [[nexp]] }} endian :: 'End_' ::= @@ -380,11 +380,11 @@ typ_sugar :: 'Typ_sugar_' ::= | [ 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 - | enummap nexp1 nexp2 endian typ :: :: enummap -% probably some sugar for enummap types, using [ ] similarly to enums: + | vector nexp1 nexp2 endian typ :: :: vector +% probably some sugar for vector types, using [ ] similarly to enums: % (but with .. not : in the former, to avoid confusion...) - | typ [ nexp ] :: :: enummap2 - | typ [ nexp : nexp' ] :: :: enummap3 + | typ [ nexp ] :: :: vector2 + | typ [ nexp : nexp' ] :: :: vector3 % ...so bit [ nexp ] etc is just an instance of that | list typ :: :: list | set typ :: :: set @@ -414,27 +414,25 @@ nexp_constraint :: 'NC_' ::= % Note only id on the left and constants on the right in a % finite-set-bound, as we don't think we need anything more -opt_kind :: 'ki_ant_' ::= +kinded_id :: 'KOpt_' ::= {{ com optionally kind-annotated identifier }} | id :: :: none - | id : kind :: :: kind - | ( opt_kind ) :: S :: paren {{ icho [[opt_kind]] }} + | kind id :: :: kind + | ( kinded_id ) :: S :: paren {{ icho [[kinded_id]] }} -typquant :: 'TQ_' ::= +typquant :: 'TypQ_' ::= {{ aux _ l }} - | forall opt_kind1 ... opt_kindn . nexp_constraint1 , ... , nexp_constrainti . :: :: Ts {{ texlong }} - -% TODO those ids have to have optional kind annotations + | forall kinded_id1 ... kinded_idn . nexp_constraint1 , ... , nexp_constrainti . :: :: tq {{ texlong }} % WHY ARE CONSTRAINTS HERE AND NOT IN THE KIND LANGUAGE - | forall opt_kind1 ... opt_kindn . :: :: Ts_no_constraint {{ com sugar }} - | :: :: Ts_no_forall {{ com sugar }} + | forall kinded_id1 ... kinded_idn . :: :: no_constraint {{ com sugar }} + | :: :: no_forall {{ com sugar }} -typschm :: 'TS_' ::= +typschm :: 'TypSchm_' ::= {{ com Type schemes }} {{ aux _ l }} - | typquant typ :: :: Ts + | typquant typ :: :: ts @@ -443,43 +441,43 @@ typschm :: 'TS_' ::= %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% grammar -ctor_def :: '' ::= +ctor_def :: 'CT_' ::= {{ com Datatype definition clauses }} - | id : typschm :: :: Cte + | id : typschm :: :: ct % but we could get away with disallowing constraints in typschm, we % think - if it's useful to do that -enum_opt :: 'Enum_' ::= +enum_opt :: 'EnumOpt_' ::= | :: :: empty | enum :: :: enum -tdefbody :: 'Te_' ::= - {{ com Type definition bodies }} - | typschm :: :: abbrev - {{ com Type abbreviations }} - | typquant <| id1 : typ1 ; ... ; idn : typn semi_opt |> :: :: record - {{ com Record types }} - | enumeration_flag_opt '|' ctor_def1 '|' ... '|' ctor_defn :: :: variant - {{ com Variant types }} - -naming_scheme_opt {{ tex \ottnt{name}^{?} }} :: 'Name_sect_' ::= - {{ com Optional variable-naming-scheme specification for variables of defined type }} - | :: :: none - | [ name = regexp ] :: :: some - -type_def :: '' ::= - {{ com Type definitions }} - | type id : kind naming_scheme_opt = tdefbody :: :: Td -% | enumeration id naming_scheme_opt = tdefbody :: :: Td2 -% the enumeration is sugar for something that uses an enum flag, where the type system will restrict the tdefbody to be a simple enum... - +%% tdefbody :: 'TD_' ::= +%% {{ com Type definition bodies }} +%% | typschm :: :: abbrev +%% {{ com Type abbreviations }} +%% | typquant <| id1 : typ1 ; ... ; idn : typn semi_opt |> :: :: record +%% {{ com Record types }} +%% | enumeration_flag_opt '|' ctor_def1 '|' ... '|' ctor_defn :: :: variant +%% {{ com Variant types }} +%% +%% naming_scheme_opt {{ tex \ottnt{name}^{?} }} :: 'Name_sect_' ::= +%% {{ com Optional variable-naming-scheme specification for variables of defined type }} +%% | :: :: none +%% | [ name = regexp ] :: :: some +%% +%% type_def :: '' ::= +%% {{ com Type definitions }} +%% | type id : kind naming_scheme_opt = tdefbody :: :: Td +%% % | enumeration id naming_scheme_opt = tdefbody :: :: Td2 +%% % the enumeration is sugar for something that uses an enum flag, where the type system will restrict the tdefbody to be a simple enum... +%% % TODO: do we need mutually recursive type definitions? %%% OR, IN C STYLE -c_tdefbody :: 'C_Te_' ::= +tdef :: 'TD_' ::= {{ com Type definition bodies }} | typedef id naming_scheme_opt = typschm :: :: abbrev {{ com Type abbreviations }} @@ -570,8 +568,8 @@ pat :: 'P_' ::= {{ com Single variable and constructor patterns }} % OR? do we invent something ghastly including a union keyword? Perhaps not... - | <| fpat1 ; ... ; fpatn semi_opt |> :: :: record - {{ com Record patterns }} +% | <| fpat1 ; ... ; fpatn semi_opt |> :: :: record +% {{ com Record patterns }} % OR | struct { fpat1 ; ... ; fpatn semi_opt } :: :: c_record {{ com C-style struct patterns }} @@ -579,10 +577,14 @@ pat :: 'P_' ::= %Patterns for vectors %Should these be the same since vector syntax has changed, and lists have also changed? - | [| pat1 ; .. ; patn semi_opt |] :: :: vector + | [ pat1 , .. , patn ] :: :: vector + {{ com Vector patterns }} + + | [ num1 = pat1 , .. , numn = patn ] :: :: vector_indexed {{ com Vector patterns }} - | [| pat1 .. patn |] :: :: vector_concat +% cf ntoes for this + | pat1 : .. : patn :: :: vector_concat {{ com Concatenated vector patterns }} | ( pat1 , .... , patn ) :: :: tup @@ -590,10 +592,10 @@ pat :: 'P_' ::= | [| pat1 , .. , patn |] :: :: list {{ com List patterns }} | ( pat ) :: :: paren - | pat1 '::' pat2 :: :: cons - {{ com Cons patterns }} - | id '+' num :: :: num_add - {{ com constant addition patterns }} +% | pat1 '::' pat2 :: :: cons +% {{ com Cons patterns }} +% | id '+' num :: :: num_add +% {{ com constant addition patterns }} | lit :: :: lit {{ com Literal constant patterns }} @@ -640,28 +642,30 @@ exp :: 'E_' ::= -% enummaps - | [ exp1 , ... , expn ] :: :: enummap +% vectors + | [ exp1 , ... , expn ] :: :: vector +% endianness comes from global command-line option??? - | [ num1 = exp1 , ... , numn = expn ] :: :: enummap_e + | [ num1 = exp1 , ... , numn = expn ] :: :: vector_indexed +% num1 .. numn must be a consecutive list of naturals -% we pick [ ] not { } for enummap literals for consistency with their +% we pick [ ] not { } for vector literals for consistency with their % array-like access syntax, in contrast to the C which has funny % syntax for array literals. We don't have to preserve [ ] for lists % as we don't expect to use lists very much. - | exp [ exp' ] :: :: enummap_access - {{ com enummap access }} + | exp [ exp' ] :: :: vector_access + {{ com vector access }} - | exp [ exp1 '..' exp2 ] :: :: enummap_subrange - {{ com Subenummap extraction }} + | exp [ exp1 : exp2 ] :: :: vector_subrange + {{ com Subvector extraction }} % do we want to allow a comma-separated list of such thingies? - | [ exp with exp1 = exp2 ] :: :: enummap_update - {{ com enummap functional update }} + | [ exp with exp1 = exp2 ] :: :: vector_update + {{ com vector functional update }} - | [ exp with exp1 .. exp2 = exp3 ] :: :: enummap_update_range - {{ com enummap functional subrange update (with another enummap)}} + | [ exp with exp1 : exp2 = exp3 ] :: :: vector_update_range + {{ com vector functional subrange update (with another vector)}} % do we want a functional update form with a comma-separated list of such? @@ -702,7 +706,7 @@ exp :: 'E_' ::= {{ com Pattern matching expressions }} % | ( typ ) exp :: :: Typed % {{ com Type-annotated expressions }} - | c_letbind in exp :: :: let + | letbind in exp :: :: let {{ com Let expressions }} | lexp := exp :: :: assign @@ -711,8 +715,8 @@ exp :: 'E_' ::= lexp :: 'LEXP_' ::= | id :: :: ident {{ com Identifiers }} - | lexp [ exp ] :: :: enummap - | lexp [ exp1 '..' exp2 ] :: :: enummap_range + | lexp [ exp ] :: :: vector + | lexp [ exp1 : exp2 ] :: :: vector_range % maybe comma-sep such lists too | lexp . id :: :: field @@ -804,43 +808,43 @@ grammar %%%%% C-ish style %%%%%%%%%% -c_tannot_opt :: 'C_typ_annot_' ::= +tannot_opt :: 'Typ_annot_opt_' ::= {{ com Optional type annotations }} | :: :: none | typ_quant typ :: :: some -c_funcl :: 'C_FCL_' ::= +funcl :: 'FCL_' ::= {{ com Function clauses }} {{ aux _ l }} | id pat = exp :: :: Funcl -c_rec_opt :: '' ::= +rec_opt :: 'Rec_' ::= {{ aux _ l }} | :: :: nonrec | rec :: :: rec -c_effects_opt :: '' ::= +effects_opt :: 'Effects_opt_' ::= {{ aux _ l }} | :: :: pure {{ com sugar for pure }} | effects :: :: nonpure -c_fundef :: 'C_FD_' ::= +fundef :: '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 }} -% TODO note that the typ in the c_tannot_opt is the *result* type, not + | 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 % the type of the whole function. The argument type comes from the -% pattern in the c_funcl +% pattern in the funcl % TODO the above is ok for single functions, but not for mutually -% recursive functions - the c_tannot_opt scopes over all the c_funcli, +% recursive functions - the tannot_opt scopes over all the funcli, % which is ok for the typ_quant part but not for the typ part -c_letbind :: 'LB_' ::= +letbind :: 'LB_' ::= {{ com Let bindings }} {{ aux _ l }} - | typschm id = exp :: :: val_exp + | typschm id = exp :: :: val_explicit {{ com Value binding }} - | let id = exp :: :: val_imp + | let id = exp :: :: val_implicit {{ com value binding with implicit type }} @@ -868,24 +872,33 @@ default_typing_spec :: 'DT_' ::= def :: 'DEF_' ::= {{ com Top-level definitions }} {{ aux _ l }} - | type_def :: :: type_def + | type_def :: :: type {{ com Type definition }} - | c_fundef :: :: fun_def + | fundef :: :: fundef {{ com Function definition }} - | c_letbind :: :: val_def + | letbind :: :: val {{ com Value definition }} - | val_spec :: :: spec_def + | val_spec :: :: spec {{ com Top-level type constraint }} - | default_typing_spec :: :: default_def + | default_typing_spec :: :: default {{ com default kind and type assumptions }} | register typ id :: :: reg_dec {{ com Register declaration }} + | split function rec_opt tannot_opt effects_opt id :: :: split_function + + | function clause funcl :: :: split_funcl + + | end id :: :: split_end + + | split typedef id naming_scheme_opt = const union typquant :: :: split_variant + + | union member id = typ id' :: :: split_unioncl defs :: '' ::= {{ com Definition sequences }} {{ aux _ l }} - | def1 .. defn :: :: Defs + | def1 .. defn :: :: Defs |