From 4a2ef2747950e8a28bfce7ca641bedd7ef71bea1 Mon Sep 17 00:00:00 2001
From: ckeller <ckeller@users.noreply.github.com>
Date: Wed, 21 Apr 2021 09:46:30 +0200
Subject: Convert hypotheses from Prop to bool (#89)

* This PR converts hypotheses given to the tactics verit, verit_no_check, smt and smt_no_check from Prop to bool when needed.

* Some current limitations are detailed in src/PropToBool.v.

* Partially enhances #30 .
---
 src/trace/coqTerms.ml  | 25 ++++++++++++++++++++++++-
 src/trace/coqTerms.mli |  4 ++++
 src/trace/smtMisc.ml   |  2 +-
 3 files changed, 29 insertions(+), 2 deletions(-)

(limited to 'src/trace')

diff --git a/src/trace/coqTerms.ml b/src/trace/coqTerms.ml
index a6d0023..ca5f3cc 100644
--- a/src/trace/coqTerms.ml
+++ b/src/trace/coqTerms.ml
@@ -355,7 +355,6 @@ let rec mk_bv_list = function
 
 
 (* Reification *)
-
 let mk_bool b =
   let c, args = Structures.decompose_app b in
   if Structures.eq_constr c (Lazy.force ctrue) then true
@@ -435,3 +434,27 @@ let mk_bvsize n =
       else assert false
     | _ -> assert false
   else mk_N n
+
+(** Switches between constr and OCaml *)
+(* Transform a option constr into a constr option *)
+let option_of_constr_option co =
+  let c, args = Structures.decompose_app co in
+  if c = Lazy.force cSome then
+    match args with
+      | [_;c] -> Some c
+      | _ -> assert false
+  else
+    None
+
+(* Transform a tuple of constr into a (reversed) list of constr *)
+let list_of_constr_tuple =
+  let rec list_of_constr_tuple acc t =
+    let c, args = Structures.decompose_app t in
+    if c = Lazy.force cpair then
+      match args with
+        | [_;_;t;l] -> list_of_constr_tuple (l::acc) t
+        | _ -> assert false
+    else
+      t::acc
+  in
+  list_of_constr_tuple []
diff --git a/src/trace/coqTerms.mli b/src/trace/coqTerms.mli
index bf626b3..b5ca6b7 100644
--- a/src/trace/coqTerms.mli
+++ b/src/trace/coqTerms.mli
@@ -261,3 +261,7 @@ val mk_nat : Structures.constr -> int
 val mk_N : Structures.constr -> int
 val mk_Z : Structures.constr -> int
 val mk_bvsize : Structures.constr -> int
+
+(* Switches between constr and OCaml *)
+val option_of_constr_option : Structures.constr -> Structures.constr option
+val list_of_constr_tuple : Structures.constr -> Structures.constr list
diff --git a/src/trace/smtMisc.ml b/src/trace/smtMisc.ml
index 92f0f09..aad8b07 100644
--- a/src/trace/smtMisc.ml
+++ b/src/trace/smtMisc.ml
@@ -23,8 +23,8 @@ let mkInt i =
 (** Generic representation of shared object *)
 type 'a gen_hashed = { index : int; hval : 'a }
 
-(** Functions over constr *)
 
+(** Functions over constr *)
 let mklApp f args = Structures.mkApp (Lazy.force f, args)
 
 let string_of_name_def d n = try Structures.string_of_name n with | _ -> d
-- 
cgit