Upgrade dolmen version

Use the current development version of Dolmen, as preparation for its
next release.

This patch does the minimal amount of work needed to make Alt-Ergo
support this version of Dolmen ; in particular, it does not exploit
Dolmen's new organization of builtins by theories or implement new
operators from the SMT-LIB 2.7 standard (except for `ubv_to_int` and
`int_to_bv`, which are now new names for `bv2nat` and `int2bv`
respectively).

Author: bclement-ocp

alt-ergo-lib.opam

@@ -60,3 +60,10 @@ license: [
   "LicenseRef-OCamlpro-Non-Commercial"
   "Apache-2.0"
 ]
+
+pin-depends: [
+  [
+    "dolmen.0.11"
+    "git+https://github.com/Gbury/dolmen.git#3c77a22b2aac2eb85aca76f198797d40ca3ec4a3"
+  ]
+]

alt-ergo-lib.opam.template

@@ -6,3 +6,10 @@ license: [
   "LicenseRef-OCamlpro-Non-Commercial"
   "Apache-2.0"
 ]
+
+pin-depends: [
+  [
+    "dolmen.0.11"
+    "git+https://github.com/Gbury/dolmen.git#3c77a22b2aac2eb85aca76f198797d40ca3ec4a3"
+  ]
+]

nix/default.nix

@@ -5,14 +5,14 @@ import sources.nixpkgs {
     (_: pkgs: { inherit sources; })
     (_: pkgs: {
       ocamlPackages = pkgs.ocaml-ng.ocamlPackages_4_14.overrideScope (self: super: {
-        pp_loc = pkgs.callPackage ./pp_loc.nix { };
-        ocplib-simplex = pkgs.callPackage ./ocplib-simplex.nix { };
-        dolmen = pkgs.callPackage ./dolmen.nix { };
-        dolmen_type = pkgs.callPackage ./dolmen_type.nix { };
-        dolmen_loop = pkgs.callPackage ./dolmen_loop.nix { };
-        landmarks = pkgs.callPackage ./landmarks.nix { };
-        landmarks-ppx = pkgs.callPackage ./landmarks-ppx.nix { };
-        zarith_stubs_js = pkgs.callPackage ./zarith_stubs_js.nix { };
+        pp_loc = self.callPackage ./pp_loc.nix { };
+        ocplib-simplex = self.callPackage ./ocplib-simplex.nix { };
+        dolmen = self.callPackage ./dolmen.nix { };
+        dolmen_type = self.callPackage ./dolmen_type.nix { };
+        dolmen_loop = self.callPackage ./dolmen_loop.nix { };
+        landmarks = self.callPackage ./landmarks.nix { };
+        landmarks-ppx = self.callPackage ./landmarks-ppx.nix { };
+        zarith_stubs_js = self.callPackage ./zarith_stubs_js.nix { };
       });
     })
   ];

nix/dolmen.nix

@@ -1,23 +1,20 @@
-{ sources, lib, ocamlPackages }:
+{ sources, lib, buildDunePackage
+, menhir, hmap, menhirLib, fmt, uutf, dune-site }:
 
-let
-  dolmen = sources.dolmen;
-in
-
-ocamlPackages.buildDunePackage {
+buildDunePackage {
   strictDeps = true;
   pname = "dolmen";
-  inherit (dolmen) version;
+  inherit (sources.dolmen) version;
 
   minimalOCamlVersion = "4.08";
   duneVersion = "3";
 
-  src = dolmen;
+  src = sources.dolmen;
 
-  nativeBuildInputs = [ ocamlPackages.menhir ];
-  propagatedBuildInputs = with ocamlPackages; [ hmap menhirLib fmt ];
+  nativeBuildInputs = [ menhir ];
+  propagatedBuildInputs = [ hmap menhirLib fmt uutf dune-site ];
 
   meta = with lib; {
-    inherit (dolmen) homepage description;
+    inherit (sources.dolmen) homepage description;
   };
 }

nix/dolmen_loop.nix

@@ -1,13 +1,14 @@
-{ sources, lib, ocamlPackages }:
+{ sources, lib, buildDunePackage
+, gen, zarith, dolmen, dolmen_type }:
 
-ocamlPackages.buildDunePackage {
+buildDunePackage {
   pname = "dolmen_loop";
-  inherit (ocamlPackages.dolmen) version src strictDeps;
+  inherit (dolmen) version src strictDeps;
 
   minimalOCamlVersion = "4.08";
   duneVersion = "3";
 
-  propagatedBuildInputs = [ ocamlPackages.gen ocamlPackages.dolmen_type ];
+  propagatedBuildInputs = [ gen dolmen_type zarith ];
 
-  meta = ocamlPackages.dolmen.meta;
+  meta = dolmen.meta;
 }

nix/sources.json

@@ -1,14 +1,14 @@
 {
     "dolmen": {
-        "branch": "v0.10",
+        "branch": "master",
         "description": "Dolmen provides a library and a binary to parse, typecheck, and evaluate languages used in automated deduction",
         "homepage": "",
         "owner": "Gbury",
         "repo": "dolmen",
-        "rev": "c33632daab31fb3bb719031169baa6c984bb860f",
-        "sha256": "1vvlg72sbwmpnh0kvwkbvnxxgwrdqcy5adqp26n3hpq3mix4sp7d",
+        "rev": "3c77a22b2aac2eb85aca76f198797d40ca3ec4a3",
+        "sha256": "0qsl5f0mh4azmqvq99l24cna8brvw00x9703wyd98gm0pbmsc3pm",
         "type": "tarball",
-        "url": "https://github.com/Gbury/dolmen/archive/c33632daab31fb3bb719031169baa6c984bb860f.tar.gz",
+        "url": "https://github.com/Gbury/dolmen/archive/3c77a22b2aac2eb85aca76f198797d40ca3ec4a3.tar.gz",
         "url_template": "https://github.com/<owner>/<repo>/archive/<rev>.tar.gz",
         "version": "0.10"
     },

src/bin/common/parse_command.ml

@@ -78,6 +78,7 @@ let format_parser s =
 let format_to_string = function
   | Native -> "native"
   | Smtlib2 `V2_6 -> "smtlib2-v2.6"
+  | Smtlib2 `V2_7 -> "smtlib2-v2.7"
   | Smtlib2 `Poly -> "psmt2"
   | Smtlib2 `Latest -> "smtlib2"
   | Why3 -> "why3"

src/bin/common/solving_loop.ml

@@ -138,7 +138,7 @@ let add_if_named
     ~(acc : DStd.Expr.term Util.MS.t)
     (stmt : Typer_Pipe.typechecked D_loop.Typer_Pipe.stmt) =
   match stmt.contents with
-  | `Defs [`Term_def ({name = Simple n; _}, id, _, _, t)] ->
+  | `Defs (_recursive, [`Term_def ({name = Simple n; _}, id, _, _, t)]) ->
     begin
       match DStd.Expr.Id.get_tag id DStd.Expr.Tags.named with
       | None -> acc
@@ -404,7 +404,7 @@ let process_source ?selector_inst ~print_status src =
       ~interactive_prompt
     |> Typer.init
       ~additional_builtins:Translate.builtins
-      ~extension_builtins:[Typer.Ext.bv2nat]
+      ~extension_builtins:[Dolmen_loop.Typer.Ext.bvconv]
     |> Typer_Pipe.init ~type_check
   in
 
@@ -608,7 +608,9 @@ let process_source ?selector_inst ~print_status src =
      issue in Dolmen, we can replace the [loc] argument by the [st_loc]
      value built in [handle_stmt]. *)
   let handle_custom_statement ~loc id args st =
-    let args = List.map Dolmen_type.Core.Smtlib2.sexpr_as_term args in
+    let args =
+      List.map (Dolmen_type.Core.Smtlib2.sexpr_as_term (`Script `Poly)) args
+    in
     let logic_file = State.get State.logic_file st in
     let st, terms = Typer.terms st ~input:(`Logic logic_file) ~loc args in
     match id, terms.ret with
@@ -638,46 +640,53 @@ let process_source ?selector_inst ~print_status src =
       st
   in
 
-  let handle_get_info ~loc (st : State.t) (name: string) =
-    let print_std =
-      fun (type a) (pp :a Fmt.t) (a : a) ->
-        Printer.print_std "(%s %a)" name pp a
-    in
-    let pp_reason_unknown st =
-      let err () =
-        recoverable_error ~loc "Invalid (get-info :reason-unknown)"
+  let handle_get_info ~loc (st : State.t) (info : DStd.Term.t) =
+    match info with
+    | { term = Builtin _ | App _ | Binder _ | Match _ | Colon _; _ }
+    | { term = Symbol { ns = (Var | Sort | Term | Decl | Track | Value _); _ }
+      ; _ }
+    | { term = Symbol { name = Indexed _ | Qualified _; ns = Attr }; _ } ->
+      unsupported_opt "get-info"
+    | { term = Symbol { name = Simple name; ns = Attr }; _ } ->
+      let print_std =
+        fun (type a) (pp :a Fmt.t) (a : a) ->
+          Printer.print_std "(%s %a)" name pp a
       in
-      match State.get partial_model_key st with
-      | None -> err ()
-      | Some Model ((module SAT), sat) ->
-        match SAT.get_unknown_reason sat with
+      let pp_reason_unknown st =
+        let err () =
+          recoverable_error ~loc "Invalid (get-info :reason-unknown)"
+        in
+        match State.get partial_model_key st with
         | None -> err ()
-        | Some ur ->
-          print_std Sat_solver_sig.pp_smt_unknown_reason ur
-    in
-    match name with
-    | ":authors" ->
-      print_std (fun fmt -> Fmt.pf fmt "%S") "Alt-Ergo developers"
-    | ":error-behavior" ->
-      let behavior =
-        if Options.get_exit_on_error () then
-          "immediate-exit"
-        else
-          "continued-execution"
+        | Some Model ((module SAT), sat) ->
+          match SAT.get_unknown_reason sat with
+          | None -> err ()
+          | Some ur ->
+            print_std Sat_solver_sig.pp_smt_unknown_reason ur
       in
-      print_std Fmt.string behavior
-    | ":name" ->
-      print_std (fun fmt -> Fmt.pf fmt "%S") "Alt-Ergo"
-    | ":reason-unknown" ->
-      pp_reason_unknown st
-    | ":version" ->
-      print_std Fmt.string Version._version
-    | ":all-statistics" ->
-      Printer.print_std "%t" Profiling.print_statistics
-    | ":assertion-stack-levels" ->
-      unsupported_opt name
-    | _ ->
-      unsupported_opt name
+      match name with
+      | ":authors" ->
+        print_std (fun fmt -> Fmt.pf fmt "%S") "Alt-Ergo developers"
+      | ":error-behavior" ->
+        let behavior =
+          if Options.get_exit_on_error () then
+            "immediate-exit"
+          else
+            "continued-execution"
+        in
+        print_std Fmt.string behavior
+      | ":name" ->
+        print_std (fun fmt -> Fmt.pf fmt "%S") "Alt-Ergo"
+      | ":reason-unknown" ->
+        pp_reason_unknown st
+      | ":version" ->
+        print_std Fmt.string Version._version
+      | ":all-statistics" ->
+        Printer.print_std "%t" Profiling.print_statistics
+      | ":assertion-stack-levels" ->
+        unsupported_opt name
+      | _ ->
+        unsupported_opt name
   in
 
   (* Fetches the term value in the current model. *)
@@ -921,7 +930,18 @@ let process_source ?selector_inst ~print_status src =
       let preludes =
         theory_preludes @
         List.map (fun path ->
-            let dir, source = State.split_input (`File path) in
+            (* Using [`File] sources with preludes is currently broken,
+               see https://github.com/Gbury/dolmen/issues/248
+               and https://github.com/OCamlPro/alt-ergo/issues/1330 *)
+            let dir, source =
+              let content =
+                let ch = open_in_bin path in
+                let s = really_input_string ch (in_channel_length ch) in
+                close_in ch;
+                s
+              in
+              Filename.dirname path, (`Raw (Filename.basename path, content))
+            in
             State.mk_file dir source) (Options.get_preludes ())
       in
       let g =