diff options
Diffstat (limited to 'language')
| -rw-r--r-- | language/l2.lem | 173 | ||||
| -rw-r--r-- | language/l2.ml | 47 | ||||
| -rw-r--r-- | language/l2.ott | 10 | ||||
| -rw-r--r-- | language/l2_parse.ml | 95 | ||||
| -rw-r--r-- | language/l2_parse.ott | 8 |
5 files changed, 183 insertions, 150 deletions
diff --git a/language/l2.lem b/language/l2.lem index 969a5bbf..4921c16b 100644 --- a/language/l2.lem +++ b/language/l2.lem @@ -75,6 +75,11 @@ type base_effect = | BE_aux of base_effect_aux * l +type id_aux = (* Identifier *) + | Id of x + | DeIid of x (* remove infix status *) + + type effect_aux = (* effect set, of kind Effects *) | Effect_var of kid | Effect_set of list base_effect (* effect set *) @@ -86,9 +91,8 @@ type order_aux = (* vector order specifications, of kind Order *) | Ord_dec (* decreasing (big-endian) *) -type id_aux = (* Identifier *) - | Id of x - | DeIid of x (* remove infix status *) +type id = + | Id_aux of id_aux * l type effect = @@ -98,10 +102,6 @@ type effect = type order = | Ord_aux of order_aux * l - -type id = - | Id_aux of id_aux * l - let effect_union e1 e2 = match (e1,e2) with | ((Effect_aux (Effect_set els) _),(Effect_aux (Effect_set els2) l)) -> Effect_aux (Effect_set (els++els2)) l @@ -142,19 +142,6 @@ type typquant_aux = (* type quantifiers and constraints *) | TypQ_no_forall (* sugar, omitting quantifier and constraints *) -type lit_aux = (* Literal constant *) - | L_unit (* $() : unit$ *) - | L_zero (* $bitzero : bit$ *) - | L_one (* $bitone : bit$ *) - | L_true (* $true : bool$ *) - | L_false (* $false : bool$ *) - | L_num of integer (* natural number constant *) - | L_hex of string (* bit vector constant, C-style *) - | L_bin of string (* bit vector constant, C-style *) - | L_undef (* constant representing undefined values *) - | L_string of string (* string constant *) - - type typ_aux = (* Type expressions, of kind $Type$ *) | Typ_wild (* Unspecified type *) | Typ_id of id (* Defined type *) @@ -180,14 +167,31 @@ type typquant = | TypQ_aux of typquant_aux * l -type lit = - | L_aux of lit_aux * l +type lit_aux = (* Literal constant *) + | L_unit (* $() : unit$ *) + | L_zero (* $bitzero : bit$ *) + | L_one (* $bitone : bit$ *) + | L_true (* $true : bool$ *) + | L_false (* $false : bool$ *) + | L_num of integer (* natural number constant *) + | L_hex of string (* bit vector constant, C-style *) + | L_bin of string (* bit vector constant, C-style *) + | L_undef (* constant representing undefined values *) + | L_string of string (* string constant *) type typschm_aux = (* type scheme *) | TypSchm_ts of typquant * typ +type lit = + | L_aux of lit_aux * l + + +type typschm = + | TypSchm_aux of typschm_aux * l + + type pat_aux 'a = (* Pattern *) | P_lit of lit (* literal constant pattern *) | P_wild (* wildcard *) @@ -212,10 +216,6 @@ and fpat 'a = | FP_aux of (fpat_aux 'a) * annot 'a -type typschm = - | TypSchm_aux of typschm_aux * l - - type exp_aux 'a = (* Expression *) | E_block of list (exp 'a) (* block (parsing conflict with structs?) *) | E_id of id (* identifier *) @@ -227,7 +227,7 @@ type exp_aux 'a = (* Expression *) | E_if of (exp 'a) * (exp 'a) * (exp 'a) (* conditional *) | E_for of id * (exp 'a) * (exp 'a) * (exp 'a) * order * (exp 'a) (* loop *) | E_vector of list (exp 'a) (* vector (indexed from 0) *) - | E_vector_indexed of list (integer * (exp 'a)) (* vector (indexed consecutively) *) + | E_vector_indexed of list (integer * (exp 'a)) * (opt_default 'a) (* vector (indexed consecutively) *) | E_vector_access of (exp 'a) * (exp 'a) (* vector access *) | E_vector_subrange of (exp 'a) * (exp 'a) * (exp 'a) (* subvector extraction *) | E_vector_update of (exp 'a) * (exp 'a) * (exp 'a) (* vector functional update *) @@ -269,6 +269,13 @@ and fexps_aux 'a = (* Field-expression list *) and fexps 'a = | FES_aux of (fexps_aux 'a) * annot 'a +and opt_default_aux 'a = (* Optional default value for indexed vectors, to define a defualt value for any unspecified positions in a sparse map *) + | Def_val_empty + | Def_val_dec of (exp 'a) + +and opt_default 'a = + | Def_val_aux of (opt_default_aux 'a) * annot 'a + and pexp_aux 'a = (* Pattern match *) | Pat_exp of (pat 'a) * (exp 'a) @@ -283,23 +290,14 @@ and letbind 'a = | LB_aux of (letbind_aux 'a) * annot 'a -type effect_opt_aux = (* Optional effect annotation for functions *) - | Effect_opt_pure (* sugar for empty effect set *) - | Effect_opt_effect of effect - - type rec_opt_aux = (* Optional recursive annotation for functions *) | Rec_nonrec (* non-recursive *) | Rec_rec (* recursive *) -type funcl_aux 'a = (* Function clause *) - | FCL_Funcl of id * (pat 'a) * (exp 'a) - - -type 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 effect type type_union_aux = (* Type union constructors *) @@ -307,34 +305,43 @@ type type_union_aux = (* Type union constructors *) | Tu_ty_id of typ * id +type funcl_aux 'a = (* Function clause *) + | FCL_Funcl of id * (pat 'a) * (exp 'a) + + type tannot_opt_aux = (* Optional type annotation for functions *) | Typ_annot_opt_some of typquant * typ -type effect_opt = - | Effect_opt_aux of effect_opt_aux * l +type name_scm_opt_aux = (* Optional variable-naming-scheme specification for variables of defined type *) + | Name_sect_none + | Name_sect_some of string type rec_opt = | Rec_aux of rec_opt_aux * l -type funcl 'a = - | FCL_aux of (funcl_aux 'a) * l - - -type name_scm_opt = - | Name_sect_aux of name_scm_opt_aux * l +type effect_opt = + | Effect_opt_aux of effect_opt_aux * l type type_union = | Tu_aux of type_union_aux * l +type funcl 'a = + | FCL_aux of (funcl_aux 'a) * l + + type tannot_opt = | Typ_annot_opt_aux of tannot_opt_aux * l +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 integer (* single index *) | BF_range of integer * integer (* index range *) @@ -344,6 +351,10 @@ and index_range = | BF_aux of index_range_aux * l +type dec_spec_aux 'a = (* Register declarations *) + | DEC_reg of typ * id + + type scattered_def_aux 'a = (* Function and type union definitions that can be spread across a file. Each one must end in $id$ *) | SD_scattered_function of rec_opt * tannot_opt * effect_opt * id (* scattered function definition header *) @@ -353,18 +364,6 @@ type scattered_def_aux 'a = (* Function and type union definitions that can be | SD_scattered_end of id (* scattered definition end *) -type type_def_aux 'a = (* Type definition body *) - | TD_abbrev of id * name_scm_opt * typschm (* type abbreviation *) - | TD_record of id * name_scm_opt * typquant * list (typ * id) * bool (* struct type definition *) - | TD_variant of id * name_scm_opt * typquant * list type_union * bool (* union type definition *) - | TD_enum of id * name_scm_opt * list id * bool (* enumeration type definition *) - | TD_register of id * nexp * nexp * list (index_range * id) (* register mutable bitfield type definition *) - - -type dec_spec_aux 'a = (* Register declarations *) - | DEC_reg of typ * id - - type fundef_aux 'a = (* Function definition *) | FD_function of rec_opt * tannot_opt * effect_opt * list (funcl 'a) @@ -374,24 +373,28 @@ type default_spec_aux 'a = (* Default kinding or typing assumption *) | DT_typ of typschm * id +type type_def_aux 'a = (* Type definition body *) + | TD_abbrev of id * name_scm_opt * typschm (* type abbreviation *) + | TD_record of id * name_scm_opt * typquant * list (typ * id) * bool (* struct type definition *) + | TD_variant of id * name_scm_opt * typquant * list type_union * bool (* union type definition *) + | TD_enum of id * name_scm_opt * list id * bool (* enumeration type definition *) + | TD_register of id * nexp * nexp * list (index_range * id) (* register mutable bitfield type definition *) + + type val_spec_aux 'a = (* Value type specification *) | VS_val_spec of typschm * id | VS_extern_no_rename of typschm * id | VS_extern_spec of typschm * id * string (* Specify the type and id of a function from Lem, where the string must provide an explicit path to the required function but will not be checked *) -type scattered_def 'a = - | SD_aux of (scattered_def_aux 'a) * annot 'a - - -type type_def 'a = - | TD_aux of (type_def_aux 'a) * annot 'a - - type dec_spec 'a = | DEC_aux of (dec_spec_aux 'a) * annot 'a +type scattered_def 'a = + | SD_aux of (scattered_def_aux 'a) * annot 'a + + type fundef 'a = | FD_aux of (fundef_aux 'a) * annot 'a @@ -400,6 +403,10 @@ type default_spec 'a = | DT_aux of (default_spec_aux 'a) * l +type type_def 'a = + | TD_aux of (type_def_aux 'a) * annot 'a + + type val_spec 'a = | VS_aux of (val_spec_aux 'a) * annot 'a @@ -440,6 +447,15 @@ let rec disjoint_all sets = end +type ne = (* internal numeric expressions *) + | Ne_var of x + | Ne_const of integer + | Ne_mult of ne * ne + | Ne_add of list ne + | Ne_exp of ne + | Ne_unary of ne + + type k = (* Internal kinds *) | Ki_typ | Ki_nat @@ -449,13 +465,11 @@ type k = (* Internal kinds *) | Ki_infer (* Representing an unknown kind, inferred by context *) -type ne = (* internal numeric expressions *) - | Ne_var of x - | Ne_const of integer - | Ne_mult of ne * ne - | Ne_add of list ne - | Ne_exp of ne - | Ne_unary of ne +type nec = (* Numeric expression constraints *) + | Nec_lteq of ne * ne + | Nec_eq of ne * ne + | Nec_gteq of ne * ne + | Nec_in of x * list integer type kinf = (* Whether a kind is default or from a local binding *) @@ -468,13 +482,6 @@ type tid = (* A type identifier or type variable *) | Tid_var of kid -type nec = (* Numeric expression constraints *) - | Nec_lteq of ne * ne - | Nec_eq of ne * ne - | Nec_gteq of ne * ne - | Nec_in of x * list integer - - type t = (* Internal types *) | T_id of x | T_var of x @@ -551,10 +558,10 @@ let fresh_kid denv = Var "x" (*TODO When strings can be manipulated, this should -type I = inf +type E = env -type E = env +type I = inf diff --git a/language/l2.ml b/language/l2.ml index 6501ff28..3ce5cac3 100644 --- a/language/l2.ml +++ b/language/l2.ml @@ -74,9 +74,9 @@ base_effect = type -effect_aux = (* effect set, of kind Effects *) - Effect_var of kid - | Effect_set of (base_effect) list (* effect set *) +id_aux = (* Identifier *) + Id of x + | DeIid of x (* remove infix status *) type @@ -87,14 +87,14 @@ order_aux = (* vector order specifications, of kind Order *) type -id_aux = (* Identifier *) - Id of x - | DeIid of x (* remove infix status *) +effect_aux = (* effect set, of kind Effects *) + Effect_var of kid + | Effect_set of (base_effect) list (* effect set *) type -effect = - Effect_aux of effect_aux * l +id = + Id_aux of id_aux * l type @@ -103,8 +103,8 @@ order = type -id = - Id_aux of id_aux * l +effect = + Effect_aux of effect_aux * l type @@ -163,11 +163,6 @@ lit_aux = (* Literal constant *) type -typquant = - TypQ_aux of typquant_aux * l - - -type typ_aux = (* Type expressions, of kind $_$ *) Typ_wild (* Unspecified type *) | Typ_id of id (* Defined type *) @@ -190,6 +185,11 @@ and typ_arg = type +typquant = + TypQ_aux of typquant_aux * l + + +type lit = L_aux of lit_aux * l @@ -200,10 +200,7 @@ typschm_aux = (* type scheme *) type -'a fpat = - FP_aux of 'a fpat_aux * 'a annot - -and 'a pat_aux = (* Pattern *) +'a pat_aux = (* Pattern *) P_lit of lit (* literal constant pattern *) | P_wild (* wildcard *) | P_as of 'a pat * id (* named pattern *) @@ -223,6 +220,9 @@ and 'a pat = and 'a fpat_aux = (* Field pattern *) FP_Fpat of id * 'a pat +and 'a fpat = + FP_aux of 'a fpat_aux * 'a annot + type typschm = @@ -241,7 +241,7 @@ type | E_if of 'a exp * 'a exp * 'a exp (* conditional *) | E_for of id * 'a exp * 'a exp * 'a exp * order * 'a exp (* loop *) | E_vector of ('a exp) list (* vector (indexed from 0) *) - | E_vector_indexed of ((int * 'a exp)) list (* vector (indexed consecutively) *) + | E_vector_indexed of ((int * 'a exp)) list * 'a opt_default (* vector (indexed consecutively) *) | E_vector_access of 'a exp * 'a exp (* vector access *) | E_vector_subrange of 'a exp * 'a exp * 'a exp (* subvector extraction *) | E_vector_update of 'a exp * 'a exp * 'a exp (* vector functional update *) @@ -283,6 +283,13 @@ and 'a fexps_aux = (* Field-expression list *) and 'a fexps = FES_aux of 'a fexps_aux * 'a annot +and 'a opt_default_aux = (* Optional default value for indexed vectors, to define a defualt value for any unspecified positions in a sparse map *) + Def_val_empty + | Def_val_dec of 'a exp + +and 'a opt_default = + Def_val_aux of 'a opt_default_aux * 'a annot + and 'a pexp_aux = (* Pattern match *) Pat_exp of 'a pat * 'a exp diff --git a/language/l2.ott b/language/l2.ott index 7b619652..a880527c 100644 --- a/language/l2.ott +++ b/language/l2.ott @@ -482,7 +482,7 @@ pat :: 'P_' ::= | [ pat1 , .. , patn ] :: :: vector {{ com vector pattern }} - | [ num1 = pat1 , .. , numn = patn ] :: :: vector_indexed + | [ num1 = pat1 , .. , numn = patn ] :: :: vector_indexed {{ com vector pattern (with explicit indices) }} % cf ntoes for this @@ -561,7 +561,7 @@ exp :: 'E_' ::= % here the expi are of type 'a and the result is a vector of 'a, whereas in exp1 : ... : expn % the expi and the result are both of type vector of 'a - | [ num1 = exp1 , ... , numn = expn ] :: :: vector_indexed {{ com vector (indexed consecutively) }} + | [ num1 = exp1 , ... , numn = expn , opt_default ] :: :: 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 @@ -655,6 +655,12 @@ fexps :: 'FES_' ::= {{ aux _ annot }} {{ auxparam 'a }} | fexp1 ; ... ; fexpn semi_opt :: :: Fexps +opt_default :: 'Def_val_' ::= + {{ com Optional default value for indexed vectors, to define a defualt value for any unspecified positions in a sparse map }} + {{ aux _ annot }} {{ auxparam 'a }} + | :: :: empty + | default = exp :: :: dec + pexp :: 'Pat_' ::= {{ com Pattern match }} {{ aux _ annot }} {{ auxparam 'a }} diff --git a/language/l2_parse.ml b/language/l2_parse.ml index 7be33bc4..a283b605 100644 --- a/language/l2_parse.ml +++ b/language/l2_parse.ml @@ -208,7 +208,7 @@ exp_aux = (* Expression *) | E_if of exp * exp * exp (* conditional *) | E_for of id * exp * exp * exp * atyp * exp (* loop *) | E_vector of (exp) list (* vector (indexed from 0) *) - | E_vector_indexed of ((int * exp)) list (* vector (indexed consecutively) *) + | E_vector_indexed of ((int * exp)) list * opt_default (* vector (indexed consecutively) *) | E_vector_access of exp * exp (* vector access *) | E_vector_subrange of exp * exp * exp (* subvector extraction *) | E_vector_update of exp * exp * exp (* vector functional update *) @@ -237,6 +237,13 @@ and fexps_aux = (* Field-expression list *) and fexps = FES_aux of fexps_aux * l +and opt_default_aux = (* Optional default value for indexed vectors, to define a defualt value for any unspecified positions in a sparse map *) + Def_val_empty + | Def_val_dec of exp + +and opt_default = + Def_val_aux of opt_default_aux * l + and pexp_aux = (* Pattern match *) Pat_exp of pat * exp @@ -264,26 +271,26 @@ type_union_aux = (* Type union constructors *) type -tannot_opt_aux = (* Optional type annotation for functions *) - Typ_annot_opt_none - | Typ_annot_opt_some of typquant * atyp +rec_opt_aux = (* Optional recursive annotation for functions *) + Rec_nonrec (* non-recursive *) + | Rec_rec (* recursive *) type -effect_opt_aux = (* Optional effect annotation for functions *) - Effect_opt_pure (* sugar for empty effect set *) - | Effect_opt_effect of atyp +funcl_aux = (* Function clause *) + FCL_Funcl of id * pat * exp type -rec_opt_aux = (* Optional recursive annotation for functions *) - Rec_nonrec (* non-recursive *) - | Rec_rec (* recursive *) +tannot_opt_aux = (* Optional type annotation for functions *) + Typ_annot_opt_none + | Typ_annot_opt_some of typquant * atyp type -funcl_aux = (* Function clause *) - FCL_Funcl of id * pat * exp +effect_opt_aux = (* Optional effect annotation for functions *) + Effect_opt_pure (* sugar for empty effect set *) + | Effect_opt_effect of atyp type @@ -307,16 +314,6 @@ type_union = type -tannot_opt = - Typ_annot_opt_aux of tannot_opt_aux * l - - -type -effect_opt = - Effect_opt_aux of effect_opt_aux * l - - -type rec_opt = Rec_aux of rec_opt_aux * l @@ -327,10 +324,13 @@ funcl = type -val_spec_aux = (* Value type specification *) - VS_val_spec of typschm * id - | VS_extern_no_rename of typschm * id - | VS_extern_spec of typschm * id * string +tannot_opt = + Typ_annot_opt_aux of tannot_opt_aux * l + + +type +effect_opt = + Effect_opt_aux of effect_opt_aux * l type @@ -343,19 +343,13 @@ type_def_aux = (* Type definition body *) type -dec_spec_aux = (* Register declarations *) - DEC_reg of atyp * id - - -type -default_typing_spec_aux = (* Default kinding or typing assumption *) - DT_kind of base_kind * kid - | DT_typ of typschm * id +fundef_aux = (* Function definition *) + FD_function of rec_opt * tannot_opt * effect_opt * (funcl) list type -fundef_aux = (* Function definition *) - FD_function of rec_opt * tannot_opt * effect_opt * (funcl) list +dec_spec_aux = (* Register declarations *) + DEC_reg of atyp * id type @@ -369,8 +363,16 @@ scattered_def_aux = (* Function and type union definitions that can be spread a type -val_spec = - VS_aux of val_spec_aux * l +val_spec_aux = (* Value type specification *) + VS_val_spec of typschm * id + | VS_extern_no_rename of typschm * id + | VS_extern_spec of typschm * id * string + + +type +default_typing_spec_aux = (* Default kinding or typing assumption *) + DT_kind of base_kind * kid + | DT_typ of typschm * id type @@ -379,23 +381,28 @@ type_def = type +fundef = + FD_aux of fundef_aux * l + + +type dec_spec = DEC_aux of dec_spec_aux * l type -default_typing_spec = - DT_aux of default_typing_spec_aux * l +scattered_def = + SD_aux of scattered_def_aux * l type -fundef = - FD_aux of fundef_aux * l +val_spec = + VS_aux of val_spec_aux * l type -scattered_def = - SD_aux of scattered_def_aux * l +default_typing_spec = + DT_aux of default_typing_spec_aux * l type diff --git a/language/l2_parse.ott b/language/l2_parse.ott index 1f365a3f..11b51f2a 100644 --- a/language/l2_parse.ott +++ b/language/l2_parse.ott @@ -452,7 +452,7 @@ exp :: 'E_' ::= % here the expi are of type 'a and the result is a vector of 'a, whereas in exp1 : ... : expn % the expi and the result are both of type vector of 'a - | [ num1 = exp1 , ... , numn = expn ] :: :: vector_indexed {{ com vector (indexed consecutively) }} + | [ num1 = exp1 , ... , numn = expn , opt_default ] :: :: 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 @@ -544,6 +544,12 @@ fexps :: 'FES_' ::= % {{ aux _ annot }} {{ auxparam 'a }} | fexp1 ; ... ; fexpn semi_opt :: :: Fexps +opt_default :: 'Def_val_' ::= + {{ com Optional default value for indexed vectors, to define a defualt value for any unspecified positions in a sparse map }} + {{ aux _ l }} + | :: :: empty + | default = exp :: :: dec + pexp :: 'Pat_' ::= {{ com Pattern match }} {{ aux _ l }} |