From 3f0a87d685b3ab639e79bc4d7afa60a3b936737c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Mon, 9 Dec 2019 11:37:42 +0100
Subject: [PATCH] [wp/qed] fix type-based filters
---
src/plugins/wp/Lang.ml | 14 ++++++++++++++
src/plugins/wp/TacSplit.ml | 2 +-
2 files changed, 15 insertions(+), 1 deletion(-)
diff --git a/src/plugins/wp/Lang.ml b/src/plugins/wp/Lang.ml
index 896f30bbd7b..cf1934d1e04 100644
--- a/src/plugins/wp/Lang.ml
+++ b/src/plugins/wp/Lang.ml
@@ -743,6 +743,20 @@ struct
let is_pfalse = is_false
let is_equal a b = is_true (e_eq a b)
+ let is_int e =
+ try typeof e = Qed.Logic.Int with Not_found -> false
+
+ let is_real e =
+ try typeof e = Qed.Logic.Real with Not_found -> false
+
+ let is_prop e =
+ try match typeof e with Qed.Logic.Prop | Qed.Logic.Bool -> true | _ -> false
+ with Not_found -> false
+
+ let is_arith e =
+ try match typeof e with Qed.Logic.Int | Qed.Logic.Real -> true | _ -> false
+ with Not_found -> false
+
let p_equal = e_eq
let p_equals = List.map (fun (x,y) -> p_equal x y)
let p_neq = e_neq
diff --git a/src/plugins/wp/TacSplit.ml b/src/plugins/wp/TacSplit.ml
index 91484aa918f..df18c879a4f 100644
--- a/src/plugins/wp/TacSplit.ml
+++ b/src/plugins/wp/TacSplit.ml
@@ -192,7 +192,7 @@ class split =
split_cmp "Split (eq.)" x y
| Neq(x,y) when not (is_prop x || is_prop y) ->
split_cmp "Split (neq.)" x y
- | _ when F.is_prop e->
+ | _ when F.is_prop e ->
feedback#set_title "Split (true,false)" ;
feedback#set_descr "Decompose between True and False values" ;
let cases = ["True",F.p_bool e;"False",F.p_not (F.p_bool e)] in
--
GitLab