diff options
| -rw-r--r-- | language/l2.ott | 99 | ||||
| -rw-r--r-- | src/ast.ml | 410 | ||||
| -rw-r--r-- | src/parser.mly | 6 |
3 files changed, 247 insertions, 268 deletions
diff --git a/language/l2.ott b/language/l2.ott index 1cc9b3fd..6051051a 100644 --- a/language/l2.ott +++ b/language/l2.ott @@ -49,30 +49,26 @@ metavar regexp ::= embed {{ ocaml +type text = Ulib.Text.t - -type text = string (* was Ulib.Text.t *) - -type 'a l = 'a -(* +type l = | Unknown | Trans of string * l option | Range of Lexing.position * Lexing.position -*) -exception Parse_error_locn of string l * string + +exception Parse_error_locn of l * string type ml_comment = - | Chars of text + | Chars of Ulib.Text.t | Comment of ml_comment list type lex_skip = | Com of ml_comment - | Ws of text + | Ws of Ulib.Text.t | Nl type lex_skips = lex_skip list option -(* let pp_lex_skips ppf sk = match sk with | None -> () @@ -93,7 +89,7 @@ let combine_lex_skips s1 s2 = | (None,_) -> s2 | (_,None) -> s1 | (Some(s1),Some(s2)) -> Some(s2@s1) -*) + type terminal = lex_skips }} @@ -160,9 +156,9 @@ metavar ix ::= grammar l :: '' ::= {{ phantom }} - {{ ocaml 'a l }} + {{ ocaml l }} {{ lem l }} - {{ hol unit }} + {{ hol unit }} {{ com Source location }} | :: :: Unknown {{ ocaml Unknown }} @@ -171,7 +167,7 @@ l :: '' ::= {{ phantom }} id :: '' ::= {{ com Identifier }} - {{ aux _ l }} {{ auxparam 'a }} + {{ aux _ l }} | x :: :: id | ( x ) :: :: deIid {{ com remove infix status }} % Note: we have just a single namespace. We don't want the same @@ -228,7 +224,7 @@ grammar % a :: 'A_' ::= -% {{ aux _ l }} {{ auxparam 'a }} +% {{ aux _ l }} % {{ ocaml terminal * text }} % {{ lem terminal * string }} % {{ hol string }} @@ -237,7 +233,7 @@ grammar % {{ ichlo [[x]] }} % % N :: 'N_' ::= -% {{ aux _ l }} {{ auxparam 'a }} +% {{ aux _ l }} % {{ ocaml terminal * text }} % {{ lem terminal * string }} % {{ hol string }} @@ -246,7 +242,7 @@ grammar % {{ ichlo [[x]] }} % % EN :: 'EN_' ::= -% {{ aux _ l }} {{ auxparam 'a }} +% {{ aux _ l }} % {{ ocaml terminal * text }} % {{ lem terminal * string }} % {{ hol string }} @@ -255,7 +251,7 @@ grammar % {{ ichlo [[x]] }} % % EFF :: 'EFF_' ::= -% {{ aux _ l }} {{ auxparam 'a }} +% {{ aux _ l }} % {{ ocaml terminal * text }} % {{ lem terminal * string }} % {{ hol string }} @@ -296,7 +292,7 @@ grammar base_kind :: 'BK_' ::= {{ com base kind}} - {{ aux _ l }} {{ auxparam 'a }} + {{ aux _ l }} | Type :: :: type {{ com kind of types }} | Nat :: :: nat {{ com kind of natural number size expressions }} | Order :: :: order {{ com kind of vector order specifications }} @@ -304,14 +300,14 @@ base_kind :: 'BK_' ::= kind :: 'K_' ::= {{ com kinds}} - {{ aux _ l }} {{ auxparam 'a }} + {{ aux _ l }} | base_kind1 -> ... -> base_kindn :: :: kind % we'll never use ...-> Nat nexp :: 'Nexp_' ::= {{ com expression of kind $[[Nat]]$, for vector sizes and origins }} - {{ aux _ l }} {{ auxparam 'a }} + {{ aux _ l }} | id :: :: id {{ com identifier }} | num :: :: constant {{ com constant }} | nexp1 * nexp2 :: :: times {{ com product }} @@ -322,7 +318,7 @@ nexp :: 'Nexp_' ::= order :: 'Ord_' ::= {{ com vector order specifications, of kind $[[Order]]$}} - {{ aux _ l }} {{ auxparam 'a }} + {{ aux _ l }} | id :: :: id {{ com identifier }} | inc :: :: inc {{ com increasing (little-endian) }} | dec :: :: dec {{ com decreasing (big-endian) }} @@ -330,7 +326,7 @@ order :: 'Ord_' ::= effect :: 'Effect_' ::= {{ com effect }} - {{ aux _ l }} {{ auxparam 'a }} + {{ aux _ l }} | rreg :: :: rreg {{ com read register }} | wreg :: :: wreg {{ com write register }} | rmem :: :: rmem {{ com read memory }} @@ -342,7 +338,7 @@ effect :: 'Effect_' ::= effects :: 'Effects_' ::= {{ com effect set, of kind $[[Effects]]$ }} - {{ aux _ l }} {{ auxparam 'a }} + {{ aux _ l }} | id :: :: var | { effect1 , .. , effectn } :: :: set {{ com effect set }} | pure :: M :: pure {{ com sugar for empty effect set }} {{ icho [] }} @@ -351,7 +347,7 @@ effects :: 'Effects_' ::= typ :: 'Typ_' ::= - {{ com Type expressions, of kind $[[Type]]$ }} {{ aux _ l }} {{ auxparam 'a }} + {{ com Type expressions, of kind $[[Type]]$ }} | _ :: :: wild {{ com Unspecified type }} | id :: :: var @@ -368,7 +364,7 @@ typ :: 'Typ_' ::= | ( typ ) :: S :: paren {{ icho [[typ]] }} typ_arg :: 'Typ_arg_' ::= - {{ com Type constructor arguments of all kinds }} {{ aux _ l}} + {{ com Type constructor arguments of all kinds }} | nexp :: :: nexp | typ :: :: typ | order :: :: order @@ -378,7 +374,7 @@ typ_arg :: 'Typ_arg_' ::= typ_lib :: 'Typ_lib_' ::= {{ com library types and syntactic sugar for them }} - {{ aux _ l }} {{ auxparam 'a }} + {{ aux _ l }} % boring base types: | unit :: :: unit {{ com unit type with value $()$ }} | bool :: :: bool {{ com booleans $[[true]]$ and $[[false]]$ }} @@ -417,7 +413,7 @@ grammar nexp_constraint :: 'NC_' ::= {{ com constraint over kind $[[Nat]]$ }} - {{ aux _ l }} {{ auxparam 'a }} + {{ aux _ l }} | nexp = nexp' :: :: fixed | nexp >= nexp' :: :: bounded_ge | nexp '<=' nexp' :: :: bounded_le @@ -427,13 +423,13 @@ nexp_constraint :: 'NC_' ::= % finite-set-bound, as we don't think we need anything more kinded_id :: 'KOpt_' ::= - {{ com optionally kind-annotated identifier }} {{ aux _ l }} {{ auxparam 'a }} + {{ com optionally kind-annotated identifier }} | id :: :: none {{ com identifier }} | kind id :: :: kind {{ com kind-annotated variable }} | ( kinded_id ) :: S :: paren {{ icho [[kinded_id]] }} typquant :: 'TypQ_' ::= - {{ aux _ l }} {{ auxparam 'a }} {{ com type quantifiers and constraints}} + {{ aux _ l }} {{ com type quantifiers and constraints}} | forall kinded_id1 ... kinded_idn . nexp_constraint1 , ... , nexp_constrainti . :: :: tq {{ texlong }} % WHY ARE CONSTRAINTS HERE AND NOT IN THE KIND LANGUAGE @@ -443,7 +439,7 @@ typquant :: 'TypQ_' ::= typschm :: 'TypSchm_' ::= {{ com type scheme }} - {{ aux _ l }} {{ auxparam 'a }} + {{ aux _ l }} | typquant typ :: :: ts @@ -563,7 +559,7 @@ semi_opt {{ tex \ottnt{;}^{?} }} :: 'semi_' ::= {{ phantom }} pat :: 'P_' ::= {{ com Pattern }} - {{ aux _ l }} {{ auxparam 'a }} + {{ aux _ l }} | lit :: :: lit {{ com literal constant pattern }} | _ :: :: wild @@ -618,7 +614,7 @@ pat :: 'P_' ::= fpat :: 'FP_' ::= {{ com Field pattern }} - {{ aux _ l }} {{ auxparam 'a }} + {{ aux _ l }} | id = pat :: :: Fpat parsing @@ -635,7 +631,7 @@ grammar exp :: 'E_' ::= {{ com Expression }} - {{ aux _ l }} {{ auxparam 'a }} + {{ aux _ l }} | { exp1 ; ... ; expn } :: :: block {{ com block (parsing conflict with structs?) }} % maybe we really should have indentation-sensitive syntax :-) (given that some of the targets do) @@ -750,23 +746,23 @@ lexp :: 'LEXP_' ::= {{ com lvalue expression }} fexp :: 'FE_' ::= {{ com Field-expression }} - {{ aux _ l }} {{ auxparam 'a }} + {{ aux _ l }} | id = exp :: :: Fexp fexps :: 'FES_' ::= {{ com Field-expression list }} - {{ aux _ l }} {{ auxparam 'a }} + {{ aux _ l }} | fexp1 ; ... ; fexpn semi_opt :: :: Fexps pexp :: 'Pat_' ::= {{ com Pattern match }} - {{ aux _ l }} {{ auxparam 'a }} + {{ aux _ l }} | pat -> exp :: :: exp % apparently could use -> or => for this. %% % psexp :: 'Pats' ::= %% % {{ com Multi-pattern matches }} -%% % {{ aux _ l }} {{ auxparam 'a }} +%% % {{ aux _ l }} %% % | pat1 ... patn -> exp :: :: exp @@ -807,12 +803,12 @@ grammar %% % %% % lem_funcl :: 'LEM_FCL' ::= %% % {{ com Function clauses }} -%% % {{ aux _ l }} {{ auxparam 'a }} +%% % {{ aux _ l }} %% % | id pat1 ... patn tannot_opt = exp :: :: Funcl %% % %% % lem_letbind :: 'LEM_LB_' ::= %% % {{ com Let bindings }} -%% % {{ aux _ l }} {{ auxparam 'a }} +%% % {{ aux _ l }} %% % | pat tannot_opt = exp :: :: Let_val %% % {{ com Value bindings }} %% % | lem_funcl :: :: Let_fun @@ -822,7 +818,7 @@ grammar %% % grammar %% % lem_val_def :: 'LEM_VD' ::= %% % {{ com Value definitions }} -%% % {{ aux _ l }} {{ auxparam 'a }} +%% % {{ aux _ l }} %% % | let lem_letbind :: :: Let_def %% % {{ com Non-recursive value definitions }} %% % | let rec lem_funcl1 and ... and lem_funcln :: :: Let_rec @@ -830,7 +826,7 @@ grammar %% % %% % lem_val_spec :: 'LEM_VS' ::= %% % {{ com Value type specifications }} -%% % {{ aux _ l }} {{ auxparam 'a }} +%% % {{ aux _ l }} %% % | val x_l : typschm :: :: Val_spec %%%%% C-ish style %%%%%%%%%% @@ -841,24 +837,25 @@ tannot_opt :: 'Typ_annot_opt_' ::= | typ_quant typ :: :: some rec_opt :: 'Rec_' ::= - {{ aux _ l }} {{ auxparam 'a }} {{ com Optional recursive annotation for functions }} +% {{ aux _ l }} + {{ com Optional recursive annotation for functions }} | :: :: nonrec {{ com non-recursive }} | rec :: :: rec {{ com recursive }} effects_opt :: 'Effects_opt_' ::= - {{ aux _ l }} {{ auxparam 'a }} {{ com Optional effect annotation for functions }} + {{ aux _ l }} {{ com Optional effect annotation for functions }} | :: :: pure {{ com sugar for empty effect set }} | effects :: :: effects funcl :: 'FCL_' ::= {{ com Function clause }} - {{ aux _ l }} {{ auxparam 'a }} + {{ aux _ l }} | id pat = exp :: :: Funcl fundef :: 'FD_' ::= {{ com Function definition}} - {{ aux _ l }} {{ auxparam 'a }} + {{ aux _ l }} | 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 @@ -870,7 +867,7 @@ fundef :: 'FD_' ::= letbind :: 'LB_' ::= {{ com Let binding }} - {{ aux _ l }} {{ auxparam 'a }} + {{ aux _ l }} | typschm pat = exp :: :: val_explicit {{ com value binding, explicit type ([[pat]] must be total)}} | let pat = exp :: :: val_implicit @@ -879,12 +876,12 @@ letbind :: 'LB_' ::= val_spec :: 'VS_' ::= {{ com Value type specification }} - {{ aux _ l }} {{ auxparam 'a }} + {{ aux _ l }} | val typschm id :: :: val_spec default_typing_spec :: 'DT_' ::= {{ com Default kinding or typing assumption }} - {{ aux _ l }} {{ auxparam 'a }} + {{ aux _ l }} | default base_kind id :: :: kind | default typschm id :: :: typ % The intended semantics of these is that if an id in binding position @@ -900,7 +897,7 @@ default_typing_spec :: 'DT_' ::= def :: 'DEF_' ::= {{ com Top-level definition }} - {{ aux _ l }} {{ auxparam 'a }} + {{ aux _ l }} | type_def :: :: type {{ com type definition }} | fundef :: :: fundef @@ -927,7 +924,7 @@ def :: 'DEF_' ::= defs :: '' ::= {{ com Definition sequence }} -% {{ aux _ l }} {{ auxparam 'a }} +% {{ aux _ l }} | def1 .. defn :: :: Defs @@ -1,30 +1,26 @@ -(* generated by Ott 0.22 from: l2.ott *) +(* generated by Ott 0.21.2 from: l2.ott *) +type text = Ulib.Text.t - -type text = string (* was Ulib.Text.t *) - -type 'a l = 'a -(* +type l = | Unknown | Trans of string * l option | Range of Lexing.position * Lexing.position -*) -exception Parse_error_locn of string l * string + +exception Parse_error_locn of l * string type ml_comment = - | Chars of text + | Chars of Ulib.Text.t | Comment of ml_comment list type lex_skip = | Com of ml_comment - | Ws of text + | Ws of Ulib.Text.t | Nl type lex_skips = lex_skip list option -(* let pp_lex_skips ppf sk = match sk with | None -> () @@ -45,7 +41,7 @@ let combine_lex_skips s1 s2 = | (None,_) -> s2 | (_,None) -> s1 | (Some(s1),Some(s2)) -> Some(s2@s1) -*) + type terminal = lex_skips @@ -53,7 +49,7 @@ type x = terminal * text (* identifier *) type ix = terminal * text (* infix identifier *) type -'a base_kind_aux = (* base kind *) +base_kind_aux = (* base kind *) BK_type of terminal (* kind of types *) | BK_nat of terminal (* kind of natural number size expressions *) | BK_order of terminal (* kind of vector order specifications *) @@ -61,28 +57,40 @@ type type -'a id_aux = (* Identifier *) +id_aux = (* Identifier *) Id of x | DeIid of terminal * x * terminal (* remove infix status *) type -'a base_kind = - BK_aux of 'a base_kind_aux * 'a l +base_kind = + BK_aux of base_kind_aux * l type -'a id = - Id_aux of 'a id_aux * 'a l +id = + Id_aux of id_aux * l type -'a kind_aux = (* kinds *) - K_kind of ('a base_kind * terminal) list +kind_aux = (* kinds *) + K_kind of (base_kind * terminal) list + + +type +nexp_aux = (* expression of kind $_$, 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 type -'a effect_aux = (* effect *) +effect_aux = (* effect *) Effect_rreg of terminal (* read register *) | Effect_wreg of terminal (* write register *) | Effect_rmem of terminal (* read memory *) @@ -93,110 +101,87 @@ type type -'a nexp_aux = (* expression of kind $_$, for vector sizes and origins *) - Nexp_id of 'a id (* identifier *) - | Nexp_constant of terminal * int (* constant *) - | Nexp_times of 'a nexp * terminal * 'a nexp (* product *) - | Nexp_sum of 'a nexp * terminal * 'a nexp (* sum *) - | Nexp_exp of terminal * terminal * 'a nexp (* exponential *) - -and 'a nexp = - Nexp_aux of 'a nexp_aux * 'a l +kind = + K_aux of kind_aux * l type -'a kind = - K_aux of 'a kind_aux * 'a l +nexp_constraint_aux = (* constraint over kind $_$ *) + 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 -'a effect = - Effect_aux of 'a effect_aux * 'a l +effect = + Effect_aux of effect_aux * l type -'a nexp_constraint_aux = (* constraint over kind $_$ *) - NC_fixed of 'a nexp * terminal * 'a nexp - | NC_bounded_ge of 'a nexp * terminal * 'a nexp - | NC_bounded_le of 'a nexp * terminal * 'a nexp - | NC_nat_set_bounded of 'a id * terminal * terminal * (terminal * int * terminal) list * terminal +kinded_id = (* optionally kind-annotated identifier *) + KOpt_none of id (* identifier *) + | KOpt_kind of kind * id (* kind-annotated variable *) type -'a kinded_id_aux = (* optionally kind-annotated identifier *) - KOpt_none of 'a id (* identifier *) - | KOpt_kind of 'a kind * 'a id (* kind-annotated variable *) +nexp_constraint = + NC_aux of nexp_constraint_aux * l type -'a order_aux = (* vector order specifications, of kind $_$ *) - Ord_id of 'a id (* identifier *) +order_aux = (* vector order specifications, of kind $_$ *) + Ord_id of id (* identifier *) | Ord_inc of terminal (* increasing (little-endian) *) | Ord_dec of terminal (* decreasing (big-endian) *) type -'a effects_aux = (* effect set, of kind $_$ *) - Effects_var of 'a id - | Effects_set of terminal * ('a effect * terminal) list * terminal (* effect set *) - - -type -'a nexp_constraint = - NC_aux of 'a nexp_constraint_aux * 'a l +effects_aux = (* effect set, of kind $_$ *) + Effects_var of id + | Effects_set of terminal * (effect * terminal) list * terminal (* effect set *) type -'a kinded_id = - KOpt_aux of 'a kinded_id_aux * 'a l +typquant_aux = (* type quantifiers and constraints *) + TypQ_tq of terminal * (kinded_id) list * terminal * (nexp_constraint * terminal) list * terminal + | TypQ_no_constraint of terminal * (kinded_id) list * terminal (* sugar, omitting constraints *) + | TypQ_no_forall (* sugar, omitting quantifier and constraints *) type -'a order = - Ord_aux of 'a order_aux * 'a l +order = + Ord_aux of order_aux * l type -'a effects = - Effects_aux of 'a effects_aux * 'a l +effects = + Effects_aux of effects_aux * l type -'a typquant_aux = (* type quantifiers and constraints *) - TypQ_tq of terminal * ('a kinded_id) list * terminal * ('a nexp_constraint * terminal) list * terminal - | TypQ_no_constraint of terminal * ('a kinded_id) list * terminal (* sugar, omitting constraints *) - | TypQ_no_forall (* sugar, omitting quantifier and constraints *) +typquant = + TypQ_aux of typquant_aux * l type -'a typ_aux = (* Type expressions, of kind $_$ *) +typ = (* Type expressions, of kind $_$ *) Typ_wild of terminal (* Unspecified type *) - | Typ_var of 'a id (* Type variable *) - | Typ_fn of 'a typ * terminal * 'a typ * 'a effects (* Function type (first-order only in user code) *) - | Typ_tup of ('a typ * terminal) list (* Tuple type *) - | Typ_app of 'a id * (typ_arg) list (* type constructor application *) - -and 'a typ = - Typ_aux of 'a typ_aux * 'a l + | 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_aux = (* Type constructor arguments of all kinds *) - Typ_arg_nexp of 'a nexp - | Typ_arg_typ of 'a typ - | Typ_arg_order of 'a order - | Typ_arg_effects of 'a effects - -and typ_arg = - Typ_arg_aux of typ_arg_aux * 'a l +and typ_arg = (* Type constructor arguments of all kinds *) + Typ_arg_nexp of nexp + | Typ_arg_typ of typ + | Typ_arg_order of order + | Typ_arg_effects of effects type -'a typquant = - TypQ_aux of 'a typquant_aux * 'a l - - -type -'a typschm_aux = (* type scheme *) - TypSchm_ts of 'a typquant * 'a typ +typschm_aux = (* type scheme *) + TypSchm_ts of typquant * typ type @@ -213,131 +198,131 @@ lit = (* Literal constant *) type -'a typschm = - TypSchm_aux of 'a typschm_aux * 'a l +typschm = + TypSchm_aux of typschm_aux * l type -'a pat_aux = (* Pattern *) +pat_aux = (* Pattern *) P_lit of lit (* literal constant pattern *) | P_wild of terminal (* wildcard *) - | P_as of terminal * 'a pat * terminal * 'a id * terminal (* named pattern *) - | P_typ of terminal * 'a typ * 'a pat * terminal (* typed pattern *) - | P_id of 'a id (* identifier *) - | P_app of 'a 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_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 *) + | 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 *) -and 'a pat = - P_aux of 'a pat_aux * 'a l +and pat = + P_aux of pat_aux * l -and 'a fpat_aux = (* Field pattern *) - FP_Fpat of 'a id * terminal * 'a pat +and fpat_aux = (* Field pattern *) + FP_Fpat of id * terminal * pat -and 'a fpat = - FP_aux of 'a fpat_aux * 'a l +and fpat = + FP_aux of fpat_aux * l type -'a exp_aux = (* Expression *) - E_block of terminal * ('a exp * terminal) list * terminal (* block (parsing conflict with structs?) *) - | E_id of 'a id (* identifier *) +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_cast of terminal * 'a typ * terminal * 'a exp (* cast *) - | E_app of 'a exp * ('a exp) list (* function application *) - | E_app_infix of 'a exp * 'a id * 'a exp (* infix function application *) - | 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_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 *) - | E_vector_update_subrange of terminal * 'a exp * terminal * 'a exp * terminal * 'a exp * terminal * 'a exp * terminal (* vector subrange update (with vector) *) - | E_list of terminal * ('a exp * terminal) list * terminal (* list *) - | E_cons of 'a exp * terminal * 'a exp (* cons *) - | E_record of terminal * 'a fexps * terminal (* struct *) - | E_record_update of terminal * 'a exp * terminal * 'a fexps * terminal (* functional update of struct *) - | E_field of 'a exp * terminal * 'a id (* field projection from struct *) - | E_case of terminal * 'a exp * terminal * ((terminal * 'a pexp)) list * terminal (* pattern matching *) - | E_let of 'a letbind * terminal * 'a exp (* let expression *) - | E_assign of lexp * terminal * 'a exp (* imperative assignment *) - -and 'a exp = - E_aux of 'a exp_aux * 'a l + | E_cast of terminal * typ * terminal * exp (* cast *) + | E_app of exp * (exp) list (* function application *) + | E_app_infix of exp * id * exp (* infix function application *) + | E_tuple 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_update of terminal * exp * terminal * exp * terminal * exp * terminal (* vector functional update *) + | E_vector_update_subrange of terminal * exp * terminal * exp * terminal * exp * terminal * exp * terminal (* vector subrange update (with vector) *) + | E_list of terminal * (exp * terminal) list * terminal (* list *) + | E_cons of exp * terminal * exp (* cons *) + | E_record of terminal * fexps * terminal (* struct *) + | E_record_update 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 = (* lvalue expression *) - LEXP_id of 'a id (* identifier *) - | LEXP_vector of lexp * terminal * 'a exp * terminal (* vector element *) - | LEXP_vector_range of lexp * terminal * 'a exp * terminal * 'a exp * terminal (* subvector *) - | LEXP_field of lexp * terminal * 'a id (* struct field *) + 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 'a fexp_aux = (* Field-expression *) - FE_Fexp of 'a id * terminal * 'a exp +and fexp_aux = (* Field-expression *) + FE_Fexp of id * terminal * exp -and 'a fexp = - FE_aux of 'a fexp_aux * 'a l +and fexp = + FE_aux of fexp_aux * l -and 'a fexps_aux = (* Field-expression list *) - FES_Fexps of ('a fexp * terminal) list * terminal * bool +and fexps_aux = (* Field-expression list *) + FES_Fexps of (fexp * terminal) list * terminal * bool -and 'a fexps = - FES_aux of 'a fexps_aux * 'a l +and fexps = + FES_aux of fexps_aux * l -and 'a pexp_aux = (* Pattern match *) - Pat_exp of 'a pat * terminal * 'a exp +and pexp_aux = (* Pattern match *) + Pat_exp of pat * terminal * exp -and 'a pexp = - Pat_aux of 'a pexp_aux * 'a l +and pexp = + Pat_aux of pexp_aux * l -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 letbind_aux = (* Let binding *) + LB_val_explicit of typschm * pat * terminal * exp (* value binding, explicit type (pat must be total) *) + | LB_val_implicit of terminal * pat * terminal * exp (* value binding, implicit type (pat must be total) *) -and 'a letbind = - LB_aux of 'a letbind_aux * 'a l +and letbind = + LB_aux of letbind_aux * l type -'a rec_opt_aux = (* Optional recursive annotation for functions *) - Rec_nonrec (* non-recursive *) - | Rec_rec of terminal (* recursive *) +funcl_aux = (* Function clause *) + FCL_Funcl of id * pat * terminal * exp type -'a effects_opt_aux = (* Optional effect annotation for functions *) +effects_opt_aux = (* Optional effect annotation for functions *) Effects_opt_pure (* sugar for empty effect set *) - | Effects_opt_effects of 'a effects + | Effects_opt_effects of effects type -'a funcl_aux = (* Function clause *) - FCL_Funcl of 'a id * 'a pat * terminal * 'a exp +funcl = + FCL_aux of funcl_aux * l type -tannot_opt = (* Optional type annotation for functions *) - Typ_annot_opt_none - | Typ_annot_opt_some of terminal * 'a typ +rec_opt = (* Optional recursive annotation for functions *) + Rec_nonrec (* non-recursive *) + | Rec_rec of terminal (* recursive *) type -'a rec_opt = - Rec_aux of 'a rec_opt_aux * 'a l +effects_opt = + Effects_opt_aux of effects_opt_aux * l type -'a effects_opt = - Effects_opt_aux of 'a effects_opt_aux * 'a l +tannot_opt = (* Optional type annotation for functions *) + Typ_annot_opt_none + | Typ_annot_opt_some of terminal * typ type -'a funcl = - FCL_aux of 'a funcl_aux * 'a l +val_spec_aux = (* Value type specification *) + VS_val_spec of terminal * typschm * id type @@ -354,96 +339,91 @@ index_range = (* index specification, for bitfields in register types *) type -'a fundef_aux = (* Function definition *) - FD_function of terminal * 'a rec_opt * tannot_opt * 'a effects_opt * ('a funcl * terminal) list +fundef_aux = (* Function definition *) + FD_function of terminal * rec_opt * tannot_opt * effects_opt * (funcl * terminal) list type -'a val_spec_aux = (* Value type specification *) - VS_val_spec of terminal * 'a typschm * 'a id +default_typing_spec_aux = (* Default kinding or typing assumption *) + DT_kind of terminal * base_kind * id + | DT_typ of terminal * typschm * id type -'a default_typing_spec_aux = (* Default kinding or typing assumption *) - DT_kind of terminal * 'a base_kind * 'a id - | DT_typ of terminal * 'a typschm * 'a id +val_spec = + VS_aux of val_spec_aux * l type type_def = (* Type definition body *) - TD_abbrev of terminal * 'a id * naming_scheme_opt * terminal * 'a typschm (* type abbreviation *) - | TD_record of terminal * 'a id * naming_scheme_opt * terminal * terminal * terminal * 'a typquant * terminal * (('a typ * 'a id) * terminal) list * terminal * bool * terminal (* struct type definition *) - | TD_variant of terminal * 'a id * naming_scheme_opt * terminal * terminal * terminal * 'a typquant * terminal * (('a typ * 'a id) * terminal) list * terminal * bool * terminal (* union type definition *) - | TD_enum of terminal * 'a id * naming_scheme_opt * terminal * terminal * terminal * ('a id * terminal) list * terminal * bool * terminal (* enumeration type definition *) - | TD_register of terminal * 'a id * terminal * terminal * terminal * terminal * 'a nexp * terminal * 'a nexp * terminal * terminal * ((index_range * terminal * 'a id) * terminal) list * terminal (* register mutable bitfield type definition *) - - -type -'a fundef = - FD_aux of 'a fundef_aux * 'a l + TD_abbrev of terminal * id * naming_scheme_opt * terminal * typschm (* type abbreviation *) + | TD_record of terminal * id * naming_scheme_opt * terminal * terminal * terminal * typquant * terminal * ((typ * id) * terminal) list * terminal * bool * terminal (* struct type definition *) + | TD_variant of terminal * id * naming_scheme_opt * terminal * terminal * terminal * typquant * terminal * ((typ * id) * terminal) list * terminal * bool * terminal (* union type definition *) + | TD_enum of terminal * id * naming_scheme_opt * 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 * ((index_range * terminal * id) * terminal) list * terminal (* register mutable bitfield type definition *) type -'a val_spec = - VS_aux of 'a val_spec_aux * 'a l +fundef = + FD_aux of fundef_aux * l type -'a default_typing_spec = - DT_aux of 'a default_typing_spec_aux * 'a l +default_typing_spec = + DT_aux of default_typing_spec_aux * l type -'a def_aux = (* Top-level definition *) +def_aux = (* Top-level definition *) DEF_type of type_def (* type definition *) - | DEF_fundef of 'a fundef (* function definition *) - | DEF_val of 'a letbind (* value definition *) - | DEF_spec of 'a val_spec (* top-level type constraint *) - | DEF_default of 'a default_typing_spec (* default kind and type assumptions *) - | DEF_reg_dec of terminal * 'a typ * 'a id (* register declaration *) - | DEF_scattered_function of terminal * terminal * 'a rec_opt * tannot_opt * 'a effects_opt * 'a id (* scattered function definition header *) - | DEF_scattered_funcl of terminal * terminal * 'a funcl (* scattered function definition clause *) - | DEF_scattered_variant of terminal * terminal * 'a id * naming_scheme_opt * terminal * terminal * terminal * 'a typquant (* scattered union definition header *) - | DEF_scattered_unioncl of terminal * 'a id * terminal * 'a typ * 'a id (* scattered union definition member *) - | DEF_scattered_end of terminal * 'a id (* scattered definition end *) + | DEF_fundef of fundef (* function definition *) + | DEF_val of letbind (* value definition *) + | DEF_spec of val_spec (* top-level type constraint *) + | DEF_default of default_typing_spec (* default kind and type assumptions *) + | DEF_reg_dec of terminal * typ * id (* register declaration *) + | DEF_scattered_function of terminal * terminal * rec_opt * tannot_opt * effects_opt * id (* scattered function definition header *) + | DEF_scattered_funcl of terminal * terminal * funcl (* scattered function definition clause *) + | DEF_scattered_variant of terminal * terminal * id * naming_scheme_opt * terminal * terminal * terminal * typquant (* scattered union definition header *) + | DEF_scattered_unioncl of terminal * id * terminal * typ * id (* scattered union definition member *) + | DEF_scattered_end of terminal * id (* scattered definition end *) type -'a typ_lib_aux = (* library types and syntactic sugar for them *) +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 * 'a nexp * 'a nexp * 'a order (* natural numbers 'a nexp .. 'a nexp+'a nexp-1, ordered by 'a order *) - | Typ_lib_enum1 of terminal * 'a nexp * terminal (* sugar for \texttt{enum nexp 0 inc} *) - | Typ_lib_enum2 of terminal * 'a nexp * terminal * 'a nexp * terminal (* sugar for \texttt{enum (nexp'-nexp+1) nexp inc} or \texttt{enum (nexp-nexp'+1) nexp' dec} *) - | Typ_lib_vector of terminal * 'a nexp * 'a nexp * 'a order * 'a typ (* vector of 'a typ, indexed by natural range *) - | Typ_lib_vector2 of 'a typ * terminal * 'a nexp * terminal (* sugar for vector indexed by [ 'a nexp ] *) - | Typ_lib_vector3 of 'a typ * terminal * 'a nexp * terminal * 'a nexp * terminal (* sugar for vector indexed by [ 'a nexp..'a nexp ] *) - | Typ_lib_list of terminal * 'a typ (* list of 'a typ *) - | Typ_lib_set of terminal * 'a typ (* finite set of 'a typ *) - | Typ_lib_reg of terminal * 'a typ (* mutable register components holding 'a typ *) + | Typ_lib_enum of terminal * nexp * nexp * order (* natural numbers nexp .. nexp+nexp-1, ordered by order *) + | 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 * order * 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 -'a def = - DEF_aux of 'a def_aux * 'a l +def = + DEF_aux of def_aux * l type -'a typ_lib = - Typ_lib_aux of 'a typ_lib_aux * 'a l +ctor_def = (* Datatype constructor definition clause *) + CT_ct of id * terminal * typschm type -ctor_def = (* Datatype constructor definition clause *) - CT_ct of 'a id * terminal * 'a typschm +typ_lib = + Typ_lib_aux of typ_lib_aux * l type defs = (* Definition sequence *) - Defs of ('a def) list + Defs of (def) list diff --git a/src/parser.mly b/src/parser.mly index 497f55d9..6ea85671 100644 --- a/src/parser.mly +++ b/src/parser.mly @@ -949,8 +949,10 @@ def: { dloc (DEF_default($1)) } | Register typ id { dloc (DEF_reg_dec($1,$2,$3)) } - | Scattered Function_ rec_opt tannot_opt effects_opt id - { dloc (DEF_scattered_function($1,$2,$3,$4,$5,$6)) } + | Scattered Function_ Rec tannot_opt effects_opt id + { dloc (DEF_scattered_function($1,$2,(Rec_rec($3)),$4,$5,$6)) } + | Scattered Function_ tannot_opt effects_opt id + { dloc (DEF_scattered_function($1,$2,Rec_nonrec,$4,$5,$6)) } | Function_ Clause funcl { dloc (DEF_funcl($1,$2,$3)) } | Scattered Typedef id name_sect_opt Equal Const Union typquant |