Merge pull request #38 from crabtw/sail2

Fix scattered mapping printing and output message for missing val spec

3 files changed, 8 insertions, 3 deletions

diff --git a/src/ocaml_backend.ml b/src/ocaml_backend.ml
index ff4a9818..9e4dbf8a 100644
--- a/src/ocaml_backend.ml
+++ b/src/ocaml_backend.ml
@@ -463,6 +463,7 @@ let ocaml_funcls ctx =
          match Bindings.find id ctx.val_specs with
          | Typ_aux (Typ_fn (typs, typ, _), _) -> (typs, typ)
          | _ -> failwith "Found val spec which was not a function!"
+         | exception Not_found -> failwith ("No val spec found for " ^ string_of_id id)
        in
        (* Any remaining type variables after simple_typ rewrite should
         ind   icate Type-polymorphism. If we have it, we need to generate
diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml
index 27f626ea..af25f189 100644
--- a/src/pretty_print_sail.ml
+++ b/src/pretty_print_sail.ml
@@ -574,7 +574,7 @@ let doc_mapdef (MD_aux (MD_mapping (id, typa, mapcls), _)) =
   | _ ->
      let sep = string "," ^^ hardline in
      let clauses = separate_map sep doc_mapcl mapcls in
-     string "mapping" ^^ space ^^ doc_id id ^^ space ^^ string "=" ^^ (surround 2 0 lbrace clauses rbrace)
+     string "mapping" ^^ space ^^ doc_id id ^^ space ^^ string "=" ^^ space ^^ (surround 2 0 lbrace clauses rbrace)
 
 let doc_dec (DEC_aux (reg,_)) =
   match reg with
@@ -663,6 +663,10 @@ let rec doc_scattered (SD_aux (sd_aux, _)) =
      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]
+  | SD_mapping (id, _) ->
+     string "scattered" ^^ space ^^ string "mapping" ^^ space ^^ doc_id id
+  | SD_mapcl (id, mapcl) ->
+     separate space [string "mapping clause"; doc_id id; equals; doc_mapcl mapcl]
 
 let rec doc_def def = group (match def with
   | DEF_default df -> doc_default df
diff --git a/src/type_check.ml b/src/type_check.ml
index 5aafe601..92425daa 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -1681,7 +1681,7 @@ let rec unify_typ l env goals (Typ_aux (aux1, _) as typ1) (Typ_aux (aux2, _) as
   | Typ_tup typs1, Typ_tup typs2 when List.length typs1 = List.length typs2 ->
      List.fold_left (merge_uvars l) KBindings.empty (List.map2 (unify_typ l env goals) typs1 typs2)
 
-  | _, _ -> unify_error l ("Cound not unify " ^ string_of_typ typ1 ^ " and " ^ string_of_typ typ2)
+  | _, _ -> unify_error l ("Could not unify " ^ string_of_typ typ1 ^ " and " ^ string_of_typ typ2)
 
 and unify_typ_arg l env goals (A_aux (aux1, _) as typ_arg1) (A_aux (aux2, _) as typ_arg2) =
   match aux1, aux2 with
@@ -1728,7 +1728,7 @@ and unify_order l goals (Ord_aux (aux1, _) as ord1) (Ord_aux (aux2, _) as ord2)
   | Ord_var v, _ when KidSet.mem v goals -> KBindings.singleton v (arg_order ord2)
   | Ord_inc, Ord_inc -> KBindings.empty
   | Ord_dec, Ord_dec -> KBindings.empty
-  | _, _ -> unify_error l ("Cound not unify " ^ string_of_order ord1 ^ " and " ^ string_of_order ord2)
+  | _, _ -> unify_error l ("Could not unify " ^ string_of_order ord1 ^ " and " ^ string_of_order ord2)
 
 and unify_nexp l env goals (Nexp_aux (nexp_aux1, _) as nexp1) (Nexp_aux (nexp_aux2, _) as nexp2) =
   typ_debug (lazy (Util.("Unify nexp " |> magenta |> clear) ^ string_of_nexp nexp1 ^ " and " ^ string_of_nexp nexp2