summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorKathy Gray2013-07-26 13:00:56 +0100
committerKathy Gray2013-07-26 13:00:56 +0100
commit37a4c2ebcfab7834c17fe44703a71da277cb285e (patch)
tree366ec0c11ec8a86009aff7986862df046ca0f202 /src
parentf79e3c770ab7b772edf0cd54993c059c4d7b969a (diff)
Remove white space/terminal tracking
Diffstat (limited to 'src')
-rw-r--r--src/ast.ml226
-rw-r--r--src/lexer.mll358
-rw-r--r--src/parse_ast.ml226
-rw-r--r--src/parser.mly394
-rw-r--r--src/process_file.ml4
-rw-r--r--src/process_file.mli2
6 files changed, 603 insertions, 607 deletions
diff --git a/src/ast.ml b/src/ast.ml
index d09526c6..8a0c6022 100644
--- a/src/ast.ml
+++ b/src/ast.ml
@@ -47,15 +47,15 @@ let combine_lex_skips s1 s2 =
type terminal = lex_skips
-type x = terminal * text (* identifier *)
-type ix = terminal * text (* infix identifier *)
+type x = text (* identifier *)
+type ix = text (* infix identifier *)
type
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 *)
- | BK_effects of terminal (* kind of effect sets *)
+ BK_type (* kind of types *)
+ | BK_nat (* kind of natural number size expressions *)
+ | BK_order (* kind of vector order specifications *)
+ | BK_effects (* kind of effect sets *)
type
@@ -66,12 +66,12 @@ base_kind =
type
id_aux = (* Identifier *)
Id of x
- | DeIid of terminal * x * terminal (* remove infix status *)
+ | DeIid of x (* remove infix status *)
type
kind_aux = (* kinds *)
- K_kind of (base_kind * terminal) list
+ K_kind of (base_kind) list
type
@@ -81,13 +81,13 @@ id =
type
efct_aux = (* effect *)
- Effect_rreg of terminal (* read register *)
- | Effect_wreg of terminal (* write register *)
- | Effect_rmem of terminal (* read memory *)
- | Effect_wmem of terminal (* write memory *)
- | Effect_undef of terminal (* undefined-instruction exception *)
- | Effect_unspec of terminal (* unspecified values *)
- | Effect_nondet of terminal (* nondeterminism from intra-instruction parallelism *)
+ Effect_rreg (* read register *)
+ | Effect_wreg (* write register *)
+ | Effect_rmem (* read memory *)
+ | Effect_wmem (* write memory *)
+ | Effect_undef (* undefined-instruction exception *)
+ | Effect_unspec (* unspecified values *)
+ | Effect_nondet (* nondeterminism from intra-instruction parallelism *)
type
@@ -98,10 +98,10 @@ kind =
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 *)
+ | Nexp_constant of int (* constant *)
+ | Nexp_times of nexp * nexp (* product *)
+ | Nexp_sum of nexp * nexp (* sum *)
+ | Nexp_exp of nexp (* exponential *)
and nexp =
Nexp_aux of nexp_aux * l
@@ -120,23 +120,23 @@ kinded_id_aux = (* optionally kind-annotated identifier *)
type
'a 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
+ NC_fixed of nexp * nexp
+ | NC_bounded_ge of nexp * nexp
+ | NC_bounded_le of nexp * nexp
+ | NC_nat_set_bounded of id * (int) list
type
effects_aux = (* effect set, of kind $_$ *)
- Effects_var of terminal * id
- | Effects_set of terminal * terminal * (efct * terminal) list * terminal (* effect set *)
+ Effects_var of id
+ | Effects_set of (efct) list (* effect set *)
type
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) *)
+ | Ord_inc (* increasing (little-endian) *)
+ | Ord_dec (* decreasing (big-endian) *)
type
@@ -161,30 +161,30 @@ order =
type
'a typquant_aux = (* type quantifiers and constraints *)
- TypQ_tq of terminal * (kinded_id) list * terminal * ('a nexp_constraint * terminal) list * terminal
- | TypQ_no_constraint of terminal * (kinded_id) list * terminal (* sugar, omitting constraints *)
+ TypQ_tq of (kinded_id) list * ('a nexp_constraint) list
+ | TypQ_no_constraint of (kinded_id) list (* sugar, omitting constraints *)
| TypQ_no_forall (* sugar, omitting quantifier and constraints *)
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 *)
+ L_unit (* $() : _$ *)
+ | L_zero (* $_ : _$ *)
+ | L_one (* $_ : _$ *)
+ | L_true (* $_ : _$ *)
+ | L_false (* $_ : _$ *)
+ | L_num of int (* natural number constant *)
+ | L_hex of string (* bit vector constant, C-style *)
+ | L_bin of string (* bit vector constant, C-style *)
+ | L_string of string (* string constant *)
type
typ_aux = (* Type expressions, of kind $_$ *)
- Typ_wild of terminal (* Unspecified type *)
+ Typ_wild (* Unspecified type *)
| 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_fn of typ * typ * effects (* Function type (first-order only in user code) *)
+ | Typ_tup of (typ) list (* Tuple type *)
| Typ_app of id * (typ_arg) list (* type constructor application *)
and typ =
@@ -218,23 +218,23 @@ type
type
'a pat_aux = (* Pattern *)
P_lit of lit (* literal constant pattern *)
- | P_wild of terminal (* wildcard *)
- | P_as of terminal * 'a pat * terminal * id * terminal (* named pattern *)
- | P_typ of terminal * typ * 'a pat * terminal (* typed pattern *)
+ | P_wild (* wildcard *)
+ | P_as of 'a pat * id (* named pattern *)
+ | P_typ of typ * 'a pat (* typed pattern *)
| P_id of id (* identifier *)
| 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_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_record of ('a fpat) list * bool (* struct pattern *)
+ | P_vector of ('a pat) list (* vector pattern *)
+ | P_vector_indexed of ((int * 'a pat)) list (* vector pattern (with explicit indices) *)
+ | P_vector_concat of ('a pat) list (* concatenated vector pattern *)
+ | P_tup of ('a pat) list (* tuple pattern *)
+ | P_list of ('a pat) list (* list pattern *)
and 'a pat =
P_aux of 'a pat_aux * 'a annot
and 'a fpat_aux = (* Field pattern *)
- FP_Fpat of id * terminal * 'a pat
+ FP_Fpat of id * 'a pat
and 'a fpat =
FP_aux of 'a fpat_aux * 'a annot
@@ -250,79 +250,79 @@ type
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_block of ('a exp) list (* block (parsing conflict with structs?) *)
| E_id of id (* identifier *)
| E_lit of lit (* literal constant *)
- | E_cast of terminal * typ * terminal * 'a exp (* cast *)
+ | E_cast of typ * 'a exp (* cast *)
| E_app of 'a exp * ('a exp) list (* function application *)
| E_app_infix of 'a exp * 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 * 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 'a lexp * terminal * 'a exp (* imperative assignment *)
+ | E_tuple of ('a exp) list (* tuple *)
+ | E_if of 'a exp * 'a exp * 'a exp (* conditional *)
+ | E_vector of ('a exp) list (* vector (indexed from 0) *)
+ | E_vector_indexed of ((int * 'a exp)) list (* 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 *)
+ | E_vector_update_subrange of 'a exp * 'a exp * 'a exp * 'a exp (* vector subrange update (with vector) *)
+ | E_list of ('a exp) list (* list *)
+ | E_cons of 'a exp * 'a exp (* cons *)
+ | E_record of 'a fexps (* struct *)
+ | E_record_update of 'a exp * 'a fexps (* functional update of struct *)
+ | E_field of 'a exp * id (* field projection from struct *)
+ | E_case of 'a exp * ('a pexp) list (* pattern matching *)
+ | E_let of 'a letbind * 'a exp (* let expression *)
+ | E_assign of 'a lexp * 'a exp (* imperative assignment *)
and 'a exp =
E_aux of 'a exp_aux * 'a annot
and 'a lexp_aux = (* lvalue expression *)
LEXP_id of id (* identifier *)
- | LEXP_vector of 'a lexp * terminal * 'a exp * terminal (* vector element *)
- | LEXP_vector_range of 'a lexp * terminal * 'a exp * terminal * 'a exp * terminal (* subvector *)
- | LEXP_field of 'a lexp * terminal * id (* struct field *)
+ | LEXP_vector of 'a lexp * 'a exp (* vector element *)
+ | LEXP_vector_range of 'a lexp * 'a exp * 'a exp (* subvector *)
+ | LEXP_field of 'a lexp * id (* struct field *)
and 'a lexp =
LEXP_aux of 'a lexp_aux * 'a annot
and 'a fexp_aux = (* Field-expression *)
- FE_Fexp of id * terminal * 'a exp
+ FE_Fexp of id * 'a exp
and 'a fexp =
FE_aux of 'a fexp_aux * 'a annot
and 'a fexps_aux = (* Field-expression list *)
- FES_Fexps of ('a fexp * terminal) list * terminal * bool
+ FES_Fexps of ('a fexp) list * bool
and 'a fexps =
FES_aux of 'a fexps_aux * 'a annot
and 'a pexp_aux = (* Pattern match *)
- Pat_exp of 'a pat * terminal * 'a exp
+ Pat_exp of 'a pat * 'a exp
and 'a pexp =
Pat_aux of 'a pexp_aux * 'a annot
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) *)
+ LB_val_explicit of 'a typschm * 'a pat * 'a exp (* value binding, explicit type ('a pat must be total) *)
+ | LB_val_implicit of 'a pat * 'a exp (* value binding, implicit type ('a pat must be total) *)
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
+ | Name_sect_some of string
type
rec_opt_aux = (* Optional recursive annotation for functions *)
Rec_nonrec (* non-recursive *)
- | Rec_rec of terminal (* recursive *)
+ | Rec_rec (* recursive *)
type
'a funcl_aux = (* Function clause *)
- FCL_Funcl of id * 'a pat * terminal * 'a exp
+ FCL_Funcl of id * 'a pat * 'a exp
type
@@ -339,9 +339,9 @@ type
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 *)
+ BF_single of int (* single index *)
+ | BF_range of int * int (* index range *)
+ | BF_concat of index_range * index_range (* concatenation of index ranges *)
and index_range =
BF_aux of index_range_aux * l
@@ -374,27 +374,27 @@ type
type
'a type_def_aux = (* Type definition body *)
- TD_abbrev of terminal * id * naming_scheme_opt * terminal * 'a typschm (* type abbreviation *)
- | TD_record of terminal * id * naming_scheme_opt * terminal * terminal * terminal * 'a typquant * terminal * ((typ * id) * terminal) list * terminal * bool * terminal (* struct type definition *)
- | TD_variant of terminal * id * naming_scheme_opt * terminal * terminal * terminal * 'a 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 *)
+ TD_abbrev of id * naming_scheme_opt * 'a typschm (* type abbreviation *)
+ | TD_record of id * naming_scheme_opt * 'a typquant * ((typ * id)) list * bool (* struct type definition *)
+ | TD_variant of id * naming_scheme_opt * 'a typquant * ((typ * id)) list * bool (* union type definition *)
+ | TD_enum of id * naming_scheme_opt * (id) list * bool (* enumeration type definition *)
+ | TD_register of id * nexp * nexp * ((index_range * id)) list (* register mutable bitfield type definition *)
type
'a val_spec_aux = (* Value type specification *)
- VS_val_spec of terminal * 'a typschm * id
+ VS_val_spec of 'a typschm * id
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
+ DT_kind of base_kind * id
+ | DT_typ of 'a typschm * id
type
'a fundef_aux = (* Function definition *)
- FD_function of terminal * rec_opt * 'a tannot_opt * 'a effects_opt * ('a funcl * terminal) list
+ FD_function of rec_opt * 'a tannot_opt * 'a effects_opt * ('a funcl) list
type
@@ -424,35 +424,35 @@ type
| 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 * typ * id (* register declaration *)
- | DEF_scattered_function of terminal * terminal * rec_opt * 'a tannot_opt * 'a effects_opt * id (* scattered function definition header *)
- | DEF_scattered_funcl of terminal * terminal * 'a funcl (* scattered function definition clause *)
- | DEF_scattered_variant of terminal * terminal * id * naming_scheme_opt * terminal * terminal * terminal * 'a 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 *)
+ | DEF_reg_dec of typ * id (* register declaration *)
+ | DEF_scattered_function of rec_opt * 'a tannot_opt * 'a effects_opt * id (* scattered function definition header *)
+ | DEF_scattered_funcl of 'a funcl (* scattered function definition clause *)
+ | DEF_scattered_variant of id * naming_scheme_opt * 'a typquant (* scattered union definition header *)
+ | DEF_scattered_unioncl of id * typ * id (* scattered union definition member *)
+ | DEF_scattered_end of id (* scattered definition end *)
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 $_$ *)
- | 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 * string (* UTF8 strings *)
- | 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 *)
+ Typ_lib_unit (* unit type with value $()$ *)
+ | Typ_lib_bool (* booleans $_$ and $_$ *)
+ | Typ_lib_bit (* pure bit values (not mutable bits) *)
+ | Typ_lib_nat (* natural numbers 0,1,2,... *)
+ | Typ_lib_string of string (* UTF8 strings *)
+ | Typ_lib_enum of nexp * nexp * order (* natural numbers nexp .. nexp+nexp-1, ordered by order *)
+ | Typ_lib_enum1 of nexp (* sugar for \texttt{enum nexp 0 inc} *)
+ | Typ_lib_enum2 of nexp * nexp (* sugar for \texttt{enum (nexp'-nexp+1) nexp inc} or \texttt{enum (nexp-nexp'+1) nexp' dec} *)
+ | Typ_lib_vector of nexp * nexp * order * typ (* vector of typ, indexed by natural range *)
+ | Typ_lib_vector2 of typ * nexp (* sugar for vector indexed by [ nexp ] *)
+ | Typ_lib_vector3 of typ * nexp * nexp (* sugar for vector indexed by [ nexp..nexp ] *)
+ | Typ_lib_list of typ (* list of typ *)
+ | Typ_lib_set of typ (* finite set of typ *)
+ | Typ_lib_reg of typ (* mutable register components holding typ *)
type
'a ctor_def_aux = (* Datatype constructor definition clause *)
- CT_ct of id * terminal * 'a typschm
+ CT_ct of id * 'a typschm
type
diff --git a/src/lexer.mll b/src/lexer.mll
index 8d2be0d3..d7726c7b 100644
--- a/src/lexer.mll
+++ b/src/lexer.mll
@@ -58,48 +58,47 @@ let kw_table =
(fun r (x,y) -> M.add x y r)
M.empty
[
- ("and", (fun x -> And(x)));
- ("as", (fun x -> As(x)));
- ("case", (fun x -> Case(x)));
- ("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)));
- ("false", (fun x -> False(x)));
- ("forall", (fun x -> Forall(x)));
- ("function", (fun x -> Function_(x)));
- ("if", (fun x -> If_(x)));
- ("in", (fun x -> In(x)));
- ("IN", (fun x -> IN(x)));
- ("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)));
- ("struct", (fun x -> Struct(x)));
- ("switch", (fun x -> Switch(x)));
- ("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)));
- ("val", (fun x -> Val(x)));
+ ("and", (fun _ -> And));
+ ("as", (fun _ -> As));
+ ("case", (fun _ -> Case));
+ ("clause", (fun _ -> Clause));
+ ("const", (fun _ -> Const));
+ ("default", (fun _ -> Default));
+ ("effect", (fun _ -> Effect));
+ ("Effects", (fun _ -> Effects));
+ ("end", (fun _ -> End));
+ ("enum", (fun _ -> Enum));
+ ("else", (fun _ -> Else));
+ ("false", (fun _ -> False));
+ ("forall", (fun _ -> Forall));
+ ("function", (fun x -> Function_));
+ ("if", (fun x -> If_));
+ ("in", (fun x -> In));
+ ("IN", (fun x -> IN));
+ ("let", (fun x -> Let_));
+ ("member", (fun x -> Member));
+ ("Nat", (fun x -> Nat));
+ ("Order", (fun x -> Order));
+ ("rec", (fun x -> Rec));
+ ("register", (fun x -> Register));
+ ("scattered", (fun x -> Scattered));
+ ("struct", (fun x -> Struct));
+ ("switch", (fun x -> Switch));
+ ("then", (fun x -> Then));
+ ("true", (fun x -> True));
+ ("Type", (fun x -> TYPE));
+ ("typedef", (fun x -> Typedef));
+ ("union", (fun x -> Union));
+ ("with", (fun x -> With));
+ ("val", (fun x -> Val));
- ("AND", (fun x -> AND(x)));
- ("div", (fun x -> Div_(x)));
- ("EOR", (fun x -> EOR(x)));
- ("mod", (fun x -> Mod(x)));
- ("OR", (fun x -> OR(x)));
- ("quot", (fun x -> Quot(x)));
- ("rem", (fun x -> Rem(x)));
+ ("AND", (fun x -> AND));
+ ("div", (fun x -> Div_));
+ ("EOR", (fun x -> EOR));
+ ("mod", (fun x -> Mod));
+ ("OR", (fun x -> OR));
+ ("quot", (fun x -> Quot));
+ ("rem", (fun x -> Rem));
]
}
@@ -119,158 +118,159 @@ let com_help = "("*safe_com2 | "*"*"("+safe_com2 | "*"*safe_com1
let com_body = com_help*"*"*
let escape_sequence = ('\\' ['\\''\"''\'''n''t''b''r']) | ('\\' digit digit digit) | ('\\' 'x' hexdigit hexdigit)
-rule token skips = parse
+rule token = parse
| ws as i
- { token (Parse_ast.Ws(r i)::skips) lexbuf }
+ { token lexbuf }
| "\n"
{ Lexing.new_line lexbuf;
- token (Parse_ast.Nl::skips) lexbuf }
+ token lexbuf }
- | "&" { (Amp(Some(skips),r"&")) }
- | "@" { (At(Some(skips),r"@")) }
- | "|" { (Bar(Some(skips))) }
- | "^" { (Carrot(Some(skips),r"^")) }
- | ":" { (Colon(Some(skips))) }
- | "," { (Comma(Some(skips))) }
- | "." { (Dot(Some(skips))) }
- | "/" { (Div(Some(skips),r"/")) }
- | "=" { (Eq(Some(skips),r"=")) }
- | "!" { (Excl(Some(skips),r"!")) }
- | ">" { (Gt(Some(skips),r">")) }
- | "-" { (Minus(Some(skips))) }
- | "<" { (Lt(Some(skips),r"<")) }
- | "+" { (Plus(Some(skips),r"+")) }
- | ";" { (Semi(Some(skips))) }
- | "*" { (Star(Some(skips),r"*")) }
- | "~" { (Tilde(Some(skips),r"~")) }
- | "_" { (Under(Some(skips))) }
- | "{" { (Lcurly(Some(skips))) }
- | "}" { (Rcurly(Some(skips))) }
- | "(" { (Lparen(Some(skips))) }
- | ")" { (Rparen(Some(skips))) }
- | "[" { (Lsquare(Some(skips))) }
- | "]" { (Rsquare(Some(skips))) }
- | "&&" as i { (AmpAmp(Some(skips),r i)) }
- | "||" { (BarBar(Some(skips))) }
- | "|>" { (BarGt(Some(skips))) }
- | "|]" { (BarSquare(Some(skips))) }
- | "^^" { (CarrotCarrot(Some(skips),r"^^")) }
- | "::" as i { (ColonColon(Some(skips),r i)) }
- | ".." { (DotDot(Some(skips))) }
- | "=/=" { (EqDivEq(Some(skips),r"=/=")) }
- | "==" { (EqEq(Some(skips),r"==")) }
- | "!=" { (ExclEq(Some(skips),r"!=")) }
- | "!!" { (ExclExcl(Some(skips),r"!!")) }
- | ">=" { (GtEq(Some(skips),r">=")) }
- | ">=+" { (GtEqPlus(Some(skips),r">=+")) }
- | ">>" { (GtGt(Some(skips),r">>")) }
- | ">>>" { (GtGtGt(Some(skips),r">>")) }
- | ">+" { (GtPlus(Some(skips),r">+")) }
- | "#>>" { (HashGtGt(Some(skips),r"#>>")) }
- | "#<<" { (HashLtLt(Some(skips),r"#<<")) }
- | "->" { (MinusGt(Some(skips))) }
- | "<=" { (LtEq(Some(skips),r"<=")) }
- | "<=+" { (LtEqPlus(Some(skips),r"<=+")) }
- | "<>" { (LtGt(Some(skips),r"<>")) }
- | "<<" { (LtLt(Some(skips),r"<<")) }
- | "<<<" { (LtLtLt(Some(skips),r"<<<")) }
- | "<+" { (LtPlus(Some(skips),r"<+")) }
- | "**" { (StarStar(Some(skips),r"**")) }
- | "~^" { (TildeCarrot(Some(skips),r"~^")) }
+ | "&" { (Amp(r"&")) }
+ | "@" { (At(r"@")) }
+ | "|" { Bar }
+ | "^" { (Carrot(r"^")) }
+ | ":" { Colon }
+ | "," { Comma }
+ | "." { Dot }
+ | "/" { (Div(r "/")) }
+ | "=" { (Eq(r"=")) }
+ | "!" { (Excl(r"!")) }
+ | ">" { (Gt(r">")) }
+ | "-" { Minus }
+ | "<" { (Lt(r"<")) }
+ | "+" { (Plus(r"+")) }
+ | ";" { Semi }
+ | "*" { (Star(r"*")) }
+ | "~" { (Tilde(r"~")) }
+ | "_" { Under }
+ | "{" { Lcurly }
+ | "}" { Rcurly }
+ | "(" { Lparen }
+ | ")" { Rparen }
+ | "[" { Lsquare }
+ | "]" { Rsquare }
+ | "&&" as i { (AmpAmp(r i)) }
+ | "||" { BarBar }
+ | "|>" { BarGt }
+ | "|]" { BarSquare }
+ | "^^" { (CarrotCarrot(r"^^")) }
+ | "::" as i { (ColonColon(r i)) }
+ | ".." { DotDot }
+ | "=/=" { (EqDivEq(r"=/=")) }
+ | "==" { (EqEq(r"==")) }
+ | "!=" { (ExclEq(r"!=")) }
+ | "!!" { (ExclExcl(r"!!")) }
+ | ">=" { (GtEq(r">=")) }
+ | ">=+" { (GtEqPlus(r">=+")) }
+ | ">>" { (GtGt(r">>")) }
+ | ">>>" { (GtGtGt(r">>>")) }
+ | ">+" { (GtPlus(r">+")) }
+ | "#>>" { (HashGtGt(r"#>>")) }
+ | "#<<" { (HashLtLt(r"#<<")) }
+ | "->" { MinusGt }
+ | "<=" { (LtEq(r"<=")) }
+ | "<=+" { (LtEqPlus(r"<=+")) }
+ | "<>" { (LtGt(r"<>")) }
+ | "<<" { (LtLt(r"<<")) }
+ | "<<<" { (LtLtLt(r"<<<")) }
+ | "<+" { (LtPlus(r"<+")) }
+ | "**" { (StarStar(r"**")) }
+ | "~^" { (TildeCarrot(r"~^")) }
- | ">=_s" { (GtEqUnderS(Some(skips),r">=_s")) }
- | ">=_si" { (GtEqUnderSi(Some(skips),r">=_si")) }
- | ">=_u" { (GtEqUnderU(Some(skips),r">=_u")) }
- | ">=_ui" { (GtEqUnderUi(Some(skips),r">=_ui")) }
- | ">>_u" { (GtGtUnderU(Some(skips),r">>_u")) }
- | ">_s" { (GtUnderS(Some(skips),r">_s")) }
- | ">_si" { (GtUnderSi(Some(skips),r">_si")) }
- | ">_u" { (GtUnderU(Some(skips),r">_u")) }
- | ">_ui" { (GtUnderUi(Some(skips),r">_ui")) }
- | "<=_s" { (LtEqUnderS(Some(skips),r"<=_s")) }
- | "<=_si" { (LtEqUnderSi(Some(skips),r"<=_si")) }
- | "<=_u" { (LtEqUnderU(Some(skips),r"<=_u")) }
- | "<=_ui" { (LtEqUnderUi(Some(skips),r"<=_ui")) }
- | "<_s" { (LtUnderS(Some(skips),r"<_s")) }
- | "<_si" { (LtUnderSi(Some(skips),r"<_si")) }
- | "<_u" { (LtUnderU(Some(skips),r"<_u")) }
- | "<_ui" { (LtUnderUi(Some(skips),r"<_ui")) }
- | "**_s" { (StarStarUnderS(Some(skips),r"**_s")) }
- | "**_si" { (StarStarUnderSi(Some(skips),r"**_si")) }
- | "*_u" { (StarUnderU(Some(skips),r"*_u")) }
- | "*_ui" { (StarUnderUi(Some(skips),r"*_ui")) }
- | "2^" { (TwoCarrot(Some(skips),r"2^")) }
+ | ">=_s" { (GtEqUnderS(r">=_s")) }
+ | ">=_si" { (GtEqUnderSi(r">=_si")) }
+ | ">=_u" { (GtEqUnderU(r">=_u")) }
+ | ">=_ui" { (GtEqUnderUi(r">=_ui")) }
+ | ">>_u" { (GtGtUnderU(r">>_u")) }
+ | ">_s" { (GtUnderS(r">_s")) }
+ | ">_si" { (GtUnderSi(r">_si")) }
+ | ">_u" { (GtUnderU(r">_u")) }
+ | ">_ui" { (GtUnderUi(r">_ui")) }
+ | "<=_s" { (LtEqUnderS(r"<=_s")) }
+ | "<=_si" { (LtEqUnderSi(r"<=_si")) }
+ | "<=_u" { (LtEqUnderU(r"<=_u")) }
+ | "<=_ui" { (LtEqUnderUi(r"<=_ui")) }
+ | "<_s" { (LtUnderS(r"<_s")) }
+ | "<_si" { (LtUnderSi(r"<_si")) }
+ | "<_u" { (LtUnderU(r"<_u")) }
+ | "<_ui" { (LtUnderUi(r"<_ui")) }
+ | "**_s" { (StarStarUnderS(r"**_s")) }
+ | "**_si" { (StarStarUnderSi(r"**_si")) }
+ | "*_u" { (StarUnderU(r"*_u")) }
+ | "*_ui" { (StarUnderUi(r"*_ui")) }
+ | "2^" { (TwoCarrot(r"2^")) }
| "--"
- { token (Parse_ast.Com(Parse_ast.Comment(comment lexbuf))::skips) lexbuf }
+ { comment lexbuf;
+ token lexbuf }
| startident ident* as i { if M.mem i kw_table then
- (M.find i kw_table) (Some(skips))
+ (M.find i kw_table) ()
else
- Id(Some(skips), r i) }
- | "&" oper_char+ as i { (AmpI(Some(skips),r i)) }
- | "@" oper_char+ as i { (AtI(Some(skips),r i)) }
- | "^" oper_char+ as i { (CarrotI(Some(skips),r i)) }
- | "/" oper_char+ as i { (DivI(Some(skips),r i)) }
- | "=" oper_char+ as i { (EqI(Some(skips),r i)) }
- | "!" oper_char+ as i { (ExclI(Some(skips),r i)) }
- | ">" oper_char+ as i { (GtI(Some(skips),r i)) }
- | "<" oper_char+ as i { (LtI(Some(skips),r i)) }
- | "+" oper_char+ as i { (PlusI(Some(skips),r i)) }
- | "*" oper_char+ as i { (StarI(Some(skips),r i)) }
- | "~" oper_char+ as i { (TildeI(Some(skips),r i)) }
- | "&&" oper_char+ as i { (AmpAmpI(Some(skips),r i)) }
- | "^^" oper_char+ as i { (CarrotCarrotI(Some(skips),r i)) }
- | "::" oper_char+ as i { (ColonColonI(Some(skips),r i)) }
- | "=/=" oper_char+ as i { (EqDivEqI(Some(skips),r i)) }
- | "==" oper_char+ as i { (EqEqI(Some(skips),r i)) }
- | "!=" oper_char+ as i { (ExclEqI(Some(skips),r i)) }
- | "!!" oper_char+ as i { (ExclExclI(Some(skips),r i)) }
- | ">=" oper_char+ as i { (GtEqI(Some(skips),r i)) }
- | ">=+" oper_char+ as i { (GtEqPlusI(Some(skips),r i)) }
- | ">>" oper_char+ as i { (GtGtI(Some(skips),r i)) }
- | ">>>" oper_char+ as i { (GtGtGtI(Some(skips),r i)) }
- | ">+" oper_char+ as i { (GtPlusI(Some(skips),r i)) }
- | "#>>" oper_char+ as i { (HashGtGt(Some(skips),r i)) }
- | "#<<" oper_char+ as i { (HashLtLt(Some(skips),r i)) }
- | "<=" oper_char+ as i { (LtEqI(Some(skips),r i)) }
- | "<=+" oper_char+ as i { (LtEqPlusI(Some(skips),r i)) }
- | "<<" oper_char+ as i { (LtLtI(Some(skips),r i)) }
- | "<<<" oper_char+ as i { (LtLtLtI(Some(skips),r i)) }
- | "<+" oper_char+ as i { (LtPlusI(Some(skips),r i)) }
- | "**" oper_char+ as i { (StarStarI(Some(skips),r i)) }
- | "~^" oper_char+ as i { (TildeCarrot(Some(skips),r i)) }
+ Id(r i) }
+ | "&" oper_char+ as i { (AmpI(r i)) }
+ | "@" oper_char+ as i { (AtI(r i)) }
+ | "^" oper_char+ as i { (CarrotI(r i)) }
+ | "/" oper_char+ as i { (DivI(r i)) }
+ | "=" oper_char+ as i { (EqI(r i)) }
+ | "!" oper_char+ as i { (ExclI(r i)) }
+ | ">" oper_char+ as i { (GtI(r i)) }
+ | "<" oper_char+ as i { (LtI(r i)) }
+ | "+" oper_char+ as i { (PlusI(r i)) }
+ | "*" oper_char+ as i { (StarI(r i)) }
+ | "~" oper_char+ as i { (TildeI(r i)) }
+ | "&&" oper_char+ as i { (AmpAmpI(r i)) }
+ | "^^" oper_char+ as i { (CarrotCarrotI(r i)) }
+ | "::" oper_char+ as i { (ColonColonI(r i)) }
+ | "=/=" oper_char+ as i { (EqDivEqI(r i)) }
+ | "==" oper_char+ as i { (EqEqI(r i)) }
+ | "!=" oper_char+ as i { (ExclEqI(r i)) }
+ | "!!" oper_char+ as i { (ExclExclI(r i)) }
+ | ">=" oper_char+ as i { (GtEqI(r i)) }
+ | ">=+" oper_char+ as i { (GtEqPlusI(r i)) }
+ | ">>" oper_char+ as i { (GtGtI(r i)) }
+ | ">>>" oper_char+ as i { (GtGtGtI(r i)) }
+ | ">+" oper_char+ as i { (GtPlusI(r i)) }
+ | "#>>" oper_char+ as i { (HashGtGt(r i)) }
+ | "#<<" oper_char+ as i { (HashLtLt(r i)) }
+ | "<=" oper_char+ as i { (LtEqI(r i)) }
+ | "<=+" oper_char+ as i { (LtEqPlusI(r i)) }
+ | "<<" oper_char+ as i { (LtLtI(r i)) }
+ | "<<<" oper_char+ as i { (LtLtLtI(r i)) }
+ | "<+" oper_char+ as i { (LtPlusI(r i)) }
+ | "**" oper_char+ as i { (StarStarI(r i)) }
+ | "~^" oper_char+ as i { (TildeCarrot(r i)) }
- | ">=_s" oper_char+ as i { (GtEqUnderSI(Some(skips),r i)) }
- | ">=_si" oper_char+ as i { (GtEqUnderSiI(Some(skips),r i)) }
- | ">=_u" oper_char+ as i { (GtEqUnderUI(Some(skips),r i)) }
- | ">=_ui" oper_char+ as i { (GtEqUnderUiI(Some(skips),r i)) }
- | ">>_u" oper_char+ as i { (GtGtUnderUI(Some(skips),r i)) }
- | ">_s" oper_char+ as i { (GtUnderSI(Some(skips),r i)) }
- | ">_si" oper_char+ as i { (GtUnderSiI(Some(skips),r i)) }
- | ">_u" oper_char+ as i { (GtUnderUI(Some(skips),r i)) }
- | ">_ui" oper_char+ as i { (GtUnderUiI(Some(skips),r i)) }
- | "<=_s" oper_char+ as i { (LtEqUnderSI(Some(skips),r i)) }
- | "<=_si" oper_char+ as i { (LtEqUnderSiI(Some(skips),r i)) }
- | "<=_u" oper_char+ as i { (LtEqUnderUI(Some(skips),r i)) }
- | "<=_ui" oper_char+ as i { (LtEqUnderUiI(Some(skips),r i)) }
- | "<_s" oper_char+ as i { (LtUnderSI(Some(skips),r i)) }
- | "<_si" oper_char+ as i { (LtUnderSiI(Some(skips),r i)) }
- | "<_u" oper_char+ as i { (LtUnderUI(Some(skips),r i)) }
- | "<_ui" oper_char+ as i { (LtUnderUiI(Some(skips),r i)) }
- | "**_s" oper_char+ as i { (StarStarUnderSI(Some(skips),r i)) }
- | "**_si" oper_char+ as i { (StarStarUnderSiI(Some(skips),r i)) }
- | "*_u" oper_char+ as i { (StarUnderUI(Some(skips),r i)) }
- | "*_ui" oper_char+ as i { (StarUnderUiI(Some(skips),r i)) }
- | "2^" oper_char+ as i { (TwoCarrotI(Some(skips),r i)) }
+ | ">=_s" oper_char+ as i { (GtEqUnderSI(r i)) }
+ | ">=_si" oper_char+ as i { (GtEqUnderSiI(r i)) }
+ | ">=_u" oper_char+ as i { (GtEqUnderUI(r i)) }
+ | ">=_ui" oper_char+ as i { (GtEqUnderUiI(r i)) }
+ | ">>_u" oper_char+ as i { (GtGtUnderUI(r i)) }
+ | ">_s" oper_char+ as i { (GtUnderSI(r i)) }
+ | ">_si" oper_char+ as i { (GtUnderSiI(r i)) }
+ | ">_u" oper_char+ as i { (GtUnderUI(r i)) }
+ | ">_ui" oper_char+ as i { (GtUnderUiI(r i)) }
+ | "<=_s" oper_char+ as i { (LtEqUnderSI(r i)) }
+ | "<=_si" oper_char+ as i { (LtEqUnderSiI(r i)) }
+ | "<=_u" oper_char+ as i { (LtEqUnderUI(r i)) }
+ | "<=_ui" oper_char+ as i { (LtEqUnderUiI(r i)) }
+ | "<_s" oper_char+ as i { (LtUnderSI(r i)) }
+ | "<_si" oper_char+ as i { (LtUnderSiI(r i)) }
+ | "<_u" oper_char+ as i { (LtUnderUI(r i)) }
+ | "<_ui" oper_char+ as i { (LtUnderUiI(r i)) }
+ | "**_s" oper_char+ as i { (StarStarUnderSI(r i)) }
+ | "**_si" oper_char+ as i { (StarStarUnderSiI(r i)) }
+ | "*_u" oper_char+ as i { (StarUnderUI(r i)) }
+ | "*_ui" oper_char+ as i { (StarUnderUiI(r i)) }
+ | "2^" oper_char+ as i { (TwoCarrotI(r i)) }
- | digit+ as i { (Num(Some(skips),int_of_string i)) }
- | "0b" (binarydigit+ as i) { (Bin(Some(skips), i)) }
- | "0x" (hexdigit+ as i) { (Hex(Some(skips), i)) }
- | '"' { (String(Some(skips),
+ | digit+ as i { (Num(int_of_string i)) }
+ | "0b" (binarydigit+ as i) { (Bin(i)) }
+ | "0x" (hexdigit+ as i) { (Hex(i)) }
+ | '"' { (String(
string (Lexing.lexeme_start_p lexbuf) (Buffer.create 10) lexbuf)) }
- | eof { (Eof(Some(skips))) }
+ | eof { Eof }
| _ as c { raise (LexError(c, Lexing.lexeme_start_p lexbuf)) }
diff --git a/src/parse_ast.ml b/src/parse_ast.ml
index c58a7cd7..74ec4c68 100644
--- a/src/parse_ast.ml
+++ b/src/parse_ast.ml
@@ -47,32 +47,32 @@ let combine_lex_skips s1 s2 =
type terminal = lex_skips
-type x = terminal * text (* identifier *)
-type ix = terminal * text (* infix identifier *)
+type x = text (* identifier *)
+type ix = text (* infix identifier *)
type
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 *)
- | BK_effects of terminal (* kind of effect sets *)
+ BK_type (* kind of types *)
+ | BK_nat (* kind of natural number size expressions *)
+ | BK_order (* kind of vector order specifications *)
+ | BK_effects (* kind of effect sets *)
type
efct_aux = (* effect *)
- Effect_rreg of terminal (* read register *)
- | Effect_wreg of terminal (* write register *)
- | Effect_rmem of terminal (* read memory *)
- | Effect_wmem of terminal (* write memory *)
- | Effect_undef of terminal (* undefined-instruction exception *)
- | Effect_unspec of terminal (* unspecified values *)
- | Effect_nondet of terminal (* nondeterminism from intra-instruction parallelism *)
+ Effect_rreg (* read register *)
+ | Effect_wreg (* write register *)
+ | Effect_rmem (* read memory *)
+ | Effect_wmem (* write memory *)
+ | Effect_undef (* undefined-instruction exception *)
+ | Effect_unspec (* unspecified values *)
+ | Effect_nondet (* nondeterminism from intra-instruction parallelism *)
type
id_aux = (* Identifier *)
Id of x
- | DeIid of terminal * x * terminal (* remove infix status *)
+ | DeIid of x (* remove infix status *)
type
@@ -92,23 +92,23 @@ id =
type
kind_aux = (* kinds *)
- K_kind of (base_kind * terminal) list
+ K_kind of (base_kind) list
type
atyp_aux = (* expression of all kinds *)
ATyp_id of id (* identifier *)
- | 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_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 *)
+ | ATyp_constant of int (* constant *)
+ | ATyp_times of atyp * atyp (* product *)
+ | ATyp_sum of atyp * atyp (* sum *)
+ | ATyp_exp of atyp (* exponential *)
+ | ATyp_inc (* increasing (little-endian) *)
+ | ATyp_dec (* decreasing (big-endian) *)
+ | ATyp_efid of id
+ | ATyp_set of (efct) list (* effect set *)
+ | ATyp_wild (* Unspecified type *)
+ | ATyp_fn of atyp * atyp * atyp (* Function type (first-order only in user code) *)
+ | ATyp_tup of (atyp) list (* Tuple type *)
| ATyp_app of id * (atyp) list (* type constructor application *)
and atyp =
@@ -122,10 +122,10 @@ kind =
type
nexp_constraint_aux = (* constraint over kind $_$ *)
- 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_fixed of atyp * atyp
+ | NC_bounded_ge of atyp * atyp
+ | NC_bounded_le of atyp * atyp
+ | NC_nat_set_bounded of id * (int) list
type
@@ -146,22 +146,22 @@ kinded_id =
type
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_tq of (kinded_id) list * (nexp_constraint) list
+ | TypQ_no_constraint of (kinded_id) list (* sugar, omitting constraints *)
| TypQ_no_forall (* sugar, omitting quantifier and constraints *)
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 *)
+ L_unit (* $() : _$ *)
+ | L_zero (* $_ : _$ *)
+ | L_one (* $_ : _$ *)
+ | L_true (* $_ : _$ *)
+ | L_false (* $_ : _$ *)
+ | L_num of int (* natural number constant *)
+ | L_hex of string (* bit vector constant, C-style *)
+ | L_bin of string (* bit vector constant, C-style *)
+ | L_string of string (* string constant *)
type
@@ -182,23 +182,23 @@ typschm_aux = (* type scheme *)
type
pat_aux = (* Pattern *)
P_lit of lit (* literal constant pattern *)
- | P_wild of terminal (* wildcard *)
- | P_as of terminal * pat * terminal * id * terminal (* named pattern *)
- | P_typ of terminal * atyp * pat * terminal (* typed pattern *)
+ | P_wild (* wildcard *)
+ | P_as of pat * id (* named pattern *)
+ | P_typ of atyp * pat (* 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 *)
+ | P_record of (fpat) list * bool (* struct pattern *)
+ | P_vector of (pat) list (* vector pattern *)
+ | P_vector_indexed of ((int * pat)) list (* vector pattern (with explicit indices) *)
+ | P_vector_concat of (pat) list (* concatenated vector pattern *)
+ | P_tup of (pat) list (* tuple pattern *)
+ | P_list of (pat) list (* list pattern *)
and pat =
P_aux of pat_aux * l
and fpat_aux = (* Field pattern *)
- FP_Fpat of id * terminal * pat
+ FP_Fpat of id * pat
and fpat =
FP_aux of fpat_aux * l
@@ -211,53 +211,53 @@ typschm =
type
exp_aux = (* Expression *)
- E_block of terminal * (exp * terminal) list * terminal (* block (parsing conflict with structs?) *)
+ E_block of (exp) list (* block (parsing conflict with structs?) *)
| E_id of id (* identifier *)
| E_lit of lit (* literal constant *)
- | E_cast of terminal * atyp * terminal * exp (* cast *)
+ | E_cast of atyp * 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 exp * terminal * exp (* imperative assignment *)
+ | E_tuple of (exp) list (* tuple *)
+ | E_if of exp * exp * exp (* conditional *)
+ | E_vector of (exp) list (* vector (indexed from 0) *)
+ | E_vector_indexed of ((int * exp)) list (* 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 *)
+ | E_vector_update_subrange of exp * exp * exp * exp (* vector subrange update (with vector) *)
+ | E_list of (exp) list (* list *)
+ | E_cons of exp * exp (* cons *)
+ | E_record of fexps (* struct *)
+ | E_record_update of exp * fexps (* functional update of struct *)
+ | E_field of exp * id (* field projection from struct *)
+ | E_case of exp * (pexp) list (* pattern matching *)
+ | E_let of letbind * exp (* let expression *)
+ | E_assign of exp * exp (* imperative assignment *)
and exp =
E_aux of exp_aux * l
and fexp_aux = (* Field-expression *)
- FE_Fexp of id * terminal * exp
+ FE_Fexp of id * exp
and fexp =
FE_aux of fexp_aux * l
and fexps_aux = (* Field-expression list *)
- FES_Fexps of (fexp * terminal) list * terminal * bool
+ FES_Fexps of (fexp) list * bool
and fexps =
FES_aux of fexps_aux * l
and pexp_aux = (* Pattern match *)
- Pat_exp of pat * terminal * exp
+ Pat_exp of pat * exp
and pexp =
Pat_aux of pexp_aux * l
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) *)
+ LB_val_explicit of typschm * pat * exp (* value binding, explicit type (pat must be total) *)
+ | LB_val_implicit of pat * exp (* value binding, implicit type (pat must be total) *)
and letbind =
LB_aux of letbind_aux * l
@@ -266,13 +266,13 @@ and 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
+ | Name_sect_some of string
type
rec_opt_aux = (* Optional recursive annotation for functions *)
Rec_nonrec (* non-recursive *)
- | Rec_rec of terminal (* recursive *)
+ | Rec_rec (* recursive *)
type
@@ -283,7 +283,7 @@ tannot_opt_aux = (* Optional type annotation for functions *)
type
funcl_aux = (* Function clause *)
- FCL_Funcl of id * pat * terminal * exp
+ FCL_Funcl of id * pat * exp
type
@@ -294,9 +294,9 @@ effects_opt_aux = (* Optional effect annotation for functions *)
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 *)
+ BF_single of int (* single index *)
+ | BF_range of int * int (* index range *)
+ | BF_concat of index_range * index_range (* concatenation of index ranges *)
and index_range =
BF_aux of index_range_aux * l
@@ -329,27 +329,27 @@ effects_opt =
type
default_typing_spec_aux = (* Default kinding or typing assumption *)
- DT_kind of terminal * base_kind * id
- | DT_typ of terminal * typschm * id
+ DT_kind of base_kind * id
+ | DT_typ of typschm * id
type
type_def_aux = (* Type definition body *)
- 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 * ((atyp * id) * terminal) list * terminal * bool * terminal (* struct type definition *)
- | TD_variant of terminal * id * naming_scheme_opt * terminal * terminal * terminal * typquant * terminal * ((atyp * 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 * atyp * terminal * atyp * terminal * terminal * ((index_range * terminal * id) * terminal) list * terminal (* register mutable bitfield type definition *)
+ TD_abbrev of id * naming_scheme_opt * typschm (* type abbreviation *)
+ | TD_record of id * naming_scheme_opt * typquant * ((atyp * id)) list * bool (* struct type definition *)
+ | TD_variant of id * naming_scheme_opt * typquant * ((atyp * id)) list * bool (* union type definition *)
+ | TD_enum of id * naming_scheme_opt * (id) list * bool (* enumeration type definition *)
+ | TD_register of id * atyp * atyp * ((index_range * id)) list (* register mutable bitfield type definition *)
type
val_spec_aux = (* Value type specification *)
- VS_val_spec of terminal * typschm * id
+ VS_val_spec of typschm * id
type
fundef_aux = (* Function definition *)
- FD_function of terminal * rec_opt * tannot_opt * effects_opt * (funcl * terminal) list
+ FD_function of rec_opt * tannot_opt * effects_opt * (funcl) list
type
@@ -379,12 +379,12 @@ def_aux = (* Top-level 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 * atyp * 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 * atyp * id (* scattered union definition member *)
- | DEF_scattered_end of terminal * id (* scattered definition end *)
+ | DEF_reg_dec of atyp * id (* register declaration *)
+ | DEF_scattered_function of rec_opt * tannot_opt * effects_opt * id (* scattered function definition header *)
+ | DEF_scattered_funcl of funcl (* scattered function definition clause *)
+ | DEF_scattered_variant of id * naming_scheme_opt * typquant (* scattered union definition header *)
+ | DEF_scattered_unioncl of id * atyp * id (* scattered union definition member *)
+ | DEF_scattered_end of id (* scattered definition end *)
type
@@ -394,33 +394,33 @@ def =
type
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 * string (* UTF8 strings *)
- | Typ_lib_enum of terminal * terminal * terminal * terminal (* natural numbers _ .. _+_-1, ordered by order *)
- | Typ_lib_enum1 of terminal * terminal * terminal (* sugar for \texttt{enum nexp 0 inc} *)
- | Typ_lib_enum2 of terminal * terminal * terminal * terminal * terminal (* sugar for \texttt{enum (nexp'-nexp+1) nexp inc} or \texttt{enum (nexp-nexp'+1) nexp' dec} *)
- | Typ_lib_vector of terminal * terminal * terminal * terminal * atyp (* vector of atyp, indexed by natural range *)
- | Typ_lib_vector2 of atyp * terminal * terminal * terminal (* sugar for vector indexed by [ atyp ] *)
- | Typ_lib_vector3 of atyp * terminal * terminal * terminal * terminal * terminal (* sugar for vector indexed by [ atyp.._ ] *)
- | Typ_lib_list of terminal * atyp (* list of atyp *)
- | Typ_lib_set of terminal * atyp (* finite set of atyp *)
- | Typ_lib_reg of terminal * atyp (* mutable register components holding atyp *)
+ Typ_lib_unit (* unit type with value $()$ *)
+ | Typ_lib_bool (* booleans $_$ and $_$ *)
+ | Typ_lib_bit (* pure bit values (not mutable bits) *)
+ | Typ_lib_nat (* natural numbers 0,1,2,... *)
+ | Typ_lib_string of string (* UTF8 strings *)
+ | Typ_lib_enum (* natural numbers _ .. _+_-1, ordered by order *)
+ | Typ_lib_enum1 (* sugar for \texttt{enum nexp 0 inc} *)
+ | Typ_lib_enum2 (* sugar for \texttt{enum (nexp'-nexp+1) nexp inc} or \texttt{enum (nexp-nexp'+1) nexp' dec} *)
+ | Typ_lib_vector of atyp (* vector of atyp, indexed by natural range *)
+ | Typ_lib_vector2 of atyp (* sugar for vector indexed by [ atyp ] *)
+ | Typ_lib_vector3 of atyp (* sugar for vector indexed by [ atyp.._ ] *)
+ | Typ_lib_list of atyp (* list of atyp *)
+ | Typ_lib_set of atyp (* finite set of atyp *)
+ | Typ_lib_reg of atyp (* mutable register components holding atyp *)
type
ctor_def_aux = (* Datatype constructor definition clause *)
- CT_ct of id * terminal * typschm
+ CT_ct of id * typschm
type
lexp_aux = (* lvalue expression *)
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 *)
+ | LEXP_vector of lexp * exp (* vector element *)
+ | LEXP_vector_range of lexp * exp * exp (* subvector *)
+ | LEXP_field of lexp * id (* struct field *)
and lexp =
LEXP_aux of lexp_aux * l
diff --git a/src/parser.mly b/src/parser.mly
index 19e66747..67a22a18 100644
--- a/src/parser.mly
+++ b/src/parser.mly
@@ -79,7 +79,7 @@ let vloc v = VS_aux(v, loc ())
let dloc d = DEF_aux(d,loc ())
let mk_typschm tq t s e = TypSchm_aux((TypSchm_ts(tq,t)),(locn s e))
-let mk_rec r i = (Rec_aux((Rec_rec (r)), locn i i))
+let mk_rec i = (Rec_aux((Rec_rec), locn i i))
let mk_recn _ = (Rec_aux((Rec_nonrec), Unknown))
let mk_typqn _ = (TypQ_aux(TypQ_no_forall,Unknown))
let mk_tannot tq t s e = Typ_annot_opt_aux(Typ_annot_opt_some(tq,t),(locn s e))
@@ -120,48 +120,48 @@ let star = "*"
/*Terminals with no content*/
-%token <Parse_ast.terminal> And As Bits Case Clause Const Default Effect Effects End Enum Else False
-%token <Parse_ast.terminal> Forall Function_ If_ In IN Let_ Member Nat Order Pure Rec Register
-%token <Parse_ast.terminal> Scattered Struct Switch Then True Type TYPE Typedef Union With Val
+%token And As Bits Case Clause Const Default Effect Effects End Enum Else False
+%token Forall Function_ If_ In IN Let_ Member Nat Order Pure Rec Register
+%token Scattered Struct Switch Then True Type TYPE Typedef Union With Val
-%token <Parse_ast.terminal> AND Div_ EOR Mod OR Quot Rem
+%token AND Div_ EOR Mod OR Quot Rem
-%token <Parse_ast.terminal> Bar Colon Comma Dot Eof Minus Semi Under
-%token <Parse_ast.terminal> Lcurly Rcurly Lparen Rparen Lsquare Rsquare
-%token <Parse_ast.terminal> BarBar BarGt BarSquare DotDot MinusGt LtBar SquareBar
+%token Bar Colon Comma Dot Eof Minus Semi Under
+%token Lcurly Rcurly Lparen Rparen Lsquare Rsquare
+%token BarBar BarGt BarSquare DotDot MinusGt LtBar SquareBar
/*Terminals with content*/
-%token <Parse_ast.terminal * string> Id
-%token <Parse_ast.terminal * int> Num
-%token <Parse_ast.terminal * string> String Bin Hex
+%token <string> Id
+%token <int> Num
+%token <string> String Bin Hex
-%token <Parse_ast.terminal * string> Amp At Carrot Div Eq Excl Gt Lt Plus Star Tilde
-%token <Parse_ast.terminal * string> AmpAmp CarrotCarrot ColonColon ColonEq EqDivEq EqEq ExclEq ExclExcl
-%token <Parse_ast.terminal * string> GtEq GtEqPlus GtGt GtGtGt GtPlus HashGtGt HashLtLt
-%token <Parse_ast.terminal * string> LtEq LtEqPlus LtGt LtLt LtLtLt LtPlus StarStar TildeCarrot
+%token <string> Amp At Carrot Div Eq Excl Gt Lt Plus Star Tilde
+%token <string> AmpAmp CarrotCarrot ColonColon ColonEq EqDivEq EqEq ExclEq ExclExcl
+%token <string> GtEq GtEqPlus GtGt GtGtGt GtPlus HashGtGt HashLtLt
+%token <string> LtEq LtEqPlus LtGt LtLt LtLtLt LtPlus StarStar TildeCarrot
-%token <Parse_ast.terminal * string> GtEqUnderS GtEqUnderSi GtEqUnderU GtEqUnderUi GtGtUnderU GtUnderS
-%token <Parse_ast.terminal * string> GtUnderSi GtUnderU GtUnderUi LtEqUnderS LtEqUnderSi LtEqUnderU
-%token <Parse_ast.terminal * string> LtEqUnderUi LtUnderS LtUnderSi LtUnderU LtUnderUi StarStarUnderS StarStarUnderSi StarUnderS
-%token <Parse_ast.terminal * string> StarUnderSi StarUnderU StarUnderUi TwoCarrot
+%token <string> GtEqUnderS GtEqUnderSi GtEqUnderU GtEqUnderUi GtGtUnderU GtUnderS
+%token <string> GtUnderSi GtUnderU GtUnderUi LtEqUnderS LtEqUnderSi LtEqUnderU
+%token <string> LtEqUnderUi LtUnderS LtUnderSi LtUnderU LtUnderUi StarStarUnderS StarStarUnderSi StarUnderS
+%token <string> StarUnderSi StarUnderU StarUnderUi TwoCarrot
-%token <Parse_ast.terminal * string> AmpI AtI CarrotI DivI EqI ExclI GtI LtI PlusI StarI TildeI
-%token <Parse_ast.terminal * string> AmpAmpI CarrotCarrotI ColonColonI ColonEqI EqDivEqI EqEqI ExclEqI ExclExclI
-%token <Parse_ast.terminal * string> GtEqI GtEqPlusI GtGtI GtGtGtI GtPlusI HashGtGtI HashLtLtI
-%token <Parse_ast.terminal * string> LtEqI LtEqPlusI LtGtI LtLtI LtLtLtI LtPlusI StarStarI TildeCarrotI
+%token <string> AmpI AtI CarrotI DivI EqI ExclI GtI LtI PlusI StarI TildeI
+%token <string> AmpAmpI CarrotCarrotI ColonColonI ColonEqI EqDivEqI EqEqI ExclEqI ExclExclI
+%token <string> GtEqI GtEqPlusI GtGtI GtGtGtI GtPlusI HashGtGtI HashLtLtI
+%token <string> LtEqI LtEqPlusI LtGtI LtLtI LtLtLtI LtPlusI StarStarI TildeCarrotI
-%token <Parse_ast.terminal * string> GtEqUnderSI GtEqUnderSiI GtEqUnderUI GtEqUnderUiI GtGtUnderUI GtUnderSI
-%token <Parse_ast.terminal * string> GtUnderSiI GtUnderUI GtUnderUiI LtEqUnderSI LtEqUnderSiI LtEqUnderUI
-%token <Parse_ast.terminal * string> LtEqUnderUiI LtUnderSI LtUnderSiI LtUnderUI LtUnderUiI StarStarUnderSI StarStarUnderSiI StarUnderSI
-%token <Parse_ast.terminal * string> StarUnderSiI StarUnderUI StarUnderUiI TwoCarrotI
+%token <string> GtEqUnderSI GtEqUnderSiI GtEqUnderUI GtEqUnderUiI GtGtUnderUI GtUnderSI
+%token <string> GtUnderSiI GtUnderUI GtUnderUiI LtEqUnderSI LtEqUnderSiI LtEqUnderUI
+%token <string> LtEqUnderUiI LtUnderSI LtUnderSiI LtUnderUI LtUnderUiI StarStarUnderSI StarStarUnderSiI StarUnderSI
+%token <string> StarUnderSiI StarUnderUI StarUnderUiI TwoCarrotI
%start file
%type <Parse_ast.defs> defs
%type <Parse_ast.atyp> typ
%type <Parse_ast.pat> pat
%type <Parse_ast.exp> exp
-%type <Parse_ast.defs * Parse_ast.terminal> file
+%type <Parse_ast.defs> file
%%
@@ -170,37 +170,37 @@ id:
| Id
{ idl (Id($1)) }
| Lparen At Rparen
- { Id_aux(DeIid($1,$2,$3),loc ()) }
+ { Id_aux(DeIid($2),loc ()) }
| Lparen Eq Rparen
- { Id_aux(DeIid($1,$2,$3),loc ()) }
+ { Id_aux(DeIid($2),loc ()) }
| Lparen IN Rparen
- { Id_aux(DeIid($1,($2,"In"),$3),loc ()) }
+ { Id_aux(DeIid("In"),loc ()) }
| Lparen BarBar Rparen
- { Id_aux(DeIid($1,($2,"||"),$3),loc ()) }
+ { Id_aux(DeIid("||"),loc ()) }
| Lparen ColonColon Rparen
- { Id_aux(DeIid($1,$2,$3),loc ()) }
+ { Id_aux(DeIid($2),loc ()) }
| Lparen Star Rparen
- { Id_aux(DeIid($1,$2,$3),loc ()) }
+ { Id_aux(DeIid($2),loc ()) }
| Lparen Plus Rparen
- { Id_aux(DeIid($1,$2,$3),loc ()) }
+ { Id_aux(DeIid($2),loc ()) }
| Lparen GtEq Rparen
- { Id_aux(DeIid($1,$2,$3),loc ()) }
+ { Id_aux(DeIid($2),loc ()) }
atomic_kind:
| TYPE
- { bkloc (BK_type($1)) }
+ { bkloc BK_type }
| Nat
- { bkloc (BK_nat($1)) }
+ { bkloc BK_nat }
| Order
- { bkloc (BK_order($1)) }
+ { bkloc BK_order }
| Effects
- { bkloc (BK_effects($1)) }
+ { bkloc BK_effects }
kind_help:
| atomic_kind
- { [ ($1,None) ] }
+ { [ $1 ] }
| atomic_kind MinusGt kind_help
- { ($1,$2)::$3 }
+ { $1::$3 }
kind:
| kind_help
@@ -209,40 +209,40 @@ kind:
effect:
| id
{ (match $1 with
- | Id_aux(Id(t,s),l) ->
+ | Id_aux(Id(s),l) ->
Effect_aux
((match s with
- | "rreg" -> (Effect_rreg t)
- | "wreg" -> (Effect_wreg t)
- | "rmem" -> (Effect_rmem t)
- | "wmem" -> (Effect_wmem t)
- | "undef" -> (Effect_undef t)
- | "unspec" -> (Effect_unspec t)
- | "nondet" -> (Effect_nondet t)
+ | "rreg" -> (Effect_rreg)
+ | "wreg" -> (Effect_wreg)
+ | "rmem" -> (Effect_rmem)
+ | "wmem" -> (Effect_wmem)
+ | "undef" -> (Effect_undef)
+ | "unspec" -> (Effect_unspec)
+ | "nondet" -> (Effect_nondet)
| _ -> raise (Parse_error_locn (l,"Invalid effect"))),l)
| _ -> raise (Parse_error_locn ((loc ()),"Invalid effect"))) }
effect_list:
| effect
- { [($1,None)] }
+ { [$1] }
| effect Comma effect_list
- { ($1,$2)::$3 }
+ { $1::$3 }
effect_typ:
| Effect id
- { tloc (ATyp_efid($1,$2)) }
+ { tloc (ATyp_efid($2)) }
| Effect Lcurly effect_list Rcurly
- { tloc (ATyp_set($1,$2,$3,$4)) }
+ { tloc (ATyp_set($3)) }
| Pure
- { tloc (ATyp_set($1,None,[],None)) }
+ { tloc (ATyp_set([])) }
atomic_typ:
| id
{ tloc (ATyp_id $1) }
| Num
- { tloc (ATyp_constant(fst $1, snd $1)) }
+ { tloc (ATyp_constant $1) }
| Under
- { tloc (ATyp_wild($1)) }
+ { tloc (ATyp_wild) }
| effect_typ
{ $1 }
| Lparen typ Rparen
@@ -274,79 +274,78 @@ app_typ:
star_typ_list:
| app_typ
- { [($1,None)] }
+ { [$1] }
| app_typ Star star_typ_list
- { ($1,fst $2)::$3 }
+ { $1::$3 }
star_typ:
| star_typ_list
{ match $1 with
| [] -> assert false
- | [(t,None)] -> t
- | [(t,Some _)] -> assert false
+ | [t] -> t
| ts -> tloc (ATyp_tup(ts)) }
exp_typ:
| star_typ
{ $1 }
| Num StarStar typ
- { if (2 = (snd $1))
- then tloc (ATyp_exp((fst $1),(fst $2),$3))
+ { if (2 = $1)
+ then tloc (ATyp_exp($3))
else raise (Parse_error_locn(loc (), "Only 2 is a valid exponent base in Nats")) }
nexp_typ:
| exp_typ
{ $1 }
| atomic_typ Plus typ
- { tloc (ATyp_sum($1,fst $2,$3)) }
+ { tloc (ATyp_sum($1,$3)) }
typ:
| nexp_typ
{ $1 }
| star_typ MinusGt atomic_typ effect_typ
- { tloc (ATyp_fn($1,$2,$3,$4)) }
+ { tloc (ATyp_fn($1,$3,$4)) }
lit:
| True
- { lloc (L_true($1)) }
+ { lloc L_true }
| False
- { lloc (L_false($1)) }
+ { lloc L_false }
| Num
- { lloc (L_num(fst $1, snd $1)) }
+ { lloc (L_num $1) }
| String
- { lloc (L_string(fst $1, snd $1)) }
+ { lloc (L_string $1) }
| Lparen Rparen
- { lloc (L_unit($1,$2)) }
+ { lloc L_unit }
| Bin
- { lloc (L_bin(fst $1, snd $1)) }
+ { lloc (L_bin $1) }
| Hex
- { lloc (L_hex(fst $1, snd $1)) }
+ { lloc (L_hex $1) }
atomic_pat:
| lit
- { ploc (P_lit($1)) }
+ { ploc (P_lit $1) }
| Under
- { ploc (P_wild($1)) }
+ { ploc P_wild }
| Lparen pat As id Rparen
- { ploc (P_as($1,$2,$3,$4,$5)) }
+ { ploc (P_as($2,$4)) }
/* Because of ( id id ) being either application or type casts, this is inherently ambiguous */
/* | Lparen atomic_typ pat Rparen
- { ploc (P_typ($1,$2,$3,$4)) } */
+ { ploc (P_typ($2,$3)) } */
| id
{ ploc (P_app($1,[])) }
| Lcurly fpats Rcurly
- { ploc (P_record($1,fst $2,fst (snd $2),snd (snd $2),$3)) }
+ { ploc (P_record((fst $2, snd $2))) }
| Lsquare pat Rsquare
- { ploc (P_vector($1,[($2,None)],$3)) }
+ { ploc (P_vector([$2])) }
| Lsquare comma_pats Rsquare
- { ploc (P_vector($1,$2,$3)) }
+ { ploc (P_vector($2)) }
| Lsquare npats Rsquare
- { ploc (P_vector_indexed($1,$2,$3)) }
+ { ploc (P_vector_indexed($2)) }
| Lparen comma_pats Rparen
- { ploc (P_tup($1,$2,$3)) }
+ { ploc (P_tup($2)) }
| SquareBar comma_pats BarSquare
- { ploc (P_list($1,$2,$3)) }
+ { ploc (P_list($2)) }
| Lparen pat Rparen
{ $2 }
@@ -358,9 +357,9 @@ app_pat:
pat_colons:
| atomic_pat Colon atomic_pat
- { ([($1,$2);($3,None)]) }
+ { ([$1;$3]) }
| atomic_pat Colon pat_colons
- { (($1,$2)::$3) }
+ { ($1::$3) }
pat:
| app_pat
@@ -370,35 +369,35 @@ pat:
comma_pats:
| atomic_pat Comma atomic_pat
- { [($1,$2);($3,None)] }
+ { [$1;$3] }
| atomic_pat Comma comma_pats
- { ($1,$2)::$3 }
+ { $1::$3 }
fpat:
| id Eq pat
- { fploc (FP_Fpat($1,fst $2,$3)) }
+ { fploc (FP_Fpat($1,$3)) }
fpats:
| fpat
- { ([($1,None)], (None,false)) }
+ { ([$1], false) }
| fpat Semi
- { ([($1,None)], ($2,true)) }
+ { ([$1], true) }
| fpat Semi fpats
- { (($1,$2)::fst $3, snd $3) }
+ { ($1::fst $3, snd $3) }
npat:
| Num Eq pat
- { ($1,fst $2,$3) }
+ { ($1,$3) }
npats:
| npat
- { ([($1,None)]) }
+ { [$1] }
| npat Comma npats
- { (($1,$2)::$3) }
+ { ($1::$3) }
atomic_exp:
| Lcurly semi_exps Rcurly
- { eloc (E_block($1,$2,$3)) }
+ { eloc (E_block $2) }
| id
{ eloc (E_id($1)) }
| lit
@@ -406,31 +405,31 @@ atomic_exp:
| Lparen exp Rparen
{ $2 }
| Lparen comma_exps Rparen
- { eloc (E_tuple($1,$2,$3)) }
+ { eloc (E_tuple($2)) }
| Lsquare comma_exps Rsquare
- { eloc (E_vector($1,$2,$3)) }
+ { eloc (E_vector($2)) }
| Lsquare exp With atomic_exp Eq exp Rsquare
- { eloc (E_vector_update($1,$2,$3,$4,fst $5,$6,$7)) }
+ { eloc (E_vector_update($2,$4,$6)) }
| Lsquare exp With atomic_exp Colon atomic_exp Eq exp Rsquare
- { eloc (E_vector_update_subrange($1,$2,$3,$4,$5,$6,fst $7,$8,$9)) }
+ { eloc (E_vector_update_subrange($2,$4,$6,$8)) }
| SquareBar comma_exps BarSquare
- { eloc (E_list($1,$2,$3)) }
+ { eloc (E_list($2)) }
| Switch exp Lcurly case_exps Rcurly
- { eloc (E_case($1,$2,$3,$4,$5)) }
+ { eloc (E_case($2,$4)) }
field_exp:
| atomic_exp
{ $1 }
| atomic_exp Dot id
- { eloc (E_field($1,$2,$3)) }
+ { eloc (E_field($1,$3)) }
vaccess_exp:
| field_exp
{ $1 }
| atomic_exp Lsquare exp Rsquare
- { eloc (E_vector_access($1,$2,$3,$4)) }
+ { eloc (E_vector_access($1,$3)) }
| atomic_exp Lsquare exp DotDot exp Rsquare
- { eloc (E_vector_subrange($1,$2,$3,$4,$5,$6)) }
+ { eloc (E_vector_subrange($1,$3,$5)) }
app_exp:
| vaccess_exp
@@ -438,13 +437,13 @@ app_exp:
| id Lparen exp Rparen
{ eloc (E_app((E_aux((E_id $1),locn 1 1)),[$3])) }
| id Lparen comma_exps Rparen
- { eloc (E_app((E_aux((E_id $1),locn 1 1)),[(E_aux((E_tuple($2,$3,$4)),locn 2 4))])) }
+ { eloc (E_app((E_aux((E_id $1),locn 1 1)),$3)) }
right_atomic_exp:
| If_ exp Then exp Else exp
- { eloc (E_if($1,$2,$3,$4,$5,$6)) }
+ { eloc (E_if($2,$4,$6)) }
| letbind In exp
- { eloc (E_let($1,$2,$3)) }
+ { eloc (E_let($1,$3)) }
starstar_exp:
| app_exp
@@ -486,13 +485,13 @@ cons_exp:
| plus_exp
{ $1 }
| plus_exp ColonColon cons_exp
- { eloc (E_cons($1,fst $2,$3)) }
+ { eloc (E_cons($1,$3)) }
cons_right_atomic_exp:
| plus_right_atomic_exp
{ $1 }
| plus_exp ColonColon cons_right_atomic_exp
- { eloc (E_cons($1,fst $2,$3)) }
+ { eloc (E_cons($1,$3)) }
at_exp:
| cons_exp
@@ -515,9 +514,9 @@ eq_exp:
| eq_exp GtEq at_exp
{ eloc (E_app_infix ($1,Id_aux(Id($2), locn 2 2), $3)) }
| eq_exp IN at_exp
- { eloc (E_app_infix($1,Id_aux(Id(($2,"In")), locn 2 2), $3)) }
+ { eloc (E_app_infix($1,Id_aux(Id("In"), locn 2 2), $3)) }
| eq_exp ColonEq at_exp
- { eloc (E_assign($1,fst $2,$3)) }
+ { eloc (E_assign($1,$3)) }
eq_right_atomic_exp:
| at_right_atomic_exp
@@ -525,7 +524,7 @@ eq_right_atomic_exp:
| eq_exp Eq at_right_atomic_exp
{ eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) }
| eq_exp ColonEq at_right_atomic_exp
- { eloc (E_assign($1,fst $2,$3)) }
+ { eloc (E_assign($1,$3)) }
and_exp:
| eq_exp
@@ -543,14 +542,14 @@ or_exp:
| and_exp
{ $1 }
| and_exp BarBar or_exp
- { eloc (E_app_infix($1,Id_aux(Id(($2,"||")), locn 2 2), $3)) }
+ { eloc (E_app_infix($1,Id_aux(Id("||"), locn 2 2), $3)) }
or_right_atomic_exp:
| and_right_atomic_exp
{ $1 }
| and_exp BarBar or_right_atomic_exp
- { eloc (E_app_infix($1,Id_aux(Id(($2,"||")), locn 2 2), $3)) }
+ { eloc (E_app_infix($1,Id_aux(Id("||"), locn 2 2), $3)) }
exp:
| or_exp
@@ -561,17 +560,17 @@ exp:
comma_exps:
| exp Comma exp
- { [($1,$2);($3,None)] }
+ { [$1;$3] }
| exp Comma comma_exps
- { ($1,$2)::$3 }
+ { $1::$3 }
semi_exps_help:
| exp
- { [($1,None)] }
+ { [$1] }
| exp Semi
- { [($1,$2)] }
+ { [$1] }
| exp Semi semi_exps_help
- { ($1,$2)::$3 }
+ { $1::$3 }
semi_exps:
|
@@ -581,7 +580,7 @@ semi_exps:
case_exp:
| Case patsexp
- { ($1,$2) }
+ { $2 }
case_exps:
| case_exp
@@ -591,62 +590,62 @@ case_exps:
patsexp:
| atomic_pat MinusGt exp
- { peloc (Pat_exp($1,$2,$3)) }
+ { peloc (Pat_exp($1,$3)) }
letbind:
| Let_ atomic_pat Eq exp
- { lbloc (LB_val_implicit($1,$2,fst $3,$4)) }
+ { lbloc (LB_val_implicit($2,$4)) }
| Let_ typquant atomic_typ atomic_pat Eq exp
- { lbloc (LB_val_explicit((mk_typschm $2 $3 2 3),$4,fst $5,$6)) }
+ { lbloc (LB_val_explicit((mk_typschm $2 $3 2 3),$4,$6)) }
/* This is ambiguous causing 4 shift/reduce and 5 reduce/reduce conflicts because the parser can't tell until the end of typ whether it was parsing a type or a pattern, and this seem to be too late. Solutions are to have a different keyword for this and the above solution besides let (while still absolutely having a keyword here)
| Let_ atomic_typ atomic_pat Eq exp
{ } */
funcl:
| id atomic_pat Eq exp
- { funclloc (FCL_Funcl($1,$2,fst $3,$4)) }
+ { funclloc (FCL_Funcl($1,$2,$4)) }
funcl_ands:
| funcl
- { [$1,None] }
+ { [$1] }
| funcl And funcl_ands
- { ($1,$2)::$3 }
+ { $1::$3 }
/* This causes ambiguity because without a type quantifier it's unclear whether the first id is a function name or a type name for the optional types.*/
fun_def:
| Function_ Rec typquant atomic_typ effect_typ funcl_ands
- { funloc (FD_function($1,mk_rec $2 2, mk_tannot $3 $4 3 4, mk_eannot $5 5, $6)) }
+ { funloc (FD_function(mk_rec 2, mk_tannot $3 $4 3 4, mk_eannot $5 5, $6)) }
| Function_ Rec typquant atomic_typ funcl_ands
- { funloc (FD_function($1,mk_rec $2 2, mk_tannot $3 $4 3 4, mk_eannotn (), $5)) }
+ { funloc (FD_function(mk_rec 2, mk_tannot $3 $4 3 4, mk_eannotn (), $5)) }
| Function_ Rec atomic_typ effect_typ funcl_ands
- { funloc (FD_function($1,mk_rec $2 2, mk_tannot (mk_typqn ()) $3 3 3, mk_eannot $4 4, $5)) }
+ { funloc (FD_function(mk_rec 2, mk_tannot (mk_typqn ()) $3 3 3, mk_eannot $4 4, $5)) }
| Function_ Rec atomic_typ funcl_ands
{ match $3 with
| ATyp_aux(ATyp_efid _, _) | ATyp_aux(ATyp_set _, _) ->
- funloc (FD_function($1,mk_rec $2 2,mk_tannotn (), mk_eannot $3 3, $4))
+ funloc (FD_function(mk_rec 2,mk_tannotn (), mk_eannot $3 3, $4))
| _ ->
- funloc (FD_function($1,mk_rec $2 2,mk_tannot (mk_typqn ()) $3 3 3, mk_eannotn (), $4)) }
+ funloc (FD_function(mk_rec 2,mk_tannot (mk_typqn ()) $3 3 3, mk_eannotn (), $4)) }
| Function_ Rec funcl_ands
- { funloc (FD_function($1,mk_rec $2 2, mk_tannotn (), mk_eannotn (), $3)) }
+ { funloc (FD_function(mk_rec 2, mk_tannotn (), mk_eannotn (), $3)) }
| Function_ typquant atomic_typ effect_typ funcl_ands
- { funloc (FD_function($1,mk_recn (), mk_tannot $2 $3 2 3, mk_eannot $4 4, $5)) }
+ { funloc (FD_function(mk_recn (), mk_tannot $2 $3 2 3, mk_eannot $4 4, $5)) }
| Function_ typquant atomic_typ funcl_ands
- { funloc (FD_function($1,mk_recn (), mk_tannot $2 $3 2 2, mk_eannotn (), $4)) }
+ { funloc (FD_function(mk_recn (), mk_tannot $2 $3 2 2, mk_eannotn (), $4)) }
| Function_ atomic_typ funcl_ands
{ match $2 with
| ATyp_aux(ATyp_efid _, _) | ATyp_aux(ATyp_set _, _) ->
- funloc (FD_function($1,mk_recn (),mk_tannotn (), mk_eannot $2 2, $3))
+ funloc (FD_function(mk_recn (),mk_tannotn (), mk_eannot $2 2, $3))
| _ ->
- funloc (FD_function($1,mk_recn (),mk_tannot (mk_typqn ()) $2 2 2, mk_eannotn (), $3)) }
+ funloc (FD_function(mk_recn (),mk_tannot (mk_typqn ()) $2 2 2, mk_eannotn (), $3)) }
| Function_ funcl_ands
- { funloc (FD_function($1,mk_recn (), mk_tannotn (), mk_eannotn (), $2)) }
+ { funloc (FD_function(mk_recn (), mk_tannotn (), mk_eannotn (), $2)) }
val_spec:
| Val typquant atomic_typ id
- { vloc (VS_val_spec($1,mk_typschm $2 $3 2 3,$4)) }
+ { vloc (VS_val_spec(mk_typschm $2 $3 2 3,$4)) }
| Val atomic_typ id
- { vloc (VS_val_spec($1,mk_typschm (mk_typqn ()) $2 2 2,$3)) }
+ { vloc (VS_val_spec(mk_typschm (mk_typqn ()) $2 2 2,$3)) }
kinded_id:
| id
@@ -664,50 +663,50 @@ kinded_ids:
nums:
| Num
- { [($1,None)] }
+ { [$1] }
| Num Comma nums
- { ($1,$2)::$3 }
+ { $1::$3 }
nexp_constraint:
| typ Eq typ
- { NC_aux(NC_fixed($1,(fst $2),$3), loc () ) }
+ { NC_aux(NC_fixed($1,$3), loc () ) }
| typ GtEq typ
- { NC_aux(NC_bounded_ge($1,(fst $2),$3), loc () ) }
+ { NC_aux(NC_bounded_ge($1,$3), loc () ) }
| typ LtEq typ
- { NC_aux(NC_bounded_le($1,(fst $2),$3), loc () ) }
+ { NC_aux(NC_bounded_le($1,$3), loc () ) }
| id IN Lcurly nums Rcurly
- { NC_aux(NC_nat_set_bounded($1,$2,$3,$4,$5), loc ()) }
+ { NC_aux(NC_nat_set_bounded($1,$4), loc ()) }
nexp_constraints:
| nexp_constraint
- { [($1,None)] }
+ { [$1] }
| nexp_constraint Comma nexp_constraints
- { ($1,$2)::$3 }
+ { $1::$3 }
typquant:
/* This is a syntactic change to avoid 6 significant shift/reduce conflicts instead of the Dot */
| Forall kinded_ids Amp nexp_constraints Dot
- { typql(TypQ_tq($1,$2,fst $3,$4,$5)) }
+ { typql(TypQ_tq($2,$4)) }
| Forall kinded_ids Dot
- { typql(TypQ_no_constraint($1,$2,$3)) }
+ { typql(TypQ_no_constraint($2)) }
name_sect:
| Lsquare Id Eq String Rsquare
- { Name_sect_aux(Name_sect_some($1,(fst $2),fst $3,(fst $4),(snd $4),$5), loc ()) }
+ { Name_sect_aux(Name_sect_some($4), loc ()) }
c_def_body:
| typ id
- { [(($1,$2),None)],(None,false) }
+ { [($1,$2)],false }
| typ id Semi
- { [(($1,$2),None)],($3,true) }
+ { [($1,$2)],true }
| typ id Semi c_def_body
- { (($1,$2),$3)::(fst $4), snd $4 }
+ { ($1,$2)::(fst $4), snd $4 }
index_range_atomic:
| Num
{ irloc (BF_single($1)) }
| Num DotDot Num
- { irloc (BF_range($1,$2,$3)) }
+ { irloc (BF_range($1,$3)) }
| Lparen index_range Rparen
{ $2 }
@@ -715,95 +714,95 @@ index_range:
| index_range_atomic
{ $1 }
| index_range_atomic Comma index_range
- { irloc(BF_concat($1,$2,$3)) }
+ { irloc(BF_concat($1,$3)) }
r_id_def:
| index_range Colon id
- { $1,$2,$3 }
+ { $1,$3 }
r_def_body:
| r_id_def
- { [($1,None)] }
+ { [$1] }
| r_id_def Semi
- { [$1,$2] }
+ { [$1] }
| r_id_def Semi r_def_body
- { ($1,$2)::$3 }
+ { $1::$3 }
type_def:
| Typedef id name_sect Eq typquant typ
- { tdloc (TD_abbrev($1,$2,$3,fst $4,mk_typschm $5 $6 5 6)) }
+ { tdloc (TD_abbrev($2,$3,mk_typschm $5 $6 5 6)) }
| Typedef id name_sect Eq typ
- { tdloc (TD_abbrev($1,$2,$3,fst $4,mk_typschm (mk_typqn ()) $5 5 5)) }
+ { tdloc (TD_abbrev($2,$3,mk_typschm (mk_typqn ()) $5 5 5)) }
| Typedef id Eq typquant typ
- { tdloc (TD_abbrev($1,$2,mk_namesectn (),fst $3, mk_typschm $4 $5 4 5))}
+ { tdloc (TD_abbrev($2,mk_namesectn (), mk_typschm $4 $5 4 5))}
| Typedef id Eq typ
- { tdloc (TD_abbrev($1,$2,mk_namesectn (),fst $3,mk_typschm (mk_typqn ()) $4 4 4)) }
+ { tdloc (TD_abbrev($2,mk_namesectn (),mk_typschm (mk_typqn ()) $4 4 4)) }
/* The below adds 4 shift/reduce conflicts. Due to c_def_body and confusions in id id and parens */
| Typedef id name_sect Eq Const Struct typquant Lcurly c_def_body Rcurly
- { tdloc (TD_record($1,$2,$3,fst $4,$5,$6,$7,$8,fst $9, fst (snd $9), snd (snd $9), $10)) }
+ { tdloc (TD_record($2,$3,$7,fst $9, snd $9)) }
| Typedef id name_sect Eq Const Struct Lcurly c_def_body Rcurly
- { tdloc (TD_record($1,$2,$3,fst $4,$5,$6,(mk_typqn ()), $7, fst $8, fst (snd $8), snd (snd $8), $9)) }
+ { tdloc (TD_record($2,$3,(mk_typqn ()), fst $8, snd $8)) }
| Typedef id Eq Const Struct typquant Lcurly c_def_body Rcurly
- { tdloc (TD_record($1,$2,mk_namesectn (), fst $3, $4, $5, $6, $7, fst $8, fst (snd $8), snd (snd $8), $9)) }
+ { tdloc (TD_record($2,mk_namesectn (), $6, fst $8, snd $8)) }
| Typedef id Eq Const Struct Lcurly c_def_body Rcurly
- { tdloc (TD_record($1,$2, mk_namesectn (), fst $3, $4, $5, mk_typqn (), $6, fst $7, fst (snd $7), snd (snd $7), $8)) }
+ { tdloc (TD_record($2, mk_namesectn (), mk_typqn (), fst $7, snd $7)) }
| Typedef id name_sect Eq Const Union typquant Lcurly c_def_body Rcurly
- { tdloc (TD_variant($1,$2,$3,fst $4, $5, $6, $7, $8, fst $9, fst (snd $9), snd (snd $9), $10)) }
+ { tdloc (TD_variant($2,$3, $7, fst $9, snd $9)) }
| Typedef id Eq Const Union typquant Lcurly c_def_body Rcurly
- { tdloc (TD_variant($1,$2,mk_namesectn (), fst $3, $4, $5, $6, $7, fst $8, fst (snd $8), snd (snd $8), $9)) }
+ { tdloc (TD_variant($2,mk_namesectn (), $6, fst $8, snd $8)) }
| Typedef id name_sect Eq Const Union Lcurly c_def_body Rcurly
- { tdloc (TD_variant($1, $2, $3, fst $4, $5, $6, mk_typqn (), $7, fst $8, fst (snd $8), snd (snd $8), $9)) }
+ { tdloc (TD_variant($2, $3, mk_typqn (), fst $8, snd $8)) }
| Typedef id Eq Const Union Lcurly c_def_body Rcurly
- { tdloc (TD_variant($1,$2, mk_namesectn (), fst $3, $4, $5, mk_typqn (), $6, fst $7, fst (snd $7), snd (snd $7), $8)) }
+ { tdloc (TD_variant($2, mk_namesectn (), mk_typqn (), fst $7, snd $7)) }
| Typedef id Eq Register Bits Lsquare typ Colon typ Rsquare Lcurly r_def_body Rcurly
- { tdloc (TD_register($1,$2,fst $3, $4, $5, $6, $7, $8, $9, $10, $11, $12, $13)) }
+ { tdloc (TD_register($2, $7, $9, $12)) }
default_typ:
| Default atomic_kind id
- { defloc (DT_kind($1,$2,$3)) }
+ { defloc (DT_kind($2,$3)) }
| Default typquant atomic_typ id
- { defloc (DT_typ($1,(mk_typschm $2 $3 2 3),$4)) }
+ { defloc (DT_typ((mk_typschm $2 $3 2 3),$4)) }
| Default atomic_typ id
- { defloc (DT_typ($1,(mk_typschm (mk_typqn ()) $2 2 2),$3)) }
+ { defloc (DT_typ((mk_typschm (mk_typqn ()) $2 2 2),$3)) }
scattered_def:
| Function_ Rec typquant atomic_typ effect_typ id
- { (DEF_scattered_function(None,$1,mk_rec $2 2, mk_tannot $3 $4 3 4, mk_eannot $5 5, $6)) }
+ { (DEF_scattered_function(mk_rec 2, mk_tannot $3 $4 3 4, mk_eannot $5 5, $6)) }
| Function_ Rec atomic_typ effect_typ id
- { (DEF_scattered_function(None,$1,mk_rec $2 2, mk_tannot (mk_typqn ()) $3 3 3, mk_eannot $4 4, $5)) }
+ { (DEF_scattered_function(mk_rec 2, mk_tannot (mk_typqn ()) $3 3 3, mk_eannot $4 4, $5)) }
| Function_ Rec typquant atomic_typ id
- { (DEF_scattered_function(None,$1,mk_rec $2 2, mk_tannot $3 $4 3 4, mk_eannotn (), $5)) }
+ { (DEF_scattered_function(mk_rec 2, mk_tannot $3 $4 3 4, mk_eannotn (), $5)) }
| Function_ Rec atomic_typ id
{ match $3 with
| (ATyp_aux(ATyp_efid _, _)) | (ATyp_aux(ATyp_set _, _)) ->
- (DEF_scattered_function(None,$1,mk_rec $2 2, mk_tannotn (), mk_eannot $3 3, $4))
+ (DEF_scattered_function(mk_rec 2, mk_tannotn (), mk_eannot $3 3, $4))
| _ ->
- (DEF_scattered_function(None,$1,mk_rec $2 2,mk_tannot (mk_typqn ()) $3 3 3, mk_eannotn (), $4)) }
+ (DEF_scattered_function(mk_rec 2,mk_tannot (mk_typqn ()) $3 3 3, mk_eannotn (), $4)) }
| Function_ Rec id
- { (DEF_scattered_function(None,$1,mk_rec $2 2,mk_tannotn (), mk_eannotn (),$3)) }
+ { (DEF_scattered_function(mk_rec 2,mk_tannotn (), mk_eannotn (),$3)) }
| Function_ typquant atomic_typ effect_typ id
- { (DEF_scattered_function(None,$1,mk_recn (),mk_tannot $2 $3 2 3, mk_eannot $4 4, $5)) }
+ { (DEF_scattered_function(mk_recn (),mk_tannot $2 $3 2 3, mk_eannot $4 4, $5)) }
| Function_ atomic_typ effect_typ id
- { (DEF_scattered_function(None,$1,mk_recn (), mk_tannot (mk_typqn ()) $2 2 2, mk_eannot $3 3, $4)) }
+ { (DEF_scattered_function(mk_recn (), mk_tannot (mk_typqn ()) $2 2 2, mk_eannot $3 3, $4)) }
| Function_ typquant atomic_typ id
- { (DEF_scattered_function(None,$1,mk_recn (), mk_tannot $2 $3 2 3, mk_eannotn (), $4)) }
+ { (DEF_scattered_function(mk_recn (), mk_tannot $2 $3 2 3, mk_eannotn (), $4)) }
| Function_ atomic_typ id
{ match $2 with
| (ATyp_aux(ATyp_efid _, _)) | (ATyp_aux(ATyp_set _, _)) ->
- (DEF_scattered_function(None,$1,mk_recn (), mk_tannotn (), mk_eannot $2 2, $3))
+ (DEF_scattered_function(mk_recn (), mk_tannotn (), mk_eannot $2 2, $3))
| _ ->
- (DEF_scattered_function(None,$1,mk_recn (), mk_tannot (mk_typqn ()) $2 2 2, mk_eannotn (), $3)) }
+ (DEF_scattered_function(mk_recn (), mk_tannot (mk_typqn ()) $2 2 2, mk_eannotn (), $3)) }
| Function_ id
- { (DEF_scattered_function(None,$1,mk_recn (), mk_tannotn (), mk_eannotn (), $2)) }
+ { (DEF_scattered_function(mk_recn (), mk_tannotn (), mk_eannotn (), $2)) }
| Typedef id name_sect Eq Const Union typquant
- { (DEF_scattered_variant(None,$1,$2,$3,fst $4,$5,$6,$7)) }
+ { (DEF_scattered_variant($2,$3,$7)) }
| Typedef id Eq Const Union typquant
- { (DEF_scattered_variant(None,$1,$2,(mk_namesectn ()),fst $3,$4,$5,$6)) }
+ { (DEF_scattered_variant($2,(mk_namesectn ()),$6)) }
| Typedef id name_sect Eq Const Union
- { (DEF_scattered_variant(None,$1,$2,$3,fst $4,$5,$6,mk_typqn ())) }
+ { (DEF_scattered_variant($2,$3,mk_typqn ())) }
| Typedef id Eq Const Union
- { (DEF_scattered_variant(None,$1,$2,mk_namesectn (),fst $3,$4,$5,mk_typqn ())) }
+ { (DEF_scattered_variant($2,mk_namesectn (),mk_typqn ())) }
def:
| type_def
@@ -817,18 +816,15 @@ def:
| default_typ
{ dloc (DEF_default($1)) }
| Register atomic_typ id
- { dloc (DEF_reg_dec($1,$2,$3)) }
+ { dloc (DEF_reg_dec($2,$3)) }
| Scattered scattered_def
- { dloc (match ($2) with
- | DEF_scattered_function(_,f,r,t,e,i) -> DEF_scattered_function($1,f,r,t,e,i)
- | DEF_scattered_variant(_,t,i,n,e,c,u,ty) -> DEF_scattered_variant($1,t,i,n,e,c,u,ty)
- | _ -> assert false) }
+ { dloc $2 }
| Function_ Clause funcl
- { dloc (DEF_scattered_funcl($1,$2,$3)) }
+ { dloc (DEF_scattered_funcl($3)) }
| Union id Member atomic_typ id
- { dloc (DEF_scattered_unioncl($1,$2,$3,$4,$5)) }
+ { dloc (DEF_scattered_unioncl($2,$4,$5)) }
| End id
- { dloc (DEF_scattered_end($1,$2)) }
+ { dloc (DEF_scattered_end($2)) }
defs_help:
| def
@@ -842,5 +838,5 @@ defs:
file:
| defs Eof
- { ($1,$2) }
+ { $1 }
diff --git a/src/process_file.ml b/src/process_file.ml
index 850a80f2..a674c66f 100644
--- a/src/process_file.ml
+++ b/src/process_file.ml
@@ -56,9 +56,9 @@ let get_lexbuf fn =
Lexing.pos_cnum = 0; };
lexbuf
-let parse_file (f : string) : (Parse_ast.defs * Parse_ast.lex_skips) =
+let parse_file (f : string) : Parse_ast.defs =
let lexbuf = get_lexbuf f in
- Parser.file (Lexer.token []) lexbuf
+ Parser.file Lexer.token lexbuf
(* try
Parser.file (Lexer.token []) lexbuf
with
diff --git a/src/process_file.mli b/src/process_file.mli
index b7b70def..1622d902 100644
--- a/src/process_file.mli
+++ b/src/process_file.mli
@@ -46,7 +46,7 @@
(* open Typed_ast *)
-val parse_file : string -> Parse_ast.defs * Parse_ast.lex_skips
+val parse_file : string -> Parse_ast.defs
(* type instances = Types.instance list Types.Pfmap.t
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-27 07:37:33 +0000