Improvements for v85

11 files changed, 62 insertions, 36 deletions

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 <options> <file1.sail> ... <fileN.sail>\n"
-    )
+  version
+  ^ "\nusage: sail <options> <file1.sail> ... <fileN.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> -> 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