Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Why3
why3
Commits
8281d57d
Commit
8281d57d
authored
Nov 04, 2017
by
Guillaume Melquiond
Browse files
Adapt tactic to Coq 8.7 representation of real literals.
parent
6469e5fc
Changes
1
Hide whitespace changes
Inline
Side-by-side
src/coq-tactic/why3tac.ml4
View file @
8281d57d
...
...
@@ -209,6 +209,11 @@ let coq_Rinv = coq_ref_Rdefinitions "Rinv"
let coq_Rminus = coq_ref_Rdefinitions "Rminus"
let coq_Rdiv = coq_ref_Rdefinitions "Rdiv"
let coq_powerRZ = coq_reference "Why3" ["Reals"; "Rfunctions"] "powerRZ"
IFDEF COQ87 THEN
let coq_IZR = coq_ref_Rdefinitions "IZR"
ELSE
let coq_IZR = coq_reference "Why3" ["Reals"; "Raxioms"] "IZR"
END
let coq_Logic = coq_reference "Why3" ["Init"; "Logic"]
let coq_False = coq_Logic "False"
...
...
@@ -479,7 +484,25 @@ let const_of_big_int b =
(Number.ConstInt (Number.int_const_dec (Big_int.string_of_big_int b)))
ty_int
let const_of_big_int_real b =
let s = Big_int.string_of_big_int b in
Term.t_const (Number.ConstReal (Number.real_const_dec s "0" None)) ty_real
(* translates a closed Coq term t:Z or R into a FOL term of type int or real *)
let rec tr_arith_constant_IZR evd dep t = match kind evd t with
| Construct _ when is_global evd coq_Z0 t ->
Term.t_const (Number.ConstReal (Number.real_const_dec "0" "0" None)) ty_real
| App (f, [|a|]) when is_global evd coq_Zpos f ->
const_of_big_int_real (tr_positive evd a)
| App (f, [|a|]) when is_global evd coq_Zneg f ->
let t = const_of_big_int_real (tr_positive evd a) in
let fs = why_constant_real dep ["prefix -"] in
Term.fs_app fs [t] ty_real
| Cast (t, _, _) ->
tr_arith_constant_IZR evd dep t
| _ ->
raise NotArithConstant
let rec tr_arith_constant evd dep t = match kind evd t with
| Construct _ when is_global evd coq_Z0 t -> Term.t_nat_const 0
| App (f, [|a|]) when is_global evd coq_Zpos f ->
...
...
@@ -488,6 +511,8 @@ let rec tr_arith_constant evd dep t = match kind evd t with
let t = const_of_big_int (tr_positive evd a) in
let fs = why_constant_int dep ["prefix -"] in
Term.fs_app fs [t] Ty.ty_int
| App (f, [|a|]) when is_global evd coq_IZR f ->
tr_arith_constant_IZR evd dep a
| Const _ when is_global evd coq_R0 t ->
Term.t_const (Number.ConstReal (Number.real_const_dec "0" "0" None))
ty_real
...
...
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment