Don't do any rewrites when checking files for Emacs

This makes sure we don't do any kind of re-writing or de-scatter any
definitions when loading files into emacs. The difference here is that
normally all files are processed together, but the emacs mode loads
each file one by one. This is probably what we want to be doing
anyway, so location information stays accurate for scattered
functions for things like type-at-cursor commands and similar.

Also fix some warnings.

Fixes #32

7 files changed, 39 insertions, 21 deletions

diff --git a/src/ast_util.ml b/src/ast_util.ml
index 5746a242..11873690 100644
--- a/src/ast_util.ml
+++ b/src/ast_util.ml
@@ -1355,6 +1355,7 @@ and undefined_of_typ_args mwords l annot (A_aux (typ_arg_aux, _) as typ_arg) =
   match typ_arg_aux with
   | A_nexp n -> [E_aux (E_sizeof n, (l, annot (atom_typ n)))]
   | A_typ typ -> [undefined_of_typ mwords l annot typ]
+  | A_bool nc -> [E_aux (E_constraint nc, (l, annot (atom_bool_typ nc)))]
   | A_order _ -> []
 
 let destruct_pexp (Pat_aux (pexp,ann)) =
diff --git a/src/isail.ml b/src/isail.ml
index 7d009791..4cfb2c6f 100644
--- a/src/isail.ml
+++ b/src/isail.ml
@@ -276,7 +276,7 @@ let load_session upto file =
   | Some upto_file when Filename.basename upto_file = file -> None
   | Some upto_file ->
      let (_, ast, env) =
-       load_files ~generate:false !Interactive.env [Filename.concat (Filename.dirname upto_file) file]
+       load_files ~check:true !Interactive.env [Filename.concat (Filename.dirname upto_file) file]
      in
      Interactive.ast := append_ast !Interactive.ast ast;
      Interactive.env := env;
@@ -464,7 +464,7 @@ let handle_input' input =
            begin
              try
                load_into_session arg;
-               let (_, ast, env) = load_files !Interactive.env [arg] in
+               let (_, ast, env) = load_files ~check:true !Interactive.env [arg] in
                Interactive.ast := append_ast !Interactive.ast ast;
                interactive_state := initial_state !Interactive.ast Value.primops;
                Interactive.env := env;
diff --git a/src/ocaml_backend.ml b/src/ocaml_backend.ml
index d51aba75..05406413 100644
--- a/src/ocaml_backend.ml
+++ b/src/ocaml_backend.ml
@@ -710,13 +710,12 @@ let ocaml_pp_generators ctx defs orig_types required =
   and add_req_from_typarg required (A_aux (arg,_)) =
     match arg with
     | A_typ typ -> add_req_from_typ required typ
-    | A_nexp _
-    | A_order _
-      -> required
+    | A_nexp _ | A_order _ | A_bool _ -> required
   and add_req_from_td required (TD_aux (td,(l,_))) =
     match td with
     | TD_abbrev (_, _, A_aux (A_typ typ, _)) ->
        add_req_from_typ required typ
+    | TD_abbrev _ -> required
     | TD_record (_, _, fields, _) ->
        List.fold_left (fun req (typ,_) -> add_req_from_typ req typ) required fields
     | TD_variant (_, _, variants, _) ->
@@ -787,7 +786,7 @@ let ocaml_pp_generators ctx defs orig_types required =
                                        | _ -> space ^^ separate space args_pp
         in
         string ("g.gen_" ^ typ_str) ^^ args_pp
-      and typearg (A_aux (arg,_)) =
+      and typearg (A_aux (arg,l)) =
         match arg with
         | A_nexp (Nexp_aux (nexp,l) as full_nexp) ->
            (match nexp with
@@ -801,6 +800,7 @@ let ocaml_pp_generators ctx defs orig_types required =
             | Ord_inc -> string "true"
             | Ord_dec -> string "false")
         | A_typ typ -> parens (string "fun g -> " ^^ gen_type typ)
+        | A_bool nc -> raise (Reporting.err_todo l ("Unsupported constraint for generators: " ^ string_of_n_constraint nc))
       in
       let make_subgen (Typ_aux (typ,l) as full_typ) =
         let typ_str, args_pp =
diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml
index f30d5135..9a374275 100644
--- a/src/pretty_print_sail.ml
+++ b/src/pretty_print_sail.ml
@@ -619,8 +619,7 @@ let doc_typdef (TD_aux(td,_)) = match td with
   | TD_variant (id, TypQ_aux (TypQ_tq qs, _), unions, _) ->
      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"
-
+  | TD_bitfield _ -> string "BITFIELD" (* should be rewritten *)
 
 let doc_spec ?comment:(comment=false) (VS_aux (v, annot)) =
   let doc_extern ext =
@@ -656,6 +655,12 @@ let rec doc_scattered (SD_aux (sd_aux, _)) =
      string "scattered" ^^ space ^^ string "union" ^^ space ^^ doc_id id
   | SD_variant (id, TypQ_aux (TypQ_tq quants, _)) ->
      string "scattered" ^^ space ^^ string "union" ^^ space ^^ doc_id id ^^ doc_param_quants quants
+  | SD_mapcl (id, mapcl) ->
+     separate space [string "mapping clause"; doc_id id; equals; doc_mapcl mapcl]
+  | SD_mapping (id, Typ_annot_opt_aux (Typ_annot_opt_none, _)) ->
+     separate space [string "scattered mapping"; doc_id id]
+  | SD_mapping (id, Typ_annot_opt_aux (Typ_annot_opt_some (_, typ), _)) ->
+     separate space [string "scattered mapping"; doc_id id; string ":"; doc_typ typ]
   | SD_unioncl (id, tu) ->
      separate space [string "union clause"; doc_id id; equals; doc_union tu]
 
diff --git a/src/rewrites.ml b/src/rewrites.ml
index 5a70a721..31117f33 100644
--- a/src/rewrites.ml
+++ b/src/rewrites.ml
@@ -3525,7 +3525,11 @@ let rewrite_defs_mapping_patterns env =
        let mapping_in_typ = typ_of_annot p_annot in
 
        let x = Env.get_val_spec mapping_id env in
-       let (_, Typ_aux(Typ_bidir(typ1, typ2), _)) = x in
+
+       let typ1, typ2 = match x with
+         | (_, Typ_aux(Typ_bidir(typ1, typ2), _)) -> typ1, typ2
+         | (_, typ) -> raise (Reporting.err_unreachable (fst p_annot) __POS__ ("Must be bi-directional mapping: " ^ string_of_typ typ))
+       in
 
        let mapping_direction =
          if mapping_in_typ = typ1 then
@@ -4642,8 +4646,11 @@ let rec remove_clause_from_pattern ctx (P_aux (rm_pat,ann)) res_pat =
         rp' @ List.map (function [rp1;rp2] -> RP_cons (rp1,rp2) | _ -> assert false) res_pats
   end
   | P_record _ ->
-     raise (Reporting.err_unreachable (fst ann) __POS__
-              "Record pattern not supported")
+     raise (Reporting.err_unreachable (fst ann) __POS__ "Record pattern not supported")
+  | P_or _ ->
+     raise (Reporting.err_unreachable (fst ann) __POS__ "Or pattern not supported")
+  | P_not _ ->
+     raise (Reporting.err_unreachable (fst ann) __POS__ "Negated pattern not supported")
   | P_vector _
   | P_vector_concat _
   | P_string_append _ ->
diff --git a/src/sail.ml b/src/sail.ml
index 06bd618e..28c5db0a 100644
--- a/src/sail.ml
+++ b/src/sail.ml
@@ -311,7 +311,7 @@ let _ =
       opt_file_arguments := (!opt_file_arguments) @ [s])
     usage_msg
 
-let load_files ?generate:(generate=true) type_envs files =
+let load_files ?check:(check=false) type_envs files =
   if !opt_memo_z3 then Constraint.load_digests () else ();
 
   let t = Profile.start () in
@@ -320,24 +320,27 @@ let load_files ?generate:(generate=true) type_envs files =
     List.fold_right (fun (_, Parse_ast.Defs ast_nodes) (Parse_ast.Defs later_nodes)
                      -> Parse_ast.Defs (ast_nodes@later_nodes)) parsed (Parse_ast.Defs []) in
   let ast = Process_file.preprocess_ast options ast in
-  let ast = Initial_check.process_ast ~generate:generate ast in
+  let ast = Initial_check.process_ast ~generate:(not check) ast in
   Profile.finish "parsing" t;
 
   let t = Profile.start () in
   let (ast, type_envs) = check_ast type_envs ast in
   Profile.finish "type checking" t;
 
-  let ast = Scattered.descatter ast in
-  let ast = rewrite_ast type_envs ast in
+  if !opt_memo_z3 then Constraint.save_digests () else ();
 
-  let out_name = match !opt_file_out with
-    | None when parsed = [] -> "out.sail"
-    | None -> fst (List.hd parsed)
-    | Some f -> f ^ ".sail" in
+  if check then
+    ("out.sail", ast, type_envs)
+  else
+    let ast = Scattered.descatter ast in
+    let ast = rewrite_ast type_envs ast in
 
-  if !opt_memo_z3 then Constraint.save_digests () else ();
+    let out_name = match !opt_file_out with
+      | None when parsed = [] -> "out.sail"
+      | None -> fst (List.hd parsed)
+      | Some f -> f ^ ".sail" in
 
-  (out_name, ast, type_envs)
+    (out_name, ast, type_envs)
 
 let main() =
   if !opt_print_version then
diff --git a/src/specialize.ml b/src/specialize.ml
index 00357557..9f6af6d6 100644
--- a/src/specialize.ml
+++ b/src/specialize.ml
@@ -160,6 +160,8 @@ let string_of_instantiation instantiation =
        kid_name (mk_kopt K_int kid) ^ " in {" ^ Util.string_of_list ", " Big_int.to_string ns ^ "}"
     | NC_aux (NC_true, _) -> "true"
     | NC_aux (NC_false, _) -> "false"
+    | NC_aux (NC_var kid, _) -> kid_name (mk_kopt K_bool kid)
+    | NC_aux (NC_app (id, args), _) -> string_of_id id ^ "(" ^ Util.string_of_list ", " string_of_typ_arg args ^ ")"
   in
 
   let string_of_binding (kid, arg) = string_of_kid kid ^ " => " ^ string_of_typ_arg arg in