diff options
| -rw-r--r-- | language/l2.ott | 8 | ||||
| -rw-r--r-- | language/l2_parse.ott | 8 | ||||
| -rw-r--r-- | src/ast.ml | 186 | ||||
| -rw-r--r-- | src/lexer.mll | 5 | ||||
| -rw-r--r-- | src/parse_ast.ml | 141 | ||||
| -rw-r--r-- | src/parser.mly | 478 |
6 files changed, 325 insertions, 501 deletions
diff --git a/language/l2.ott b/language/l2.ott index 3bdfeba8..47283a84 100644 --- a/language/l2.ott +++ b/language/l2.ott @@ -5,7 +5,7 @@ indexvar n , i , j , k ::= metavar num ::= {{ phantom }} {{ lex numeric }} - {{ ocaml terminal * int }} + {{ ocaml (terminal * int) }} {{ hol num }} {{ lem (terminal * num) }} {{ com Numeric literals }} @@ -332,7 +332,7 @@ order :: 'Ord_' ::= | dec :: :: dec {{ com decreasing (big-endian) }} | ( order ) :: S :: paren {{ icho [[order]] }} -effect :: 'Effect_' ::= +efct :: 'Effect_' ::= {{ com effect }} {{ aux _ l }} | rreg :: :: rreg {{ com read register }} @@ -347,8 +347,8 @@ effect :: 'Effect_' ::= effects :: 'Effects_' ::= {{ com effect set, of kind $[[Effects]]$ }} {{ aux _ l }} - | id :: :: var - | { effect1 , .. , effectn } :: :: set {{ com effect set }} + | effect id :: :: var + | effect { efct1 , .. , efctn } :: :: set {{ com effect set }} | pure :: M :: pure {{ com sugar for empty effect set }} {{ icho [] }} % TODO: are we going to need any effect polymorphism? Conceivably for built-in maps and folds. Yes. But we think we don't need any interesting effect-set expressions, eg effectset-variable union {rreg}. diff --git a/language/l2_parse.ott b/language/l2_parse.ott index 86f31122..0481c602 100644 --- a/language/l2_parse.ott +++ b/language/l2_parse.ott @@ -5,7 +5,7 @@ indexvar n , i , j , k ::= metavar num ::= {{ phantom }} {{ lex numeric }} - {{ ocaml terminal * int }} + {{ ocaml (terminal * int) }} {{ hol num }} {{ lem (terminal * num) }} {{ com Numeric literals }} @@ -304,7 +304,7 @@ kind :: 'K_' ::= | base_kind1 -> ... -> base_kindn :: :: kind % we'll never use ...-> Nat -effect :: 'Effect_' ::= +efct :: 'Effect_' ::= {{ com effect }} {{ aux _ l }} | rreg :: :: rreg {{ com read register }} @@ -328,8 +328,8 @@ atyp :: 'ATyp_' ::= | inc :: :: inc {{ com increasing (little-endian) }} | dec :: :: dec {{ com decreasing (big-endian) }} - - | { effect1 , .. , effectn } :: :: set {{ com effect set }} + | effect id :: :: efid + | effect { efct1 , .. , efctn } :: :: set {{ com effect set }} | pure :: M :: pure {{ com sugar for empty effect set }} {{ icho [] }} % TODO: are we going to need any effect polymorphism? Conceivably for built-in maps and folds. Yes. But we think we don't need any interesting effect-set expressions, eg effectset-variable union {rreg}. @@ -59,14 +59,19 @@ base_kind_aux = (* base kind *) type +base_kind = + BK_aux of base_kind_aux * l + + +type id_aux = (* Identifier *) Id of x | DeIid of terminal * x * terminal (* remove infix status *) type -base_kind = - BK_aux of base_kind_aux * l +kind_aux = (* kinds *) + K_kind of (base_kind * terminal) list type @@ -75,12 +80,7 @@ id = type -kind_aux = (* kinds *) - K_kind of (base_kind * terminal) list - - -type -effect_aux = (* effect *) +efct_aux = (* effect *) Effect_rreg of terminal (* read register *) | Effect_wreg of terminal (* write register *) | Effect_rmem of terminal (* read memory *) @@ -91,9 +91,14 @@ effect_aux = (* effect *) type +kind = + K_aux of kind_aux * l + + +type nexp_aux = (* expression of kind $_$, for vector sizes and origins *) Nexp_id of id (* identifier *) - | Nexp_constant of terminal * int (* constant *) + | 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 *) @@ -103,13 +108,14 @@ and nexp = type -kind = - K_aux of kind_aux * l +efct = + Effect_aux of efct_aux * l type -effect = - Effect_aux of effect_aux * l +kinded_id_aux = (* optionally kind-annotated identifier *) + KOpt_none of id (* identifier *) + | KOpt_kind of kind * id (* kind-annotated variable *) type @@ -117,19 +123,13 @@ type NC_fixed of nexp * terminal * nexp | NC_bounded_ge of nexp * terminal * nexp | NC_bounded_le of nexp * terminal * nexp - | NC_nat_set_bounded of id * terminal * terminal * (terminal * int * terminal) list * terminal - - -type -kinded_id_aux = (* optionally kind-annotated identifier *) - KOpt_none of id (* identifier *) - | KOpt_kind of kind * id (* kind-annotated variable *) + | NC_nat_set_bounded of id * terminal * terminal * ((terminal * int) * terminal) list * terminal type effects_aux = (* effect set, of kind $_$ *) - Effects_var of id - | Effects_set of terminal * (effect * terminal) list * terminal (* effect set *) + Effects_var of terminal * id + | Effects_set of terminal * terminal * (efct * terminal) list * terminal (* effect set *) type @@ -140,13 +140,13 @@ order_aux = (* vector order specifications, of kind $_$ *) type -'a nexp_constraint = - NC_aux of 'a nexp_constraint_aux * 'a annot +kinded_id = + KOpt_aux of kinded_id_aux * l type -kinded_id = - KOpt_aux of kinded_id_aux * l +'a nexp_constraint = + NC_aux of 'a nexp_constraint_aux * 'a annot type @@ -167,6 +167,19 @@ type type +lit_aux = (* 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 * string (* string constant *) + + +type typ_aux = (* Type expressions, of kind $_$ *) Typ_wild of terminal (* Unspecified type *) | Typ_var of id (* Type variable *) @@ -193,31 +206,13 @@ type type -lit_aux = (* 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 * string (* string constant *) - - -type -'a typschm_aux = (* type scheme *) - TypSchm_ts of 'a typquant * typ - - -type lit = L_aux of lit_aux * l type -'a typschm = - TypSchm_aux of 'a typschm_aux * 'a annot +'a typschm_aux = (* type scheme *) + TypSchm_ts of 'a typquant * typ type @@ -230,7 +225,7 @@ type | P_app of id * ('a pat) list (* union constructor pattern *) | P_record of terminal * ('a fpat * terminal) list * terminal * bool * terminal (* struct pattern *) | P_vector of terminal * ('a pat * terminal) list * terminal (* vector pattern *) - | P_vector_indexed of terminal * ((terminal * int * terminal * 'a pat) * terminal) list * terminal (* vector pattern (with explicit indices) *) + | P_vector_indexed of terminal * (((terminal * int) * terminal * 'a pat) * terminal) list * terminal (* vector pattern (with explicit indices) *) | P_vector_concat of ('a pat * terminal) list (* concatenated vector pattern *) | P_tup of terminal * ('a pat * terminal) list * terminal (* tuple pattern *) | P_list of terminal * ('a pat * terminal) list * terminal (* list pattern *) @@ -246,7 +241,15 @@ and 'a fpat = type -'a exp_aux = (* Expression *) +'a typschm = + TypSchm_aux of 'a typschm_aux * 'a annot + + +type +'a letbind = + LB_aux of 'a letbind_aux * 'a annot + +and 'a exp_aux = (* Expression *) E_block of terminal * ('a exp * terminal) list * terminal (* block (parsing conflict with structs?) *) | E_id of id (* identifier *) | E_lit of lit (* literal constant *) @@ -256,7 +259,7 @@ type | E_tuple of terminal * ('a exp * terminal) list * terminal (* tuple *) | E_if of terminal * 'a exp * terminal * 'a exp * terminal * 'a exp (* conditional *) | E_vector of terminal * ('a exp * terminal) list * terminal (* vector (indexed from 0) *) - | E_vector_indexed of terminal * ((terminal * int * terminal * 'a exp) * terminal) list * terminal (* vector (indexed consecutively) *) + | E_vector_indexed of terminal * (((terminal * int) * terminal * 'a exp) * terminal) list * terminal (* vector (indexed consecutively) *) | E_vector_access of 'a exp * terminal * 'a exp * terminal (* vector access *) | E_vector_subrange of 'a exp * terminal * 'a exp * terminal * 'a exp * terminal (* subvector extraction *) | E_vector_update of terminal * 'a exp * terminal * 'a exp * terminal * 'a exp * terminal (* vector functional update *) @@ -304,9 +307,6 @@ and 'a letbind_aux = (* Let binding *) LB_val_explicit of 'a typschm * 'a pat * terminal * 'a exp (* value binding, explicit type ('a pat must be total) *) | LB_val_implicit of terminal * 'a pat * terminal * 'a exp (* value binding, implicit type ('a pat must be total) *) -and 'a letbind = - LB_aux of 'a letbind_aux * 'a annot - type naming_scheme_opt_aux = (* Optional variable-naming-scheme specification for variables of defined type *) @@ -315,37 +315,32 @@ naming_scheme_opt_aux = (* Optional variable-naming-scheme specification for va type -'a tannot_opt_aux = (* Optional type annotation for functions *) - Typ_annot_opt_none - | Typ_annot_opt_some of terminal * typ - - -type rec_opt_aux = (* Optional recursive annotation for functions *) Rec_nonrec (* non-recursive *) | Rec_rec of terminal (* recursive *) type -'a effects_opt_aux = (* Optional effect annotation for functions *) - Effects_opt_pure (* sugar for empty effect set *) - | Effects_opt_effects of effects +'a funcl_aux = (* Function clause *) + FCL_Funcl of id * 'a pat * terminal * 'a exp type -'a funcl_aux = (* Function clause *) - FCL_Funcl of id * 'a pat * terminal * 'a exp +'a tannot_opt_aux = (* Optional type annotation for functions *) + Typ_annot_opt_none + | Typ_annot_opt_some of terminal * typ type -naming_scheme_opt = - Name_sect_aux of naming_scheme_opt_aux * l +'a effects_opt_aux = (* Optional effect annotation for functions *) + Effects_opt_pure (* sugar for empty effect set *) + | Effects_opt_effects of effects type index_range_aux = (* index specification, for bitfields in register types *) - BF_single of terminal * int (* single index *) - | BF_range of terminal * int * terminal * terminal * int (* index range *) + 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 *) and index_range = @@ -353,8 +348,8 @@ and index_range = type -'a tannot_opt = - Typ_annot_opt_aux of 'a tannot_opt_aux * 'a annot +naming_scheme_opt = + Name_sect_aux of naming_scheme_opt_aux * l type @@ -363,19 +358,18 @@ rec_opt = type -'a effects_opt = - Effects_opt_aux of 'a effects_opt_aux * 'a annot +'a funcl = + FCL_aux of 'a funcl_aux * 'a annot type -'a funcl = - FCL_aux of 'a funcl_aux * 'a annot +'a tannot_opt = + Typ_annot_opt_aux of 'a tannot_opt_aux * 'a annot type -'a default_typing_spec_aux = (* Default kinding or typing assumption *) - DT_kind of terminal * base_kind * id - | DT_typ of terminal * 'a typschm * id +'a effects_opt = + Effects_opt_aux of 'a effects_opt_aux * 'a annot type @@ -388,18 +382,19 @@ type type -'a fundef_aux = (* Function definition *) - FD_function of terminal * rec_opt * 'a tannot_opt * 'a effects_opt * ('a funcl * terminal) list +'a val_spec_aux = (* Value type specification *) + VS_val_spec of terminal * 'a typschm * id type -'a val_spec_aux = (* Value type specification *) - VS_val_spec of terminal * 'a typschm * id +'a default_typing_spec_aux = (* Default kinding or typing assumption *) + DT_kind of terminal * base_kind * id + | DT_typ of terminal * 'a typschm * id type -'a default_typing_spec = - DT_aux of 'a default_typing_spec_aux * 'a annot +'a fundef_aux = (* Function definition *) + FD_function of terminal * rec_opt * 'a tannot_opt * 'a effects_opt * ('a funcl * terminal) list type @@ -408,13 +403,18 @@ type type -'a fundef = - FD_aux of 'a fundef_aux * 'a annot +'a val_spec = + VS_aux of 'a val_spec_aux * 'a annot type -'a val_spec = - VS_aux of 'a val_spec_aux * 'a annot +'a default_typing_spec = + DT_aux of 'a default_typing_spec_aux * 'a annot + + +type +'a fundef = + FD_aux of 'a fundef_aux * 'a annot type @@ -433,11 +433,6 @@ type type -'a def = - DEF_aux of 'a def_aux * 'a annot - - -type 'a 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 $_$ *) @@ -461,8 +456,8 @@ type type -'a defs = (* Definition sequence *) - Defs of ('a def) list +'a def = + DEF_aux of 'a def_aux * 'a annot type @@ -475,4 +470,9 @@ type CT_aux of 'a ctor_def_aux * 'a annot +type +'a defs = (* Definition sequence *) + Defs of ('a def) list + + diff --git a/src/lexer.mll b/src/lexer.mll index 6c2fac21..c637984f 100644 --- a/src/lexer.mll +++ b/src/lexer.mll @@ -65,6 +65,8 @@ let kw_table = ("clause", (fun x -> Clause(x))); ("const", (fun x -> Const(x))); ("default", (fun x -> Default(x))); + ("effect", (fun x -> Effect(x))); + ("Effects", (fun x -> Effects(x))); ("end", (fun x -> End(x))); ("enum", (fun x -> Enum(x))); ("else", (fun x -> Else(x))); @@ -76,6 +78,8 @@ let kw_table = ("IN", (fun x -> IN(x,r"IN"))); ("let", (fun x -> Let_(x))); ("member", (fun x -> Member(x))); + ("Nat", (fun x -> Nat(x))); + ("Order", (fun x -> Order(x))); ("rec", (fun x -> Rec(x))); ("register", (fun x -> Register(x))); ("scattered", (fun x -> Scattered(x))); @@ -84,6 +88,7 @@ let kw_table = ("then", (fun x -> Then(x))); ("true", (fun x -> True(x))); ("type", (fun x -> Type(x))); + ("Type", (fun x -> TYPE(x))); ("typedef", (fun x -> Typedef(x))); ("union", (fun x -> Union(x))) ("with", (fun x -> With(x))); diff --git a/src/parse_ast.ml b/src/parse_ast.ml index 2ecf279d..c1ccb79a 100644 --- a/src/parse_ast.ml +++ b/src/parse_ast.ml @@ -59,13 +59,7 @@ base_kind_aux = (* base kind *) type -id_aux = (* Identifier *) - Id of x - | DeIid of terminal * x * terminal (* remove infix status *) - - -type -effect_aux = (* effect *) +efct_aux = (* effect *) Effect_rreg of terminal (* read register *) | Effect_wreg of terminal (* write register *) | Effect_rmem of terminal (* read memory *) @@ -76,18 +70,24 @@ effect_aux = (* effect *) type +id_aux = (* Identifier *) + Id of x + | DeIid of terminal * x * terminal (* remove infix status *) + + +type base_kind = BK_aux of base_kind_aux * l type -id = - Id_aux of id_aux * l +efct = + Effect_aux of efct_aux * l type -effect = - Effect_aux of effect_aux * l +id = + Id_aux of id_aux * l type @@ -98,13 +98,14 @@ kind_aux = (* kinds *) type atyp_aux = (* expression of all kinds *) ATyp_id of id (* identifier *) - | ATyp_constant of terminal * int (* constant *) + | ATyp_constant of (terminal * int) (* constant *) | ATyp_times of atyp * terminal * atyp (* product *) | ATyp_sum of atyp * terminal * atyp (* sum *) | ATyp_exp of terminal * terminal * atyp (* exponential *) | ATyp_inc of terminal (* increasing (little-endian) *) | ATyp_dec of terminal (* decreasing (big-endian) *) - | ATyp_set of terminal * (effect * terminal) list * terminal (* effect set *) + | ATyp_efid of terminal * id + | ATyp_set of terminal * terminal * (efct * terminal) list * terminal (* effect set *) | ATyp_wild of terminal (* Unspecified type *) | ATyp_fn of atyp * terminal * atyp * atyp (* Function type (first-order only in user code) *) | ATyp_tup of (atyp * terminal) list (* Tuple type *) @@ -124,7 +125,7 @@ type NC_fixed of atyp * terminal * atyp | NC_bounded_ge of atyp * terminal * atyp | NC_bounded_le of atyp * terminal * atyp - | NC_nat_set_bounded of id * terminal * terminal * (terminal * int * terminal) list * terminal + | NC_nat_set_bounded of id * terminal * terminal * ((terminal * int) * terminal) list * terminal type @@ -151,26 +152,21 @@ type type -'a typquant = - TypQ_aux of 'a typquant_aux * 'a annot - - -type lit_aux = (* 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_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 * string (* string constant *) type -'a typschm_aux = (* type scheme *) - TypSchm_ts of 'a typquant * atyp +'a typquant = + TypQ_aux of 'a typquant_aux * 'a annot type @@ -179,8 +175,8 @@ lit = type -'a typschm = - TypSchm_aux of 'a typschm_aux * 'a annot +'a typschm_aux = (* type scheme *) + TypSchm_ts of 'a typquant * atyp type @@ -193,7 +189,7 @@ type | P_app of id * ('a pat) list (* union constructor pattern *) | P_record of terminal * ('a fpat * terminal) list * terminal * bool * terminal (* struct pattern *) | P_vector of terminal * ('a pat * terminal) list * terminal (* vector pattern *) - | P_vector_indexed of terminal * ((terminal * int * terminal * 'a pat) * terminal) list * terminal (* vector pattern (with explicit indices) *) + | P_vector_indexed of terminal * (((terminal * int) * terminal * 'a pat) * terminal) list * terminal (* vector pattern (with explicit indices) *) | P_vector_concat of ('a pat * terminal) list (* concatenated vector pattern *) | P_tup of terminal * ('a pat * terminal) list * terminal (* tuple pattern *) | P_list of terminal * ('a pat * terminal) list * terminal (* list pattern *) @@ -209,6 +205,11 @@ and 'a fpat = type +'a typschm = + TypSchm_aux of 'a typschm_aux * 'a annot + + +type 'a exp_aux = (* Expression *) E_block of terminal * ('a exp * terminal) list * terminal (* block (parsing conflict with structs?) *) | E_id of id (* identifier *) @@ -219,7 +220,7 @@ type | E_tuple of terminal * ('a exp * terminal) list * terminal (* tuple *) | E_if of terminal * 'a exp * terminal * 'a exp * terminal * 'a exp (* conditional *) | E_vector of terminal * ('a exp * terminal) list * terminal (* vector (indexed from 0) *) - | E_vector_indexed of terminal * ((terminal * int * terminal * 'a exp) * terminal) list * terminal (* vector (indexed consecutively) *) + | E_vector_indexed of terminal * (((terminal * int) * terminal * 'a exp) * terminal) list * terminal (* vector (indexed consecutively) *) | E_vector_access of 'a exp * terminal * 'a exp * terminal (* vector access *) | E_vector_subrange of 'a exp * terminal * 'a exp * terminal * 'a exp * terminal (* subvector extraction *) | E_vector_update of terminal * 'a exp * terminal * 'a exp * terminal * 'a exp * terminal (* vector functional update *) @@ -272,15 +273,8 @@ and 'a letbind = type -naming_scheme_opt_aux = (* Optional variable-naming-scheme specification for variables of defined type *) - Name_sect_none - | Name_sect_some of terminal * terminal * terminal * terminal * string * terminal - - -type -'a tannot_opt_aux = (* Optional type annotation for functions *) - Typ_annot_opt_none - | Typ_annot_opt_some of terminal * terminal +'a funcl_aux = (* Function clause *) + FCL_Funcl of id * 'a pat * terminal * 'a exp type @@ -296,23 +290,30 @@ type type -'a funcl_aux = (* Function clause *) - FCL_Funcl of id * 'a pat * terminal * 'a exp +'a tannot_opt_aux = (* Optional type annotation for functions *) + Typ_annot_opt_none + | Typ_annot_opt_some of terminal * terminal type -naming_scheme_opt = - Name_sect_aux of naming_scheme_opt_aux * l +naming_scheme_opt_aux = (* Optional variable-naming-scheme specification for variables of defined type *) + Name_sect_none + | Name_sect_some of terminal * terminal * terminal * terminal * string * terminal type -index_range_aux = (* index specification, for bitfields in register types *) - 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 *) +'a funcl = + FCL_aux of 'a funcl_aux * 'a annot -and index_range = - BF_aux of index_range_aux * l + +type +rec_opt = + Rec_aux of rec_opt_aux * l + + +type +'a effects_opt = + Effects_opt_aux of 'a effects_opt_aux * 'a annot type @@ -321,18 +322,23 @@ type type -rec_opt = - Rec_aux of rec_opt_aux * l +index_range_aux = (* index specification, for bitfields in register types *) + 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 *) + +and index_range = + BF_aux of index_range_aux * l type -'a effects_opt = - Effects_opt_aux of 'a effects_opt_aux * 'a annot +naming_scheme_opt = + Name_sect_aux of naming_scheme_opt_aux * l type -'a funcl = - FCL_aux of 'a funcl_aux * 'a annot +'a fundef_aux = (* Function definition *) + FD_function of terminal * rec_opt * 'a tannot_opt * 'a effects_opt * ('a funcl * terminal) list type @@ -345,8 +351,9 @@ type type -'a fundef_aux = (* Function definition *) - FD_function of terminal * rec_opt * 'a tannot_opt * 'a effects_opt * ('a funcl * terminal) list +'a default_typing_spec_aux = (* Default kinding or typing assumption *) + DT_kind of terminal * base_kind * id + | DT_typ of terminal * 'a typschm * id type @@ -355,9 +362,8 @@ type type -'a default_typing_spec_aux = (* Default kinding or typing assumption *) - DT_kind of terminal * base_kind * id - | DT_typ of terminal * 'a typschm * id +'a fundef = + FD_aux of 'a fundef_aux * 'a annot type @@ -366,8 +372,8 @@ type type -'a fundef = - FD_aux of 'a fundef_aux * 'a annot +'a default_typing_spec = + DT_aux of 'a default_typing_spec_aux * 'a annot type @@ -376,11 +382,6 @@ type type -'a default_typing_spec = - DT_aux of 'a default_typing_spec_aux * 'a annot - - -type 'a def_aux = (* Top-level definition *) DEF_type of 'a type_def (* type definition *) | DEF_fundef of 'a fundef (* function definition *) @@ -396,6 +397,11 @@ type type +'a def = + DEF_aux of 'a def_aux * 'a annot + + +type 'a 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 $_$ *) @@ -419,8 +425,8 @@ type type -'a def = - DEF_aux of 'a def_aux * 'a annot +'a defs = (* Definition sequence *) + Defs of ('a def) list type @@ -433,9 +439,4 @@ type CT_aux of 'a ctor_def_aux * 'a annot -type -'a defs = (* Definition sequence *) - Defs of ('a def) list - - diff --git a/src/parser.mly b/src/parser.mly index 39537010..7285146c 100644 --- a/src/parser.mly +++ b/src/parser.mly @@ -62,6 +62,7 @@ let kloc k = K_aux(k,loc ()) let tloc t = ATyp_aux(t,loc ()) let lloc l = L_aux(l,loc ()) let ploc p = P_aux(p,(None,loc ())) +let fploc p = FP_aux(p,(None,loc ())) let dloc d = DEF_aux(d,loc ()) @@ -111,9 +112,9 @@ let star = "*" /*Terminals with no content*/ -%token <Ast.terminal> And As Case Clause Const Default Effects End Enum Else False Forall -%token <Ast.terminal> Function_ If_ In IN Let_ Member Nat Order Pure Rec Register Scattered -%token <Ast.terminal> Struct Switch Then True Type TYPE Typedef Union With Val +%token <Ast.terminal> And As Case Clause Const Default Effect Effects End Enum Else False +%token <Ast.terminal> Forall Function_ If_ In IN Let_ Member Nat Order Pure Rec Register +%token <Ast.terminal> Scattered Struct Switch Then True Type TYPE Typedef Union With Val %token <Ast.terminal> AND Div_ EOR Mod OR Quot Rem @@ -217,17 +218,23 @@ effect_list: | effect Comma effect_list { ($1,Some($2))::$3 } +effect_typ: + | Effect id + { tloc (ATyp_efid($1,$2)) } + | Effect Lcurly effect_list Rcurly + { tloc (ATyp_effects($1,$2,$3,$4)) } + | Pure + { tloc (ATyp_effects($1,[],None)) } + atomic_typ: | id - { tloc (Atyp_var (fst $1, snd $1)) } + { tloc (ATyp_var $1) } | Num - { tloc (Atyp_constant(fst $1, snd$1)) } - | Pure - { tloc (Atyp_pure($1)) } + { tloc (ATyp_constant(fst $1, snd$1)) } | Under { tloc (ATyp_wild($1)) } - | Lcurly effect_list Rcurly - { tloc (ATyp_effects($1,$2,$3)) } + | effect_typ + { $1 } | Lparen typ Rparen { $2 } @@ -274,12 +281,8 @@ nexp_typ: typ: | nexp_typ { $1 } - | star_typ MinusGt typ id - { tloc (ATyp_fn($1,$2,$3,(tloc (ATyp_id($4))))) } - | star_typ MinusGt typ Pure - { tloc (ATyp_fn($1,$2,$3,(tloc (ATyp_pure($4))))) } - | star_typ MinusGt typ Lcurly effect_list Rcurly - { tloc (ATyp_fn($1,$2,$3,(tloc (ATyp_effects($4,$5,$6))))) } + | star_typ MinusGt typ effect_typ + { tloc (ATyp_fn($1,$2,$3,$4)) } lit: | True @@ -305,19 +308,21 @@ atomic_pat: | Lparen pat As id Rparen { ploc (P_as($1,$2,$3,$4,$5)) } | Lparen atyp pat Rparen - { ploc (P_typ($1,$2,$3,$4,$5)) } + { ploc (P_typ($1,$2,$3,$4)) } | id { ploc (P_app($1,[])) } - | LtBar fpats BarGt + | Lcurly fpats Rcurly { ploc (P_record($1,fst $2,fst (snd $2),snd (snd $2),$3)) } - | Lsquare semi_pats_atomic Rsquare - { ploc (P_vector($1,fst $2,fst (snd $2),snd (snd $2),$3)) } + | Lsquare coma_pats Rsquare + { ploc (P_vector($1,$2,$3)) } + | Lsquare npats Rsquare + { ploc (P_vector_indexed($1,$2,$3)) } | Lparen comma_pats Rparen { ploc (P_tup($1,$2,$3)) } + | LsquareBar comma_pats BarRsquare + { ploc (P_list($1,$2,$3)) } | Lparen pat Rparen { $2 } - | LsquareBar semi_pats BarRsquare - { ploc (P_list($1,fst $2,fst (snd $2),snd (snd $2),$3)) } atomic_pats: | atomic_pat @@ -331,19 +336,17 @@ app_pat: | id atomic_pats { ploc (P_app($1,$2)) } +pat_colons: + | atomic_pat Colon atomic_pat + { ([($1,$2);($3,None)]) } + | atomic_pat Colon pat_colons + { (($1,$2)::$3) } + pat: | app_pat { $1 } - | app_pat ColonColon pat - { ploc (P_cons($1,fst $2,$3)) } - -semi_pats_atomic: - | atomic_pat - { ([($1,None)], (None,false))} - | atomic_pat Semi - { ([($1,None)], ($2,true)) } - | atomic_pat Semi semi_pats_atomic - { (($1,$2)::fst $3, snd $3) } + | pat_colons + { ploc (P_vector_concat($1)) } semi_pats_help: | pat @@ -367,7 +370,7 @@ comma_pats: fpat: | id Eq pat - { Fpat($1,fst $2,$3,loc ()) } + { fploc (FP_Fpat($1,fst $2,$3)) } fpats: | fpat @@ -377,7 +380,19 @@ fpats: | fpat Semi fpats { (($1,$2)::fst $3, snd $3) } +npat: + | num Eq pat + { ($1,fst $2,$3) } + +npats: + | npat + { ([($1,None)]) } + | npat Comma npats + { (($1,$2)::$3) } + atomic_exp: + | Lcurly semi_exps Rcurly + { eloc (E_block($1,$2,$3)) } | id { eloc (E_id($1)) } | lit @@ -386,213 +401,151 @@ atomic_exp: { $2 } | Lparen atyp Rparen exp { eloc (E_cast($1,$2,$3,$4)) } - | LtBar fexps BarGt - { eloc (Record($1,$2,$3)) } - | LtBar at_exp With fexps BarGt - { eloc (Recup($1,$2,$3,$4,$5)) } - | Lparen exp Colon typ Rparen - { eloc (Typed($1,$2,$3,$4,$5)) } - | BraceBar semi_exps BarBrace - { eloc (Vector($1,fst $2, fst (snd $2), snd (snd $2), $3)) } - | Lsquare semi_exps Rsquare - { eloc (Elist($1,fst $2,fst (snd $2), snd (snd $2), $3)) } | Lparen comma_exps Rparen - { eloc (Tup($1,$2,$3)) } - | Begin_ exp End - { eloc (Begin($1,$2,$3)) } - | Lcurly exp Bar exp Rcurly - { eloc (Setcomp($1,$2,$3,$4,$5)) } - | Lcurly exp Bar Forall quant_bindings Bar exp Rcurly - { eloc (Setcomp_binding($1,$2,$3,$4,$5,$6,$7,$8)) } - | Lcurly semi_exps Rcurly - { eloc (Set($1,fst $2,fst (snd $2), snd (snd $2),$3)) } - | Lsquare exp Bar Forall quant_bindings Bar exp Rsquare - { eloc (Listcomp($1,$2,$3,$4,$5,$6,$7,$8)) } - | Function_ patexps End - { eloc (Function($1,None,false,$2,$3)) } - | Function_ Bar patexps End - { eloc (Function($1,$2,true,$3,$4)) } - | Match exp With patexps End - { eloc (Case($1,$2,$3,None,false,$4,locn 4 4,$5)) } - | Match exp With Bar patexps End - { eloc (Case($1,$2,$3,$4,true,$5,locn 5 5,$6)) } - | Do id do_exps In exp End - { eloc (Do($1,$2,$3,$4,$5,$6)) } + { eloc (E_tup($1,$2,$3)) } + | Lsquare comma_exps Rsquare + { eloc (E_vector($1,$2,$3)) } + | Lsquare num_exps Rsquare + { eloc (E_vector_indexed($1,$2,$3)) } + | Lsquare exp With exp Eq exp Rsquare + { eloc (E_vector_update($1,$2,$3,$4,fst $5,$6,$7)) } + | Lsquare exp With exp Colon exp Eq exp Rsquare + { eloc (E_vector_subrance($1,$2,$3,$4,$5,fst $6,$7,$8)) } + | SquareBar comma_exps BarSquare + { eloc (E_list($1,$2,$3)) } + | Switch exp Lcurly case_exps Rcurly + { eloc (E_case($1,$2,$3,$4,$5)) } field_exp: | atomic_exp { $1 } | atomic_exp Dot id - { eloc (Field($1,$2,$3)) } - | atomic_exp DotBrace nexp Rsquare - { eloc (VAccess($1,$2,$3,$4)) } - | atomic_exp DotBrace nexp Dot Dot nexp Rsquare - { eloc (VAccessR($1,$2,$3,$4,$6,$7)) } - | id DotBrace nexp Rsquare - { eloc (VAccess((eloc (Ident ($1))),$2,$3,$4)) } - | id DotBrace nexp Dot Dot nexp Rsquare - { eloc (VAccessR((eloc (Ident ($1))),$2,$3,$4,$6,$7)) } - | id - { eloc (Ident($1)) } + { eloc (E_field($1,$2,$3)) } + | atomic_exp Lsquare exp Rsquare + { eloc (E_vector_access($1,$2,$3,$4)) } + | atomic_exp Lsquare exp DotDot exp Rsquare + { eloc (E_vector_subrange($1,$2,$3,$4,$5,$6)) } app_exp: | field_exp { $1 } | app_exp field_exp - { eloc (App($1,$2)) } + { eloc (E_app($1,[$2])) } right_atomic_exp: - | Forall quant_bindings Dot exp - { eloc (Quant(Q_forall($1), $2,$3,$4)) } - | Exists quant_bindings Dot exp - { eloc (Quant(Q_exists($1), $2,$3,$4)) } | If_ exp Then exp Else exp - { eloc (If($1,$2,$3,$4,$5,$6)) } - | Fun_ patsexp - { eloc (Fun($1,$2)) } + { eloc (E_if($1,$2,$3,$4,$5,$6)) } | Let_ letbind In exp - { eloc (Let($1,$2,$3,$4)) } - -starstar_exp: - | app_exp - { $1 } - | app_exp StarstarX starstar_exp - { eloc (Infix($1, SymX_l($2, locn 2 2), $3)) } - -starstar_right_atomic_exp: - | right_atomic_exp - { $1 } - | app_exp StarstarX starstar_right_atomic_exp - { eloc (Infix($1, SymX_l($2, locn 2 2), $3)) } + { eloc (E_let($1,$2,$3,$4)) } star_exp: | starstar_exp { $1 } | star_exp Star starstar_exp - { eloc (Infix($1,SymX_l($2, locn 2 2), $3)) } + { eloc (E_app_infix($1,SymX_l($2, locn 2 2), $3)) } | star_exp StarX starstar_exp - { eloc (Infix($1,SymX_l($2, locn 2 2), $3)) } + { eloc (E_app_infix($1,SymX_l($2, locn 2 2), $3)) } star_right_atomic_exp: | starstar_right_atomic_exp { $1 } | star_exp Star starstar_right_atomic_exp - { eloc (Infix($1,SymX_l($2, locn 2 2), $3)) } + { eloc (E_app_infix($1,SymX_l($2, locn 2 2), $3)) } | star_exp StarX starstar_right_atomic_exp - { eloc (Infix($1,SymX_l($2, locn 2 2), $3)) } + { eloc (E_app_infix($1,SymX_l($2, locn 2 2), $3)) } plus_exp: | star_exp { $1 } | plus_exp Plus star_exp - { eloc (Infix($1,SymX_l($2, locn 2 2), $3)) } + { eloc (E_app_infix($1,SymX_l($2, locn 2 2), $3)) } | plus_exp PlusX star_exp - { eloc (Infix($1,SymX_l($2, locn 2 2), $3)) } + { eloc (E_app_infix($1,SymX_l($2, locn 2 2), $3)) } plus_right_atomic_exp: | star_right_atomic_exp { $1 } | plus_exp Plus star_right_atomic_exp - { eloc (Infix($1,SymX_l($2, locn 2 2), $3)) } + { eloc (E_app_infix($1,SymX_l($2, locn 2 2), $3)) } | plus_exp PlusX star_right_atomic_exp - { eloc (Infix($1,SymX_l($2, locn 2 2), $3)) } + { eloc (E_app_infix($1,SymX_l($2, locn 2 2), $3)) } cons_exp: | plus_exp { $1 } | plus_exp ColonColon cons_exp - { eloc (Cons($1,fst $2,$3)) } + { eloc (E_cons($1,fst $2,$3)) } cons_right_atomic_exp: | plus_right_atomic_exp { $1 } | plus_exp ColonColon cons_right_atomic_exp - { eloc (Cons($1,fst $2,$3)) } + { eloc (E_cons($1,fst $2,$3)) } at_exp: | cons_exp { $1 } | cons_exp At at_exp - { eloc (Infix($1,SymX_l($2, locn 2 2), $3)) } + { eloc (E_app_infix($1,SymX_l($2, locn 2 2), $3)) } | cons_exp AtX at_exp - { eloc (Infix($1,SymX_l($2, locn 2 2), $3)) } + { eloc (E_app_infix($1,SymX_l($2, locn 2 2), $3)) } at_right_atomic_exp: | cons_right_atomic_exp { $1 } | cons_exp At at_right_atomic_exp - { eloc (Infix($1,SymX_l($2, locn 2 2), $3)) } + { eloc (E_app_infix($1,SymX_l($2, locn 2 2), $3)) } | cons_exp AtX at_right_atomic_exp - { eloc (Infix($1,SymX_l($2, locn 2 2), $3)) } + { eloc (E_app_infix($1,SymX_l($2, locn 2 2), $3)) } eq_exp: | at_exp { $1 } | eq_exp Eq at_exp - { eloc (Infix($1,SymX_l($2, locn 2 2), $3)) } - | eq_exp EqualX at_exp - { eloc (Infix($1,SymX_l($2, locn 2 2), $3)) } + { eloc (E_app_infix($1,SymX_l($2, locn 2 2), $3)) } | eq_exp GtEq at_exp - { eloc (Infix ($1,SymX_l($2, locn 2 2), $3)) } + { eloc (E_app_infix ($1,SymX_l($2, locn 2 2), $3)) } | eq_exp GtEqX at_exp - { eloc (Infix ($1,SymX_l($2, locn 2 2), $3)) } + { eloc (E_app_infix ($1,SymX_l($2, locn 2 2), $3)) } | eq_exp IN at_exp - { eloc (Infix($1,SymX_l($2, locn 2 2), $3)) } - | eq_exp MEM at_exp - { eloc (Infix($1,SymX_l($2, locn 2 2), $3)) } + { eloc (E_app_infix($1,SymX_l($2, locn 2 2), $3)) } + | eq_exp ColonEq at_exp + { eloc (E_assign($1,$2,$3)) } eq_right_atomic_exp: | at_right_atomic_exp { $1 } | eq_exp Eq at_right_atomic_exp - { eloc (Infix($1,SymX_l($2, locn 2 2), $3)) } - | eq_exp EqualX at_right_atomic_exp - { eloc (Infix($1,SymX_l($2, locn 2 2), $3)) } - | eq_exp IN at_right_atomic_exp - { eloc (Infix($1,SymX_l($2, locn 2 2), $3)) } - | eq_exp MEM at_right_atomic_exp - { eloc (Infix($1,SymX_l($2, locn 2 2), $3)) } + { eloc (E_app_infix($1,SymX_l($2, locn 2 2), $3)) } and_exp: | eq_exp { $1 } | eq_exp AmpAmp and_exp - { eloc (Infix($1,SymX_l($2, locn 2 2), $3)) } + { eloc (E_app_infix($1,SymX_l($2, locn 2 2), $3)) } and_right_atomic_exp: | eq_right_atomic_exp { $1 } | eq_exp AmpAmp and_right_atomic_exp - { eloc (Infix($1,SymX_l($2, locn 2 2), $3)) } + { eloc (E_app_infix($1,SymX_l($2, locn 2 2), $3)) } or_exp: | and_exp { $1 } | and_exp BarBar or_exp - { eloc (Infix($1,SymX_l($2, locn 2 2), $3)) } + { eloc (E_app_infix($1,SymX_l($2, locn 2 2), $3)) } or_right_atomic_exp: | and_right_atomic_exp { $1 } | and_exp BarBar or_right_atomic_exp - { eloc (Infix($1,SymX_l($2, locn 2 2), $3)) } - -imp_exp: - | or_exp - { $1 } - | or_exp MinusMinusGt imp_exp - { eloc (Infix($1,SymX_l($2, locn 2 2), $3)) } - -imp_right_atomic_exp: - | or_right_atomic_exp - { $1 } - | or_exp MinusMinusGt imp_right_atomic_exp - { eloc (Infix($1,SymX_l($2, locn 2 2), $3)) } + { eloc (E_app_infix($1,SymX_l($2, locn 2 2), $3)) } exp: - | imp_right_atomic_exp + | or_right_atomic_exp { $1 } - | imp_exp + | or_exp { $1 } comma_exps: @@ -615,20 +568,6 @@ semi_exps: | semi_exps_help { $1 } -quant_bindings: - | x - { [Qb_var($1)] } - | Lparen pat IN exp Rparen - { [Qb_restr($1,$2,fst $3,$4,$5)] } - | Lparen pat MEM exp Rparen - { [Qb_list_restr($1,$2,fst $3,$4,$5)] } - | x quant_bindings - { Qb_var($1)::$2 } - | Lparen pat IN exp Rparen quant_bindings - { Qb_restr($1,$2,fst $3,$4,$5)::$6 } - | Lparen pat MEM exp Rparen quant_bindings - { Qb_list_restr($1,$2,fst $3,$4,$5)::$6 } - patsexp: | atomic_pats1 Arrow exp { Patsexp($1,$2,$3,loc ()) } @@ -675,12 +614,6 @@ letbind: | None -> lbloc (Let_val($1,$2,fst $3,$4)) } -do_exps: - | - { [] } - | pat LeftArrow exp Semi do_exps - { ($1,$2,$3,$4)::$5 } - funcl: | x atomic_pats1 opt_typ_annot Eq exp { reclloc (Funcl($1,$2,$3,fst $4,$5)) } @@ -691,106 +624,12 @@ funcls: | funcl And funcls { ($1,$2)::$3 } -xs: - | - { [] } - | x xs - { $1::$2 } - exps: | { [] } | field_exp exps { $1::$2 } -x_opt: - | - { X_l_none } - | x Colon - { X_l_some ($1, $2) } - -indreln_clause: - | x_opt Forall xs Dot exp EqEqGt x exps - { irloc (Rule($1,$2,$3,$4,$5,$6,$7,$8)) } - - -and_indreln_clauses: - | indreln_clause - { [($1,None)] } - | indreln_clause And and_indreln_clauses - { ($1,$2)::$3 } - -tnvs: - | - { [] } - | tnvar tnvs - { $1::$2 } - -c: - | id tnvar - { C($1,$2) } - -cs: - | c - { [($1,None)] } - | c Comma cs - { ($1,$2)::$3 } - -c2: - | id typ - { - match $2 with - | Typ_l(Typ_var(a_l),_) -> - C($1,Avl(a_l)) - | _ -> - raise (Parse_error_locn(loc (),"Invalid class constraint")) - } - -cs2: - | c2 - { [($1, None)] } - | c2 Comma cs2 - { ($1,$2)::$3 } - -range: - | nexp Eq nexp - { Range_l(Fixed($1,(fst $2),$3), loc () ) } - | nexp GtEq nexp - { Range_l(Bounded($1,(fst $2),$3), loc () ) } - -ranges: - | range - { [($1,None)] } - | range Comma ranges - { ($1,$2)::$3 } - -typschm: - | typ - { Ts(C_pre_empty, $1) } - | Forall tnvs Dot typ - { Ts(C_pre_forall($1,$2,$3,Cs_empty),$4) } - | Forall tnvs Dot cs EqGt typ - { Ts(C_pre_forall($1,$2,$3,Cs_classes($4,$5)), $6) } - | Forall tnvs Dot ranges EqGt typ - { Ts(C_pre_forall($1,$2,$3,Cs_lengths($4,$5)), $6) } - | Forall tnvs Dot cs Semi ranges EqGt typ - { Ts(C_pre_forall($1,$2,$3,Cs_both($4,$5,$6,$7)),$8) } - - -insttyp: - | typ - { $1 } - | nexp - { tloc (Typ_Nexps($1)) } - -instschm: - | Lparen id insttyp Rparen - { Is(C_pre_empty, $1,$2,$3,$4) } - | Forall tnvs Dot Lparen id insttyp Rparen - { Is(C_pre_forall($1,$2,$3,Cs_empty),$4,$5,$6,$7) } - | Forall tnvs Dot cs2 EqGt Lparen id insttyp Rparen - { Is(C_pre_forall($1,$2,$3,Cs_classes($4,$5)),$6,$7,$8,$9) } - val_spec: | Val x Colon typschm { Val_spec($1,$2,$3,$4) } @@ -805,34 +644,6 @@ class_val_specs: | class_val_spec class_val_specs { ((fun (a,b,c,d) -> (a,b,c,d,loc())) $1)::$2 } -targets: - | X - { [(get_target $1,None)] } - | X Semi targets - { (get_target $1, $2)::$3 } - -targets_opt: - | - { None } - | Lcurly Rcurly - { Some(Targets_concrete($1,[],$2)) } - | Lcurly targets Rcurly - { Some(Targets_concrete($1,$2,$3)) } - -lemma_typ: - | Lemma - { Lemma_lemma $1 } - | Theorem - { Lemma_theorem $1 } - | Assert - { Lemma_assert $1 } - -lemma: - | lemma_typ targets_opt Lparen exp Rparen - { Lemma_unnamed ($1, $2, $3, $4, $5) } - | lemma_typ targets_opt x Colon Lparen exp Rparen - { Lemma_named ($1, $2, $3, $4, $5, $6, $7) } - val_def: | Let_ targets_opt letbind { Let_def($1,$2,$3) } @@ -847,36 +658,6 @@ val_defs: | val_def val_defs { ($1,loc ())::$2 } - - -xtyp: - | x Colon typ - { ($1,$2,$3) } - -xtyps: - | xtyp - { ([($1,None)], (None, false)) } - | xtyp Semi - { ([($1,None)], ($2, true)) } - | xtyp Semi xtyps - { (($1,$2)::fst $3, snd $3) } - -ctor_texp: - | x Of star_typ_list - { Cte($1,$2,$3) } - | x - { Cte($1,None,[]) } - -ctor_single_texp: - | x Of star_typ_list - { Cte($1,$2,$3) } - -ctor_texps: - | ctor_texp - { [($1,None)] } - | ctor_texp Bar ctor_texps - { ($1,$2)::$3 } - texp: | typ { Te_abbrev($1) } @@ -889,26 +670,63 @@ texp: | ctor_single_texp { Te_variant(None,false,[($1,None)]) } -name_sect: - | Lsquare id Eq String Rsquare - { Name_sect_some($1,$2,fst $3,(fst $4),(snd $4),$5) } +kinded_id: + | id + { } + | kind id + { } + | Lparen kinded_id Rparen + { } + +kinded_ids: + | kinded_id + { [$1] } + | kinded_id kinded_ids + { $1::$2 } + +nums: + | num + { [($1,None)] } + | num Comma nums + { ($1,$2)::$3 } + +nexp_constraint: + | atyp Eq atyp + { NC_aux(NC_fixed($1,(fst $2),$3), loc () ) } + | atyp GtEq atyp + { NC_aux(NC_bounded_ge($1,(fst $2),$3), loc () ) } + | atyp LtEq atyp + { NC_aux(NC_bounded_le($1,(fst $2),$3), loc () ) } + | id IN Lcurly nums Rcurly + { NC_aux(NC_nat_set_bounded($1,$2,$3,$4,$5)) } + -td: - | x tnvs - { Td_opaque($1,$2,Name_sect_none) } - | x tnvs name_sect - { Td_opaque($1,$2,$3) } - | x tnvs Eq texp - { Td($1,$2,Name_sect_none,fst $3,$4) } - | x tnvs name_sect Eq texp - { Td($1,$2,$3,fst $4,$5) } - -tds: - | td + +ranges: + | range { [($1,None)] } - | td And tds + | range Comma ranges { ($1,$2)::$3 } + +typquant: + | Forall kinded_ids Dot nexp_constraints Dot + {} + | Forall kinded_ids Dot + {} + | + {} + +name_sect: + | Lsquare id Eq String Rsquare + { Name_sect_some($1,$2,fst $3,(fst $4),(snd $4),$5) } + +type_def: + | Typedef id name_sect Eq typschm + | Typedef id name_sect Eq Const Struct typquant Lcurly c_def_body Rcurly + | Typedef id name_sect Eq Const Union typquant Lcurly c_def_body Rcurly + | Typedef id Eq register bits Lsquare typ Colon typ Rsquare Lcurly r_def_body Rcurly + scattered_def: | Function_ Rec tannot_opt effects_opt id { (DEF_scattered_function(None,$1,(Rec_rec ($2)),$3,$4,$5)) } |