add missing Bofbool case in Const_eval

shell.nix

@@ -0,0 +1,65 @@
+{ pkgs ? import (builtins.fetchTarball {
+    url = "https://github.com/NixOS/nixpkgs/archive/master.tar.gz";
+  }) {}
+}:
+
+pkgs.mkShell {
+  name = "codex-dev-shell";
+  dontDetectOcamlConflicts = true;
+  nativeBuildInputs = with pkgs.ocamlPackages; [
+    dune_3
+    findlib
+    # tests
+    mdx
+    mdx.bin
+    qcheck-core
+    # dev dependencies
+    merlin
+    ocaml
+    ocamlformat
+    ocp-browser
+    ocp-index
+    ocb
+    odoc
+  ];
+  buildInputs = with pkgs.ocamlPackages; [
+    js_of_ocaml
+    js_of_ocaml-ppx
+    ppx_deriving
+    ppx_inline_test
+  ];
+  propagatedBuildInputs = with pkgs.ocamlPackages; [
+    base64
+    bheap
+    camlp-streams
+    cudd
+    fmt
+    pacomb
+    patricia-tree
+    vdom
+    zarith
+  ];
+
+  shellHook = ''
+    mkdir -p utils/gui/deps/js
+
+    fetch_if_missing () {
+      if [ ! -f "$1" ]; then
+        echo "Fetching $1"
+        curl -L "$2" -o "$1"
+      fi
+    }
+
+    fetch_if_missing \
+      utils/gui/deps/tailwind4.1.5.css \
+      https://github.com/codex-semantics-library/codex/releases/download/1.0-rc4/tailwind4.1.5.css
+
+    fetch_if_missing \
+      utils/gui/deps/graphviz.umd.js \
+      https://github.com/codex-semantics-library/codex/releases/download/1.0-rc4/graphviz.umd.js
+
+    fetch_if_missing \
+      utils/gui/deps/js/bundle-output.js \
+      https://github.com/codex-semantics-library/codex/releases/download/1.0-rc4/bundle-output.js
+  '';
+}

terms/const_eval.ml

@@ -29,9 +29,38 @@ module Make(Terms: Sig.TERMS) = struct
   let wraps ~(size:In_bits.t) x = Z.signed_extract x 0 (size:>int)
   let wrapu ~(size:In_bits.t) x = Z.extract x 0 (size:>int)
 
+  let rec integer = function
+    | Terms.(Integer{term=T0{tag=TC.Iconst k}}) -> k
+    | Terms.(Integer{term=T1{tag;a}}) ->
+      (* Codex_log.warning "A constant integer was not simplified: %a" Terms.pretty x; *)
+      (match tag with
+       | TC.Itimes k -> Z.mul k (integer a)
+       | _ -> .
+      )
+
+    | Terms.(Integer{term=T2{tag;a;b}}) ->
+      (* Codex_log.warning "A constant integer was not simplified: %a" Terms.pretty x; *)
+      (match tag with
+       | TC.Imul -> Z.mul (integer a) (integer b)
+       | TC.Iadd -> Z.add (integer a) (integer b)
+       | TC.Isub -> Z.sub (integer a) (integer b)
+       | TC.Idiv ->
+         let b = integer b in
+         if Z.equal b Z.zero then raise Empty
+         else Z.div (integer a) b
+       | TC.Imod -> Z.rem (integer a) (integer b)
+       | TC.Ishl -> Z.shift_left (integer a) (Z.to_int (integer b))
+       | TC.Ishr -> Z.shift_right (integer a) (Z.to_int (integer b))
+       | TC.Ior -> Z.logor (integer a) (integer b)
+       | TC.Iand -> Z.logand (integer a) (integer b)
+       | TC.Ixor -> Z.logxor (integer a) (integer b)
+      )
+    | Terms.(Integer{term=Empty}) -> raise Empty
+    | x -> Codex_log.fatal "get const on %a" Terms.pretty x
+
   (* For binaries, we return a Z whose last size bits correspond to
      the requested bitvector. *)
-  let rec binary x = match x with
+  let rec binary : type a. a Terms.t -> Z.t = function
     | Terms.(Binary{term=T0{tag=TC.Biconst(size,k)}}) -> k
     | Terms.(Binary{term=T1{tag;a};size}) -> begin match tag with
         | TC.Bextract{size;oldsize;index} ->
@@ -42,7 +71,8 @@ module Make(Terms: Sig.TERMS) = struct
         | TC.Bsext _ ->
           let Terms.Binary{size=oldsize} = a in
           wraps ~size:oldsize (binary a)
-        | TC.Bofbool _ -> assert false
+        | TC.Bofbool _size ->
+          if boolean a then Z.one else Z.zero
         | TC.Bchoose _ -> binary a
       end
     | Terms.(Binary{term=T2{tag;a;b};size}) -> begin try
@@ -66,40 +96,9 @@ module Make(Terms: Sig.TERMS) = struct
         with Division_by_zero -> raise Empty
       end
     | Terms.(Binary{term=Empty}) -> raise Empty
-    | _ -> Codex_log.fatal "Const eval on %a" Terms.pretty x
-
-  and bitvector x = binary x
+    | x -> Codex_log.fatal "Const eval on %a" Terms.pretty x
 
-  and integer x = match x with
-    | Terms.(Integer{term=T0{tag=TC.Iconst k}}) -> k
-    | Terms.(Integer{term=T1{tag;a}}) ->
-      (* Codex_log.warning "A constant integer was not simplified: %a" Terms.pretty x; *)
-      (match tag with
-       | TC.Itimes k -> Z.mul k (integer a)
-       | _ -> .
-      )
-
-    | Terms.(Integer{term=T2{tag;a;b}}) ->
-      (* Codex_log.warning "A constant integer was not simplified: %a" Terms.pretty x; *)
-      (match tag with
-       | TC.Imul -> Z.mul (integer a) (integer b)
-       | TC.Iadd -> Z.add (integer a) (integer b)
-       | TC.Isub -> Z.sub (integer a) (integer b)
-       | TC.Idiv ->
-         let b = integer b in
-         if Z.equal b Z.zero then raise Empty
-         else Z.div (integer a) b
-       | TC.Imod -> Z.rem (integer a) (integer b)
-       | TC.Ishl -> Z.shift_left (integer a) (Z.to_int (integer b))
-       | TC.Ishr -> Z.shift_right (integer a) (Z.to_int (integer b))
-       | TC.Ior -> Z.logor (integer a) (integer b)
-       | TC.Iand -> Z.logand (integer a) (integer b)
-       | TC.Ixor -> Z.logxor (integer a) (integer b)
-      )
-    | Terms.(Integer{term=Empty}) -> raise Empty
-    | _ -> Codex_log.fatal "get const on %a" Terms.pretty x
-
-  and boolean x = match x with
+  and boolean : type a. a Terms.t -> bool = function
     | Terms.(Bool{term=T0{tag=TC.True}}) -> true
     | Terms.(Bool{term=T0{tag=TC.False}}) -> false
     | Terms.(Bool{term=Empty}) -> raise Empty
@@ -123,10 +122,12 @@ module Make(Terms: Sig.TERMS) = struct
        | TC.Bisle size -> Z.leq (wraps ~size @@ binary a) (wraps ~size @@ binary b)
        | _ -> .
       )
-    | _ -> Codex_log.fatal "get const on %a" Terms.pretty x
+    | x -> Codex_log.fatal "get const on %a" Terms.pretty x
+
+  let bitvector x = binary x
 
-  and enum x = match x with
+  let enum = function
     | Terms.(Enum{term=Empty}) -> raise Empty
-    | _ -> Codex_log.fatal "get const on %a" Terms.pretty x
+    | x -> Codex_log.fatal "get const on %a" Terms.pretty x
 
 end