fixed issue #7

bench/bench

@@ -182,6 +182,7 @@ goods bench/typing/bad --parse-only
 goods bench/programs/bad-typing --parse-only
 bads bench/typing/bad --type-only
 bads bench/programs/bad-typing --type-only
+bads examples/bad-bts
 echo ""
 
 echo "=== Checking good files ==="

examples/bad-bts/7.why

+
+(* Issue #7:
+
+   https://gitlab.inria.fr/why3/why3/issues/7
+
+*)
+
+theory T
+  use ieee_float.Float32 as B32
+  goal g : (1.:B32.t) = (1:B32.t)
+end

src/core/pretty.ml

@@ -554,8 +554,10 @@ let () = Exn_printer.register
       fprintf fmt "Not a term: %a" print_term t
   | Term.FmlaExpected t ->
       fprintf fmt "Not a formula: %a" print_term t
-  | Term.InvalidLiteralType ty ->
-      fprintf fmt "Type %a cannot be used for a numeric literal" print_ty ty
+  | Term.InvalidIntegerLiteralType ty ->
+      fprintf fmt "Cannot cast an integer literal to type %a" print_ty ty
+  | Term.InvalidRealLiteralType ty ->
+      fprintf fmt "Cannot cast a real literal to type %a" print_ty ty
   | Pattern.ConstructorExpected (ls,ty) ->
       fprintf fmt "%s %a is not a constructor of type %a"
         (if ls.ls_value = None then "Predicate" else "Function") print_ls ls

src/core/term.ml

@@ -825,26 +825,32 @@ let ps_app ps tl    = t_app ps tl None
 let t_nat_const n =
   t_const (Number.ConstInt (Number.int_const_dec (string_of_int n))) ty_int
 
-exception InvalidLiteralType of ty
+exception InvalidIntegerLiteralType of ty
+exception InvalidRealLiteralType of ty
 
 let t_const c ty =
   let ts = match ty.ty_node with
     | Tyapp (ts,[]) -> ts
-    | _ -> raise (InvalidLiteralType ty) in
-  begin match c with
-    | Number.ConstInt c when not (ts_equal ts ts_int) ->
-        begin match ts.ts_def with
-          | Range ir -> Number.check_range c ir
-          | _ -> raise (InvalidLiteralType ty)
-        end
-    | Number.ConstReal c when not (ts_equal ts ts_real) ->
-        begin match ts.ts_def with
-          | Float fp -> Number.check_float c fp
-          | _ -> raise (InvalidLiteralType ty)
-        end
-    | _ -> ()
-  end;
-  t_const c ty
+    | _ ->
+       match c with
+             | Number.ConstInt _ -> raise (InvalidIntegerLiteralType ty)
+             | Number.ConstReal _ -> raise (InvalidRealLiteralType ty)
+  in
+  match c with
+  | Number.ConstInt _ when ts_equal ts ts_int ->
+     t_const c ty
+  | Number.ConstInt n ->
+     begin match ts.ts_def with
+           | Range ir -> Number.check_range n ir; t_const c ty
+           | _ -> raise (InvalidIntegerLiteralType ty)
+     end
+  | Number.ConstReal _ when ts_equal ts ts_real ->
+     t_const c ty
+  | Number.ConstReal r ->
+     begin match ts.ts_def with
+           | Float fp -> Number.check_float r fp; t_const c ty
+           | _ -> raise (InvalidRealLiteralType ty)
+     end
 
 let t_if f t1 t2 =
   t_ty_check t2 t1.t_ty;

src/core/term.mli

@@ -71,7 +71,8 @@ exception BadArity of lsymbol * int
 exception FunctionSymbolExpected of lsymbol
 exception PredicateSymbolExpected of lsymbol
 exception ConstructorExpected of lsymbol
-exception InvalidLiteralType of ty
+exception InvalidIntegerLiteralType of ty
+exception InvalidRealLiteralType of ty
 
 (** {2 Patterns} *)