Added real number literals to sail, to better support full ASL translation

11 files changed, 35 insertions, 22 deletions

diff --git a/editors/sail-mode.el b/editors/sail-mode.el
index b667b084..e4579034 100644
--- a/editors/sail-mode.el
+++ b/editors/sail-mode.el
@@ -717,7 +717,7 @@ Based on Tuareg mode. See Tuareg mode for usage"
       2 font-lock-variable-name-face keep nil)
      ("\\<\\(typedef\\|union\\)\\>[ \t\n]*\\(\\(\\w\\|[_ \t()*,]\\)+\\)"
       2 font-lock-type-face keep nil)
-     ("\\<\\(Type\\|Nat\\|Num\\|Order\\|Effect\\|inc\\|dec\\|implicit\\|vector\\|rreg\\|wreg\\|rmem\\|wmem\\|wmv\\|eamem\\|barr\\|undef\\|escape\\|unspec\\|nondet\\|pure\\|effect\\|IN\\|forall\\|bit\\|unit\\|bool\\|nat\\|int\\)\\>"
+     ("\\<\\(Type\\|Nat\\|Num\\|Order\\|Effect\\|inc\\|dec\\|implicit\\|vector\\|rreg\\|wreg\\|rmem\\|wmem\\|wmv\\|eamem\\|barr\\|undef\\|escape\\|unspec\\|nondet\\|pure\\|effect\\|IN\\|forall\\|bit\\|unit\\|bool\\|nat\\|real\\|int\\)\\>"
       0 font-lock-type-face keep nil)
      ("\\<\\(val\\|extern\\|clause\\|and\\||let\\|rec\\>[ \t\n]*\\(\\(\\w\\|[_,?~.]\\)*\\)"
       2 font-lock-variable-name-face keep nil)
diff --git a/src/ast.ml b/src/ast.ml
index 5444e580..f26bcba8 100644
--- a/src/ast.ml
+++ b/src/ast.ml
@@ -215,7 +215,7 @@ lit_aux =  (* Literal constant *)
  | L_bin of string (* bit vector constant, C-style *)
  | L_undef (* constant representing undefined values *)
  | L_string of string (* string constant *)
-
+ | L_real of string
 
 type
 typquant =
diff --git a/src/ast_util.ml b/src/ast_util.ml
index fc59fcf2..d8e1e7a6 100644
--- a/src/ast_util.ml
+++ b/src/ast_util.ml
@@ -250,6 +250,7 @@ let string_of_lit (L_aux (lit, _)) =
   | L_hex n -> "0x" ^ n
   | L_bin n -> "0b" ^ n
   | L_undef -> "undefined"
+  | L_real r -> r
   | L_string str -> "\"" ^ str ^ "\""
 
 let rec string_of_exp (E_aux (exp, _)) =
diff --git a/src/initial_check.ml b/src/initial_check.ml
index 89dad186..528a1526 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -392,6 +392,7 @@ let to_ast_lit (Parse_ast.L_aux(lit,l)) : lit =
     | Parse_ast.L_num(i) -> L_num(i)
     | Parse_ast.L_hex(h) -> L_hex(h)
     | Parse_ast.L_bin(b) -> L_bin(b)
+    | Parse_ast.L_real r -> L_real r
     | Parse_ast.L_string(s) -> L_string(s))
       ,l)
 
diff --git a/src/lexer.mll b/src/lexer.mll
index 36aefb1d..76f2e0a5 100644
--- a/src/lexer.mll
+++ b/src/lexer.mll
@@ -134,7 +134,7 @@ let kw_table =
 
 ]
 
-let default_type_names = ["bool";"unit";"vector";"range";"list";"bit";"nat"; "int";
+let default_type_names = ["bool";"unit";"vector";"range";"list";"bit";"nat"; "int"; "real";
 			  "uint8";"uint16";"uint32";"uint64";"atom";"implicit";"string";"option"]
 let custom_type_names : string list ref = ref []
 
@@ -310,16 +310,18 @@ rule token = parse
   | "*_ui" oper_char+ as i				{ (StarUnderUiI(r i)) }
   | "2^" oper_char+ as i				{ (TwoCarrotI(r i)) }
 
-  | digit+ as i                         { (Num(int_of_string i)) }
-  | "-" digit+ as i                     { (Num(int_of_string i)) }
-  | "0b" (binarydigit+ as i)		{ (Bin(i)) }
-  | "0x" (hexdigit+ as i) 		{ (Hex(i)) }
-  | '"'                                 { (String(
-                                           string (Lexing.lexeme_start_p lexbuf) (Buffer.create 10) lexbuf)) }
-  | eof                                 { Eof }
-  | _  as c                             { raise (LexError(
-                                          Printf.sprintf "Unexpected character: %c" c,
-                                          Lexing.lexeme_start_p lexbuf)) }
+  | (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)) }
+  | "0b" (binarydigit+ as i)	          { (Bin(i)) }
+  | "0x" (hexdigit+ as i) 		  { (Hex(i)) }
+  | '"'                                   { (String(
+					     string (Lexing.lexeme_start_p lexbuf) (Buffer.create 10) lexbuf)) }
+  | eof                                   { Eof }
+  | _  as c                               { raise (LexError(
+					    Printf.sprintf "Unexpected character: %c" c,
+					    Lexing.lexeme_start_p lexbuf)) }
 
 
 and comment pos depth = parse
diff --git a/src/parse_ast.ml b/src/parse_ast.ml
index 4529aa8f..e020e0d5 100644
--- a/src/parse_ast.ml
+++ b/src/parse_ast.ml
@@ -207,7 +207,7 @@ lit_aux =  (* Literal constant *)
  | L_bin of string (* bit vector constant, C-style *)
  | L_undef (* undefined value *)
  | L_string of string (* string constant *)
-
+ | L_real of string
 
 type 
 typschm_aux =  (* type scheme *)
diff --git a/src/parser.mly b/src/parser.mly
index b64e0de6..0b3d3a5e 100644
--- a/src/parser.mly
+++ b/src/parser.mly
@@ -150,7 +150,7 @@ let make_vector_sugar order_set is_inc typ typ1 =
 
 %token <string> Id TyVar TyId
 %token <int> Num
-%token <string> String Bin Hex
+%token <string> String Bin Hex Real
 
 %token <string> Amp At Carrot  Div Eq Excl Gt Lt Plus Star Tilde
 %token <string> AmpAmp CarrotCarrot Colon ColonColon EqEq ExclEq ExclExcl
@@ -463,6 +463,8 @@ lit:
     { lloc (L_bin $1) }
   | Hex
     { lloc (L_hex $1) }
+  | Real
+    { lloc (L_real $1) }
   | Undefined
     { lloc L_undef }
   | Bitzero
diff --git a/src/type_check_new.ml b/src/type_check_new.ml
index 094d11de..9aeded29 100644
--- a/src/type_check_new.ml
+++ b/src/type_check_new.ml
@@ -84,6 +84,7 @@ 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")
 let bit_typ = mk_id_typ (mk_id "bit")
+let real_typ = mk_id_typ (mk_id "real")
 let app_typ id args = mk_typ (Typ_app (id, args))
 let atom_typ nexp = mk_typ (Typ_app (mk_id "atom", [mk_typ_arg (Typ_arg_nexp nexp)]))
 let range_typ nexp1 nexp2 = mk_typ (Typ_app (mk_id "range", [mk_typ_arg (Typ_arg_nexp nexp1); mk_typ_arg (Typ_arg_nexp nexp2)]))
@@ -459,6 +460,7 @@ end = struct
     || Id.compare id (mk_id "int") = 0
     || Id.compare id (mk_id "nat") = 0
     || Id.compare id (mk_id "bool") = 0
+    || Id.compare id (mk_id "real") = 0
 
   (* Check if a type, order, or n-expression is well-formed. Throws a
      type error if the type is badly formed. FIXME: Add arity to type
@@ -1286,13 +1288,14 @@ type tannot = (Env.t * typ * effect) option
 
 let infer_lit env (L_aux (lit_aux, l) as lit) =
   match lit_aux with
-  | L_unit -> mk_typ (Typ_id (mk_id "unit"))
-  | L_zero -> mk_typ (Typ_id (mk_id "bit"))
-  | L_one -> mk_typ (Typ_id (mk_id "bit"))
-  | L_num n -> mk_typ (Typ_app (mk_id "atom", [mk_typ_arg (Typ_arg_nexp (nconstant n))]))
-  | L_true -> mk_typ (Typ_id (mk_id "bool"))
-  | L_false -> mk_typ (Typ_id (mk_id "bool"))
-  | L_string _ -> mk_typ (Typ_id (mk_id "string"))
+  | L_unit -> unit_typ
+  | L_zero -> bit_typ
+  | L_one -> bit_typ
+  | L_num n -> atom_typ (nconstant n)
+  | L_true -> bool_typ
+  | L_false -> bool_typ
+  | L_string _ -> string_typ
+  | L_real _ -> real_typ
   | L_bin str ->
      begin
        match Env.get_default_order env with
diff --git a/src/type_check_new.mli b/src/type_check_new.mli
index d4fe97e7..2989aa1d 100644
--- a/src/type_check_new.mli
+++ b/src/type_check_new.mli
@@ -145,6 +145,7 @@ val bit_typ : typ
 val bool_typ : typ
 val unit_typ : typ
 val string_typ : typ
+val real_typ : typ
 val vector_typ : nexp -> nexp -> order -> typ -> typ
 
 (* Vector with default order. *)
diff --git a/src/type_internal.ml b/src/type_internal.ml
index 5df5e94d..96e8fbe1 100644
--- a/src/type_internal.ml
+++ b/src/type_internal.ml
@@ -1956,6 +1956,7 @@ let initial_kind_env =
     ("unit", {k = K_Typ});
     ("bit", {k = K_Typ});
     ("string", {k = K_Typ});
+    ("real", {k = K_Typ});
     ("list", {k = K_Lam( [{k = K_Typ}], {k = K_Typ})});
     ("reg", {k = K_Lam( [{k = K_Typ}], {k= K_Typ})});
     ("register", {k = K_Lam( [{k = K_Typ}], {k= K_Typ})});
diff --git a/test/typecheck/pass/real.sail b/test/typecheck/pass/real.sail
new file mode 100644
index 00000000..5ae1456b
--- /dev/null
+++ b/test/typecheck/pass/real.sail
@@ -0,0 +1,2 @@
+
+let (real) r = 2.2