summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/ast.ml2
-rw-r--r--src/initial_check.ml22
-rw-r--r--src/lexer2.mll22
-rw-r--r--src/ocaml_backend.ml14
-rw-r--r--src/parse_ast.ml6
-rw-r--r--src/parser2.mly61
-rw-r--r--src/pretty_print_sail.ml1
-rw-r--r--src/pretty_print_sail2.ml92
-rw-r--r--src/process_file.ml27
-rw-r--r--src/rewriter.ml2
-rw-r--r--src/type_check.ml5
11 files changed, 184 insertions, 70 deletions
diff --git a/src/ast.ml b/src/ast.ml
index 76c926bb..6f702a78 100644
--- a/src/ast.ml
+++ b/src/ast.ml
@@ -553,6 +553,7 @@ type
'a dec_spec =
DEC_aux of 'a dec_spec_aux * 'a annot
+type prec = Infix | InfixL | InfixR
type
'a dec_comm = (* Top-level generated comments *)
@@ -565,6 +566,7 @@ and 'a def = (* Top-level definition *)
| DEF_fundef of 'a fundef (* function definition *)
| DEF_val of 'a letbind (* value definition *)
| DEF_spec of 'a val_spec (* top-level type constraint *)
+ | DEF_fixity of prec * int * id (* fixity declaration *)
| DEF_overload of id * id list (* operator overload specification *)
| DEF_default of 'a default_spec (* default kind and type assumptions *)
| DEF_scattered of 'a scattered_def (* scattered function and type definition *)
diff --git a/src/initial_check.ml b/src/initial_check.ml
index 36b6478e..6a7a1b0a 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -765,12 +765,19 @@ let to_ast_dec (names,k_env,def_ord) (Parse_ast.DEC_aux(regdec,l)) =
| Parse_ast.DEC_typ_alias(typ,id,e) ->
DEC_typ_alias(to_ast_typ k_env def_ord typ,to_ast_id id,to_ast_alias_spec k_env def_ord e)
),(l,()))
-
+
+let to_ast_prec = function
+ | Parse_ast.Infix -> Infix
+ | Parse_ast.InfixL -> InfixL
+ | Parse_ast.InfixR -> InfixR
+
let to_ast_def (names, k_env, def_ord) partial_defs def : def_progress envs_out * (id * partial_def) list =
let envs = (names,k_env,def_ord) in
match def with
| Parse_ast.DEF_overload(id,ids) ->
- ((Finished(DEF_overload(to_ast_id id, List.map to_ast_id ids))),envs),partial_defs
+ ((Finished(DEF_overload(to_ast_id id, List.map to_ast_id ids))),envs),partial_defs
+ | Parse_ast.DEF_fixity (prec, n, op) ->
+ ((Finished(DEF_fixity (to_ast_prec prec, n, to_ast_id op)),envs),partial_defs)
| Parse_ast.DEF_kind(k_def) ->
let kd,envs = to_ast_kdef envs k_def in
((Finished(DEF_kind(kd))),envs),partial_defs
@@ -913,7 +920,7 @@ let typschm_of_string order str =
let (typschm, _, _) = to_ast_typschm initial_kind_env order typschm in
typschm
-let val_spec_of_string order id str = mk_val_spec (VS_val_spec (typschm_of_string order str, id, Some str, false))
+let val_spec_of_string order id str = mk_val_spec (VS_val_spec (typschm_of_string order str, id, Some (string_of_id id), false))
let val_spec_ids (Defs defs) =
let val_spec_id (VS_aux (vs_aux, _)) =
@@ -965,6 +972,10 @@ let generate_undefineds vs_ids (Defs defs) =
gen_vs (mk_id "undefined_vector") "forall 'n 'm ('a:Type). (atom('n), atom('m), 'a) -> vector('n, 'm, dec,'a) effect {undef}";
gen_vs (mk_id "undefined_unit") "unit -> unit effect {undef}"]
in
+ let undefined_tu = function
+ | Tu_aux (Tu_id id, _) -> mk_exp (E_id id)
+ | Tu_aux (Tu_ty_id (typ, id), _) -> mk_exp (E_app (id, [mk_lit_exp L_undef]))
+ in
let undefined_td = function
| TD_enum (id, _, ids, _) when not (IdSet.mem (prepend_id "undefined_" id) vs_ids) ->
let typschm = typschm_of_string dec_ord ("unit -> " ^ string_of_id id ^ " effect {undef}") in
@@ -980,11 +991,12 @@ let generate_undefineds vs_ids (Defs defs) =
pat
(mk_exp (E_record (mk_fexps (List.map (fun (_, id) -> mk_fexp id (mk_lit_exp L_undef)) fields))))]]
| TD_variant (id, _, typq, tus, _) when not (IdSet.mem (prepend_id "undefined_" id) vs_ids) ->
+ let pat = mk_pat (P_tup (quant_items typq |> List.map quant_item_param |> List.concat |> List.map (fun id -> mk_pat (P_id id)))) in
[mk_val_spec (VS_val_spec (undefined_typschm id typq, prepend_id "undefined_" id, None, false));
mk_fundef [mk_funcl (prepend_id "undefined_" id)
- (mk_pat (P_lit (mk_lit L_unit)))
+ pat
(mk_exp (E_app (mk_id "internal_pick",
- [])))]]
+ [mk_exp (E_list (List.map undefined_tu tus))])))]]
| _ -> []
in
let rec undefined_defs = function
diff --git a/src/lexer2.mll b/src/lexer2.mll
index 1ab5b98b..5b711287 100644
--- a/src/lexer2.mll
+++ b/src/lexer2.mll
@@ -42,6 +42,7 @@
{
open Parser2
+open Parse_ast
module M = Map.Make(String)
exception LexError of string * Lexing.position
@@ -49,8 +50,6 @@ let r = fun s -> s (* Ulib.Text.of_latin1 *)
(* Available as Scanf.unescaped since OCaml 4.0 but 3.12 is still common *)
let unescaped s = Scanf.sscanf ("\"" ^ s ^ "\"") "%S%!" (fun x -> x)
-type prec = Infix | InfixL | InfixR
-
let mk_operator prec n op =
match prec, n with
| Infix, 0 -> Op0 op
@@ -102,13 +101,14 @@ let kw_table =
("clause", (fun _ -> Clause));
("dec", (fun _ -> Dec));
("def", (fun _ -> Def));
- ("op", (fun _ -> Op));
+ ("operator", (fun _ -> Op));
("default", (fun _ -> Default));
("effect", (fun _ -> Effect));
("Effect", (fun _ -> EFFECT));
("end", (fun _ -> End));
("enum", (fun _ -> Enum));
("else", (fun _ -> Else));
+ ("exit", (fun _ -> Exit));
("extern", (fun _ -> Extern));
("cast", (fun _ -> Cast));
("false", (fun _ -> False));
@@ -172,8 +172,8 @@ let alphanum = letter|digit
let startident = letter|'_'
let ident = alphanum|['_''\'']
let tyvar_start = '\''
-let oper_char = ['!''$''%''&''*''+''-''.''/'':''<''=''>''?''@''^''|''~']
-let operator = oper_char+ ('_' ident)?
+let oper_char = ['!''$''%''&''*''+''-''.''/'':''<''=''>''?''@''^''|']
+let operator = (oper_char+ ('_' ident)?)
let escape_sequence = ('\\' ['\\''\"''\'''n''t''b''r']) | ('\\' digit digit digit) | ('\\' 'x' hexdigit hexdigit)
rule token = parse
@@ -190,6 +190,9 @@ rule token = parse
| "," { Comma }
| ".." { DotDot }
| "." { Dot }
+ | "==" as op
+ { try M.find op !operators
+ with Not_found -> raise (LexError ("Operator fixity undeclared " ^ op, Lexing.lexeme_start_p lexbuf)) }
| "=" { (Eq(r"=")) }
| ">" { (Gt(r">")) }
| "-" { Minus }
@@ -215,19 +218,20 @@ rule token = parse
| "<=" { (LtEq(r"<=")) }
| "infix" ws (digit as p) ws (operator as op)
{ operators := M.add op (mk_operator Infix (int_of_string (Char.escaped p)) op) !operators;
- token lexbuf }
+ Fixity (Infix, int_of_string (Char.escaped p), op) }
| "infixl" ws (digit as p) ws (operator as op)
{ operators := M.add op (mk_operator InfixL (int_of_string (Char.escaped p)) op) !operators;
- token lexbuf }
+ Fixity (InfixL, int_of_string (Char.escaped p), op) }
| "infixr" ws (digit as p) ws (operator as op)
{ operators := M.add op (mk_operator InfixR (int_of_string (Char.escaped p)) op) !operators;
- token lexbuf }
+ Fixity (InfixR, int_of_string (Char.escaped p), op) }
| operator as op
{ try M.find op !operators
- with Not_found -> raise (LexError ("Operator fixity undeclared", Lexing.lexeme_start_p lexbuf)) }
+ with Not_found -> raise (LexError ("Operator fixity undeclared " ^ op, Lexing.lexeme_start_p lexbuf)) }
| "(*" { comment (Lexing.lexeme_start_p lexbuf) 0 lexbuf; token lexbuf }
| "*)" { raise (LexError("Unbalanced comment", Lexing.lexeme_start_p lexbuf)) }
| tyvar_start startident ident* as i { TyVar(r i) }
+ | "~" { Id(r"~") }
| startident ident* as i { if M.mem i kw_table then
(M.find i kw_table) ()
(* else if
diff --git a/src/ocaml_backend.ml b/src/ocaml_backend.ml
index 38b3cc9d..dc8c056e 100644
--- a/src/ocaml_backend.ml
+++ b/src/ocaml_backend.ml
@@ -107,8 +107,13 @@ let begin_end doc = group (string "begin" ^^ nest 2 (break 1 ^^ doc) ^/^ string
let rec ocaml_exp ctx (E_aux (exp_aux, _) as exp) =
match exp_aux with
+ | E_app (f, [x]) when Env.is_union_constructor f (env_of exp) -> zencode_upper ctx f ^^ space ^^ ocaml_atomic_exp ctx x
| E_app (f, [x]) -> zencode ctx f ^^ space ^^ ocaml_atomic_exp ctx x
- | E_app (f, xs) -> zencode ctx f ^^ space ^^ parens (separate_map (comma ^^ space) (ocaml_exp ctx) xs)
+ | E_app (f, xs) when Env.is_union_constructor f (env_of exp) ->
+ zencode_upper ctx f ^^ space ^^ parens (separate_map (comma ^^ space) (ocaml_exp ctx) xs)
+ | E_app (f, xs) ->
+ zencode ctx f ^^ space ^^ parens (separate_map (comma ^^ space) (ocaml_exp ctx) xs)
+ | E_vector_subrange (exp1, exp2, exp3) -> string "subrange" ^^ space ^^ parens (separate_map (comma ^^ space) (ocaml_exp ctx) [exp1; exp2; exp3])
| E_return exp -> separate space [string "r.return"; ocaml_atomic_exp ctx exp]
| E_assert (exp, _) -> separate space [string "assert"; ocaml_atomic_exp ctx exp]
| E_cast (_, exp) -> ocaml_exp ctx exp
@@ -176,9 +181,8 @@ and ocaml_atomic_exp ctx (E_aux (exp_aux, _) as exp) =
begin
match Env.lookup_id id (env_of exp) with
| Local (Immutable, _) | Unbound -> zencode ctx id
- | Enum _ -> zencode_upper ctx id
+ | Enum _ | Union _ -> zencode_upper ctx id
| Register _ | Local (Mutable, _) -> bang ^^ zencode ctx id
- | _ -> failwith ("Union constructor: " ^ zencode_string (string_of_id id))
end
| E_list exps -> enclose lbracket rbracket (separate_map (semi ^^ space) (ocaml_exp ctx) exps)
| E_tuple exps -> parens (separate_map (comma ^^ space) (ocaml_exp ctx) exps)
@@ -255,8 +259,8 @@ let rec ocaml_fields ctx =
let rec ocaml_cases ctx =
let ocaml_case = function
- | Tu_aux (Tu_id id, _) -> separate space [bar; zencode ctx id]
- | Tu_aux (Tu_ty_id (typ, id), _) -> separate space [bar; zencode ctx id; string "of"; ocaml_typ ctx typ]
+ | Tu_aux (Tu_id id, _) -> separate space [bar; zencode_upper ctx id]
+ | Tu_aux (Tu_ty_id (typ, id), _) -> separate space [bar; zencode_upper ctx id; string "of"; ocaml_typ ctx typ]
in
function
| [tu] -> ocaml_case tu
diff --git a/src/parse_ast.ml b/src/parse_ast.ml
index 9532b858..cfd749ba 100644
--- a/src/parse_ast.ml
+++ b/src/parse_ast.ml
@@ -481,14 +481,18 @@ type
scattered_def =
SD_aux of scattered_def_aux * l
+type prec = Infix | InfixL | InfixR
-type
+type fixity_token = (prec * int * string)
+
+type
def = (* Top-level definition *)
DEF_kind of kind_def (* definition of named kind identifiers *)
| DEF_type of type_def (* type definition *)
| DEF_fundef of fundef (* function definition *)
| DEF_val of letbind (* value definition *)
| DEF_overload of id * id list (* operator overload specifications *)
+ | DEF_fixity of prec * int * id (* fixity declaration *)
| DEF_spec of val_spec (* top-level type constraint *)
| DEF_default of default_typing_spec (* default kind and type assumptions *)
| DEF_scattered of scattered_def (* scattered definition *)
diff --git a/src/parser2.mly b/src/parser2.mly
index 59db84a1..a2fb3bfb 100644
--- a/src/parser2.mly
+++ b/src/parser2.mly
@@ -127,7 +127,7 @@ let rec desugar_rchain chain s e =
%token And As Assert Bitzero Bitone Bits By Match Clause Dec Def Default Effect EFFECT End Op
%token Enum Else Extern False Forall Exist Foreach Overload Function_ If_ In IN Inc Let_ Member Int Order Cast
%token Pure Rec Register Return Scattered Sizeof Struct Then True TwoCaret Type TYPE Typedef
-%token Undefined Union With Val Constraint Throw Try Catch
+%token Undefined Union With Val Constraint Throw Try Catch Exit
%token Barr Depend Rreg Wreg Rmem Rmemt Wmem Wmv Wmvt Eamem Exmem Undef Unspec Nondet Escape
%nonassoc Then
@@ -152,6 +152,8 @@ let rec desugar_rchain chain s e =
%token <string> Op0l Op1l Op2l Op3l Op4l Op5l Op6l Op7l Op8l Op9l
%token <string> Op0r Op1r Op2r Op3r Op4r Op5r Op6r Op7r Op8r Op9r
+%token <Parse_ast.fixity_token> Fixity
+
%start file
%start typschm_eof
%type <Parse_ast.typschm> typschm_eof
@@ -198,6 +200,14 @@ id:
| Op Plus { mk_id (DeIid "+") $startpos $endpos }
| Op Minus { mk_id (DeIid "-") $startpos $endpos }
| Op Star { mk_id (DeIid "*") $startpos $endpos }
+ | Op ExclEq { mk_id (DeIid "!=") $startpos $endpos }
+ | Op Lt { mk_id (DeIid "<") $startpos $endpos }
+ | Op Gt { mk_id (DeIid ">") $startpos $endpos }
+ | Op LtEq { mk_id (DeIid "<=") $startpos $endpos }
+ | Op GtEq { mk_id (DeIid ">=") $startpos $endpos }
+ | Op Amp { mk_id (DeIid "&") $startpos $endpos }
+ | Op Bar { mk_id (DeIid "|") $startpos $endpos }
+ | Op Caret { mk_id (DeIid "^") $startpos $endpos }
op0: Op0 { mk_id (Id $1) $startpos $endpos }
op1: Op1 { mk_id (Id $1) $startpos $endpos }
@@ -585,12 +595,24 @@ typschm_eof:
| typschm Eof
{ $1 }
-pat:
+pat1:
| atomic_pat
{ $1 }
- | atomic_pat As id
+ | atomic_pat At pat_concat
+ { mk_pat (P_vector_concat ($1 :: $3)) $startpos $endpos }
+
+pat_concat:
+ | atomic_pat
+ { [$1] }
+ | atomic_pat At pat_concat
+ { $1 :: $3 }
+
+pat:
+ | pat1
+ { $1 }
+ | pat1 As id
{ mk_pat (P_as ($1, $3)) $startpos $endpos }
- | atomic_pat As kid
+ | pat1 As kid
{ mk_pat (P_var ($1, $3)) $startpos $endpos }
pat_list:
@@ -610,12 +632,14 @@ atomic_pat:
{ mk_pat (P_var (mk_pat (P_id (id_of_kid $1)) $startpos $endpos, $1)) $startpos $endpos }
| id Lparen pat_list Rparen
{ mk_pat (P_app ($1, $3)) $startpos $endpos }
- | pat Colon typ
+ | atomic_pat Colon typ
{ mk_pat (P_typ ($3, $1)) $startpos $endpos }
| Lparen pat Rparen
{ $2 }
| Lparen pat Comma pat_list Rparen
{ mk_pat (P_tup ($2 :: $4)) $startpos $endpos }
+ | Lsquare pat_list Rsquare
+ { mk_pat (P_vector $2) $startpos $endpos }
lit:
| True
@@ -695,6 +719,7 @@ exp2:
| exp3 op2 exp3 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
| exp2l op2l exp3 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
| exp3 op2r exp2r { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
+ | exp3 Bar exp2r { mk_exp (E_app_infix ($1, mk_id (Id "|") $startpos($2) $endpos($2), $3)) $startpos $endpos }
| exp3 { $1 }
exp2l:
| exp3 op2 exp3 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
@@ -703,12 +728,14 @@ exp2l:
exp2r:
| exp3 op2 exp3 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
| exp3 op2r exp2r { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
+ | exp3 Bar exp2r { mk_exp (E_app_infix ($1, mk_id (Id "|") $startpos($2) $endpos($2), $3)) $startpos $endpos }
| exp3 { $1 }
exp3:
| exp4 op3 exp4 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
| exp3l op3l exp4 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
| exp4 op3r exp3r { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
+ | exp4 Amp exp3r { mk_exp (E_app_infix ($1, mk_id (Id "&") $startpos($2) $endpos($2), $3)) $startpos $endpos }
| exp4 { $1 }
exp3l:
| exp4 op3 exp4 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
@@ -717,10 +744,16 @@ exp3l:
exp3r:
| exp4 op3 exp4 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
| exp4 op3r exp3r { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
+ | exp4 Amp exp3r { mk_exp (E_app_infix ($1, mk_id (Id "&") $startpos($2) $endpos($2), $3)) $startpos $endpos }
| exp4 { $1 }
exp4:
| exp5 op4 exp5 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
+ | exp5 Lt exp5 { mk_exp (E_app_infix ($1, mk_id (Id "<") $startpos($2) $endpos($2), $3)) $startpos $endpos }
+ | exp5 Gt exp5 { mk_exp (E_app_infix ($1, mk_id (Id ">") $startpos($2) $endpos($2), $3)) $startpos $endpos }
+ | exp5 LtEq exp5 { mk_exp (E_app_infix ($1, mk_id (Id "<=") $startpos($2) $endpos($2), $3)) $startpos $endpos }
+ | exp5 GtEq exp5 { mk_exp (E_app_infix ($1, mk_id (Id ">=") $startpos($2) $endpos($2), $3)) $startpos $endpos }
+ | exp5 ExclEq exp5 { mk_exp (E_app_infix ($1, mk_id (Id "!=") $startpos($2) $endpos($2), $3)) $startpos $endpos }
| exp4l op4l exp5 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
| exp5 op4r exp4r { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
| exp5 { $1 }
@@ -845,6 +878,8 @@ atomic_exp:
{ mk_exp (E_cast ($3, $1)) $startpos $endpos }
| lit
{ mk_exp (E_lit $1) $startpos $endpos }
+ | atomic_exp Dot id
+ { mk_exp (E_field ($1, $3)) $startpos $endpos }
| id
{ mk_exp (E_id $1) $startpos $endpos }
| kid
@@ -853,6 +888,8 @@ atomic_exp:
{ mk_exp (E_app ($1, [mk_lit_exp L_unit $startpos($2) $endpos])) $startpos $endpos }
| id Lparen exp_list Rparen
{ mk_exp (E_app ($1, $3)) $startpos $endpos }
+ | Exit Lparen exp Rparen
+ { mk_exp (E_exit $3) $startpos $endpos }
| Sizeof Lparen typ Rparen
{ mk_exp (E_sizeof $3) $startpos $endpos }
| Constraint Lparen nc Rparen
@@ -886,11 +923,19 @@ funcl:
| id pat Eq exp
{ mk_funcl (FCL_Funcl ($1, $2, $4)) $startpos $endpos }
+funcls:
+ | id pat Eq exp
+ { [mk_funcl (FCL_Funcl ($1, $2, $4)) $startpos $endpos] }
+ | id pat Eq exp And funcls
+ { mk_funcl (FCL_Funcl ($1, $2, $4)) $startpos $endpos :: $6 }
+
type_def:
| Typedef id typquant 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
{ mk_td (TD_record ($2, mk_namesectn, $3, $6, false)) $startpos $endpos }
| Enum id Eq enum_bar
@@ -939,8 +984,8 @@ type_unions:
{ $1 :: $3 }
fun_def:
- | Function_ funcl
- { mk_fun (FD_function (mk_recn, mk_tannotn, mk_eannotn, [$2])) $startpos $endpos }
+ | Function_ funcls
+ { mk_fun (FD_function (mk_recn, mk_tannotn, mk_eannotn, $2)) $startpos $endpos }
let_def:
| Let_ letbind
@@ -977,6 +1022,8 @@ scattered_def:
def:
| fun_def
{ DEF_fundef $1 }
+ | Fixity
+ { let (prec, n, op) = $1 in DEF_fixity (prec, n, Id_aux (Id op, loc $startpos $endpos)) }
| val_spec_def
{ DEF_spec $1 }
| type_def
diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml
index 99263bc7..0f8e482a 100644
--- a/src/pretty_print_sail.ml
+++ b/src/pretty_print_sail.ml
@@ -526,6 +526,7 @@ let rec doc_def def = group (match def with
string "overload" ^^ space ^^ doc_id id ^^ space ^^ brackets ids_doc
| DEF_comm (DC_comm s) -> comment (string s)
| DEF_comm (DC_comm_struct d) -> comment (doc_def d)
+ | DEF_fixity _ -> empty
) ^^ hardline
let doc_defs (Defs(defs)) =
diff --git a/src/pretty_print_sail2.ml b/src/pretty_print_sail2.ml
index bb7aa3b4..23452813 100644
--- a/src/pretty_print_sail2.ml
+++ b/src/pretty_print_sail2.ml
@@ -8,7 +8,7 @@ let doc_op symb a b = infix 2 1 symb a b
let doc_id (Id_aux (id_aux, _)) =
string (match id_aux with
| Id v -> v
- | DeIid op -> "op " ^ op)
+ | DeIid op -> "operator " ^ op)
let doc_kid kid = string (Ast_util.string_of_kid kid)
@@ -76,6 +76,8 @@ let rec doc_typ (Typ_aux (typ_aux, _)) =
| Typ_app (id, []) -> doc_id id
| Typ_app (Id_aux (DeIid str, _), [x; y]) ->
separate space [doc_typ_arg x; doc_typ_arg y]
+ | Typ_app (id, [_; len; _; Typ_arg_aux (Typ_arg_typ (Typ_aux (Typ_id tid, _)), _)]) when Id.compare (mk_id "vector") id == 0 && Id.compare (mk_id "bit") tid == 0->
+ string "bits" ^^ parens (doc_typ_arg len)
| Typ_app (id, typs) -> doc_id id ^^ parens (separate_map (string ", ") doc_typ_arg typs)
| Typ_tup typs -> parens (separate_map (string ", ") doc_typ typs)
| Typ_var kid -> doc_kid kid
@@ -144,7 +146,7 @@ let doc_lit (L_aux(l,_)) =
| L_undef -> "undefined"
| L_string s -> "\"" ^ String.escaped s ^ "\"")
-let rec doc_pat (P_aux (p_aux, _)) =
+let rec doc_pat (P_aux (p_aux, _) as pat) =
match p_aux with
| P_id id -> doc_id id
| P_tup pats -> lparen ^^ separate_map (comma ^^ space) doc_pat pats ^^ rparen
@@ -155,63 +157,85 @@ let rec doc_pat (P_aux (p_aux, _)) =
| P_var (P_aux (P_id id, _), kid) when Id.compare (id_of_kid kid) id == 0 ->
doc_kid kid
| P_var (pat, kid) -> separate space [doc_pat pat; string "as"; doc_kid kid]
+ | P_vector pats -> brackets (separate_map (comma ^^ space) doc_pat pats)
| P_vector_concat pats -> separate_map (space ^^ string "@" ^^ space) doc_pat pats
| P_wild -> string "_"
- | _ -> string "PAT"
+ | P_as (pat, id) -> separate space [doc_pat pat; string "as"; doc_id id]
+ | P_app (id, pats) -> doc_id id ^^ parens (separate_map (comma ^^ space) doc_pat pats)
+ | _ -> string (string_of_pat pat)
let rec doc_exp (E_aux (e_aux, _) as exp) =
- match e_aux with
+ match e_aux with
+ | E_block [exp] -> doc_exp exp
| E_block exps -> surround 2 0 lbrace (doc_block exps) rbrace
| E_nondet exps -> assert false
- | E_id id -> doc_id id
- | E_lit lit -> doc_lit lit
- | E_cast (typ, exp) ->
- separate space [doc_exp exp; colon; doc_typ typ]
- (* Format a function with a unit argument as f() rather than f(()) *)
- | E_app (id, [E_aux (E_lit (L_aux (L_unit, _)), _)]) -> doc_id id ^^ string "()"
- | E_app (id, exps) -> doc_id id ^^ parens (separate_map (comma ^^ space) doc_exp exps)
- | E_app_infix (x, id, y) -> doc_op (doc_id id) (doc_exp x) (doc_exp y)
+ (* This is mostly for the -convert option *)
+ | E_app_infix (x, id, y) when Id.compare (mk_id "quot") id == 0 ->
+ separate space [doc_atomic_exp x; string "/"; doc_atomic_exp y]
+ | E_app_infix (x, id, y) -> doc_op (doc_id id) (doc_atomic_exp x) (doc_atomic_exp y)
| E_tuple exps -> parens (separate_map (comma ^^ space) doc_exp exps)
- | E_if (if_exp, then_exp, else_exp) -> string "E_if"
+ | E_if (if_exp, then_exp, else_exp) ->
+ group (separate space [string "if"; doc_exp if_exp; string "then"; doc_exp then_exp; string "else"; doc_exp else_exp])
| E_for (id, exp1, exp2, exp3, order, exp4) -> string "E_for"
- | E_vector exps -> string "E_vector"
- | E_vector_access (exp1, exp2) -> string "E_vector_access"
- | E_vector_subrange (exp1, exp2, exp3) -> doc_exp exp1 ^^ brackets (separate space [doc_exp exp2; string ".."; doc_exp exp3])
- | E_vector_update (exp1, exp2, exp3) -> string "E_vector_update"
- | E_vector_update_subrange (exp1, exp2, exp3, exp4) -> string "E_vector_update_subrange"
| E_list exps -> string "E_list"
| E_cons (exp1, exp2) -> string "E_cons"
| E_record fexps -> string "E_record"
| E_record_update (exp, fexps) -> string "E_record_update"
- | E_field (exp, id) -> string "E_field"
| E_case (exp, pexps) ->
separate space [string "match"; doc_exp exp; doc_pexps pexps]
| E_let (LB_aux (LB_val (pat, binding), _), exp) ->
separate space [string "let"; doc_pat pat; equals; doc_exp binding; string "in"; doc_exp exp]
| E_assign (lexp, exp) ->
separate space [doc_lexp lexp; equals; doc_exp exp]
+ (* Resugar an assert with an empty message *)
+ | E_throw exp -> assert false
+ | E_try (exp, pexps) -> assert false
+ | E_return exp -> string "return" ^^ parens (doc_exp exp)
+ | _ -> doc_atomic_exp exp
+and doc_atomic_exp (E_aux (e_aux, _) as exp) =
+ match e_aux with
+ | E_cast (typ, exp) ->
+ separate space [doc_atomic_exp exp; colon; doc_typ typ]
+ | E_lit lit -> doc_lit lit
+ | E_id id -> doc_id id
+ | E_field (exp, id) -> doc_atomic_exp exp ^^ dot ^^ doc_id id
| E_sizeof (Nexp_aux (Nexp_var kid, _)) -> doc_kid kid
| E_sizeof nexp -> string "sizeof" ^^ parens (doc_nexp nexp)
+ (* Format a function with a unit argument as f() rather than f(()) *)
+ | E_app (id, [E_aux (E_lit (L_aux (L_unit, _)), _)]) -> doc_id id ^^ string "()"
+ | E_app (id, exps) -> doc_id id ^^ parens (separate_map (comma ^^ space) doc_exp exps)
| E_constraint nc -> string "constraint" ^^ parens (doc_nc nc)
- | E_exit exp -> assert false
- (* Resugar an assert with an empty message *)
| E_assert (exp1, E_aux (E_lit (L_aux (L_string "", _)), _)) -> string "assert" ^^ parens (doc_exp exp1)
| E_assert (exp1, exp2) -> string "assert" ^^ parens (doc_exp exp1 ^^ comma ^^ space ^^ doc_exp exp2)
- | E_throw exp -> assert false
- | E_try (exp, pexps) -> assert false
- | E_return exp -> string "return" ^^ parens (doc_exp exp)
+ | E_exit exp -> string "exit" ^^ parens (doc_exp exp)
+ | E_vector_access (exp1, exp2) -> doc_atomic_exp exp1 ^^ brackets (doc_exp exp2)
+ | E_vector_subrange (exp1, exp2, exp3) -> doc_atomic_exp exp1 ^^ brackets (separate space [doc_exp exp2; string ".."; doc_exp exp3])
+ | E_vector exps -> brackets (separate_map (comma ^^ space) doc_exp exps)
+ | E_vector_update (exp1, exp2, exp3) ->
+ brackets (separate space [doc_exp exp1; string "with"; doc_atomic_exp exp2; equals; doc_exp exp3])
+ | E_vector_update_subrange (exp1, exp2, exp3, exp4) ->
+ brackets (separate space [doc_exp exp1; string "with"; doc_atomic_exp exp2; string ".."; doc_atomic_exp exp3; equals; doc_exp exp4])
+ | _ -> parens (doc_exp exp)
and doc_block = function
| [] -> assert false
| [E_aux (E_let (LB_aux (LB_val (pat, binding), _), E_aux (E_block exps, _)), _)] ->
separate space [string "let"; doc_pat pat; equals; doc_exp binding] ^^ semi ^^ hardline ^^ doc_block exps
| [exp] -> doc_exp exp
| exp :: exps -> doc_exp exp ^^ semi ^^ hardline ^^ doc_block exps
-and doc_lexp (LEXP_aux (l_aux, _)) =
+and doc_lexp (LEXP_aux (l_aux, _) as lexp) =
+ match l_aux with
+ | LEXP_cast (typ, id) -> separate space [doc_id id; colon; doc_typ typ]
+ | _ -> doc_atomic_lexp lexp
+and doc_atomic_lexp (LEXP_aux (l_aux, _) as lexp) =
match l_aux with
| LEXP_id id -> doc_id id
| LEXP_tup lexps -> lparen ^^ separate_map (comma ^^ space) doc_lexp lexps ^^ rparen
- | _ -> string "LEXP"
-and doc_pexps pexps = surround 2 0 lbrace (separate_map (semi ^^ hardline) doc_pexp pexps) rbrace
+ | LEXP_field (lexp, id) -> doc_atomic_lexp lexp ^^ dot ^^ doc_id id
+ | LEXP_vector (lexp, exp) -> doc_atomic_lexp lexp ^^ brackets (doc_exp exp)
+ | LEXP_vector_range (lexp, exp1, exp2) -> doc_atomic_lexp lexp ^^ brackets (separate space [doc_exp exp1; string ".."; doc_exp exp2])
+ | LEXP_memory (id, exps) -> doc_id id ^^ parens (separate_map (comma ^^ space) doc_exp exps)
+ | _ -> parens (doc_lexp lexp)
+and doc_pexps pexps = surround 2 0 lbrace (separate_map (comma ^^ hardline) doc_pexp pexps) rbrace
and doc_pexp (Pat_aux (pat_aux, _)) =
match pat_aux with
| Pat_exp (pat, exp) -> separate space [doc_pat pat; string "=>"; doc_exp exp]
@@ -246,8 +270,11 @@ let doc_dec (DEC_aux (reg,_)) =
| DEC_alias(id,alspec) -> string "ALIAS"
| DEC_typ_alias(typ,id,alspec) -> string "ALIAS"
+let doc_field (typ, id) =
+ separate space [doc_id id; colon; doc_typ typ]
+
let doc_typdef (TD_aux(td,_)) = match td with
- | TD_abbrev(id, _, typschm) ->
+ | TD_abbrev (id, _, typschm) ->
begin
match doc_typschm_quants typschm with
| Some qdoc ->
@@ -255,6 +282,13 @@ let doc_typdef (TD_aux(td,_)) = match td with
| None ->
doc_op equals (concat [string "type"; space; doc_id id]) (doc_typschm_typ typschm)
end
+ | TD_enum (id, _, ids, _) ->
+ separate space [string "enum"; doc_id id; equals; surround 2 0 lbrace (separate_map (comma ^^ break 1) doc_id ids) rbrace]
+ | 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;
+ surround 2 0 lbrace (separate_map (comma ^^ break 1) doc_field fields) rbrace]
| _ -> string "TYPEDEF"
let doc_spec (VS_aux(v,_)) =
@@ -289,7 +323,7 @@ let rec doc_def def = group (match def with
| DEF_reg_dec dec -> doc_dec dec
| DEF_scattered sdef -> string "TOPLEVEL"
| DEF_overload (id, ids) ->
- separate space [string "overload"; doc_id id; equals; surround 2 0 lbrace (separate_map (semi ^^ break 1) doc_id ids) rbrace]
+ separate space [string "overload"; doc_id id; equals; surround 2 0 lbrace (separate_map (comma ^^ break 1) doc_id ids) rbrace]
| DEF_comm (DC_comm s) -> string "TOPLEVEL"
| DEF_comm (DC_comm_struct d) -> string "TOPLEVEL"
) ^^ hardline
diff --git a/src/process_file.ml b/src/process_file.ml
index 1749bc03..f176f198 100644
--- a/src/process_file.ml
+++ b/src/process_file.ml
@@ -59,20 +59,25 @@ let get_lexbuf f =
lexbuf, in_chan
let parse_file (f : string) : Parse_ast.defs =
- let scanbuf, in_chan = get_lexbuf f in
- let type_names =
- try
- Pre_parser.file Pre_lexer.token scanbuf
- with
+ if not !opt_new_parser
+ then
+ let scanbuf, in_chan = get_lexbuf f in
+ let type_names =
+ try
+ Pre_parser.file Pre_lexer.token scanbuf
+ with
| Parsing.Parse_error ->
- let pos = Lexing.lexeme_start_p scanbuf in
- raise (Reporting_basic.Fatal_error (Reporting_basic.Err_syntax (pos, "pre")))
+ let pos = Lexing.lexeme_start_p scanbuf in
+ raise (Reporting_basic.Fatal_error (Reporting_basic.Err_syntax (pos, "pre")))
| Parse_ast.Parse_error_locn(l,m) ->
- raise (Reporting_basic.Fatal_error (Reporting_basic.Err_syntax_locn (l, m)))
+ raise (Reporting_basic.Fatal_error (Reporting_basic.Err_syntax_locn (l, m)))
| Lexer.LexError(s,p) ->
- raise (Reporting_basic.Fatal_error (Reporting_basic.Err_lex (p, s))) in
- let () = Lexer.custom_type_names := !Lexer.custom_type_names @ type_names in
- close_in in_chan;
+ raise (Reporting_basic.Fatal_error (Reporting_basic.Err_lex (p, s)))
+ in
+ close_in in_chan;
+ Lexer.custom_type_names := !Lexer.custom_type_names @ type_names
+ else ();
+
let lexbuf, in_chan = get_lexbuf f in
try
let ast =
diff --git a/src/rewriter.ml b/src/rewriter.ml
index 1c02b161..82ebaec5 100644
--- a/src/rewriter.ml
+++ b/src/rewriter.ml
@@ -561,7 +561,7 @@ let rewrite_fun rewriters (FD_aux (FD_function(recopt,tannotopt,effectopt,funcls
in FD_aux (FD_function(recopt,tannotopt,effectopt,List.map rewrite_funcl funcls),(l,fdannot))
let rewrite_def rewriters d = match d with
- | DEF_type _ | DEF_kind _ | DEF_spec _ | DEF_default _ | DEF_reg_dec _ | DEF_comm _ | DEF_overload _ -> d
+ | DEF_type _ | DEF_kind _ | DEF_spec _ | DEF_default _ | DEF_reg_dec _ | DEF_comm _ | DEF_overload _ | DEF_fixity _ -> d
| DEF_fundef fdef -> DEF_fundef (rewriters.rewrite_fun rewriters fdef)
| DEF_val letbind -> DEF_val (rewriters.rewrite_let rewriters letbind)
| DEF_scattered _ -> raise (Reporting_basic.err_unreachable Parse_ast.Unknown "DEF_scattered survived to rewritter")
diff --git a/src/type_check.ml b/src/type_check.ml
index 06083211..7f204fca 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -1959,7 +1959,7 @@ let rec check_exp env (E_aux (exp_aux, (l, ())) as exp : unit exp) (Typ_aux (typ
let tpat, env = bind_pat env pat (typ_of inferred_bind) in
annot_exp (E_let (LB_aux (LB_val (tpat, inferred_bind), (let_loc, None)), crule check_exp env exp typ)) typ
end
- | E_app_infix (x, op, y), _ when List.length (Env.get_overloads (deinfix op) env) > 0 ->
+ | E_app_infix (x, op, y), _ ->
check_exp env (E_aux (E_app (deinfix op, [x; y]), (l, ()))) typ
| E_app (f, [E_aux (E_constraint nc, _)]), _ when Id.compare f (mk_id "_prove") = 0 ->
if prove env nc
@@ -2592,7 +2592,7 @@ and infer_exp env (E_aux (exp_aux, (l, ())) as exp) =
| E_cast (typ, exp) ->
let checked_exp = crule check_exp env exp typ in
annot_exp (E_cast (typ, checked_exp)) typ
- | E_app_infix (x, op, y) when List.length (Env.get_overloads (deinfix op) env) > 0 -> infer_exp env (E_aux (E_app (deinfix op, [x; y]), (l, ())))
+ | E_app_infix (x, op, y) -> infer_exp env (E_aux (E_app (deinfix op, [x; y]), (l, ())))
| E_app (f, xs) when List.length (Env.get_overloads f env) > 0 ->
let rec try_overload = function
| (errs, []) -> typ_raise l (Err_no_overloading (f, errs))
@@ -3275,6 +3275,7 @@ let rec check_def env def =
match def with
| DEF_kind kdef -> check_kinddef env kdef
| DEF_type tdef -> check_typedef env tdef
+ | DEF_fixity (prec, n, op) -> [DEF_fixity (prec, n, op)], env
| DEF_fundef fdef -> check_fundef env fdef
| DEF_val letdef -> check_letdef env letdef
| DEF_spec vs -> check_val_spec env vs
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-02 18:47:59 +0000