From 402504b97deedd3a6cee078c2ca416fa5b3d7833 Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Thu, 10 Jun 2021 12:21:26 -0400
Subject: [PATCH] run simplex tests only on OCaml >= 4.08

---
 src/arith/tests/dune                                  | 11 +++++++++++
 .../tests/{test_simplex2.ml => test_simplex2.real.ml} |  0
 src/core/Sidekick_core.ml                             | 10 ++++++++++
 3 files changed, 21 insertions(+)
 rename src/arith/tests/{test_simplex2.ml => test_simplex2.real.ml} (100%)

diff --git a/src/arith/tests/dune b/src/arith/tests/dune
index fa402df0..8a5b690d 100644
--- a/src/arith/tests/dune
+++ b/src/arith/tests/dune
@@ -1,5 +1,6 @@
 (executable
  (name run_tests)
+ (modules run_tests test_simplex2)
  (libraries containers sidekick-arith.lra zarith iter alcotest qcheck)
  (flags :standard -warn-error -a+8 -color always))
 
@@ -11,3 +12,13 @@
    (progn
      (run ./run_tests.exe alcotest) ; run regressions first
      (run ./run_tests.exe qcheck --verbose))))
+
+(rule
+  (targets test_simplex2.ml)
+  (enabled_if (>= %{ocaml_version} 4.08.0))
+  (action (copy test_simplex2.real.ml %{targets})))
+
+(rule
+  (targets test_simplex2.ml)
+  (enabled_if (< %{ocaml_version} 4.08.0))
+  (action (with-stdout-to %{targets} (echo "let props=[]"))))
diff --git a/src/arith/tests/test_simplex2.ml b/src/arith/tests/test_simplex2.real.ml
similarity index 100%
rename from src/arith/tests/test_simplex2.ml
rename to src/arith/tests/test_simplex2.real.ml
diff --git a/src/core/Sidekick_core.ml b/src/core/Sidekick_core.ml
index 1091952e..9dcdac68 100644
--- a/src/core/Sidekick_core.ml
+++ b/src/core/Sidekick_core.ml
@@ -10,7 +10,14 @@
 
 module Fmt = CCFormat
 
+(** View terms through the lens of the Congruence Closure *)
 module CC_view = struct
+  (** A view of a term fron the point of view of the congruence closure.
+
+      - ['f] is the type of function symbols
+      - ['t] is the type of terms
+      - ['ts] is the type of sequences of terms (arguments of function application)
+  *)
   type ('f, 't, 'ts) t =
     | Bool of bool
     | App_fun of 'f * 'ts
@@ -20,6 +27,8 @@ module CC_view = struct
     | Not of 't
     | Opaque of 't (* do not enter *)
 
+(** Map function over a view, one level deep.
+    Each function maps over a different type, e.g. [f_t] maps over terms *)
   let map_view ~f_f ~f_t ~f_ts (v:_ t) : _ t =
     match v with
     | Bool b -> Bool b
@@ -30,6 +39,7 @@ module CC_view = struct
     | Eq (a,b) -> Eq (f_t a, f_t b)
     | Opaque t -> Opaque (f_t t)
 
+  (** Iterate over a view, one level deep. *)
   let iter_view ~f_f ~f_t ~f_ts (v:_ t) : unit =
     match v with
     | Bool _ -> ()