Better pretty printing for sail functions with no inline type annotations

Also added some additional helper functions in type_check_new.mli and changed real literals slightly

5 files changed, 16 insertions, 5 deletions

diff --git a/src/lexer.mll b/src/lexer.mll
index 12640480..34fd56f9 100644
--- a/src/lexer.mll
+++ b/src/lexer.mll
@@ -310,7 +310,7 @@ rule token = parse
   | "*_ui" oper_char+ as i				{ (StarUnderUiI(r i)) }
   | "2^" oper_char+ as i				{ (TwoCarrotI(r i)) }
 
-  | (digit* as i1) "." (digit+ as i2)     { (Real (i1 ^ "." ^ i2)) }
+  | (digit+ as i1) "." (digit+ as i2)     { (Real (i1 ^ "." ^ i2)) }
   | "-" (digit* as i1) "." (digit+ as i2) { (Real ("-" ^ i1 ^ "." ^ i2)) }
   | digit+ as i                           { (Num(int_of_string i)) }
   | "-" digit+ as i                       { (Num(int_of_string i)) }
diff --git a/src/parser.mly b/src/parser.mly
index 0b3d3a5e..6a76cec9 100644
--- a/src/parser.mly
+++ b/src/parser.mly
@@ -405,6 +405,8 @@ nexp_typ:
     { tloc (ATyp_sum ($1, $3)) }
   | nexp_typ Minus nexp_typ2
     { tloc (ATyp_minus ($1, $3)) }
+  | Minus nexp_typ2
+    { tloc (ATyp_neg $2) }
   | nexp_typ2
     { $1 }
 
diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml
index 7544146e..d4278b56 100644
--- a/src/pretty_print_sail.ml
+++ b/src/pretty_print_sail.ml
@@ -489,10 +489,10 @@ let doc_rec (Rec_aux(r,_)) = match r with
   | Rec_nonrec -> empty
   (* include trailing space because caller doesn't know if we return
    * empty *)
-  | Rec_rec -> string "rec" ^^ space
+  | Rec_rec -> space ^^ string "rec"
 
 let doc_tannot_opt (Typ_annot_opt_aux(t,_)) = match t with
-  | Typ_annot_opt_some(tq,typ) -> doc_typquant tq (doc_typ typ)
+  | Typ_annot_opt_some(tq,typ) -> space ^^ doc_typquant tq (doc_typ typ)
   | Typ_annot_opt_none -> empty
 
 let doc_effects_opt (Effect_opt_aux(e,_)) = match e with
@@ -508,8 +508,7 @@ let doc_fundef (FD_aux(FD_function(r, typa, efa, fcls),_)) =
   | _ ->
       let sep = hardline ^^ string "and" ^^ space in
       let clauses = separate_map sep doc_funcl fcls in
-      separate space ([string "function";
-                      doc_rec r ^^ doc_tannot_opt typa;]@
+      separate space ([string "function" ^^ doc_rec r ^^ doc_tannot_opt typa]@
                       (match efa with
                        | Effect_opt_aux (Effect_opt_pure,_) -> []
                        | _ -> [string "effect";
diff --git a/src/type_check_new.ml b/src/type_check_new.ml
index 5e625112..69994797 100644
--- a/src/type_check_new.ml
+++ b/src/type_check_new.ml
@@ -80,6 +80,9 @@ let mk_infix_id str = Id_aux (DeIid str, Parse_ast.Unknown)
 
 let mk_id_typ id = Typ_aux (Typ_id id, Parse_ast.Unknown)
 
+let inc_ord = Ord_aux (Ord_inc, Parse_ast.Unknown)
+let dec_ord = Ord_aux (Ord_dec, Parse_ast.Unknown)
+
 let int_typ = mk_id_typ (mk_id "int")
 let nat_typ = mk_id_typ (mk_id "nat")
 let unit_typ = mk_id_typ (mk_id "unit")
@@ -109,6 +112,8 @@ let is_range (Typ_aux (typ_aux, _)) =
 let nconstant c = Nexp_aux (Nexp_constant c, Parse_ast.Unknown)
 let nminus n1 n2 = Nexp_aux (Nexp_minus (n1, n2), Parse_ast.Unknown)
 let nsum n1 n2 = Nexp_aux (Nexp_sum (n1, n2), Parse_ast.Unknown)
+let ntimes n1 n2 = Nexp_aux (Nexp_times (n1, n2), Parse_ast.Unknown)
+let npow2 n = Nexp_aux (Nexp_exp n, Parse_ast.Unknown)
 let nvar kid = Nexp_aux (Nexp_var kid, Parse_ast.Unknown)
 
 let nc_lteq n1 n2 = NC_aux (NC_bounded_le (n1, n2), Parse_ast.Unknown)
diff --git a/src/type_check_new.mli b/src/type_check_new.mli
index 757b6fe3..a8a1378d 100644
--- a/src/type_check_new.mli
+++ b/src/type_check_new.mli
@@ -134,6 +134,8 @@ val equal_effects : effect -> effect -> bool
 val nconstant : int -> nexp
 val nminus : nexp -> nexp -> nexp
 val nsum : nexp -> nexp -> nexp
+val ntimes : nexp -> nexp -> nexp
+val npow2 : nexp -> nexp
 val nvar : kid -> nexp
 
 (* Sail builtin types. *)
@@ -148,6 +150,9 @@ val string_typ : typ
 val real_typ : typ
 val vector_typ : nexp -> nexp -> order -> typ -> typ
 
+val inc_ord : order
+val dec_ord : order
+
 (* Vector with default order. *)
 val dvector_typ : Env.t -> nexp -> nexp -> typ -> typ