diff options
Diffstat (limited to 'language')
| -rw-r--r-- | language/l2.lem | 1 | ||||
| -rw-r--r-- | language/l2.ml | 1 | ||||
| -rw-r--r-- | language/l2.ott | 4 | ||||
| -rw-r--r-- | language/l2_parse.ml | 133 | ||||
| -rw-r--r-- | language/l2_parse.ott | 6 |
5 files changed, 73 insertions, 72 deletions
diff --git a/language/l2.lem b/language/l2.lem index 30027846..4ba01310 100644 --- a/language/l2.lem +++ b/language/l2.lem @@ -55,6 +55,7 @@ type nexp_aux = (* expression of kind Nat, for vector sizes and origins *) | Nexp_times of nexp * nexp (* product *) | Nexp_sum of nexp * nexp (* sum *) | Nexp_exp of nexp (* exponential *) + | Nexp_neg of nexp (* For internal use. Not M as a dataconstructor is required *) and nexp = | Nexp_aux of nexp_aux * l diff --git a/language/l2.ml b/language/l2.ml index 1c2a6c09..4e58d63c 100644 --- a/language/l2.ml +++ b/language/l2.ml @@ -46,6 +46,7 @@ nexp_aux = (* expression of kind Nat, for vector sizes and origins *) | Nexp_times of nexp * nexp (* product *) | Nexp_sum of nexp * nexp (* sum *) | Nexp_exp of nexp (* exponential *) + | Nexp_neg of nexp (* For internal use. Not M as a dataconstructor is required *) and nexp = Nexp_aux of nexp_aux * l diff --git a/language/l2.ott b/language/l2.ott index aa981cc7..6efabf62 100644 --- a/language/l2.ott +++ b/language/l2.ott @@ -164,9 +164,9 @@ nexp :: 'Nexp_' ::= | kid :: :: var {{ com variable }} | 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 }} + | neg nexp :: :: neg {{ com For internal use. Not M as a dataconstructor is required }} | ( nexp ) :: S :: paren {{ ichlo [[nexp]] }} order :: 'Ord_' ::= @@ -240,6 +240,8 @@ typ :: 'Typ_' ::= % (but with .. not : in the former, to avoid confusion...) | typ [ nexp ] :: S :: vector2 {{ichlo vector < [[nexp]],0,inc,[[typ]] > }} {{ com sugar for vector indexed by [ [[nexp]] ] }} | typ [ nexp : nexp' ] :: S :: vector3 {{ ichlo vector < [[nexp]],[[nexp']],inc,[[typ]] }} {{ com sugar for vector indexed by [ [[nexp]]..[[nexp']] ] }} + | typ [ nexp <: nexp' ] :: S :: vector4 {{ ichlo vector < [[nexp]],[[nexp']],inc,[[typ]] }} {{ com sugar for increasing vector indexed as above }} + | typ [ nexp :> nexp' ] :: S :: vector5 {{ ichlo vector < [[nexp]],[[nexp']],dec,[[typ]] }} {{ com sugar for decreasing vector indexed as above }} % ...so bit [ nexp ] etc is just an instance of that % | List < typ > :: :: list {{ com list of [[typ]] }} % | Set < typ > :: :: set {{ com finite set of [[typ]] }} diff --git a/language/l2_parse.ml b/language/l2_parse.ml index 8615faa6..92d00530 100644 --- a/language/l2_parse.ml +++ b/language/l2_parse.ml @@ -1,4 +1,4 @@ -(* generated by Ott 0.23 from: l2_parse.ott *) +(* generated by Ott 0.24 from: l2_parse.ott *) type text = string @@ -25,9 +25,8 @@ base_kind_aux = (* base kind *) type -id_aux = (* Identifier *) - Id of x - | DeIid of x (* remove infix status *) +base_kind = + BK_aux of base_kind_aux * l type @@ -47,13 +46,14 @@ base_effect_aux = (* effect *) type -base_kind = - BK_aux of base_kind_aux * l +id_aux = (* Identifier *) + Id of x + | DeIid of x (* remove infix status *) type -id = - Id_aux of id_aux * l +kind_aux = (* kinds *) + K_kind of (base_kind) list type @@ -67,8 +67,13 @@ base_effect = type -kind_aux = (* kinds *) - K_kind of (base_kind) list +id = + Id_aux of id_aux * l + + +type +kind = + K_aux of kind_aux * l type @@ -79,6 +84,7 @@ atyp_aux = (* expressions of all kinds, to be translated to types, nats, orders | ATyp_times of atyp * atyp (* product *) | ATyp_sum of atyp * atyp (* sum *) | ATyp_exp of atyp (* exponential *) + | ATyp_neg of atyp (* Internal (but not M as I want a datatype constructor) negative nexp *) | ATyp_inc (* increasing (little-endian) *) | ATyp_dec (* decreasing (big-endian) *) | ATyp_set of (base_effect) list (* effect set *) @@ -91,8 +97,9 @@ and atyp = type -kind = - K_aux of kind_aux * l +kinded_id_aux = (* optionally kind-annotated identifier *) + KOpt_none of kid (* identifier *) + | KOpt_kind of kind * kid (* kind-annotated variable *) type @@ -104,9 +111,8 @@ n_constraint_aux = (* constraint over kind $_$ *) type -kinded_id_aux = (* optionally kind-annotated identifier *) - KOpt_none of kid (* identifier *) - | KOpt_kind of kind * kid (* kind-annotated variable *) +kinded_id = + KOpt_aux of kinded_id_aux * l type @@ -115,11 +121,6 @@ n_constraint = type -kinded_id = - KOpt_aux of kinded_id_aux * l - - -type quant_item_aux = (* Either a kinded identifier or a nexp constraint for a typquant *) QI_id of kinded_id (* An optionally kinded identifier *) | QI_const of n_constraint (* A constraint for this type *) @@ -137,11 +138,6 @@ typquant_aux = (* type quantifiers and constraints *) type -typquant = - TypQ_aux of typquant_aux * l - - -type lit_aux = (* Literal constant *) L_unit (* $() : _$ *) | L_zero (* $_ : _$ *) @@ -156,8 +152,8 @@ lit_aux = (* Literal constant *) type -typschm_aux = (* type scheme *) - TypSchm_ts of typquant * atyp +typquant = + TypQ_aux of typquant_aux * l type @@ -166,8 +162,8 @@ lit = type -typschm = - TypSchm_aux of typschm_aux * l +typschm_aux = (* type scheme *) + TypSchm_ts of typquant * atyp type @@ -196,6 +192,11 @@ and fpat = type +typschm = + TypSchm_aux of typschm_aux * l + + +type exp_aux = (* Expression *) E_block of (exp) list (* block (parsing conflict with structs?) *) | E_id of id (* identifier *) @@ -251,21 +252,21 @@ and letbind = type -name_scm_opt_aux = (* Optional variable-naming-scheme specification for variables of defined type *) - Name_sect_none - | Name_sect_some of string - - -type type_union_aux = (* Type union constructors *) Tu_id of id | Tu_ty_id of atyp * id type -rec_opt_aux = (* Optional recursive annotation for functions *) - Rec_nonrec (* non-recursive *) - | Rec_rec (* recursive *) +name_scm_opt_aux = (* Optional variable-naming-scheme specification for variables of defined type *) + Name_sect_none + | Name_sect_some of string + + +type +effect_opt_aux = (* Optional effect annotation for functions *) + Effect_opt_pure (* sugar for empty effect set *) + | Effect_opt_effect of atyp type @@ -275,9 +276,9 @@ tannot_opt_aux = (* Optional type annotation for functions *) type -effect_opt_aux = (* Optional effect annotation for functions *) - Effect_opt_pure (* sugar for empty effect set *) - | Effect_opt_effect of atyp +rec_opt_aux = (* Optional recursive annotation for functions *) + Rec_nonrec (* non-recursive *) + | Rec_rec (* recursive *) type @@ -286,11 +287,6 @@ funcl_aux = (* Function clause *) type -name_scm_opt = - Name_sect_aux of name_scm_opt_aux * l - - -type index_range_aux = (* index specification, for bitfields in register types *) BF_single of int (* single index *) | BF_range of int * int (* index range *) @@ -306,8 +302,13 @@ type_union = type -rec_opt = - Rec_aux of rec_opt_aux * l +name_scm_opt = + Name_sect_aux of name_scm_opt_aux * l + + +type +effect_opt = + Effect_opt_aux of effect_opt_aux * l type @@ -316,8 +317,8 @@ tannot_opt = type -effect_opt = - Effect_opt_aux of effect_opt_aux * l +rec_opt = + Rec_aux of rec_opt_aux * l type @@ -335,6 +336,12 @@ type_def_aux = (* Type definition body *) type +default_typing_spec_aux = (* Default kinding or typing assumption *) + DT_kind of base_kind * kid + | DT_typ of typschm * id + + +type scattered_def_aux = (* Function and type union definitions that can be spread across a file. Each one must end in $_$ *) SD_scattered_function of rec_opt * tannot_opt * effect_opt * id (* scattered function definition header *) @@ -352,12 +359,6 @@ val_spec_aux = (* Value type specification *) type -default_typing_spec_aux = (* Default kinding or typing assumption *) - DT_kind of base_kind * kid - | DT_typ of typschm * id - - -type fundef_aux = (* Function definition *) FD_function of rec_opt * tannot_opt * effect_opt * (funcl) list @@ -368,6 +369,11 @@ type_def = type +default_typing_spec = + DT_aux of default_typing_spec_aux * l + + +type scattered_def = SD_aux of scattered_def_aux * l @@ -378,11 +384,6 @@ val_spec = type -default_typing_spec = - DT_aux of default_typing_spec_aux * l - - -type fundef = FD_aux of fundef_aux * l @@ -404,6 +405,11 @@ def = type +defs = (* Definition sequence *) + Defs of (def) list + + +type lexp_aux = (* lvalue expression *) LEXP_id of id (* identifier *) | LEXP_mem of id * (exp) list @@ -415,9 +421,4 @@ and lexp = LEXP_aux of lexp_aux * l -type -defs = (* Definition sequence *) - Defs of (def) list - - diff --git a/language/l2_parse.ott b/language/l2_parse.ott index da3d57ca..3ef811bb 100644 --- a/language/l2_parse.ott +++ b/language/l2_parse.ott @@ -106,11 +106,6 @@ l :: '' ::= {{ phantom }} {{ lem Unknown }} {{ hol () }} -annot :: '' ::= - {{ phantom }} - {{ ocaml 'a annot }} - {{ lem annot }} - {{ hol unit }} id :: '' ::= {{ com Identifier }} @@ -173,6 +168,7 @@ atyp :: 'ATyp_' ::= | atyp1 * atyp2 :: :: times {{ com product }} | atyp1 + atyp2 :: :: sum {{ com sum }} | 2** atyp :: :: exp {{ com exponential }} + | neg atyp :: :: neg {{ com Internal (but not M as I want a datatype constructor) negative nexp }} | ( atyp ) :: S :: paren {{ icho [[atyp]] }} | inc :: :: inc {{ com increasing (little-endian) }} |