Uniformize Dolmen alias modules

Dolmen paths are a bit mouthful so we use aliases. Most of these
aliases have been introduced in `Solving_loop` but we do not always
stick to this conventions and we have to repeat them at the beginning of
many files. This commit introduces a new module `Alias` which contains
these aliases and can be open in implementation files.

src/bin/common/solving_loop.ml

@@ -32,6 +32,8 @@ module DO = D_state_option
 module Sy = Symbols
 module O = Options
 
+open Alias.Dolmen
+
 type solver_ctx = {
   ctx    : Commands.sat_tdecl list;
   local  : Commands.sat_tdecl list;
@@ -223,16 +225,16 @@ let process_source ?selector_inst ~print_status src =
   let debug_parsed_pipe st c =
     if State.get State.debug st then
       Format.eprintf "[logic][parsed][%a] @[<hov>%a@]@."
-        Dolmen.Std.Loc.print_compact c.Dolmen.Std.Statement.loc
-        Dolmen.Std.Statement.print c;
+        DStd.Loc.print_compact c.DStd.Statement.loc
+        DStd.Statement.print c;
     if O.get_parse_only () then
       st, `Done ()
     else
       st, `Continue c
   in
   let debug_stmt stmt =
     Format.eprintf "[logic][typed][%a] @[<hov>%a@]@\n@."
-      Dolmen.Std.Loc.print_compact stmt.Typer_Pipe.loc
+      DStd.Loc.print_compact stmt.Typer_Pipe.loc
       Typer_Pipe.print stmt
   in
   let debug_typed_pipe st stmts =
@@ -244,7 +246,7 @@ let process_source ?selector_inst ~print_status src =
       st, `Continue stmts
   in
   let handle_exn st bt = function
-    | Dolmen.Std.Loc.Syntax_error (_, `Regular msg) ->
+    | DStd.Loc.Syntax_error (_, `Regular msg) ->
       recoverable_error "%t" msg; st
     | Util.Timeout ->
       Printer.print_status_timeout None None None None;
@@ -553,16 +555,16 @@ let process_source ?selector_inst ~print_status src =
     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
-    | Dolmen.Std.Id.{name = Simple "minimize"; _}, [term] ->
+    | DStd.Id.{name = Simple "minimize"; _}, [term] ->
       cmd_on_modes st [Assert] "minimize";
       handle_optimize_stmt ~is_max:false loc id term st
-    | Dolmen.Std.Id.{name = Simple "maximize"; _}, [term] ->
+    | DStd.Id.{name = Simple "maximize"; _}, [term] ->
       cmd_on_modes st [Assert] "maximize";
       handle_optimize_stmt ~is_max:true loc id term st
-    | Dolmen.Std.Id.{name = Simple "get-objectives"; _}, terms ->
+    | DStd.Id.{name = Simple "get-objectives"; _}, terms ->
       cmd_on_modes st [Sat] "get-objectives";
       handle_get_objectives terms st
-    | Dolmen.Std.Id.{name = Simple (("minimize" | "maximize") as ext); _}, _ ->
+    | DStd.Id.{name = Simple (("minimize" | "maximize") as ext); _}, _ ->
       recoverable_error
         "Statement %s only expects 1 argument (%i given)"
         ext
@@ -571,7 +573,7 @@ let process_source ?selector_inst ~print_status src =
     | n, _ ->
       recoverable_error
         "Unknown statement %a."
-        Dolmen.Std.Id.print
+        DStd.Id.print
         n;
       st
   in

src/lib/dune

@@ -61,7 +61,7 @@
     ; util
     Emap Gc_debug Hconsing Hstring Heap Loc Numbers Uqueue
     Options Timers Util Vec Version Steps Printer
-    My_zip My_list Theories Nest Compat
+    My_zip My_list Theories Nest Compat Alias
   )
 
  (js_of_ocaml

src/lib/frontend/d_loop.ml

@@ -16,16 +16,16 @@
 (*                                                                        *)
 (**************************************************************************)
 
-module DStd = Dolmen.Std
 module Dl = Dolmen_loop
+open Alias.Dolmen
 
 module State = struct
   include Dl.State
 
   (* Overriding error function so that error does not savagely exit. *)
   let error ?file ?loc st error payload =
     let st = flush st () in
-    let loc = Dolmen.Std.Misc.opt_map loc Dolmen.Std.Loc.full_loc in
+    let loc = DStd.Misc.opt_map loc DStd.Loc.full_loc in
     let aux _ =
       let code, descr = Dl.(Code.descr Dl.Report.Error.(code error)) in
       raise (Errors.(error (Dolmen_error (code, descr))))
@@ -42,10 +42,9 @@ module State = struct
         Dl.Report.Error.print (error, payload)
         Dl.Report.Error.print_hints (error, payload)
 end
-module Pipeline = Dl.Pipeline.Make(State)
 
-module Parser = Dolmen_loop.Parser.Make(State)
-module Header = Dolmen_loop.Headers.Make(State)
-module Typer = Dolmen_loop.Typer.Typer(State)
-module Typer_Pipe =
-  Dolmen_loop.Typer.Make(DStd.Expr)(DStd.Expr.Print)(State)(Typer)
+module Pipeline = Dl.Pipeline.Make(State)
+module Parser = Dl.Parser.Make(State)
+module Header = Dl.Headers.Make(State)
+module Typer = Dl.Typer.Typer(State)
+module Typer_Pipe = Dolmen_loop.Typer.Make(DE)(DE.Print)(State)(Typer)

src/lib/frontend/models.ml

@@ -20,7 +20,8 @@ module Sy = Symbols
 module X = Shostak.Combine
 module E = Expr
 module MS = Map.Make(String)
-module DE = Dolmen.Std.Expr
+
+open Alias.Dolmen
 
 let constraints = ref MS.empty
 

src/lib/frontend/translate.ml

@@ -25,9 +25,8 @@ module C = Commands
 module Sy = Symbols
 module SM = Sy.Map
 
-module DE = DStd.Expr
-module DT = DE.Ty
-module B = DStd.Builtin
+open Alias.Dolmen
+module B = DBuiltin
 
 let unsupported msg =
   Fmt.kstr

src/lib/frontend/translate.mli

@@ -19,7 +19,7 @@
 val clear_cache : unit -> unit
 (** Empties the internal cache of the module. *)
 
-val dty_to_ty : ?update:bool -> ?is_var:bool -> D_loop.DStd.Expr.ty -> Ty.t
+val dty_to_ty : ?update:bool -> ?is_var:bool -> Dolmen.Std.Expr.ty -> Ty.t
 (** [dty_to_ty update is_var subst tyv_substs dty]
 
     Converts a Dolmen type to an Alt-Ergo type.
@@ -34,13 +34,13 @@ val dty_to_ty : ?update:bool -> ?is_var:bool -> D_loop.DStd.Expr.ty -> Ty.t
 
 val make_form :
   string ->
-  D_loop.DStd.Expr.term ->
+  Dolmen.Std.Expr.term ->
   Loc.t ->
   decl_kind:Expr.decl_kind ->
   Expr.t
 
 val make :
-  D_loop.DStd.Loc.file ->
+  Dolmen.Std.Loc.file ->
   Commands.sat_tdecl list ->
   [< D_loop.Typer_Pipe.typechecked
   | `Optimize of Dolmen.Std.Expr.term * bool

src/lib/reasoners/adt.ml

@@ -27,7 +27,8 @@
 
 module Sy = Symbols
 module E  = Expr
-module DE = Dolmen.Std.Expr
+
+open Alias.Dolmen
 
 let src = Logs.Src.create ~doc:"Adt" __MODULE__
 module Log = (val Logs.src_log src : Logs.LOG)

src/lib/reasoners/adt_rel.ml

@@ -36,9 +36,7 @@ module LR = Uf.LX
 module Th = Shostak.Adt
 module SLR = Set.Make(LR)
 
-module DE = Dolmen.Std.Expr
-module DT = Dolmen.Std.Expr.Ty
-module B = Dolmen.Std.Builtin
+open Alias.Dolmen
 
 let src = Logs.Src.create ~doc:"Adt_rel" __MODULE__
 module Log = (val Logs.src_log src : Logs.LOG)

src/lib/reasoners/records.ml

@@ -27,7 +27,8 @@
 
 module E = Expr
 module Sy = Symbols
-module DE = Dolmen.Std.Expr
+
+open Alias.Dolmen
 
 type 'a abstract =
   | Record of (DE.term_cst * 'a abstract) list * Ty.t

src/lib/reasoners/theory.ml

@@ -31,14 +31,12 @@ module E = Expr
 module A = Xliteral
 module LR = Uf.LX
 module SE = Expr.Set
-module DE = Dolmen.Std.Expr
-
 module Sy = Symbols
-
 module CC_X = Ccx.Main
-
 module L = Shostak.Literal
 
+open Alias.Dolmen
+
 module type S = sig
   type t
 

src/lib/structures/expr.ml

@@ -26,8 +26,7 @@
 (**************************************************************************)
 
 module Sy = Symbols
-module DE = Dolmen.Std.Expr
-module DStd = Dolmen.Std
+open Alias.Dolmen
 
 (** Data structures *)
 
@@ -1323,7 +1322,7 @@ let mk_tester cons t =
 
 let mk_record xs ty = mk_term (Sy.Op Record) xs ty
 
-let void = mk_constr Dolmen.Std.Expr.Term.Cstr.void [] Ty.tunit
+let void = mk_constr DE.Term.Cstr.void [] Ty.tunit
 
 (** Substitutions *)
 

src/lib/structures/fpa_rounding.ml

@@ -25,11 +25,11 @@
 (*                                                                        *)
 (**************************************************************************)
 
-module DStd = Dolmen.Std
-module DE = DStd.Expr
 module Q = Numbers.Q
 module Z = Numbers.Z
 
+open Alias.Dolmen
+
 (** The five standard rounding modes of the SMTLIB.
     Note that the SMTLIB defines these rounding modes to be the only
     possible modes. *)

src/lib/structures/fpa_rounding.mli

@@ -25,8 +25,6 @@
 (*                                                                        *)
 (**************************************************************************)
 
-module DE = Dolmen.Std.Expr
-
 (** The rounding modes for the Floating Point Arithmetic theory.
     In the legacy frontend, the rounding mode type was `fpa_rounding_mode`
     and defined 5 rounding modes (see the [rounding_mode] type below).
@@ -51,7 +49,7 @@ val fpa_rounding_mode_ae_type_name : string
 val fpa_rounding_mode_dty : Dolmen.Std.Expr.Ty.t
 
 (** The Dolmen constructors of [rounding_mode]. *)
-val d_constrs : DE.term_cst list
+val d_constrs : Dolmen.Std.Expr.term_cst list
 
 (** The rounding mode type. *)
 val fpa_rounding_mode : Ty.t

src/lib/structures/id.ml

@@ -16,6 +16,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
+open Alias.Dolmen
+
 type t = Hstring.t [@@deriving ord]
 
 type typed = t * Ty.t list * Ty.t [@@deriving ord]
@@ -24,7 +26,7 @@ let equal = Hstring.equal
 
 let pp ppf id =
   Dolmen.Smtlib2.Script.Poly.Print.id ppf
-    (Dolmen.Std.Name.simple (Hstring.view id))
+    (DStd.Name.simple (Hstring.view id))
 
 let show id = Fmt.str "%a" pp id
 

src/lib/structures/symbols.ml

@@ -25,7 +25,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-module DE = Dolmen.Std.Expr
+open Alias.Dolmen
 
 type builtin =
     LE | LT (* arithmetic *)

src/lib/structures/ty.ml

@@ -25,7 +25,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-module DE = Dolmen.Std.Expr
+open Alias.Dolmen
 
 type t =
   | Tint
@@ -518,7 +518,6 @@ let type_body name args = Decls.body name args
 let text l s = Text (l, s)
 
 let fresh_empty_text =
-  let module DStd = Dolmen.Std in
   let cpt = ref (-1) in
   fun () ->
     incr cpt;
@@ -551,12 +550,12 @@ let t_adt ?(body=None) s ty_vars =
 
 let tunit =
   let () =
-    match Dolmen.Std.Expr.Ty.definition DE.Ty.Const.unit with
+    match DE.Ty.definition DT.Const.unit with
     | Some def -> Nest.attach_orders [def]
     | None -> assert false
   in
   let body = Some [DE.Term.Cstr.void, []] in
-  let ty = t_adt ~body DE.Ty.Const.unit [] in
+  let ty = t_adt ~body DT.Const.unit [] in
   ty
 
 let trecord ~record_constr lv name lbs =

src/lib/structures/typed.ml

@@ -27,7 +27,7 @@
 
 (** Anotations (used by the GUI). *)
 
-module DE = Dolmen.Std.Expr
+open Alias.Dolmen
 
 type ('a, 'b) annoted =
   { c : 'a;

src/lib/structures/xliteral.ml

@@ -25,7 +25,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-module DE = Dolmen.Std.Expr
+open Alias.Dolmen
 
 type builtin = Symbols.builtin =
     LE | LT | (* arithmetic *)

src/lib/util/alias.ml

@@ -0,0 +1,24 @@
+(**************************************************************************)
+(*                                                                        *)
+(*     Alt-Ergo: The SMT Solver For Software Verification                 *)
+(*     Copyright (C) --- OCamlPro SAS                                     *)
+(*                                                                        *)
+(*     This file is distributed under the terms of OCamlPro               *)
+(*     Non-Commercial Purpose License, version 1.                         *)
+(*                                                                        *)
+(*     As an exception, Alt-Ergo Club members at the Gold level can       *)
+(*     use this file under the terms of the Apache Software License       *)
+(*     version 2.0.                                                       *)
+(*                                                                        *)
+(*     ---------------------------------------------------------------    *)
+(*                                                                        *)
+(*     More details can be found in the directory licenses/               *)
+(*                                                                        *)
+(**************************************************************************)
+
+module Dolmen = struct
+  module DStd = Dolmen.Std
+  module DE = Dolmen.Std.Expr
+  module DT = Dolmen.Std.Expr.Ty
+  module DBuiltin = Dolmen.Std.Builtin
+end

src/lib/util/nest.ml

@@ -16,10 +16,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-module DStd = Dolmen.Std
-module DE = DStd.Expr
-module DT = DE.Ty
-module B = DStd.Builtin
+open Alias.Dolmen
 
 (* A nest is the set of all the constructors of a mutually recursive definition
    of ADTs.
@@ -83,7 +80,7 @@ let (let*) = Option.bind
 let def_of_dstr dstr =
   let* ty_cst =
     match dstr with
-    | DE.{ builtin = B.Destructor _; id_ty; _ } ->
+    | DE.{ builtin = DBuiltin.Destructor _; id_ty; _ } ->
       begin match DT.view id_ty with
         | `Arrow (_, ty) ->
           begin match DT.view ty with
@@ -150,7 +147,7 @@ end
 
 let ty_cst_of_constr DE.{ builtin; _ } =
   match builtin with
-  | B.Constructor { adt; _ } -> adt
+  | DBuiltin.Constructor { adt; _ } -> adt
   | _ -> Fmt.failwith "expect an ADT constructor"
 
 let order_tag : int DStd.Tag.t = DStd.Tag.create ()
@@ -178,7 +175,7 @@ let attach_orders defs =
 
 let perfect_hash id =
   match (id : DE.term_cst) with
-  | { builtin = B.Constructor _; _ } as id ->
+  | { builtin = DBuiltin.Constructor _; _ } as id ->
     begin match DE.Term.Const.get_tag id order_tag with
       | Some h -> h
       | None ->