remove t_real_const

plugins/tptp/tptp_typing.ml

@@ -286,6 +286,7 @@ let rec ty denv env impl { e_loc = loc; e_node = n } = match n with
   | Enot _ | Eequ _ | Edob _ | Enum _ -> error ~loc TypeExpected
 
 let t_int_const s = t_const (ConstInt (int_const_decimal s))
+let t_real_const r = t_const (ConstReal r)
 
 let rec term denv env impl { e_loc = loc; e_node = n } = match n with
   | Eapp (aw,al) ->

src/coq-tactic/why3tac.ml

@@ -389,8 +389,8 @@ let rec tr_positive p = match kind_of_term p with
   | _ ->
       raise NotArithConstant
 
-let const_of_big_int b = 
-  Term.t_const 
+let const_of_big_int b =
+  Term.t_const
     (Term.ConstInt (Term.int_const_decimal (Big_int.string_of_big_int b)))
 
 (* translates a closed Coq term t:Z or R into a FOL term of type int or real *)
@@ -401,9 +401,9 @@ let rec tr_arith_constant t = match kind_of_term t with
   | App (f, [|a|]) when is_constant f coq_Zneg ->
       const_of_big_int (Big_int.minus_big_int (tr_positive a))
   | Const _ when is_constant t coq_R0 ->
-      Term.t_real_const (Term.RConstDecimal ("0", "0", None))
+      Term.t_const (Term.ConstReal (Term.RConstDecimal ("0", "0", None)))
   | Const _ when is_constant t coq_R1 ->
-      Term.t_real_const (Term.RConstDecimal ("1", "0", None))
+      Term.t_const (Term.ConstReal (Term.RConstDecimal ("1", "0", None)))
 (*   | App (f, [|a;b|]) when f = Lazy.force coq_Rplus -> *)
 (*       let ta = tr_arith_constant a in *)
 (*       let tb = tr_arith_constant b in *)

src/core/term.ml

@@ -268,7 +268,7 @@ let check_integer_literal n f s =
   done
 
 let int_const_decimal s =
-  check_integer_literal 10 
+  check_integer_literal 10
     (function '0'..'9' -> true | _ -> false) s;
   IConstDecimal s
 
@@ -498,10 +498,6 @@ let mk_term n ty = Hsterm.hashcons {
 
 let t_var v         = mk_term (Tvar v) (Some v.vs_ty)
 let t_const c ty    = mk_term (Tconst c) (Some ty)
-(*
-let t_int_const s   = mk_term (Tconst (ConstInt (int_const_decimal s))) (Some Ty.ty_int)
-*)
-let t_real_const r  = mk_term (Tconst (ConstReal r)) (Some Ty.ty_real)
 let t_app f tl ty   = mk_term (Tapp (f, tl)) ty
 let t_if f t1 t2    = mk_term (Tif (f, t1, t2)) t2.t_ty
 let t_let t1 bt ty  = mk_term (Tlet (t1, bt)) ty
@@ -765,7 +761,7 @@ let t_const c = match c with
   | ConstInt _  -> t_const c ty_int
   | ConstReal _ -> t_const c ty_real
 
-let t_nat_const n = 
+let t_nat_const n =
   t_const (ConstInt (int_const_decimal (string_of_int n)))
 
 let t_if f t1 t2 =

src/core/term.mli

@@ -125,7 +125,7 @@ val int_const_binary : string -> integer_constant
     InvalidConstantLiteral(base,s) is raised if [s] contains invalid
     characters for the given base. *)
 
-type real_constant = 
+type real_constant =
   | RConstDecimal of string * string * string option (* int / frac / exp *)
   | RConstHexa of string * string * string
 
@@ -221,10 +221,6 @@ val ls_app_inst : lsymbol -> term list -> ty option -> ty Mtv.t
 
 val t_var : vsymbol -> term
 val t_const : constant -> term
-val t_nat_const : int -> term
-(** [t_nat_const n] builds the constant integer term [n],
-    n must be non-negative *)
-  val t_real_const : real_constant -> term
 val t_if : term -> term -> term -> term
 val t_let : term -> term_bound -> term
 val t_case : term -> term_branch list -> term
@@ -241,6 +237,10 @@ val t_not : term -> term
 val t_true : term
 val t_false : term
 
+val t_nat_const : int -> term
+(** [t_nat_const n] builds the constant integer term [n],
+    n must be non-negative *)
+
 val asym_label : label
 val t_and_asym : term -> term -> term
 val t_or_asym : term -> term -> term

src/transform/eliminate_algebraic.ml

@@ -231,8 +231,7 @@ let add_indexer (state,task) ts ty csl =
     let pr = create_prsymbol (id_derive id cs.ls_name) in
     let vl = List.rev_map (create_vsymbol (id_fresh "u")) cs.ls_args in
     let hd = fs_app cs (List.rev_map t_var vl) (Opt.get cs.ls_value) in
-    let ix = t_const (ConstInt (int_const_decimal (string_of_int !index))) in
-    let ax = t_equ (fs_app mt_ls [hd] ty_int) ix in
+    let ax = t_equ (fs_app mt_ls [hd] ty_int) (t_nat_const !index) in
     let ax = t_forall_close (List.rev vl) [[hd]] ax in
     add_prop_decl tsk Paxiom pr ax
   in

src/whyml/mlw_expr.ml

@@ -791,10 +791,6 @@ let e_const t =
   let vtv = vty_value (ity_of_ty_opt t.t_ty) in
   mk_expr (Elogic t) (VTvalue vtv) eff_empty Mid.empty
 
-(*
-let e_int_const s = e_const (t_int_const s)
-let e_real_const rc = e_const (t_real_const rc)
-*)
 let e_const c = e_const (t_const c)
 
 (* boolean expressions *)

src/whyml/mlw_expr.mli

@@ -222,10 +222,6 @@ val t_void : term
 val e_void : expr
 
 val e_const : constant -> expr
-(*
-val e_int_const : string -> expr
-val e_real_const : real_constant -> expr
-*)
 val e_lazy_and : expr -> expr -> expr
 val e_lazy_or : expr -> expr -> expr
 val e_not : expr -> expr