udpate CI; bump minimal ocaml to 4.04; add auto-doc

run simplex tests only on OCaml >= 4.08

.github/workflows/gh-pages.yml

@@ -0,0 +1,43 @@
+name: github pages
+
+on:
+  push:
+    branches:
+      - master  # Set a branch name to trigger deployment
+
+jobs:
+  deploy:
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@main
+
+      - name: Cache opam
+        id: cache-opam
+        uses: actions/cache@v2
+        with:
+          path: ~/.opam
+          key: opam-ubuntu-latest-4.12.0
+
+      - uses: avsm/setup-ocaml@v1
+        with:
+          ocaml-version: '4.12.0'
+
+      - name: Pin
+        run: opam pin -n .
+
+      - name: Depext
+        run: opam depext -yt sidekick sidekick-arith
+
+      - name: Deps
+        run: opam install -d . --deps-only
+
+      - name: Build
+        run: opam exec -- dune build @doc
+
+      - name: Deploy
+        uses: peaceiris/actions-gh-pages@v3
+        with:
+          github_token: ${{ secrets.GITHUB_TOKEN }}
+          publish_dir: ./_build/default/_doc/_html/
+          destination_dir: dev
+          enable_jekyll: true

.github/workflows/main.yml

@@ -3,27 +3,25 @@ on: [push]
 jobs:
   run:
     name: Build
-    runs-on: ${{ matrix.operating-system }}
     strategy:
       matrix:
-        #operating-system: [macos-latest, ubuntu-latest, windows-latest]
-        operating-system: [ubuntu-latest]
-        ocaml-version: [ '4.08.0' ]
+        os:
+          - macos-latest
+          - ubuntu-latest
+          - windows-latest
+        ocaml-compiler:
+          - 4.04.x
+          - 4.10.x
+          - 4.12.x
+    runs-on: ${{ matrix.os }}
     steps:
-    - uses: actions/checkout@master
-    - uses: avsm/setup-ocaml@master
+    - uses: actions/checkout@v2
+    - uses: ocaml/setup-ocaml@v2
       with:
-        ocaml-version: ${{ matrix.ocaml-version }}
-        #- name: cache opam
-        #  id: cache-opam
-        #  uses: actions/cache@v2
-        #  with:
-        #    path: _opam
-        #    key: opam-${{matrix.operating-system}}-${{matrix.ocaml-version}}
+        ocaml-compiler: ${{ matrix.ocaml-compiler }}
     - run: opam pin -n .
-    - run: opam depext -yt sidekick-bin
-      #if: steps.cache-opam.outputs.cache-hit != 'true'
+    - run: opam depext -yt sidekick sidekick-arith sidekick-bin
     - run: opam install -t . --deps-only
-      #if: steps.cache-opam.outputs.cache-hit != 'true'
     - run: opam exec -- dune build
     - run: opam exec -- dune runtest
+      if: ${{ matrix.os == 'ubuntu-latest'}}

sidekick-arith.opam

@@ -14,7 +14,7 @@ depends: [
   "dune" { >= "1.1" }
   "containers" { >= "3.0" & < "4.0" }
   "iter" { >= "1.0" & < "2.0" }
-  "ocaml" { >= "4.03" }
+  "ocaml" { >= "4.04" }
   "sidekick" { = version }
   "zarith" { >= "1.8" } # constraint for infix ops
   "alcotest" {with-test}

sidekick-bin.opam

@@ -15,12 +15,12 @@ depends: [
   "containers" { >= "3.0" & < "4.0" }
   "iter" { >= "1.0" & < "2.0" }
   "zarith"
-  "smtlib-utils" { >= "0.1" & < "0.3" }
+  "smtlib-utils" { >= "0.1" & < "0.4" }
   "sidekick" { = version }
   "sidekick-arith" { = version }
   "menhir"
   "mtime"
-  "ocaml" { >= "4.03" }
+  "ocaml" { >= "4.04" }
 ]
 tags: [ "sat" "smt" ]
 homepage: "https://github.com/c-cube/sidekick"

sidekick.opam

@@ -15,7 +15,7 @@ depends: [
   "containers" { >= "3.0" & < "4.0" }
   "iter" { >= "1.0" & < "2.0" }
   "msat" { >= "0.9" < "0.10" }
-  "ocaml" { >= "4.03" }
+  "ocaml" { >= "4.04" }
   "alcotest" {with-test}
 ]
 depopts: [

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=[];; let tests=\"simplex2\",[]"))))

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 _ -> ()