summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/c_backend.ml3
-rw-r--r--src/lexer.mll1
-rw-r--r--src/parser.mly94
-rw-r--r--src/pretty_print_sail.ml31
4 files changed, 79 insertions, 50 deletions
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> String Bin Hex Real
%token <string> Amp At Caret Eq Gt Lt Plus Star EqGt Unit
-%token <string> Colon ColonColon (* CaretCaret *) TildeTilde ExclEq
+%token <string> Colon ColonColon TildeTilde ExclEq
%token <string> EqEq
%token <string> GtEq
%token <string> 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"
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 23:02:49 +0000