Commit 71ff2e9c authored by MARCHE Claude's avatar MARCHE Claude

core/Term: renamed and secured t_int_const to t_nat_const

parent 68cb1a45
......@@ -64,18 +64,23 @@ let read_channel env path filename cin =
let th_int = Env.find_theory (Env.env_of_library env) ["int"] "Int" in
let leq = ns_find_ls th_int.th_export ["infix <"] in
let plus_symbol = Theory.ns_find_ls th_int.Theory.th_export ["infix +"] in
let neg_symbol = Theory.ns_find_ls th_int.Theory.th_export ["prefix -"] in
let mult_symbol = Theory.ns_find_ls th_int.Theory.th_export ["infix *"] in
let zero = t_int_const "0" in
let zero = t_nat_const 0 in
let t_int_const n =
if n >= 0 then t_nat_const n else
t_app_infer neg_symbol [t_nat_const (-n)]
in
(** create a contraint : polynome <= constant *)
let create_lit lvar k lits _ =
let left = List.fold_left (fun acc e ->
let const = string_of_int ((Random.int k) - (k/2)) in
let const = (Random.int k) - (k/2) in
let monome = t_app mult_symbol [e;t_int_const const]
(Some Ty.ty_int) in
t_app plus_symbol [acc;monome] (Some Ty.ty_int)) zero lvar in
let rconst = string_of_int ((Random.int k) - (k/2)) in
let rconst = (Random.int k) - (k/2) in
t_and_simp lits (t_app leq [left;t_int_const rconst] None) in
(** create a set of constraints *)
......
......@@ -285,6 +285,8 @@ let rec ty denv env impl { e_loc = loc; e_node = n } = match n with
| Elet _ | Eite _ | Eqnt _ | Ebin _
| Enot _ | Eequ _ | Edob _ | Enum _ -> error ~loc TypeExpected
let t_int_const s = t_const (ConstInt (int_const_decimal s))
let rec term denv env impl { e_loc = loc; e_node = n } = match n with
| Eapp (aw,al) ->
begin match find_fs ~loc denv env impl aw al with
......@@ -300,8 +302,7 @@ let rec term denv env impl { e_loc = loc; e_node = n } = match n with
find_vs ~loc denv env impl v
| Edob s ->
find_dobj ~loc denv env impl s
| Enum (Nint s) ->
t_int_const s
| Enum (Nint s) -> t_int_const s
| Enum (Nreal (i,f,e)) ->
t_real_const (RConstDecimal (i,Opt.get_def "0" f,e))
| Enum (Nrat (n,d)) ->
......
......@@ -389,12 +389,13 @@ let rec tr_positive p = match kind_of_term p with
| _ ->
raise NotArithConstant
let const_of_big_int b = Term.t_int_const (Big_int.string_of_big_int b)
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 *)
let rec tr_arith_constant t = match kind_of_term t with
| Construct _ when is_constant t coq_Z0 ->
Term.t_int_const "0"
| Construct _ when is_constant t coq_Z0 -> Term.t_nat_const 0
| App (f, [|a|]) when is_constant f coq_Zpos ->
const_of_big_int (tr_positive a)
| App (f, [|a|]) when is_constant f coq_Zneg ->
......
......@@ -498,7 +498,9 @@ 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 (IConstDecimal s))) (Some Ty.ty_int)
(*
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
......@@ -763,6 +765,9 @@ let t_const c = match c with
| ConstInt _ -> t_const c ty_int
| ConstReal _ -> t_const c ty_real
let t_nat_const n =
t_const (ConstInt (int_const_decimal (string_of_int n)))
let t_if f t1 t2 =
t_ty_check t2 t1.t_ty;
t_if (t_prop f) t1 t2
......
......@@ -120,6 +120,10 @@ val int_const_decimal : string -> integer_constant
val int_const_hexa : string -> integer_constant
val int_const_octal : string -> integer_constant
val int_const_binary : string -> integer_constant
(** 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
characters for the given base. *)
type real_constant =
| RConstDecimal of string * string * string option (* int / frac / exp *)
......@@ -217,8 +221,10 @@ val ls_app_inst : lsymbol -> term list -> ty option -> ty Mtv.t
val t_var : vsymbol -> term
val t_const : constant -> term
val t_int_const : string -> term
val t_real_const : real_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
......
......@@ -404,7 +404,7 @@ let lex_order_ivl (le_int,lt_int) ivl rvl =
| v :: tl, v':: tl' -> ((List.map create_v rvl), (v, v', tl, tl'))
| _ -> assert false in
let nonneg_ivl' =
let positive v = ps_app le_int [t_int_const "0"; t_var v] in
let positive v = ps_app le_int [t_nat_const 0; t_var v] in
List.fold_left (fun t v -> t_and t (positive v)) (positive hd') tl' in
let lt_lex =
let lt_hd = ps_app lt_int [t_var hd'; t_var hd] in
......
......@@ -62,10 +62,10 @@ let ls_selects_def_of_ts acc ts =
in
let tvars = List.map t_var vars in
(** type to int *)
let id = string_of_int (id_hash ts.ts_name) in
let id = id_hash ts.ts_name in
let acc =
let t = fs_app ls tvars ty_type in
let f = t_equ (fs_app ls_int_of_ty [t] ty_int) (t_int_const id) in
let f = t_equ (fs_app ls_int_of_ty [t] ty_int) (t_nat_const id) in
let f = t_forall_close vars [[t]] f in
let prsymbol = create_prsymbol (id_clone ts.ts_name) in
create_prop_decl Paxiom prsymbol f :: acc
......
......@@ -791,8 +791,10 @@ 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 *)
......
......@@ -221,9 +221,10 @@ 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
......
......@@ -208,6 +208,7 @@ type wp_env = {
ps_int_lt : Term.lsymbol;
ps_int_gt : Term.lsymbol;
fs_int_pl : Term.lsymbol;
fs_int_mn : Term.lsymbol;
letrec_var : term list Mint.t;
}
......@@ -235,7 +236,7 @@ let decrease_rel ?loc env old_t t = function
| Some ls -> ps_app ls [t; old_t]
| None when ty_equal (t_type t) ty_int ->
t_and
(ps_app env.ps_int_le [t_int_const "0"; old_t])
(ps_app env.ps_int_le [t_nat_const 0; old_t])
(ps_app env.ps_int_lt [t; old_t])
| None -> decrease_alg ?loc env old_t t
......@@ -751,19 +752,21 @@ and wp_desc env e q xq = match e.e_node with
I(i) -> wp(e1, I(i+1), R)
and I(v2+1) -> Q *)
let gt, le, incr = match d with
| Mlw_expr.To -> env.ps_int_gt, env.ps_int_le, t_int_const "1"
| Mlw_expr.DownTo -> env.ps_int_lt, env.ps_int_ge, t_int_const "-1" in
| Mlw_expr.To -> env.ps_int_gt, env.ps_int_le, env.fs_int_pl
| Mlw_expr.DownTo -> env.ps_int_lt, env.ps_int_ge, env.fs_int_mn
in
let one = t_nat_const 1 in
let v1_gt_v2 = ps_app gt [t_var v1; t_var v2] in
let v1_le_v2 = ps_app le [t_var v1; t_var v2] in
let q = open_unit_post q in
let wp_init =
wp_expl expl_loop_init (t_subst_single x (t_var v1) inv) in
let wp_step =
let next = fs_app env.fs_int_pl [t_var x; incr] ty_int in
let next = fs_app incr [t_var x; one] ty_int in
let post = wp_expl expl_loop_keep (t_subst_single x next inv) in
wp_expr env e1 (create_unit_post post) xq in
let wp_last =
let v2pl1 = fs_app env.fs_int_pl [t_var v2; incr] ty_int in
let v2pl1 = fs_app incr [t_var v2; one] ty_int in
wp_implies (t_subst_single x v2pl1 inv) q in
let wp_good = wp_and ~sym:true
wp_init
......@@ -915,6 +918,7 @@ let mk_env env km th =
ps_int_lt = Theory.ns_find_ls th_int.th_export ["infix <"];
ps_int_gt = Theory.ns_find_ls th_int.th_export ["infix >"];
fs_int_pl = Theory.ns_find_ls th_int.th_export ["infix +"];
fs_int_mn = Theory.ns_find_ls th_int.th_export ["infix -"];
letrec_var = Mint.empty;
}
......
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