From eb837a0ae70ef5dc8a2a3a28d59a736c57a952b3 Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Tue, 8 Jan 2019 17:08:34 +0000 Subject: Improvements for v85 --- src/ast_util.ml | 2 +- src/error_format.ml | 12 ++++++------ src/lexer.mll | 1 - src/parser.mly | 2 +- src/pretty_print_sail.ml | 2 ++ src/rewrites.ml | 16 ++++++++++------ src/sail.ml | 20 +++++++++++++++----- src/specialize.ml | 2 ++ src/type_check.ml | 2 +- src/type_check.mli | 2 ++ src/type_error.ml | 37 ++++++++++++++++++++++--------------- 11 files changed, 62 insertions(+), 36 deletions(-) (limited to 'src') diff --git a/src/ast_util.ml b/src/ast_util.ml index b04a07e3..14f3346a 100644 --- a/src/ast_util.ml +++ b/src/ast_util.ml @@ -128,7 +128,7 @@ let mk_val_spec vs_aux = let kopt_kid (KOpt_aux (KOpt_kind (_, kid), _)) = kid let kopt_kind (KOpt_aux (KOpt_kind (k, _), _)) = k - + let is_nat_kopt = function | KOpt_aux (KOpt_kind (K_aux (K_int, _), _), _) -> true | _ -> false diff --git a/src/error_format.ml b/src/error_format.ml index f152f0ae..8e00c2b7 100644 --- a/src/error_format.ml +++ b/src/error_format.ml @@ -114,18 +114,18 @@ type message = let bullet = Util.(clear (blue "*")) -let rec format_message msg = +let rec format_message msg ppf = match msg with | Location (l, msg) -> - format_loc l (format_message msg) + format_loc l (format_message msg) ppf | Line str -> - format_endline str + format_endline str ppf | Seq messages -> - fun ppf -> List.iter (fun msg -> format_message msg ppf) messages + List.iter (fun msg -> format_message msg ppf) messages | List list -> let format_list_item ppf (header, msg) = format_endline (Util.(clear (blue "*")) ^ " " ^ header) ppf; format_message msg { ppf with indent = ppf.indent ^ " " } in - fun ppf -> List.iter (format_list_item ppf) list - | With (f, msg) -> fun ppf -> format_message msg (f ppf) + List.iter (format_list_item ppf) list + | With (f, msg) -> format_message msg (f ppf) diff --git a/src/lexer.mll b/src/lexer.mll index 55e765d9..8df728e2 100644 --- a/src/lexer.mll +++ b/src/lexer.mll @@ -163,7 +163,6 @@ let kw_table = ("do", (fun _ -> Do)); ("mutual", (fun _ -> Mutual)); ("bitfield", (fun _ -> Bitfield)); - ("where", (fun _ -> Where)); ("barr", (fun x -> Barr)); ("depend", (fun x -> Depend)); diff --git a/src/parser.mly b/src/parser.mly index ef30991f..3b42d498 100644 --- a/src/parser.mly +++ b/src/parser.mly @@ -177,7 +177,7 @@ let rec desugar_rchain chain s e = /*Terminals with no content*/ -%token And As Assert Bitzero Bitone By Match Clause Dec Default Effect End Op Where +%token And As Assert Bitzero Bitone By Match Clause Dec Default Effect End Op %token Enum Else False Forall Foreach Overload Function_ Mapping If_ In Inc Let_ Int Order Bool Cast %token Pure Register Return Scattered Sizeof Struct Then True TwoCaret TYPE Typedef %token Undefined Union Newtype With Val Constraint Throw Try Catch Exit Bitfield diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml index df494036..75a7e4f9 100644 --- a/src/pretty_print_sail.ml +++ b/src/pretty_print_sail.ml @@ -371,6 +371,8 @@ let rec doc_exp (E_aux (e_aux, _) as exp) = | E_if (if_exp, then_exp, else_exp) when if_block_then then_exp -> (separate space [string "if"; doc_exp if_exp; string "then"] ^//^ doc_exp then_exp) ^/^ (string "else" ^^ space ^^ doc_exp else_exp) + | E_if (if_exp, then_exp, E_aux ((E_lit (L_aux (L_unit, _)) | E_block []), _)) -> + group (separate space [string "if"; doc_exp if_exp; string "then"; doc_exp then_exp]) | 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]) diff --git a/src/rewrites.ml b/src/rewrites.ml index 9f082f49..7536edf4 100644 --- a/src/rewrites.ml +++ b/src/rewrites.ml @@ -2274,25 +2274,29 @@ let rewrite_fix_val_specs (Defs defs) = (* Turn constraints into numeric expressions with sizeof *) let rewrite_constraint = - let rec rewrite_nc (NC_aux (nc_aux, l)) = mk_exp (rewrite_nc_aux nc_aux) - and rewrite_nc_aux = function + let rec rewrite_nc env (NC_aux (nc_aux, l)) = mk_exp (rewrite_nc_aux l env nc_aux) + and rewrite_nc_aux l env = function | NC_bounded_ge (n1, n2) -> E_app_infix (mk_exp (E_sizeof n1), mk_id ">=", mk_exp (E_sizeof n2)) | NC_bounded_le (n1, n2) -> E_app_infix (mk_exp (E_sizeof n1), mk_id "<=", mk_exp (E_sizeof n2)) | NC_equal (n1, n2) -> E_app_infix (mk_exp (E_sizeof n1), mk_id "==", mk_exp (E_sizeof n2)) | NC_not_equal (n1, n2) -> E_app_infix (mk_exp (E_sizeof n1), mk_id "!=", mk_exp (E_sizeof n2)) - | NC_and (nc1, nc2) -> E_app_infix (rewrite_nc nc1, mk_id "&", rewrite_nc nc2) - | NC_or (nc1, nc2) -> E_app_infix (rewrite_nc nc1, mk_id "|", rewrite_nc nc2) + | NC_and (nc1, nc2) -> E_app_infix (rewrite_nc env nc1, mk_id "&", rewrite_nc env nc2) + | NC_or (nc1, nc2) -> E_app_infix (rewrite_nc env nc1, mk_id "|", rewrite_nc env nc2) | NC_false -> E_lit (mk_lit L_false) | NC_true -> E_lit (mk_lit L_true) | NC_set (kid, []) -> E_lit (mk_lit (L_false)) | NC_set (kid, int :: ints) -> let kid_eq kid int = nc_eq (nvar kid) (nconstant int) in - unaux_exp (rewrite_nc (List.fold_left (fun nc int -> nc_or nc (kid_eq kid int)) (kid_eq kid int) ints)) + unaux_exp (rewrite_nc env (List.fold_left (fun nc int -> nc_or nc (kid_eq kid int)) (kid_eq kid int) ints)) + | NC_app (f, args) -> + unaux_exp (rewrite_nc env (Env.expand_constraint_synonyms env (mk_nc (NC_app (f, args))))) + | NC_var v -> + Reporting.unreachable l __POS__ "Cannot rewrite this constraint" in let rewrite_e_aux (E_aux (e_aux, _) as exp) = match e_aux with | E_constraint nc -> - check_exp (env_of exp) (rewrite_nc nc) bool_typ + check_exp (env_of exp) (rewrite_nc (env_of exp) nc) bool_typ | _ -> exp in diff --git a/src/sail.ml b/src/sail.ml index 71bf4577..7bf7d135 100644 --- a/src/sail.ml +++ b/src/sail.ml @@ -261,10 +261,22 @@ let options = Arg.align ([ " print version"); ] ) +let version = + let open Manifest in + let default = Printf.sprintf "Sail %s @ %s" branch commit in + (* version is parsed from the output of git describe *) + match String.split_on_char '-' version with + | [vnum; _; _] -> + (try + let vnum = float_of_string vnum +. 2.0 in + Printf.sprintf "Sail %.1f (%s @ %s)" vnum branch commit + with + | Failure _ -> default) + | _ -> default + let usage_msg = - ("Sail 2.0\n" - ^ "usage: sail ... \n" - ) + version + ^ "\nusage: sail ... \n" let _ = Arg.parse options @@ -272,7 +284,6 @@ let _ = opt_file_arguments := (!opt_file_arguments) @ [s]) usage_msg - let load_files type_envs files = if !opt_memo_z3 then Constraint.load_digests () else (); @@ -344,7 +355,6 @@ let main() = | _ -> Some (Ocaml_backend.orig_types_for_ocaml_generator ast, !opt_ocaml_generators) in - (*let _ = Printf.eprintf "Type checked, next to pretty print" in*) begin (if !(Interactive.opt_interactive) then diff --git a/src/specialize.ml b/src/specialize.ml index b619edde..e7f686d8 100644 --- a/src/specialize.ml +++ b/src/specialize.ml @@ -258,6 +258,7 @@ and typ_arg_frees ?exs:(exs=KidSet.empty) (A_aux (typ_arg_aux, l)) = | A_nexp n -> KidSet.empty | A_typ typ -> typ_frees ~exs:exs typ | A_order ord -> KidSet.empty + | A_bool _ -> KidSet.empty let rec typ_int_frees ?exs:(exs=KidSet.empty) (Typ_aux (typ_aux, l)) = match typ_aux with @@ -275,6 +276,7 @@ and typ_arg_int_frees ?exs:(exs=KidSet.empty) (A_aux (typ_arg_aux, l)) = | A_nexp n -> KidSet.diff (tyvars_of_nexp n) exs | A_typ typ -> typ_int_frees ~exs:exs typ | A_order ord -> KidSet.empty + | A_bool _ -> KidSet.empty let specialize_id_valspec instantiations id ast = match split_defs (is_valspec id) ast with diff --git a/src/type_check.ml b/src/type_check.ml index b891f4c7..4ed234f2 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -1076,7 +1076,7 @@ end = struct let add_constraint constr env = wf_constraint env constr; - let (NC_aux (nc_aux, l) as constr) = expand_constraint_synonyms env constr in + let (NC_aux (nc_aux, l) as constr) = constraint_simp (expand_constraint_synonyms env constr) in match nc_aux with | NC_true -> env | _ -> diff --git a/src/type_check.mli b/src/type_check.mli index e3a22c8d..7a5a3446 100644 --- a/src/type_check.mli +++ b/src/type_check.mli @@ -184,6 +184,8 @@ module Env : sig old one. *) val fresh_kid : ?kid:kid -> t -> kid + val expand_constraint_synonyms : t -> n_constraint -> n_constraint + val expand_synonyms : t -> typ -> typ (** Expand type synonyms and remove register annotations (i.e. register -> t)) *) diff --git a/src/type_error.ml b/src/type_error.ml index 6f856480..e75d2cd4 100644 --- a/src/type_error.ml +++ b/src/type_error.ml @@ -151,21 +151,28 @@ let rec string_of_type_error err = Buffer.contents b let rec collapse_errors = function - | (Err_no_overloading (_, (err :: errs)) as no_collapse) -> - let err = collapse_errors (snd err) in - let errs = List.map (fun (_, err) -> collapse_errors err) errs in - let fold_equal msg err = - match msg, err with - | Some msg, Err_no_overloading _ -> Some msg - | Some msg, Err_other _ -> Some msg - | Some msg, Err_no_casts _ -> Some msg - | Some msg, err when msg = string_of_type_error err -> Some msg - | _, _ -> None - in - begin match List.fold_left fold_equal (Some (string_of_type_error err)) errs with - | Some _ -> err - | None -> no_collapse - end + | (Err_no_overloading (_, errs) as no_collapse) -> + let errs = List.map (fun (_, err) -> collapse_errors err) errs in + let interesting = function + | Err_other _ -> false + | Err_no_casts _ -> false + | _ -> true + in + begin match List.filter interesting errs with + | err :: errs -> + let fold_equal msg err = + match msg, err with + | Some msg, Err_no_overloading _ -> Some msg + | Some msg, Err_no_casts _ -> Some msg + | Some msg, err when msg = string_of_type_error err -> Some msg + | _, _ -> None + in + begin match List.fold_left fold_equal (Some (string_of_type_error err)) errs with + | Some _ -> err + | None -> no_collapse + end + | [] -> no_collapse + end | Err_because (err1, l, err2) as no_collapse -> let err1 = collapse_errors err1 in let err2 = collapse_errors err2 in -- cgit v1.2.3