refactor(th-bool): parametrize bool_view by type of lists

use iterator instead of a IArray.t on the view side

src/smtlib/Form.ml

@@ -10,18 +10,18 @@ let id_imply = ID.make "=>"
 
 let view_id fid args =
   if ID.equal fid id_and then (
-    B_and args
+    B_and (IArray.to_iter args)
   ) else if ID.equal fid id_or then (
-    B_or args
+    B_or (IArray.to_iter args)
   ) else if ID.equal fid id_imply && IArray.length args >= 2 then (
     (* conclusion is stored first *)
     let len = IArray.length args in
-    B_imply (IArray.sub args 1 (len-1), IArray.get args 0)
+    B_imply (IArray.to_iter_sub args 1 (len-1), IArray.get args 0)
   ) else (
     raise_notrace Not_a_th_term
   )
 
-let view_as_bool (t:T.t) : T.t bool_view =
+let view_as_bool (t:T.t) : (T.t, _) bool_view =
   match T.view t with
   | Bool b -> B_bool b
   | Not u -> B_not u
@@ -47,13 +47,13 @@ module Funs = struct
     match view_id id args with
     | B_bool b -> Value.bool b
     | B_not (V_bool b) -> Value.bool (not b)
-    | B_and a when IArray.for_all Value.is_true a -> Value.true_
-    | B_and a when IArray.exists Value.is_false a -> Value.false_
-    | B_or a when IArray.exists Value.is_true a -> Value.true_
-    | B_or a when IArray.for_all Value.is_false a -> Value.false_
+    | B_and a when Iter.for_all Value.is_true a -> Value.true_
+    | B_and a when Iter.exists Value.is_false a -> Value.false_
+    | B_or a when Iter.exists Value.is_true a -> Value.true_
+    | B_or a when Iter.for_all Value.is_false a -> Value.false_
     | B_imply (_, V_bool true) -> Value.true_
-    | B_imply (a,_) when IArray.exists Value.is_false a -> Value.true_
-    | B_imply (a,b) when IArray.for_all Value.is_bool a && Value.is_bool b -> Value.false_
+    | B_imply (a,_) when Iter.exists Value.is_false a -> Value.true_
+    | B_imply (a,b) when Iter.for_all Value.is_bool a && Value.is_bool b -> Value.false_
     | B_ite(a,b,c) ->
       if Value.is_true a then b
       else if Value.is_false a then c

src/th-bool-static/Sidekick_th_bool_static.ml

@@ -1,11 +1,11 @@
 (** {2 Signatures for booleans} *)
 
-type 'a bool_view =
+type ('a, 'args) bool_view =
   | B_bool of bool
   | B_not of 'a
-  | B_and of 'a IArray.t
-  | B_or of 'a IArray.t
-  | B_imply of 'a IArray.t * 'a
+  | B_and of 'args
+  | B_or of 'args
+  | B_imply of 'args * 'a
   | B_equiv of 'a * 'a
   | B_eq of 'a * 'a
   | B_ite of 'a * 'a * 'a
@@ -17,10 +17,10 @@ module type ARG = sig
 
   type term = S.T.Term.t
 
-  val view_as_bool : term -> term bool_view
+  val view_as_bool : term -> (term, term Iter.t) bool_view
   (** Project the term into the boolean view *)
 
-  val mk_bool : S.T.Term.state -> term bool_view -> term
+  val mk_bool : S.T.Term.state -> (term, term IArray.t) bool_view -> term
   (** Make a term from the given boolean view *)
 
   val check_congruence_classes : bool
@@ -95,18 +95,19 @@ module Make(A : ARG) : S with module A = A = struct
     | B_not _ -> None
     | B_opaque_bool _ -> None
     | B_and a ->
-      if IArray.exists is_false a then Some (T.bool tst false)
-      else if IArray.for_all is_true a then Some (T.bool tst true)
+      if Iter.exists is_false a then Some (T.bool tst false)
+      else if Iter.for_all is_true a then Some (T.bool tst true)
       else None
     | B_or a ->
-      if IArray.exists is_true a then Some (T.bool tst true)
-      else if IArray.for_all is_false a then Some (T.bool tst false)
+      if Iter.exists is_true a then Some (T.bool tst true)
+      else if Iter.for_all is_false a then Some (T.bool tst false)
       else None
     | B_imply (args, u) ->
       (* turn into a disjunction *)
       let u =
-        or_a tst @@
-        IArray.append (IArray.map (not_ tst) args) (IArray.singleton u)
+        let args =
+          args |> Iter.map (not_ tst) |> IArray.of_iter in
+        or_a tst @@ IArray.append args (IArray.singleton u)
       in
       Some u
     | B_ite (a,b,c) ->
@@ -176,14 +177,14 @@ module Make(A : ARG) : S with module A = A = struct
         let lit = get_lit u in
         Lit.neg lit
       | B_and l ->
-        let subs = IArray.to_list_map get_lit l in
+        let subs = l |> Iter.map get_lit |> Iter.to_list in
         let proxy = fresh_lit ~mk_lit ~pre:"and_" self in
         (* add clauses *)
         List.iter (fun u -> add_clause [Lit.neg proxy; u]) subs;
         add_clause (proxy :: List.map Lit.neg subs);
         proxy
       | B_or l ->
-        let subs = IArray.to_list_map get_lit l in
+        let subs = l |> Iter.map get_lit |> Iter.to_list in
         let proxy = fresh_lit ~mk_lit ~pre:"or_" self in
         (* add clauses *)
         List.iter (fun u -> add_clause [Lit.neg u; proxy]) subs;
@@ -191,8 +192,10 @@ module Make(A : ARG) : S with module A = A = struct
         proxy
       | B_imply (args, u) ->
         let t' =
-          or_a self.tst @@
-          IArray.append (IArray.map (not_ self.tst) args) (IArray.singleton u) in
+          let args =
+            args |> Iter.map (not_ self.tst) |> IArray.of_iter
+          in
+          or_a self.tst @@ IArray.append args (IArray.singleton u) in
         get_lit t'
       | B_ite _ | B_eq _ -> mk_lit t
       | B_equiv (a,b) ->

src/util/IArray.ml

@@ -92,6 +92,11 @@ let to_array_map = Array.map
 let of_array_unsafe a = a (* careful with that axe, Eugene *)
 
 let to_iter a k = iter k a
+let to_iter_sub a i len k =
+  if i<0 || i+len > Array.length a then invalid_arg "IArray.iter_sub";
+  for j=i to i+len-1 do
+    k (Array.unsafe_get a j)
+  done
 
 let of_iter s =
   let l = ref [] in

src/util/IArray.mli

@@ -76,6 +76,8 @@ val of_array_unsafe : 'a array -> 'a t
 
 val to_iter : 'a t -> 'a iter
 
+val to_iter_sub : 'a t -> int -> int -> 'a iter
+
 val of_iter : 'a iter -> 'a t
 
 val of_gen : 'a gen -> 'a t