chore(dolmen): Use Dolmen builtins for bv2nat and int2bv (#1053)

Use the new "bvconv" typing extension introduced in
Gbury/dolmen#208 instead of our own custom
builtins.

alt-ergo-lib.opam.locked

@@ -88,15 +88,15 @@ conflicts: [
 pin-depends: [
   [
     "dolmen.dev"
-    "git+https://github.com/Gbury/dolmen.git#4637064b98d0af7e42e8a55845ca80cb19fe1f36"
+    "git+https://github.com/Gbury/dolmen.git#5e22e653ec376336bbbed50aca4946db8edbc90f"
   ]
   [
     "dolmen_loop.dev"
-    "git+https://github.com/Gbury/dolmen.git#4637064b98d0af7e42e8a55845ca80cb19fe1f36"
+    "git+https://github.com/Gbury/dolmen.git#5e22e653ec376336bbbed50aca4946db8edbc90f"
   ]
   [
     "dolmen_type.dev"
-    "git+https://github.com/Gbury/dolmen.git#4637064b98d0af7e42e8a55845ca80cb19fe1f36"
+    "git+https://github.com/Gbury/dolmen.git#5e22e653ec376336bbbed50aca4946db8edbc90f"
   ]
   [
     "js_of_ocaml.5.4.0"

nix/dolmen.nix

@@ -15,7 +15,7 @@ ocamlPackages.buildDunePackage {
   src = dolmen;
 
   nativeBuildInputs = [ ocamlPackages.menhir ];
-  propagatedBuildInputs = [ ocamlPackages.menhirLib ocamlPackages.fmt ];
+  propagatedBuildInputs = with ocamlPackages; [ hmap menhirLib fmt ];
 
   meta = with lib; {
     inherit (dolmen) homepage description;

nix/sources.json

@@ -1,14 +1,14 @@
 {
     "dolmen": {
-        "branch": "4637064b98d0af7e42e8a55845ca80cb19fe1f36",
+        "branch": "5e22e653ec376336bbbed50aca4946db8edbc90f",
         "description": "Dolmen provides a library and a binary to parse, typecheck, and evaluate languages used in automated deduction",
         "homepage": "",
         "owner": "Gbury",
         "repo": "dolmen",
-        "rev": "4637064b98d0af7e42e8a55845ca80cb19fe1f36",
-        "sha256": "0r3p5dfp684xccqz9jm9cf1lr6xzjvrhsk6kb7ydnadls30xdvgw",
+        "rev": "5e22e653ec376336bbbed50aca4946db8edbc90f",
+        "sha256": "1wmmq3x8zcp2zh3xpchjvhyj85qbydrpd2cf9awn4nxxaqi06yjn",
         "type": "tarball",
-        "url": "https://github.com/Gbury/dolmen/archive/4637064b98d0af7e42e8a55845ca80cb19fe1f36.tar.gz",
+        "url": "https://github.com/Gbury/dolmen/archive/5e22e653ec376336bbbed50aca4946db8edbc90f.tar.gz",
         "url_template": "https://github.com/<owner>/<repo>/archive/<rev>.tar.gz",
         "version": "dev"
     },

src/bin/common/solving_loop.ml

@@ -523,6 +523,8 @@ let main () =
       ~size_limit ~response_file
     |> Parser.init
     |> Typer.init
+      ~additional_builtins:D_cnf.builtins
+      ~extension_builtins:[Typer.Ext.bv2nat]
     |> Typer_Pipe.init ~type_check
   in
 
@@ -1052,7 +1054,6 @@ let main () =
       let g =
         Parser.parse_logic ~preludes logic_file
       in
-      let st = State.set Typer.additional_builtins D_cnf.builtins st in
       let all_used_context = Frontend.init_all_used_context () in
       let finally = finally ~handle_exn in
       let st =

src/lib/frontend/d_cnf.ml

@@ -176,8 +176,6 @@ type _ DStd.Builtin.t +=
   | Integer_round
   | Abs_real
   | Sqrt_real
-  | Int2BV of int
-  | BV2Nat of int
   | Sqrt_real_default
   | Sqrt_real_excess
   | Ceiling_to_int of [ `Real ]
@@ -235,18 +233,6 @@ let fpa_rounding_mode, rounding_modes, add_rounding_modes =
 module Const = struct
   open DE
 
-  let bv2nat =
-    with_cache (fun n ->
-        let name = "bv2nat" in
-        DE.Id.mk ~name ~builtin:(BV2Nat n)
-          (DStd.Path.global name) Ty.(arrow [bitv n] int))
-
-  let int2bv =
-    with_cache (fun n ->
-        let name = "int2bv" in
-        DE.Id.mk ~name ~builtin:(Int2BV n)
-          (DStd.Path.global name) Ty.(arrow [int] (bitv n)))
-
   let smt_round =
     with_cache (fun (n, m) ->
         let name = "ae.round" in
@@ -257,41 +243,9 @@ module Const = struct
           Ty.(arrow [fpa_rounding_mode; real] real))
 end
 
-let bv2nat t =
-  let n =
-    match DT.view (DE.Term.ty t) with
-    | `Bitv n -> n
-    | _ -> raise (DE.Term.Wrong_type (t, DT.bitv 0))
-  in
-  DE.Term.apply_cst (Const.bv2nat n) [] [t]
-
-let int2bv n t =
-  DE.Term.apply_cst (Const.int2bv n) [] [t]
-
 let smt_round n m rm t =
   DE.Term.apply_cst (Const.smt_round (n, m)) [] [rm; t]
 
-let bv_builtins env s =
-  let term_app1 f =
-    Dl.Typer.T.builtin_term @@
-    Dolmen_type.Base.term_app1 (module Dl.Typer.T) env s f
-  in
-  match s with
-  | Dl.Typer.T.Id {
-      ns = Term  ;
-      name = Simple "bv2nat" } ->
-    term_app1 bv2nat
-  | Id {
-      ns = Term ;
-      name = Indexed {
-          basename = "int2bv" ;
-          indexes = [ n ] } } ->
-    begin match int_of_string n with
-      | n -> term_app1 (int2bv n)
-      | exception Failure _ -> `Not_found
-    end
-  | _ -> `Not_found
-
 (** Takes a dolmen identifier [id] and injects it in Alt-Ergo's registered
     identifiers.
     It transforms "fpa_rounding_mode", the Alt-Ergo builtin type into the SMT2
@@ -493,18 +447,11 @@ let smt_fpa_builtins =
       end
     | _ -> `Not_found
 
-(** Concatenation of builtins handlers. *)
-let (++) bt1 bt2 =
-  fun a b ->
-  match bt1 a b with
-  | `Not_found -> bt2 a b
-  | res -> res
-
 let builtins =
   fun _st (lang : Typer.lang) ->
   match lang with
   | `Logic Alt_ergo -> ae_fpa_builtins
-  | `Logic (Smtlib2 _) -> bv_builtins ++ smt_fpa_builtins
+  | `Logic (Smtlib2 _) -> smt_fpa_builtins
   | _ -> fun _ _ -> `Not_found
 
 (** Translates dolmen locs to Alt-Ergo's locs *)
@@ -1460,8 +1407,8 @@ let rec mk_expr
           | Integer_round, _ -> op Integer_round
           | Abs_real, _ -> op Abs_real
           | Sqrt_real, _ -> op Sqrt_real
-          | Int2BV n, _ -> op (Int2BV n)
-          | BV2Nat _, _ -> op BV2Nat
+          | B.Bitv_of_int { n }, _ -> op (Int2BV n)
+          | B.Bitv_to_nat { n = _ }, _ -> op BV2Nat
           | Sqrt_real_default, _ -> op Sqrt_real_default
           | Sqrt_real_excess, _ -> op Sqrt_real_excess
           | B.Abs, _ -> op Abs_int