Commit f82ee030 authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files

Coq plug-in (in progress)

parent b4aaa7b0
......@@ -875,23 +875,23 @@ endif
ifeq (@enable_coq_plugin@,yes)
COQGENERATED = src/coq-plugin/g_whytac.ml
COQPGENERATED = src/coq-plugin/g_whytac.ml
COQ_FILES = whytac g_whytac
COQP_FILES = whytac g_whytac
COQMODULES = $(addprefix src/coq-plugin/, $(COQ_FILES))
COQPMODULES = $(addprefix src/coq-plugin/, $(COQP_FILES))
COQDEP = $(addsuffix .dep, $(COQMODULES))
COQCMO = $(addsuffix .cmo, $(COQMODULES))
COQCMX = $(addsuffix .cmx, $(COQMODULES))
COQPDEP = $(addsuffix .dep, $(COQPMODULES))
COQPCMO = $(addsuffix .cmo, $(COQPMODULES))
COQPCMX = $(addsuffix .cmx, $(COQPMODULES))
COQTREES = kernel lib interp parsing proofs pretyping tactics library toplevel
COQINCLUDES = -I src/coq-plugin $(addprefix -I @COQLIB@/, $(COQTREES))
COQPTREES = kernel lib interp parsing proofs pretyping tactics library toplevel
COQPINCLUDES = -I src/coq-plugin $(addprefix -I @COQLIB@/, $(COQPTREES))
$(COQDEP): DEPFLAGS += -I src/coq-plugin
$(COQCMO) $(COQCMX): INCLUDES += $(COQINCLUDES)
$(COQPDEP): DEPFLAGS += -I src/coq-plugin
$(COQPCMO) $(COQPCMX): INCLUDES += $(COQPINCLUDES)
$(COQDEP): $(COQGENERATED)
$(COQPDEP): $(COQPGENERATED)
byte: src/coq-plugin/whytac.cma
opt: src/coq-plugin/whytac.cmxs
......@@ -899,10 +899,10 @@ opt: src/coq-plugin/whytac.cmxs
src/coq-plugin/whytac.cma: BFLAGS+=-rectypes -I +camlp5
src/coq-plugin/whytac.cmxs: OFLAGS+=-rectypes -I +camlp5
src/coq-plugin/whytac.cmxs: src/why3.cmxa $(COQCMX)
src/coq-plugin/whytac.cmxs: src/why3.cmxa $(COQPCMX)
$(OCAMLOPT) $(OFLAGS) -o $@ -shared $^
src/coq-plugin/whytac.cma: src/why3.cma $(COQCMO)
src/coq-plugin/whytac.cma: src/why3.cma $(COQPCMO)
$(OCAMLC) -a $(BFLAGS) -o $@ $^
src/coq-plugin/g_whytac.ml: src/coq-plugin/g_whytac.ml4
......@@ -911,16 +911,16 @@ src/coq-plugin/g_whytac.ml: src/coq-plugin/g_whytac.ml4
# depend and clean targets
ifneq "$(MAKECMDGOALS)" "clean"
include $(COQDEP)
include $(COQPDEP)
endif
depend: $(COQDEP)
depend: $(COQPDEP)
clean::
rm -f src/coq-plugin/*.cm[iox] src/coq-plugin/*.o
rm -f src/coq-plugin/*.cma src/coq-plugin/*.cmxs
rm -f src/coq-plugin/*.annot src/coq-plugin/*.dep src/coq-plugin/*~
rm -f $(COQGENERATED)
rm -f $(COQPGENERATED)
endif
......
......@@ -399,8 +399,8 @@ if test "$enable_coq_plugin" = yes -a "$CAMLP5O" = no; then
fi
# coq-plugin currently disabled
enable_coq_plugin=no
reason_coq_plugin=" (not yet implemented)"
dnl enable_coq_plugin=no
dnl reason_coq_plugin=" (not yet implemented)"
if test "$enable_coq_libs" = yes; then
AC_CHECK_PROG(COQDEP,coqdep,coqdep,no)
......
......@@ -21,6 +21,6 @@
open Whytac
TACTIC EXTEND Why
[ "why" string(s) ] -> [ whytac s ]
TACTIC EXTEND Why3
[ "why3" string(s) ] -> [ whytac s ]
END
......@@ -3,11 +3,36 @@ Require Export ZArith.
Open Scope Z_scope.
Require Export List.
Ltac ae := why "alt-ergo".
Ltac z3 := why "z3".
Ltac spass := why "spass".
Ltac ae := why3 "alt-ergo".
Ltac Z3 := why3 "z3-2".
Ltac spass := why3 "spass".
Print length.
(*
Inductive sorted (a: Set) : list a -> Prop :=
c: sorted _ (@nil a)
| d: forall x: a, sorted _ (cons x nil).
Goal sorted _ (@nil Z).
ae.
*)
Parameter p: Z -> Prop.
(* let in *)
Goal
let t := Z in
let f := p 0 in
(forall x:t, p x -> p (let y := x+1 in y)) ->
f -> p 1.
ae.
(* cast *)
Goal
(
(forall x:Z, p x -> p (x+1)) -> p (0 : Z) -> p 1 : Prop).
ae.
Qed.
(* type definitions *)
......@@ -24,9 +49,9 @@ Qed.
(* predicate definition *)
Definition p (x:nat) := x=O.
Definition p' (x:nat) := x=O.
Goal p O.
Goal p' O.
ae.
Qed.
......@@ -36,9 +61,11 @@ Goal plus O O = O.
ae.
Qed.
Definition eq (A:Set) (x y : A) := x=y.
Goal eq nat O O.
Definition eq' (A:Set) (x y : A) := x=y.
Goal
eq' nat O O.
ae.
(*
why "z3". (* BUG encoding decorate ici ? *)
......@@ -80,9 +107,7 @@ Qed.
Print In.
Goal In 0 (cons 1 (cons 0 nil)).
spass.
(*ae.*)
(* ICI *)
ae.
Qed.
(* inductive types *)
......@@ -106,13 +131,15 @@ ae.
Qed.
Goal (match (S (S (S O))) with (S (S _)) => True | _ => False end).
spass.
ae.
Qed.
Goal forall a, forall (x: list (list a)), 1<=2 -> match x with nil => 1 | x :: r => 2 end <= 2.
Goal
forall a, forall (x: list (list a)),
1<=2 -> match x with nil => 1 | x :: r => 2 end <= 2.
intros a x.
spass.
Z3.
Qed.
......@@ -156,6 +183,17 @@ Goal forall x : ptree Z, x=x.
ae.
Qed.
Definition a := 0+0.
Definition b := a.
Goal b=0.
ae.
Qed.
Goal b=0.
ae.
Fixpoint ptree_size (a:Set) (t:ptree a) : Z := match t with
| PLeaf => 0
| PNode _ f => 1 + pforest_size _ f end
......@@ -167,10 +205,10 @@ Goal ptree_size _ (@PLeaf Z) = 0.
ae.
Qed.
Goal forall (a:Set), ptree_size a (PLeaf _) = 0.
Goal forall (a:Set), ptree_size a (PLeaf a) = 0.
intros.
(* BUG ICI *)
spass.
ae.
(* TODO: intro context *)
Admitted.
......
......@@ -19,6 +19,7 @@
open Names
open Nameops
open Namegen
open Term
open Termops
open Tacmach
......@@ -37,16 +38,15 @@ open Ty
open Term
let debug =
try let _ = Sys.getenv "WHYDEBUG" in true
try let _ = Sys.getenv "WHY3DEBUG" in true
with Not_found -> false
let config = Whyconf.read_config None
let main = Whyconf.get_main config
let cprovers = Whyconf.get_provers config
let timelimit = timelimit main
let env = Lexer.create_env (loadpath main)
let env = Env.create_env (loadpath main)
let provers = Hashtbl.create 17
......@@ -54,8 +54,8 @@ let get_prover s =
try
Hashtbl.find provers s
with Not_found ->
let cp = Util.Mstr.find s cprovers in
let drv = Driver.load_driver env cp.driver in
let cp = Whyconf.prover_by_id config s in
let drv = Driver.load_driver env cp.driver cp.extra_drivers in
Hashtbl.add provers s (cp, drv);
cp, drv
......@@ -175,7 +175,7 @@ let decomp_type_quantifiers env t =
let t = substl (List.map mkVar vars) t in
let add m id =
let tv = Ty.create_tvsymbol (preid_of_id id) in
Idmap.add id tv m, tv
Idmap.add id (Ty.ty_var tv) m, tv
in
Util.map_fold_left add Idmap.empty vars, env, t
in
......@@ -190,7 +190,7 @@ let decomp_type_lambdas tvm env vars t =
| tv :: vars, Lambda (n, a, t) when is_Set a || is_Type a ->
let id, env = coq_rename_var env (n, a) in
let t = subst1 (mkVar id) t in
let tvm = Idmap.add id tv tvm in
let tvm = Idmap.add id (Ty.ty_var tv) tvm in
loop tvm env vars t
| _ ->
assert false (*TODO: eta-expansion*)
......@@ -235,7 +235,7 @@ let global_ls = ref Refmap.empty
(* polymorphic arity (i.e. number of type variables) *)
let poly_arity = ref Mls.empty
let add_poly_arith ls n = poly_arity := Mls.add ls n !poly_arity
let add_poly_arity ls n = poly_arity := Mls.add ls n !poly_arity
let get_poly_arity ls = assert (Mls.mem ls !poly_arity); Mls.find ls !poly_arity
(* ident -> decl *)
......@@ -255,7 +255,10 @@ let rec add_local_decls d =
try
task := Task.add_decl !task d
with Decl.UnknownIdent id ->
Format.eprintf "unknown ident %s@." id.Ident.id_string; exit 42
Format.eprintf "unknown ident %s@." id.Ident.id_string;
Format.eprintf " @[%a@]@.@." Pretty.print_decl d;
Format.eprintf "task=@[%a@]@." Pretty.print_task !task;
assert false
end
let empty_dep () = ref Decl.Sdecl.empty
......@@ -285,8 +288,8 @@ let () =
poly_arity := Mls.empty;
global_decl := Ident.Mid.empty;
global_dep := Decl.Mdecl.empty);
Summary.survive_module = true;
Summary.survive_section = true;
(* Summary.survive_module = true; *)
(* Summary.survive_section = true; *)
}
let lookup_table table r = match Refmap.find r !table with
......@@ -360,7 +363,7 @@ let rec tr_type dep tvm env t =
Ty.ty_real
else match kind_of_term t with
| Var x when Idmap.mem x tvm ->
Ty.ty_var (Idmap.find x tvm)
Idmap.find x tvm
| _ ->
let f, cl = decompose_app t in
begin try
......@@ -405,7 +408,7 @@ and tr_global_ts dep env r =
let ty = Global.type_of_global r in
let (_,vars), _, t = decomp_type_quantifiers env ty in
if not (is_Set t) && not (is_Type t) then raise NotFO;
let id = preid_of_id (Nametab.id_of_global r) in
let id = preid_of_id (Nametab.basename_of_global r) in
let ts = match (Global.lookup_constant c).const_body with
| Some b ->
let b = force b in
......@@ -431,7 +434,7 @@ and tr_global_ts dep env r =
let ty = Global.type_of_global r in
let (_,vars), _, t = decomp_type_quantifiers env ty in
if not (is_Set t) && not (is_Type t) then raise NotFO;
let id = preid_of_id (Nametab.id_of_global r) in
let id = preid_of_id (Nametab.basename_of_global r) in
let ts = Ty.create_tysymbol id vars None in
all_ids := ts.ts_name :: !all_ids;
add_table global_ts r (Some ts)
......@@ -448,18 +451,19 @@ and tr_global_ts dep env r =
let (_,vars), env, t = decomp_type_quantifiers env ty in
let tvm =
let add v1 v2 tvm =
let v2 = Ty.ty_var v2 in
Idmap.add (id_of_string v1.tv_name.Ident.id_string) v2 tvm
in
List.fold_right2 add vars ts.Ty.ts_args Idmap.empty
in
let l, _ = decompose_arrows t in
let l = List.map (tr_type dep' tvm env) l in
let id = preid_of_id (Nametab.id_of_global r) in
let id = preid_of_id (Nametab.basename_of_global r) in
let ls = Term.create_lsymbol id l (Some tyj) in
all_ids := ls.Term.ls_name :: !all_ids;
add_table global_ls r (Some ls);
add_poly_arith ls (List.length vars);
ls
add_poly_arity ls (List.length vars);
ls, List.map (fun _ -> None) ls.ls_args
in
let ls = Array.to_list (Array.mapi mk_constructor oib.mind_nf_lc) in
ts, Decl.Talgebraic ls
......@@ -561,7 +565,7 @@ and decompose_definition dep env c =
let l, t = decompose_arrows t in
let args = List.map (tr_type dep tvm env) l in
let ls =
let id = preid_of_id (Nametab.id_of_global r) in
let id = preid_of_id (Nametab.basename_of_global r) in
if is_Prop t then
(* predicate definition *)
create_lsymbol id args None
......@@ -575,7 +579,7 @@ and decompose_definition dep env c =
raise NotFO
in
add_table global_ls r (Some ls);
add_poly_arith ls (List.length vars)
add_poly_arity ls (List.length vars)
in
List.iter (fun (r, _) -> make_one_ls r) dl;
let make_one_decl (r, b) =
......@@ -584,21 +588,25 @@ and decompose_definition dep env c =
| None ->
ls, None
| Some b ->
let tvs = List.fold_left Ty.ty_freevars Stv.empty
(Ty.oty_cons ls.ls_args ls.ls_value) in
let add tv tvm = Util.Mstr.add tv.tv_name.Ident.id_string tv tvm in
let tvm = Stv.fold add tvs Util.Mstr.empty in
let ty = Global.type_of_global r in
let (tvm, vars), env, ty = decomp_type_quantifiers env ty in
let tyl, _ = decompose_arrows ty in
let tyl = List.map (tr_type dep tvm env) tyl in
let (_, vars), env, _ = decomp_type_quantifiers env ty in
let conv tv = Util.Mstr.find tv.tv_name.Ident.id_string tvm in
let vars = List.map conv vars in
let tvm, env, b = decomp_type_lambdas Idmap.empty env vars b in
let (bv, vsl), env, b =
decomp_lambdas dep tvm Idmap.empty env tyl b
decomp_lambdas dep tvm Idmap.empty env ls.ls_args b
in
begin match ls.ls_value with
| None ->
let b = tr_formula dep tvm bv env b in
Decl.make_ps_defn ls vsl b
Decl.make_ls_defn ls vsl b
| Some _ ->
let b = tr_term dep tvm bv env b in
Decl.make_fs_defn ls vsl b
Decl.make_ls_defn ls vsl b
end
in
List.map make_one_decl dl
......@@ -628,52 +636,52 @@ and tr_term dep tvm bv env t =
(* binary operations on integers *)
| App (c, [|a;b|]) when is_constant c coq_Zplus ->
let ls = why_constant ["int"] "Int" ["infix +"] in
Term.t_app ls [tr_term dep tvm bv env a; tr_term dep tvm bv env b]
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 ->
let ls = why_constant ["int"] "Int" ["infix -"] in
Term.t_app ls [tr_term dep tvm bv env a; tr_term dep tvm bv env b]
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 ->
let ls = why_constant ["int"] "Int" ["infix *"] in
Term.t_app ls [tr_term dep tvm bv env a; tr_term dep tvm bv env b]
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 ->
let ls = why_constant ["int"] "EuclideanDivision" ["div"] in
Term.t_app ls [tr_term dep tvm bv env a; tr_term dep tvm bv env b]
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 ->
let ls = why_constant ["int"] "Int" ["prefix -"] in
Term.t_app ls [tr_term dep tvm bv env a] Ty.ty_int
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 ->
let ls = why_constant ["real"] "Real" ["infix +"] in
Term.t_app ls [tr_term dep tvm bv env a; tr_term dep tvm bv env b]
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 ->
let ls = why_constant ["real"] "Real" ["infix -"] in
Term.t_app ls [tr_term dep tvm bv env a; tr_term dep tvm bv env b]
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 ->
let ls = why_constant ["real"] "Real" ["infix *"] in
Term.t_app ls [tr_term dep tvm bv env a; tr_term dep tvm bv env b]
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 ->
let ls = why_constant ["real"] "Real" ["infix /"] in
Term.t_app ls [tr_term dep tvm bv env a; tr_term dep tvm bv env b]
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 ->
let ls = why_constant ["real"] "Real" ["prefix -"] in
Term.t_app ls [tr_term dep tvm bv env a] Ty.ty_real
Term.fs_app ls [tr_term dep tvm bv env a] Ty.ty_real
| App (c, [|a|]) when is_constant c coq_Rinv ->
let ls = why_constant ["real"] "Real" ["inv"] in
Term.t_app ls [tr_term dep tvm bv env a] Ty.ty_real
Term.fs_app ls [tr_term dep tvm bv env a] Ty.ty_real
(* first-order terms *)
| Var id when Idmap.mem id bv ->
Term.t_var (Idmap.find id bv)
| Var id ->
Format.eprintf "tr_term: unbound variable %s@." (string_of_id id);
exit 1
| Var _ ->
(* Format.eprintf "tr_term: unbound variable %s@." (string_of_id id); *)
assert false
| Case (ci, _, e, br) ->
let ty = type_of env Evd.empty e in
let ty = tr_type dep tvm env ty in
......@@ -694,9 +702,27 @@ and tr_term dep tvm bv env t =
let ty = type_of env Evd.empty t in
let _ty = tr_type dep tvm env ty in
t_case e (Array.to_list (Array.mapi branch br))
| _ ->
| LetIn (x, e1, ty1, e2) ->
if is_Prop ty1 || is_Set ty1 || is_Type ty1 then
let e2 = subst1 e1 e2 in
tr_term dep tvm bv env e2
else begin
let s1 = type_of env Evd.empty ty1 in
if not (is_Set s1 || is_Type s1) then raise NotFO;
let t1 = tr_term dep tvm bv env e1 in
let vs, _, bv, env, e2 = quantifiers x ty1 e2 dep tvm bv env in
let t2 = tr_term dep tvm bv env e2 in
t_let_close vs t1 t2
end
| CoFix _ | Fix _ | Lambda _ | Prod _ | Sort _ | Evar _ | Meta _ ->
raise NotFO
| Rel _ ->
assert false
| Cast (t, _, _) ->
tr_term dep tvm bv env t
| App _ | Construct _ | Ind _ | Const _ ->
let f, cl = decompose_app t in
let r = global_of_constr f in
let r = try global_of_constr f with _ -> raise NotFO in
let ls = tr_task_ls dep env r in
begin match ls.Term.ls_value with
| Some _ ->
......@@ -704,7 +730,7 @@ and tr_term dep tvm bv env t =
let cl = skip_k_args k cl in
let ty = type_of env Evd.empty t in
let ty = tr_type dep tvm env ty in
Term.t_app ls (List.map (tr_term dep tvm bv env) cl) ty
Term.fs_app ls (List.map (tr_term dep tvm bv env) cl) ty
| None ->
raise NotFO
end
......@@ -736,107 +762,118 @@ 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 =
let c, args = decompose_app f in
match kind_of_term c, args with
(*
| Var id, [] ->
Fatom (Pred (rename_global (VarRef id), []))
*)
| _, [t;a;b] when c = build_coq_eq () ->
let ty = type_of env Evd.empty t in
if is_Set ty || is_Type ty then
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)
else
raise NotFO
(* comparisons on integers *)
| _, [a;b] when is_constant c coq_Zle ->
let ls = why_constant ["int"] "Int" ["infix <="] in
Term.f_app ls [tr_term dep tvm bv env a; tr_term dep tvm bv env b]
| _, [a;b] when is_constant c coq_Zlt ->
let ls = why_constant ["int"] "Int" ["infix <"] in
Term.f_app ls [tr_term dep tvm bv env a; tr_term dep tvm bv env b]
| _, [a;b] when is_constant c coq_Zge ->
let ls = why_constant ["int"] "Int" ["infix >="] in
Term.f_app ls [tr_term dep tvm bv env a; tr_term dep tvm bv env b]
| _, [a;b] when is_constant c coq_Zgt ->
let ls = why_constant ["int"] "Int" ["infix >"] in
Term.f_app ls [tr_term dep tvm bv env a; tr_term dep tvm bv env b]
(* comparisons on reals *)
| _, [a;b] when is_constant c coq_Rle ->
let ls = why_constant ["real"] "Real" ["infix <="] in
Term.f_app ls [tr_term dep tvm bv env a; tr_term dep tvm bv env b]
| _, [a;b] when is_constant c coq_Rlt ->
let ls = why_constant ["real"] "Real" ["infix <"] in
Term.f_app ls [tr_term dep tvm bv env a; tr_term dep tvm bv env b]
| _, [a;b] when is_constant c coq_Rge ->
let ls = why_constant ["real"] "Real" ["infix >="] in
Term.f_app ls [tr_term dep tvm bv env a; tr_term dep tvm bv env b]
| _, [a;b] when is_constant c coq_Rgt ->
let ls = why_constant ["real"] "Real" ["infix >"] in
Term.f_app ls [tr_term dep tvm bv env a; tr_term dep tvm bv env b]
(* propositional logic *)
| _, [] when c = build_coq_False () ->
Term.t_false
| _, [] when c = build_coq_True () ->
Term.t_true
| _, [a] when c = build_coq_not () ->
Term.t_not (tr_formula dep tvm bv env a)
| _, [a;b] when c = build_coq_and () ->
Term.t_and (tr_formula dep tvm bv env a) (tr_formula dep tvm bv env b)
| _, [a;b] when c = build_coq_or () ->
Term.t_or (tr_formula dep tvm bv env a) (tr_formula dep tvm bv env b)
| _, [a;b] when c = Lazy.force coq_iff ->
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
Term.t_implies
(tr_formula dep tvm bv env a) (tr_formula dep tvm bv env b)
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)
| _, [_; a] when c = build_coq_ex () ->
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
Term.t_exists_close [vs] [] (tr_formula dep tvm bv env b)
| _ ->
and tr_formula dep tvm bv env f = match kind_of_term f with
| App(c, [|t;a;b|]) when c = build_coq_eq () ->
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 ->
let ls = why_constant ["int"] "Int" ["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 ->
let ls = why_constant ["int"] "Int" ["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 ->
let ls = why_constant ["int"] "Int" ["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 ->
let ls = why_constant ["int"] "Int" ["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 ->
let ls = why_constant ["real"] "Real" ["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 ->
let ls = why_constant ["real"] "Real" ["infix <"] in
Term.ps_app ls [tr_term dep tvm bv