Commit 609cfacf authored by Guillaume Melquiond's avatar Guillaume Melquiond

Rename functions int_const_* into int_literal_* to reflect their types.

This commit also gets rid of `int_const_dec (string_of_int ...)`.
parent e728bb92
......@@ -347,8 +347,7 @@ let d2 =
(* e1 : the appropriate instance of "ref" *)
let e1 = Mlw_expr.e_arrow ref_fun [Mlw_ty.ity_int] ity in
(* we apply it to 0 *)
let c0 = Mlw_expr.e_const
Number.(ConstInt { ic_negative = false ; ic_abs = int_const_dec "0" }) Mlw_ty.ity_int in
let c0 = Mlw_expr.e_const (Number.const_of_int 0) Mlw_ty.ity_int in
Mlw_expr.e_app e1 [c0]
in
(* building the first part of the let x = ref 0 *)
......
......@@ -134,8 +134,7 @@ let d2 =
(* e1 : the appropriate instance of "ref" *)
let e1 = Mlw_expr.e_arrow ref_fun [Mlw_ty.ity_int] ity in
(* we apply it to 0 *)
let c0 = Mlw_expr.e_const
Number.(ConstInt { ic_negative = false ; ic_abs = int_const_dec "0" }) Mlw_ty.ity_int in
let c0 = Mlw_expr.e_const (Number.const_of_int 0) Mlw_ty.ity_int in
Mlw_expr.e_app e1 [c0]
in
(* building the first part of the let x = ref 0 *)
......
......@@ -97,7 +97,7 @@ let mk_lexpr p = { term_loc = Loc.dummy_position;
term_desc = p }
let mk_const s =
mk_lexpr (Tconst Number.(ConstInt { ic_negative = false ; ic_abs = int_const_dec s }))
mk_lexpr (Tconst Number.(ConstInt { ic_negative = false ; ic_abs = int_literal_dec s }))
let mk_expr e = { expr_desc = e; expr_loc = Loc.dummy_position }
......
......@@ -44,8 +44,10 @@ let deref_id ~loc id =
mk_expr ~loc (Eidapp (prefix ~loc "!", [mk_expr ~loc (Eident (Qident id))]))
let array_set ~loc a i v =
mk_expr ~loc (Eidapp (mixfix ~loc "[]<-", [a; i; v]))
let constant ~loc s =
mk_expr ~loc (Econst (Number.(ConstInt { ic_negative = false ; ic_abs = int_const_dec s})))
let constant ~loc i =
mk_expr ~loc (Econst (Number.const_of_int i))
let constant_s ~loc s =
mk_expr ~loc (Econst (Number.(ConstInt { ic_negative = false ; ic_abs = int_literal_dec s})))
let len ~loc =
Qident (mk_id ~loc "len")
let break ~loc =
......@@ -142,7 +144,7 @@ let rec expr env {Py_ast.expr_loc = loc; Py_ast.expr_desc = d } = match d with
| Py_ast.Ebool b ->
mk_expr ~loc (if b then Etrue else Efalse)
| Py_ast.Eint s ->
constant ~loc s
constant_s ~loc s
| Py_ast.Estring _s ->
mk_unit ~loc (*FIXME*)
| Py_ast.Eident id ->
......@@ -180,15 +182,15 @@ let rec expr env {Py_ast.expr_loc = loc; Py_ast.expr_desc = d } = match d with
| Py_ast.Emake (e1, e2) -> (* [e1]*e2 *)
array_make ~loc (expr env e2) (expr env e1)
| Py_ast.Elist [] ->
array_make ~loc (constant ~loc "0") (constant ~loc "0")
array_make ~loc (constant ~loc 0) (constant ~loc 0)
| Py_ast.Elist el ->
let n = List.length el in
let n = constant ~loc (string_of_int n) in
let n = constant ~loc n in
let id = mk_id ~loc "new array" in
mk_expr ~loc (Elet (id, Gnone, array_make ~loc n (constant ~loc "0"),
mk_expr ~loc (Elet (id, Gnone, array_make ~loc n (constant ~loc 0),
let i = ref (-1) in
let init seq e =
incr i; let i = constant ~loc (string_of_int !i) in
incr i; let i = constant ~loc !i in
let assign = array_set ~loc (mk_var ~loc id) i (expr env e) in
mk_expr ~loc (Esequence (assign, seq)) in
List.fold_left init (mk_var ~loc id) el))
......@@ -242,7 +244,7 @@ let rec stmt env ({Py_ast.stmt_loc = loc; Py_ast.stmt_desc = d } as s) =
inv, body) ->
let inv = List.map (deref env) inv in
let e_to = expr env e2 in
let ub = mk_expr ~loc (Eidapp (infix ~loc "-", [e_to;constant ~loc "1"])) in
let ub = mk_expr ~loc (Eidapp (infix ~loc "-", [e_to;constant ~loc 1])) in
mk_expr ~loc (Efor (id, expr env e1, To, ub, inv,
mk_expr ~loc (Elet (id, Gnone, mk_ref ~loc (mk_var ~loc id),
let env = add_var env id in
......@@ -263,9 +265,9 @@ let rec stmt env ({Py_ast.stmt_loc = loc; Py_ast.stmt_desc = d } as s) =
let i, l, env = for_vars ~loc env in
let e = expr env e in
mk_expr ~loc (Elet (l, Gnone, e, (* evaluate e only once *)
let lb = constant ~loc "0" in
let lb = constant ~loc 0 in
let lenl = mk_expr ~loc (Eidapp (len ~loc, [mk_var ~loc l])) in
let ub = mk_expr ~loc (Eidapp (infix ~loc "-", [lenl;constant ~loc "1"])) in
let ub = mk_expr ~loc (Eidapp (infix ~loc "-", [lenl;constant ~loc 1])) in
let invariant inv =
let loc = inv.term_loc in
let li = mk_term ~loc
......
......@@ -308,7 +308,7 @@ term_arg: mk_term(term_arg_) { $1 }
term_arg_:
| ident { Tident (Qident $1) }
| INTEGER { Tconst (Number.(ConstInt { ic_negative = false ; ic_abs = int_const_dec $1})) }
| INTEGER { Tconst (Number.(ConstInt { ic_negative = false ; ic_abs = int_literal_dec $1})) }
| NONE { Ttuple [] }
| TRUE { Ttrue }
| FALSE { Tfalse }
......
......@@ -285,7 +285,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 (Number.(ConstInt { ic_negative = false; ic_abs = int_const_dec s})) ty_int
t_const (Number.(ConstInt { ic_negative = false; ic_abs = int_literal_dec s})) ty_int
(* unused
let t_real_const r = t_const (Number.ConstReal r)
......
......@@ -463,17 +463,15 @@ exception NotArithConstant
(* translates a closed Coq term p:positive into a FOL term of type int *)
let big_two = Big_int.succ_big_int Big_int.unit_big_int
let rec tr_positive evd p = match kind evd p with
| Construct _ when is_global evd coq_xH p ->
Big_int.unit_big_int
BigInt.one
| App (f, [|a|]) when is_global evd coq_xI f ->
(* Plus (Mult (Cst 2, tr_positive a), Cst 1) *)
Big_int.succ_big_int (Big_int.mult_big_int big_two (tr_positive evd a))
BigInt.succ (BigInt.mul_int 2 (tr_positive evd a))
| App (f, [|a|]) when is_global evd coq_xO f ->
(* Mult (Cst 2, tr_positive a) *)
Big_int.mult_big_int big_two (tr_positive evd a)
BigInt.mul_int 2 (tr_positive evd a)
| Cast (p, _, _) ->
tr_positive evd p
| _ ->
......@@ -482,11 +480,11 @@ let rec tr_positive evd p = match kind evd p with
let const_of_big_int is_neg b =
Term.t_const
(Number.(ConstInt { ic_negative = is_neg ;
ic_abs = Number.int_const_dec (Big_int.string_of_big_int b) }))
ic_abs = int_literal_raw b }))
ty_int
let const_of_big_int_real is_neg b =
let s = Big_int.string_of_big_int b in
let s = BigInt.to_string b in
Term.t_const (Number.(ConstReal { rc_negative = is_neg ;
rc_abs = real_const_dec s "0" None}))
ty_real
......
......@@ -831,10 +831,7 @@ let ps_app ps tl = t_app ps tl None
let t_nat_const n =
assert (n >= 0);
let a =
Number.{ic_negative = false ; ic_abs = int_const_dec (string_of_int n)}
in
t_const (Number.ConstInt a) ty_int
t_const (Number.const_of_int n) ty_int
let t_bigint_const n = t_const (Number.const_of_big_int n) Ty.ty_int
......
......@@ -432,10 +432,7 @@ let e_const c =
let e_nat_const n =
assert (n >= 0);
let a =
Number.{ ic_negative = false ; ic_abs = int_const_dec (string_of_int n)}
in
e_const (Number.ConstInt a)
e_const (Number.const_of_int n)
let e_ghostify gh ({e_effect = eff} as e) =
if eff.eff_ghost || not gh then e else
......
......@@ -147,13 +147,13 @@ rule token = parse
| uident_quote as id
{ UIDENT_QUOTE id }
| ['0'-'9'] ['0'-'9' '_']* as s
{ INTEGER (Number.int_const_dec (Lexlib.remove_underscores s)) }
{ INTEGER (Number.int_literal_dec (Lexlib.remove_underscores s)) }
| '0' ['x' 'X'] (['0'-'9' 'A'-'F' 'a'-'f']['0'-'9' 'A'-'F' 'a'-'f' '_']* as s)
{ INTEGER (Number.int_const_hex (Lexlib.remove_underscores s)) }
{ INTEGER (Number.int_literal_hex (Lexlib.remove_underscores s)) }
| '0' ['o' 'O'] (['0'-'7'] ['0'-'7' '_']* as s)
{ INTEGER (Number.int_const_oct (Lexlib.remove_underscores s)) }
{ INTEGER (Number.int_literal_oct (Lexlib.remove_underscores s)) }
| '0' ['b' 'B'] (['0'-'1'] ['0'-'1' '_']* as s)
{ INTEGER (Number.int_const_bin (Lexlib.remove_underscores s)) }
{ INTEGER (Number.int_literal_bin (Lexlib.remove_underscores s)) }
| (digit+ as i) ("" as f) ['e' 'E'] (['-' '+']? digit+ as e)
| (digit+ as i) '.' (digit* as f) (['e' 'E'] (['-' '+']? digit+ as e))?
| (digit* as i) '.' (digit+ as f) (['e' 'E'] (['-' '+']? digit+ as e))?
......
......@@ -58,19 +58,19 @@ let is_dec = function '0'..'9' -> true | _ -> false
let is_oct = function '0'..'7' -> true | _ -> false
let is_bin = function '0'..'1' -> true | _ -> false
let int_const_dec s =
let int_literal_dec s =
check_integer_literal 10 is_dec s;
IConstDec s
let int_const_hex s =
let int_literal_hex s =
check_integer_literal 16 is_hex s;
IConstHex s
let int_const_oct s =
let int_literal_oct s =
check_integer_literal 8 is_oct s;
IConstOct s
let int_const_bin s =
let int_literal_bin s =
check_integer_literal 2 is_bin s;
IConstBin s
......
......@@ -42,10 +42,10 @@ type constant =
val is_negative : constant -> bool
val int_const_dec : string -> integer_literal
val int_const_hex : string -> integer_literal
val int_const_oct : string -> integer_literal
val int_const_bin : string -> integer_literal
val int_literal_dec : string -> integer_literal
val int_literal_hex : string -> integer_literal
val int_literal_oct : string -> integer_literal
val int_literal_bin : string -> integer_literal
(** these four functions construct integer constant terms from some
string [s] of digits in the corresponding base. Exception
InvalidConstantLiteral(base,s) is raised if [s] contains invalid
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment