Fix a few AST and parsing-related bugs

6 files changed, 40 insertions, 15 deletions

diff --git a/src/monomorphise.ml b/src/monomorphise.ml
index 2c3dda0e..f00cfd44 100644
--- a/src/monomorphise.ml
+++ b/src/monomorphise.ml
@@ -1438,6 +1438,8 @@ let split_defs splits defs =
       | DEF_reg_dec _
       | DEF_comm _
       | DEF_overload _
+      | DEF_fixity _
+      | DEF_internal_mutrec _
         -> [d]
       | DEF_fundef fd -> [DEF_fundef (map_fundef fd)]
       | DEF_val lb -> [DEF_val (map_letbind lb)]
@@ -1447,4 +1449,3 @@ let split_defs splits defs =
     Defs (List.concat (List.map map_def defs))
   in
   map_locs splits defs'
-
diff --git a/src/parser.mly b/src/parser.mly
index df4a273d..8c055b33 100644
--- a/src/parser.mly
+++ b/src/parser.mly
@@ -1064,6 +1064,14 @@ val_spec:
     { vloc (VS_val_spec (mk_typschm $3 $4 3 4,$5, Some $7, false)) }
   | Val Extern typ id Eq String
     { vloc (VS_val_spec (mk_typschm (mk_typqn ()) $3 3 3,$4, Some $6, false)) }
+  | Val Cast Extern typquant typ id
+    { vloc (VS_val_spec (mk_typschm $4 $5 4 5,$6, Some (string_of_id $6), true)) }
+  | Val Cast Extern typ id
+    { vloc (VS_val_spec (mk_typschm (mk_typqn ()) $4 4 4, $5, Some (string_of_id $5), true)) }
+  | Val Cast Extern typquant typ id Eq String
+    { vloc (VS_val_spec (mk_typschm $4 $5 4 5,$6, Some $8, true)) }
+  | Val Cast Extern typ id Eq String
+    { vloc (VS_val_spec (mk_typschm (mk_typqn ()) $4 4 4,$5, Some $7, true)) }
 
 kinded_id:
   | tyvar
@@ -1335,4 +1343,3 @@ file:
 
 nonempty_exp_list:
   | semi_exps_help Eof { $1 }
-
diff --git a/src/parser2.mly b/src/parser2.mly
index 5a4ad667..78724c4d 100644
--- a/src/parser2.mly
+++ b/src/parser2.mly
@@ -487,6 +487,9 @@ atomic_typ:
     { mk_typ ATyp_inc $startpos $endpos }
   | id Lparen typ_list Rparen
     { mk_typ (ATyp_app ($1, $3)) $startpos $endpos }
+  | Register Lparen typ Rparen
+    { let register_id = mk_id (Id "register") $startpos $endpos in
+      mk_typ (ATyp_app (register_id, [$3])) $startpos $endpos }
   | Lparen typ Rparen
     { $2 }
   | Lparen typ Comma typ_list Rparen
diff --git a/src/pretty_print_lem_ast.ml b/src/pretty_print_lem_ast.ml
index 2232b4de..fa387ad4 100644
--- a/src/pretty_print_lem_ast.ml
+++ b/src/pretty_print_lem_ast.ml
@@ -57,8 +57,17 @@ let rec list_pp i_format l_format =
     | [i] -> fprintf ppf "%a" l_format i
     | i::is -> fprintf ppf "%a%a" i_format i (list_pp i_format l_format) is
 
+let pp_option_lem some_format =
+  fun ppf opt ->
+    match opt with
+    | Some a -> fprintf ppf "(Just %a)" some_format a
+    | None -> fprintf ppf "Nothing"
+
+let pp_bool_lem ppf b = fprintf ppf (if b then "true" else "false")
+
 let kwd ppf s = fprintf ppf "%s" s
 let base ppf s = fprintf ppf "%s" s
+let quot_string ppf s = fprintf ppf "\"%s\"" s
 
 let lemnum default n = match n with
   | 0   -> "zero"
@@ -523,12 +532,8 @@ let pp_lem_default ppf (DT_aux(df,l)) =
 let pp_lem_spec ppf (VS_aux(v,(l,annot))) =
   let print_spec ppf v =
     match v with
-    | VS_val_spec(ts,id,None,false) ->
-      fprintf ppf "@[<0>(%a %a %a)@]@\n" kwd "VS_val_spec" pp_lem_typscm ts pp_lem_id id
-    | VS_val_spec(ts,id,Some s,false) ->
-      fprintf ppf "@[<0>(%a %a %a \"%s\")@]@\n" kwd "VS_extern_spec" pp_lem_typscm ts pp_lem_id id s
-    | VS_val_spec(ts,id,None,true) ->
-       fprintf ppf "@[<0>(%a %a %a)@]@\n" kwd "VS_cast_spec" pp_lem_typscm ts pp_lem_id id
+    | VS_val_spec(ts,id,ext_opt,is_cast) ->
+      fprintf ppf "@[<0>(%a %a %a %a %a)@]@\n" kwd "VS_val_spec" pp_lem_typscm ts pp_lem_id id (pp_option_lem quot_string) ext_opt pp_bool_lem is_cast
     | _ -> failwith "Invalid valspec"
   in
   fprintf ppf "@[<0>(VS_aux %a (%a, %a))@]" print_spec v pp_lem_l l pp_annot annot
diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml
index d346c801..a870f454 100644
--- a/src/pretty_print_sail.ml
+++ b/src/pretty_print_sail.ml
@@ -408,13 +408,13 @@ let doc_default (DT_aux(df,_)) = match df with
   | DT_order(ord) -> separate space [string "default"; string "Order"; doc_ord ord]
 
 let doc_spec (VS_aux(v,_)) = match v with
-  | VS_val_spec(ts,id,None,false) ->
-     separate space [string "val"; doc_typscm ts; doc_id id]
-  | VS_val_spec (ts, id,None,true) ->
-     separate space [string "val"; string "cast"; doc_typscm ts; doc_id id]
-  | VS_val_spec(ts,id,Some ext,false) ->
-     separate space [string "val"; string "extern"; doc_typscm ts;
-                     doc_op equals (doc_id id) (dquotes (string ext))]
+  | VS_val_spec(ts,id,ext_opt,is_cast) ->
+     let cast_pp = if is_cast then [string "cast"] else [] in
+     let extern_kwd_pp, id_pp = match ext_opt with
+       | Some ext -> [string "extern"], doc_op equals (doc_id id) (dquotes (string ext))
+       | None -> [], doc_id id
+     in
+     separate space ([string "val"] @ cast_pp @ extern_kwd_pp @ [doc_typscm ts] @ [id_pp])
   | _ -> failwith "Invalid valspec"
 
 let doc_namescm (Name_sect_aux(ns,_)) = match ns with
diff --git a/src/pretty_print_sail2.ml b/src/pretty_print_sail2.ml
index 5662fe1a..39fc25d3 100644
--- a/src/pretty_print_sail2.ml
+++ b/src/pretty_print_sail2.ml
@@ -300,6 +300,10 @@ let doc_dec (DEC_aux (reg,_)) =
 let doc_field (typ, id) =
   separate space [doc_id id; colon; doc_typ typ]
 
+let doc_union (Tu_aux (tu, l)) = match tu with
+  | Tu_id id -> doc_id id
+  | Tu_ty_id (typ, id) -> separate space [doc_id id; colon; doc_typ typ]
+
 let doc_typdef (TD_aux(td,_)) = match td with
   | TD_abbrev (id, _, typschm) ->
      begin
@@ -316,6 +320,11 @@ let doc_typdef (TD_aux(td,_)) = match td with
   | 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]
+  | TD_variant (id, _, TypQ_aux (TypQ_no_forall, _), unions, _) | TD_variant (id, _, TypQ_aux (TypQ_tq [], _), unions, _) ->
+     separate space [string "union"; doc_id id; equals; surround 2 0 lbrace (separate_map (comma ^^ break 1) doc_union unions) rbrace]
+  | TD_variant (id, _, TypQ_aux (TypQ_tq qs, _), unions, _) ->
+     separate space [string "union"; doc_id id; doc_quants qs; equals;
+                     surround 2 0 lbrace (separate_map (comma ^^ break 1) doc_union unions) rbrace]
   | _ -> string "TYPEDEF"
 
 let doc_spec (VS_aux(v,_)) =