From 0363a325ca6c498e086519c4ecaf1f51dbff7f64 Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Fri, 30 Nov 2018 18:54:42 +0000 Subject: Parser tweaks and fixes - Completely remove the nexp = nexp syntax in favour of nexp == nexp. All our existing specs have already switched over. As part of this fix every test that used the old syntax, and update the generated aarch64 specs - Remove the `type when constraint` syntax. It just makes changing the parser in any way really awkward. - Change the syntax for declaring new types with multiple type parameters from: type foo('a : Type) ('n : Int), constraint = ... to type foo('a: Type, 'n: Int), constraint = ... This makes type declarations mimic function declarations, and makes the syntax for declaring types match the syntax for using types, as foo is used as foo(type, nexp). None of our specifications use types with multiple type parameters so this change doesn't actually break anything, other than some tests. The brackets around the type parameters are now mandatory. - Experiment with splitting Type/Order type parameters from Int type parameters in the parser. Currently in a type bar(x, y, z) all of x, y, and z could be either numeric expressions, orders, or types. This means that in the parser we are severely restricted in what we can parse in numeric expressions because everything has to be parseable as a type (atyp) - it also means we can't introduce boolean type variables/expressions or other minisail features (like removing ticks from type variables!) because we are heavily constrained by what we can parse unambigiously due to how these different type parameters can be mixed and interleaved. There is now experimental syntax: vector::<'o, 'a>('n) <--> vector('n, 'o, 'a) which splits the type argument list into two between Type/Order-polymorphic arguments and Int-polymorphic arguments. The exact choice of delimiters isn't set in stone - ::< and > match generics in Rust. The obvious choices of < and > / [ and ] are ambigious in various ways. Using this syntax right now triggers a warning. - Fix undefined behaviour in C compilation when concatenating a 0-length vector with a 64-length vector. --- src/c_backend.ml | 3 ++ src/lexer.mll | 1 + src/parser.mly | 94 +++++++++++++++++++++++++----------------------- src/pretty_print_sail.ml | 31 +++++++++++++--- 4 files changed, 79 insertions(+), 50 deletions(-) (limited to 'src') diff --git a/src/c_backend.ml b/src/c_backend.ml index 326f742a..2f57a802 100644 --- a/src/c_backend.ml +++ b/src/c_backend.ml @@ -496,6 +496,9 @@ let analyze_primop' ctx id args typ = (* Optimized routines for all combinations of fixed and small bits appends, where the result is guaranteed to be smaller than 64. *) + | "append", [AV_C_fragment (vec1, _, CT_fbits (0, ord1)); AV_C_fragment (vec2, _, CT_fbits (n2, ord2)) as v2] + when ord1 = ord2 -> + AE_val v2 | "append", [AV_C_fragment (vec1, _, CT_fbits (n1, ord1)); AV_C_fragment (vec2, _, CT_fbits (n2, ord2))] when ord1 = ord2 && n1 + n2 <= 64 -> AE_val (AV_C_fragment (F_op (F_op (vec1, "<<", v_int n2), "|", vec2), typ, CT_fbits (n1 + n2, ord1))) diff --git a/src/lexer.mll b/src/lexer.mll index f5a982eb..a1f3ace2 100644 --- a/src/lexer.mll +++ b/src/lexer.mll @@ -217,6 +217,7 @@ rule token = parse | "@" { (At "@") } | "2" ws "^" { TwoCaret } | "^" { (Caret(r"^")) } + | "::<" { ColonColonLt } | "::" { ColonColon(r "::") } (* | "^^" { CaretCaret(r "^^") } *) | "~~" { TildeTilde(r "~~") } diff --git a/src/parser.mly b/src/parser.mly index fec38669..8287060c 100644 --- a/src/parser.mly +++ b/src/parser.mly @@ -133,6 +133,8 @@ let mk_tannot typq typ n m = Typ_annot_opt_aux(Typ_annot_opt_some (typq, typ), l let mk_eannotn = Effect_opt_aux(Effect_opt_pure,Unknown) let mk_namesectn = Name_sect_aux(Name_sect_none,Unknown) +let mk_typq kopts nc n m = TypQ_aux (TypQ_tq (List.map qi_id_of_kopt kopts @ nc), loc n m) + type lchain = LC_lt | LC_lteq @@ -171,6 +173,8 @@ let rec desugar_rchain chain s e = mk_nc (NC_and (nc1, desugar_rchain (RC_nexp n2 :: chain) s e)) s e | _ -> assert false +let future_syntax l = Util.warn (Reporting.loc_to_string l ^ "\n\nThis syntax is currently experimental") + %} /*Terminals with no content*/ @@ -185,7 +189,7 @@ let rec desugar_rchain chain s e = %nonassoc Then %nonassoc Else -%token Bar Comma Dot Eof Minus Semi Under DotDot +%token Bar Comma Dot Eof Minus Semi Under DotDot ColonColonLt %token Lcurly Rcurly Lparen Rparen Lsquare Rsquare LcurlyBar RcurlyBar LsquareBar RsquareBar %token MinusGt Bidir LtMinus @@ -196,7 +200,7 @@ let rec desugar_rchain chain s e = %token String Bin Hex Real %token Amp At Caret Eq Gt Lt Plus Star EqGt Unit -%token Colon ColonColon (* CaretCaret *) TildeTilde ExclEq +%token Colon ColonColon TildeTilde ExclEq %token EqEq %token GtEq %token LtEq @@ -339,9 +343,6 @@ atomic_nc: { mk_nc NC_true $startpos $endpos } | False { mk_nc NC_false $startpos $endpos } - | typ0 Eq typ0 - { Util.warn ("Deprecated syntax, use == instead at " ^ Reporting.loc_to_string (loc $startpos($2) $endpos($2)) ^ "\n"); - mk_nc (NC_equal ($1, $3)) $startpos $endpos } | typ0 EqEq typ0 { mk_nc (NC_equal ($1, $3)) $startpos $endpos } | typ0 ExclEq typ0 @@ -355,38 +356,6 @@ atomic_nc: | kid In Lcurly num_list Rcurly { mk_nc (NC_set ($1, $4)) $startpos $endpos } -new_nc: - | new_nc Bar new_nc_and - { mk_nc (NC_or ($1, $3)) $startpos $endpos } - | nc_and - { $1 } - -new_nc_and: - | new_nc_and Amp new_atomic_nc - { mk_nc (NC_and ($1, $3)) $startpos $endpos } - | new_atomic_nc - { $1 } - -new_atomic_nc: - | Where id Lparen typ_list Rparen - { mk_nc (NC_app ($2, $4)) $startpos $endpos } - | True - { mk_nc NC_true $startpos $endpos } - | False - { mk_nc NC_false $startpos $endpos } - | typ0 EqEq typ0 - { mk_nc (NC_equal ($1, $3)) $startpos $endpos } - | typ0 ExclEq typ0 - { mk_nc (NC_not_equal ($1, $3)) $startpos $endpos } - | nc_lchain - { desugar_lchain $1 $startpos $endpos } - | nc_rchain - { desugar_rchain $1 $startpos $endpos } - | Lparen new_nc Rparen - { $2 } - | kid In Lcurly num_list Rcurly - { mk_nc (NC_set ($1, $4)) $startpos $endpos } - num_list: | Num { [$1] } @@ -413,11 +382,17 @@ nc_rchain: | typ0 Gt nc_rchain { RC_nexp $1 :: RC_gt :: $3 } +tyarg: + | ColonColonLt typ_list Gt + { future_syntax (loc $startpos($1) $endpos($3)); $2, [] } + | Lparen typ_list Rparen + { [], $2 } + | ColonColonLt typ_list Gt Lparen typ_list Rparen + { future_syntax (loc $startpos($1) $endpos($3)); $2, $5 } + typ: | typ0 { $1 } - | typ0 With new_nc - { mk_typ (ATyp_with ($1, $3)) $startpos $endpos } /* The following implements all nine levels of user-defined precedence for operators in types, with both left, right and non-associative operators */ @@ -587,8 +562,8 @@ atomic_typ: { mk_typ ATyp_dec $startpos $endpos } | Inc { mk_typ ATyp_inc $startpos $endpos } - | id Lparen typ_list Rparen - { mk_typ (ATyp_app ($1, $3)) $startpos $endpos } + | id tyarg + { mk_typ (ATyp_app ($1, snd $2 @ fst $2)) $startpos $endpos } | Register Lparen typ Rparen { let register_id = mk_id (Id "register") $startpos($1) $endpos($1) in mk_typ (ATyp_app (register_id, [$3])) $startpos $endpos } @@ -1193,14 +1168,43 @@ r_def_body: | r_id_def Comma r_def_body { $1 :: $3 } +param_kopt: + | kid Colon kind + { KOpt_aux (KOpt_kind ($3, $1), loc $startpos $endpos) } + | kid + { KOpt_aux (KOpt_none $1, loc $startpos $endpos) } + +param_kopt_list: + | param_kopt + { [$1] } + | param_kopt Comma param_kopt_list + { $1 :: $3 } + +typaram: + | ColonColonLt param_kopt_list Gt Lparen param_kopt_list Rparen Comma nc + { future_syntax (loc $startpos($1) $endpos($3)); + let qi_nc = QI_aux (QI_const $8, loc $startpos($8) $endpos($8)) in + mk_typq ($5 @ $2) [qi_nc] $startpos $endpos } + | ColonColonLt param_kopt_list Gt Lparen param_kopt_list Rparen + { future_syntax (loc $startpos($1) $endpos($3)); + mk_typq ($5 @ $2) [] $startpos $endpos } + | ColonColonLt param_kopt_list Gt + { future_syntax (loc $startpos($1) $endpos($3)); + mk_typq $2 [] $startpos $endpos } + | Lparen param_kopt_list Rparen Comma nc + { let qi_nc = QI_aux (QI_const $5, loc $startpos($5) $endpos($5)) in + mk_typq $2 [qi_nc] $startpos $endpos } + | Lparen param_kopt_list Rparen + { mk_typq $2 [] $startpos $endpos } + type_def: - | Typedef id typquant Eq typ + | Typedef id typaram Eq typ { mk_td (TD_abbrev ($2, mk_namesectn, mk_typschm $3 $5 $startpos($3) $endpos)) $startpos $endpos } | Typedef id Eq typ { mk_td (TD_abbrev ($2, mk_namesectn, mk_typschm mk_typqn $4 $startpos($4) $endpos)) $startpos $endpos } | Struct id Eq Lcurly struct_fields Rcurly { mk_td (TD_record ($2, mk_namesectn, TypQ_aux (TypQ_tq [], loc $endpos($2) $startpos($3)), $5, false)) $startpos $endpos } - | Struct id typquant Eq Lcurly struct_fields Rcurly + | Struct id typaram Eq Lcurly struct_fields Rcurly { mk_td (TD_record ($2, mk_namesectn, $3, $6, false)) $startpos $endpos } | Enum id Eq enum_bar { mk_td (TD_enum ($2, mk_namesectn, $4, false)) $startpos $endpos } @@ -1208,11 +1212,11 @@ type_def: { mk_td (TD_enum ($2, mk_namesectn, $5, false)) $startpos $endpos } | Newtype id Eq type_union { mk_td (TD_variant ($2, mk_namesectn, TypQ_aux (TypQ_tq [], loc $endpos($2) $startpos($3)), [$4], false)) $startpos $endpos } - | Newtype id typquant Eq type_union + | Newtype id typaram Eq type_union { mk_td (TD_variant ($2, mk_namesectn, $3, [$5], false)) $startpos $endpos } | Union id Eq Lcurly type_unions Rcurly { mk_td (TD_variant ($2, mk_namesectn, TypQ_aux (TypQ_tq [], loc $endpos($2) $startpos($3)), $5, false)) $startpos $endpos } - | Union id typquant Eq Lcurly type_unions Rcurly + | Union id typaram Eq Lcurly type_unions Rcurly { mk_td (TD_variant ($2, mk_namesectn, $3, $6, false)) $startpos $endpos } | Bitfield id Colon typ Eq Lcurly r_def_body Rcurly { mk_td (TD_bitfield ($2, $4, $7)) $startpos $endpos } diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml index a2771ae1..53e77df2 100644 --- a/src/pretty_print_sail.ml +++ b/src/pretty_print_sail.ml @@ -151,7 +151,7 @@ let doc_nc nc = | NC_and (c1, c2) -> separate space [nc1 c1; string "&"; atomic_nc c2] | _ -> atomic_nc nc in - nc0 ~parenthesize:true (constraint_simp nc) + atomic_nc (constraint_simp nc) let rec doc_typ ?(simple=false) (Typ_aux (typ_aux, l)) = match typ_aux with @@ -219,6 +219,27 @@ let doc_quants quants = | [nc] -> kdoc ^^ comma ^^ space ^^ doc_nc nc | nc :: ncs -> kdoc ^^ comma ^^ space ^^ doc_nc (List.fold_left nc_and nc ncs) +let doc_param_quants quants = + let doc_qi_kopt (QI_aux (qi_aux, _)) = + match qi_aux with + | QI_id (KOpt_aux (KOpt_none kid, _)) -> [doc_kid kid] + | QI_id kopt when is_nat_kopt kopt -> [doc_kid (kopt_kid kopt) ^^ colon ^^ space ^^ string "Int"] + | QI_id kopt when is_typ_kopt kopt -> [doc_kid (kopt_kid kopt) ^^ colon ^^ space ^^ string "Type"] + | QI_id kopt -> [doc_kid (kopt_kid kopt) ^^ colon ^^ space ^^ string "Order"] + | QI_const nc -> [] + in + let qi_nc (QI_aux (qi_aux, _)) = + match qi_aux with + | QI_const nc -> [nc] + | _ -> [] + in + let kdoc = separate (comma ^^ space) (List.concat (List.map doc_qi_kopt quants)) in + let ncs = List.concat (List.map qi_nc quants) in + match ncs with + | [] -> parens kdoc + | [nc] -> parens kdoc ^^ comma ^^ space ^^ doc_nc nc + | nc :: ncs -> parens kdoc ^^ comma ^^ space ^^ doc_nc (List.fold_left nc_and nc ncs) + let doc_binding ?(simple=false) ((TypQ_aux (tq_aux, _) as typq), typ) = match tq_aux with | TypQ_no_forall -> doc_typ ~simple:simple typ @@ -244,7 +265,7 @@ let doc_typschm_quants (TypSchm_aux (TypSchm_ts (TypQ_aux (tq_aux, _), typ), _)) match tq_aux with | TypQ_no_forall -> None | TypQ_tq [] -> None - | TypQ_tq qs -> Some (doc_quants qs) + | TypQ_tq qs -> Some (doc_param_quants qs) let doc_lit (L_aux(l,_)) = utf8string (match l with @@ -547,7 +568,7 @@ let doc_typdef (TD_aux(td,_)) = match td with begin match doc_typschm_quants typschm with | Some qdoc -> - doc_op equals (concat [string "type"; space; doc_id id; space; qdoc]) (doc_typschm_typ typschm) + doc_op equals (concat [string "type"; space; doc_id id; qdoc]) (doc_typschm_typ typschm) | None -> doc_op equals (concat [string "type"; space; doc_id id]) (doc_typschm_typ typschm) end @@ -556,12 +577,12 @@ let doc_typdef (TD_aux(td,_)) = match td with | TD_record (id, _, TypQ_aux (TypQ_no_forall, _), fields, _) | TD_record (id, _, TypQ_aux (TypQ_tq [], _), fields, _) -> separate space [string "struct"; doc_id id; equals; surround 2 0 lbrace (separate_map (comma ^^ break 1) doc_field fields) rbrace] | TD_record (id, _, TypQ_aux (TypQ_tq qs, _), fields, _) -> - separate space [string "struct"; doc_id id; doc_quants qs; equals; + separate space [string "struct"; doc_id id; doc_param_quants qs; equals; surround 2 0 lbrace (separate_map (comma ^^ break 1) doc_field fields) rbrace] | TD_variant (id, _, TypQ_aux (TypQ_no_forall, _), unions, _) | TD_variant (id, _, TypQ_aux (TypQ_tq [], _), unions, _) -> separate space [string "union"; doc_id id; equals; surround 2 0 lbrace (separate_map (comma ^^ break 1) doc_union unions) rbrace] | TD_variant (id, _, TypQ_aux (TypQ_tq qs, _), unions, _) -> - separate space [string "union"; doc_id id; doc_quants qs; equals; + separate space [string "union"; doc_id id; doc_param_quants qs; equals; surround 2 0 lbrace (separate_map (comma ^^ break 1) doc_union unions) rbrace] | _ -> string "TYPEDEF" -- cgit v1.2.3