Skip to content

GitLab

why3
why3
Commit 48c6b603 authored by Guillaume Melquiond's avatar Guillaume Melquiond
Browse files
Options

Reference symbols instead of constructing whole terms from the tactic. 

This commit also removes the laziness for accessing symbols, since they
are already in the scope at the time the plugin is loaded.
parent fc927c12
Hide whitespace changes
Inline Side-by-side
Showing with 92 additions and 93 deletions
src/coq-tactic/why3tac.ml4
View file @ 48c6b603
......@@ -45,10 +45,16 @@ let finite_ind v = v
let admit_as_an_axiom = Tactics.admit_as_an_axiom
let eq_constr = (=)
let map_to_list = Util.array_map_to_list
let is_global c t =
match c, kind_of_term t with
| ConstRef c, Const c' -> eq_constant c c'
| IndRef i, Ind i' -> eq_ind i i'
| ConstructRef i, Construct i' -> eq_constructor i i'
| VarRef id, Var id' -> id = id'
| _ -> false
ELSE
open Universes
......@@ -74,8 +80,6 @@ let type_of_global = Global.type_of_global_unsafe
let finite_ind v = v <> Decl_kinds.CoFinite
let build_coq_eq () = constr_of_global (build_coq_eq ())
let pr_str = Pp.str
let pr_spc = Pp.spc
......@@ -167,62 +171,57 @@ let print_bv fmt m =
(string_of_id id) Why3.Pretty.print_vsty vs) m
(* Coq constants *)
let logic_dir = ["Coq";"Logic";"Decidable"]
let coq_modules =
init_modules @ [logic_dir] @ arith_modules @ zarith_base_modules
@ [["Coq"; "ZArith"; "BinInt"];
["Coq"; "Reals"; "Rdefinitions"];
["Coq"; "Reals"; "Raxioms";];
["Coq"; "Reals"; "Rbasic_fun";];
["Coq"; "Reals"; "R_sqrt";];
["Coq"; "Reals"; "Rfunctions";]]
@ [["Coq"; "omega"; "OmegaLemmas"]]
let constant = gen_constant_in_modules "why" coq_modules
let coq_Z = lazy (constant "Z")
let coq_Zplus = lazy (constant "Zplus")
let coq_Zmult = lazy (constant "Zmult")
let coq_Zopp = lazy (constant "Zopp")
let coq_Zminus = lazy (constant "Zminus")
let coq_Zdiv = lazy (constant "Zdiv")
let coq_Zs = lazy (constant "Zs")
let coq_Zgt = lazy (constant "Zgt")
let coq_Zle = lazy (constant "Zle")
let coq_Zge = lazy (constant "Zge")
let coq_Zlt = lazy (constant "Zlt")
let coq_Z0 = lazy (constant "Z0")
let coq_Zpos = lazy (constant "Zpos")
let coq_Zneg = lazy (constant "Zneg")
let coq_xH = lazy (constant "xH")
let coq_xI = lazy (constant "xI")
let coq_xO = lazy (constant "xO")
let coq_R = lazy (constant "R")
let coq_R0 = lazy (constant "R0")
let coq_R1 = lazy (constant "R1")
let coq_Rgt = lazy (constant "Rgt")
let coq_Rle = lazy (constant "Rle")
let coq_Rge = lazy (constant "Rge")
let coq_Rlt = lazy (constant "Rlt")
let coq_Rplus = lazy (constant "Rplus")
let coq_Rmult = lazy (constant "Rmult")
let coq_Ropp = lazy (constant "Ropp")
let coq_Rinv = lazy (constant "Rinv")
let coq_Rminus = lazy (constant "Rminus")
let coq_Rdiv = lazy (constant "Rdiv")
let coq_powerRZ = lazy (constant "powerRZ")
let coq_iff = lazy (constant "iff")
let is_constant t c = try eq_constr t (Lazy.force c) with _ -> false
let coq_ref_BinInt = coq_reference "Why3" ["ZArith"; "BinInt"]
let coq_Z = coq_ref_BinInt "Z"
let coq_Zplus = coq_ref_BinInt "Zplus"
let coq_Zmult = coq_ref_BinInt "Zmult"
let coq_Zopp = coq_ref_BinInt "Zopp"
let coq_Zminus = coq_ref_BinInt "Zminus"
let coq_Zdiv = coq_reference "Why3" ["ZArith"; "Zdiv"] "Zdiv"
let coq_Zgt = coq_ref_BinInt "Zgt"
let coq_Zle = coq_ref_BinInt "Zle"
let coq_Zge = coq_ref_BinInt "Zge"
let coq_Zlt = coq_ref_BinInt "Zlt"
let coq_ref_BinNums = coq_reference "Why3" ["Numbers"; "BinNums"]
let coq_Z0 = coq_ref_BinNums "Z0"
let coq_Zpos = coq_ref_BinNums "Zpos"
let coq_Zneg = coq_ref_BinNums "Zneg"
let coq_xH = coq_ref_BinNums "xH"
let coq_xI = coq_ref_BinNums "xI"
let coq_xO = coq_ref_BinNums "xO"
let coq_ref_Rdefinitions = coq_reference "Why3" ["Reals"; "Rdefinitions"]
let coq_R = coq_ref_Rdefinitions "R"
let coq_R0 = coq_ref_Rdefinitions "R0"
let coq_R1 = coq_ref_Rdefinitions "R1"
let coq_Rgt = coq_ref_Rdefinitions "Rgt"
let coq_Rle = coq_ref_Rdefinitions "Rle"
let coq_Rge = coq_ref_Rdefinitions "Rge"
let coq_Rlt = coq_ref_Rdefinitions "Rlt"
let coq_Rplus = coq_ref_Rdefinitions "Rplus"
let coq_Rmult = coq_ref_Rdefinitions "Rmult"
let coq_Ropp = coq_ref_Rdefinitions "Ropp"
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"
let coq_Logic = coq_reference "Why3" ["Init"; "Logic"]
let coq_False = coq_Logic "False"
let coq_True = coq_Logic "True"
let coq_eq = coq_Logic "eq"
let coq_not = coq_Logic "not"
let coq_and = coq_Logic "and"
let coq_or = coq_Logic "or"
let coq_ex = coq_Logic "ex"
let coq_iff = coq_Logic "iff"
let coq_WhyType =
lazy (gen_constant_in_modules "why" [["Why3"; "BuiltIn"]] "WhyType")
find_reference "Why3" ["Why3"; "BuiltIn"] "WhyType"
let rec is_WhyType c = match kind_of_term c with
| App (f, [|_|]) -> is_constant f coq_WhyType
| App (f, [|_|]) -> is_global coq_WhyType f
| Cast (c, _, _) -> is_WhyType c
| _ -> false
......@@ -459,12 +458,12 @@ exception NotArithConstant
let big_two = Big_int.succ_big_int Big_int.unit_big_int
let rec tr_positive p = match kind_of_term p with
| Construct _ when is_constant p coq_xH ->
| Construct _ when is_global coq_xH p ->
Big_int.unit_big_int
| App (f, [|a|]) when is_constant f coq_xI ->
| App (f, [|a|]) when is_global 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 a))
| App (f, [|a|]) when is_constant f coq_xO ->
| App (f, [|a|]) when is_global coq_xO f ->
(* Mult (Cst 2, tr_positive a) *)
Big_int.mult_big_int big_two (tr_positive a)
| Cast (p, _, _) ->
......@@ -478,16 +477,16 @@ let const_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 dep t = match kind_of_term t with
| Construct _ when is_constant t coq_Z0 -> Term.t_nat_const 0
| App (f, [|a|]) when is_constant f coq_Zpos ->
| Construct _ when is_global coq_Z0 t -> Term.t_nat_const 0
| App (f, [|a|]) when is_global coq_Zpos f ->
const_of_big_int (tr_positive a)
| App (f, [|a|]) when is_constant f coq_Zneg ->
| App (f, [|a|]) when is_global coq_Zneg f ->
let t = const_of_big_int (tr_positive a) in
let fs = why_constant_int dep ["prefix -"] in
Term.fs_app fs [t] Ty.ty_int
| Const _ when is_constant t coq_R0 ->
| Const _ when is_global coq_R0 t ->
Term.t_const (Number.ConstReal (Number.real_const_dec "0" "0" None))
| Const _ when is_constant t coq_R1 ->
| Const _ when is_global coq_R1 t ->
Term.t_const (Number.ConstReal (Number.real_const_dec "1" "0" None))
(* | App (f, [|a;b|]) when f = Lazy.force coq_Rplus -> *)
(* let ta = tr_arith_constant a in *)
......@@ -515,9 +514,9 @@ let rec tr_type dep tvm env t =
(Closure.RedFlags.red_add_transparent
Closure.betadeltaiota (get_transp_state env))
env Evd.empty t in
if is_constant t coq_Z then
if is_global coq_Z t then
Ty.ty_int
else if is_constant t coq_R then
else if is_global coq_R t then
Ty.ty_real
else match kind_of_term t with
| Var x when Idmap.mem x tvm ->
......@@ -886,46 +885,46 @@ and tr_term dep tvm bv env t =
tr_arith_constant dep t
with NotArithConstant -> match kind_of_term t with
(* binary operations on integers *)
| App (c, [|a;b|]) when is_constant c coq_Zplus ->
| App (c, [|a;b|]) when is_global coq_Zplus c ->
let ls = why_constant_int dep ["infix +"] in
Term.fs_app ls [tr_term dep tvm bv env a; tr_term dep tvm bv env b]
Ty.ty_int
| App (c, [|a;b|]) when is_constant c coq_Zminus ->
| App (c, [|a;b|]) when is_global coq_Zminus c ->
let ls = why_constant_int dep ["infix -"] in
Term.fs_app ls [tr_term dep tvm bv env a; tr_term dep tvm bv env b]
Ty.ty_int
| App (c, [|a;b|]) when is_constant c coq_Zmult ->
| App (c, [|a;b|]) when is_global coq_Zmult c ->
let ls = why_constant_int dep ["infix *"] in
Term.fs_app ls [tr_term dep tvm bv env a; tr_term dep tvm bv env b]
Ty.ty_int
| App (c, [|a;b|]) when is_constant c coq_Zdiv ->
| App (c, [|a;b|]) when is_global coq_Zdiv c ->
let ls = why_constant_eucl dep ["div"] in
Term.fs_app ls [tr_term dep tvm bv env a; tr_term dep tvm bv env b]
Ty.ty_int
| App (c, [|a|]) when is_constant c coq_Zopp ->
| App (c, [|a|]) when is_global coq_Zopp c ->
let ls = why_constant_int dep ["prefix -"] in
Term.fs_app ls [tr_term dep tvm bv env a] Ty.ty_int
(* binary operations on reals *)
| App (c, [|a;b|]) when is_constant c coq_Rplus ->
| App (c, [|a;b|]) when is_global coq_Rplus c ->
let ls = why_constant_real dep ["infix +"] in
Term.fs_app ls [tr_term dep tvm bv env a; tr_term dep tvm bv env b]
Ty.ty_real
| App (c, [|a;b|]) when is_constant c coq_Rminus ->
| App (c, [|a;b|]) when is_global coq_Rminus c ->
let ls = why_constant_real dep ["infix -"] in
Term.fs_app ls [tr_term dep tvm bv env a; tr_term dep tvm bv env b]
Ty.ty_real
| App (c, [|a;b|]) when is_constant c coq_Rmult ->
| App (c, [|a;b|]) when is_global coq_Rmult c ->
let ls = why_constant_real dep ["infix *"] in
Term.fs_app ls [tr_term dep tvm bv env a; tr_term dep tvm bv env b]
Ty.ty_real
| App (c, [|a;b|]) when is_constant c coq_Rdiv ->
| App (c, [|a;b|]) when is_global coq_Rdiv c ->
let ls = why_constant_real dep ["infix /"] in
Term.fs_app ls [tr_term dep tvm bv env a; tr_term dep tvm bv env b]
Ty.ty_real
| App (c, [|a|]) when is_constant c coq_Ropp ->
| App (c, [|a|]) when is_global coq_Ropp c ->
let ls = why_constant_real dep ["prefix -"] in
Term.fs_app ls [tr_term dep tvm bv env a] Ty.ty_real
| App (c, [|a|]) when is_constant c coq_Rinv ->
| App (c, [|a|]) when is_global coq_Rinv c ->
let ls = why_constant_real dep ["inv"] in
Term.fs_app ls [tr_term dep tvm bv env a] Ty.ty_real
(* first-order terms *)
......@@ -1021,49 +1020,49 @@ and quantifiers n a b dep tvm bv env =
(* translation of a Coq formula
assumption f:Prop *)
and tr_formula dep tvm bv env f = match kind_of_term f with
| App(c, [|t;a;b|]) when eq_constr c (build_coq_eq ()) ->
| App(c, [|t;a;b|]) when is_global coq_eq c ->
let ty = type_of env Evd.empty t in
if not (is_Set ty || is_Type ty) then raise NotFO;
let _ = tr_type dep tvm env t in
Term.t_equ (tr_term dep tvm bv env a) (tr_term dep tvm bv env b)
(* comparisons on integers *)
| App(c, [|a;b|]) when is_constant c coq_Zle ->
| App(c, [|a;b|]) when is_global coq_Zle c ->
let ls = why_constant_int dep ["infix <="] in
Term.ps_app ls [tr_term dep tvm bv env a; tr_term dep tvm bv env b]
| App(c, [|a;b|]) when is_constant c coq_Zlt ->
| App(c, [|a;b|]) when is_global coq_Zlt c ->
let ls = why_constant_int dep ["infix <"] in
Term.ps_app ls [tr_term dep tvm bv env a; tr_term dep tvm bv env b]
| App(c, [|a;b|]) when is_constant c coq_Zge ->
| App(c, [|a;b|]) when is_global coq_Zge c ->
let ls = why_constant_int dep ["infix >="] in
Term.ps_app ls [tr_term dep tvm bv env a; tr_term dep tvm bv env b]
| App(c, [|a;b|]) when is_constant c coq_Zgt ->
| App(c, [|a;b|]) when is_global coq_Zgt c ->
let ls = why_constant_int dep ["infix >"] in
Term.ps_app ls [tr_term dep tvm bv env a; tr_term dep tvm bv env b]
(* comparisons on reals *)
| App(c, [|a;b|]) when is_constant c coq_Rle ->
| App(c, [|a;b|]) when is_global coq_Rle c ->
let ls = why_constant_real dep ["infix <="] in
Term.ps_app ls [tr_term dep tvm bv env a; tr_term dep tvm bv env b]
| App(c, [|a;b|]) when is_constant c coq_Rlt ->
| App(c, [|a;b|]) when is_global coq_Rlt c ->
let ls = why_constant_real dep ["infix <"] in
Term.ps_app ls [tr_term dep tvm bv env a; tr_term dep tvm bv env b]
| App(c, [|a;b|]) when is_constant c coq_Rge ->
| App(c, [|a;b|]) when is_global coq_Rge c ->
let ls = why_constant_real dep ["infix >="] in
Term.ps_app ls [tr_term dep tvm bv env a; tr_term dep tvm bv env b]
| App(c, [|a;b|]) when is_constant c coq_Rgt ->
| App(c, [|a;b|]) when is_global coq_Rgt c ->
let ls = why_constant_real dep ["infix >"] in
Term.ps_app ls [tr_term dep tvm bv env a; tr_term dep tvm bv env b]
(* propositional logic *)
| _ when eq_constr f (build_coq_False ()) ->
| _ when is_global coq_False f ->
Term.t_false
| _ when eq_constr f (build_coq_True ()) ->
| _ when is_global coq_True f ->
Term.t_true
| App(c, [|a|]) when eq_constr c (build_coq_not ()) ->
| App(c, [|a|]) when is_global coq_not c ->
Term.t_not (tr_formula dep tvm bv env a)
| App(c, [|a;b|]) when eq_constr c (build_coq_and ()) ->
| App(c, [|a;b|]) when is_global coq_and c ->
Term.t_and (tr_formula dep tvm bv env a) (tr_formula dep tvm bv env b)
| App(c, [|a;b|]) when eq_constr c (build_coq_or ()) ->
| App(c, [|a;b|]) when is_global coq_or c ->
Term.t_or (tr_formula dep tvm bv env a) (tr_formula dep tvm bv env b)
| App(c, [|a;b|]) when is_constant c coq_iff ->
| App(c, [|a;b|]) when is_global coq_iff c ->
Term.t_iff (tr_formula dep tvm bv env a) (tr_formula dep tvm bv env b)
| Prod (n, a, b) ->
if is_imp_term f && is_Prop (type_of env Evd.empty a) then
......@@ -1072,7 +1071,7 @@ and tr_formula dep tvm bv env f = match kind_of_term f with
else
let vs, _t, bv, env, b = quantifiers n a b dep tvm bv env in
Term.t_forall_close [vs] [] (tr_formula dep tvm bv env b)
| App(c, [|_; a|]) when eq_constr c (build_coq_ex ()) ->
| App(c, [|_; a|]) when is_global coq_ex c ->
begin match kind_of_term a with
| Lambda(n, a, b) ->
let vs, _t, bv, env, b = quantifiers n a b dep tvm bv env in
......
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