From 328fe3da0bc6ce58d6616b6d4721f57a43ea712a Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Wed, 9 Oct 2024 15:15:06 +0200 Subject: [PATCH] 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 | 20 +++++++++++--------- src/lib/dune | 2 +- src/lib/frontend/d_loop.ml | 15 +++++++-------- src/lib/frontend/models.ml | 3 ++- src/lib/frontend/translate.ml | 5 ++--- src/lib/frontend/translate.mli | 6 +++--- src/lib/reasoners/adt.ml | 3 ++- src/lib/reasoners/adt_rel.ml | 4 +--- src/lib/reasoners/records.ml | 3 ++- src/lib/reasoners/theory.ml | 6 ++---- src/lib/structures/expr.ml | 5 ++--- src/lib/structures/fpa_rounding.ml | 4 ++-- src/lib/structures/fpa_rounding.mli | 4 +--- src/lib/structures/id.ml | 4 +++- src/lib/structures/symbols.ml | 2 +- src/lib/structures/ty.ml | 7 +++---- src/lib/structures/typed.ml | 2 +- src/lib/structures/xliteral.ml | 2 +- src/lib/util/alias.ml | 24 ++++++++++++++++++++++++ src/lib/util/nest.ml | 11 ++++------- src/lib/util/nest.mli | 4 +--- 21 files changed, 76 insertions(+), 60 deletions(-) create mode 100644 src/lib/util/alias.ml diff --git a/src/bin/common/solving_loop.ml b/src/bin/common/solving_loop.ml index 52c465ab2..b054dcfcb 100644 --- a/src/bin/common/solving_loop.ml +++ b/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,8 +225,8 @@ 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] @[%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 @@ -232,7 +234,7 @@ let process_source ?selector_inst ~print_status src = in let debug_stmt stmt = Format.eprintf "[logic][typed][%a] @[%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 diff --git a/src/lib/dune b/src/lib/dune index 30cc3b00b..978587057 100644 --- a/src/lib/dune +++ b/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 diff --git a/src/lib/frontend/d_loop.ml b/src/lib/frontend/d_loop.ml index c11592a12..a44b769d5 100644 --- a/src/lib/frontend/d_loop.ml +++ b/src/lib/frontend/d_loop.ml @@ -16,8 +16,8 @@ (* *) (**************************************************************************) -module DStd = Dolmen.Std module Dl = Dolmen_loop +open Alias.Dolmen module State = struct include Dl.State @@ -25,7 +25,7 @@ module State = struct (* 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) diff --git a/src/lib/frontend/models.ml b/src/lib/frontend/models.ml index afa71e83d..40d3bea89 100644 --- a/src/lib/frontend/models.ml +++ b/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 diff --git a/src/lib/frontend/translate.ml b/src/lib/frontend/translate.ml index 262eff96d..69f7b2b5a 100644 --- a/src/lib/frontend/translate.ml +++ b/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 diff --git a/src/lib/frontend/translate.mli b/src/lib/frontend/translate.mli index abb36451c..911b1dfcf 100644 --- a/src/lib/frontend/translate.mli +++ b/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 diff --git a/src/lib/reasoners/adt.ml b/src/lib/reasoners/adt.ml index fca71829f..f459a68c0 100644 --- a/src/lib/reasoners/adt.ml +++ b/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) diff --git a/src/lib/reasoners/adt_rel.ml b/src/lib/reasoners/adt_rel.ml index f156fd4da..69b3c6fbf 100644 --- a/src/lib/reasoners/adt_rel.ml +++ b/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) diff --git a/src/lib/reasoners/records.ml b/src/lib/reasoners/records.ml index bc6c2a452..7ec6280ee 100644 --- a/src/lib/reasoners/records.ml +++ b/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 diff --git a/src/lib/reasoners/theory.ml b/src/lib/reasoners/theory.ml index ad9ad7962..0baad16d0 100644 --- a/src/lib/reasoners/theory.ml +++ b/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 diff --git a/src/lib/structures/expr.ml b/src/lib/structures/expr.ml index 7945afddd..c85ceec96 100644 --- a/src/lib/structures/expr.ml +++ b/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 *) diff --git a/src/lib/structures/fpa_rounding.ml b/src/lib/structures/fpa_rounding.ml index 26d87ac7e..8158d381e 100644 --- a/src/lib/structures/fpa_rounding.ml +++ b/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. *) diff --git a/src/lib/structures/fpa_rounding.mli b/src/lib/structures/fpa_rounding.mli index 85ad8b944..7d5192d38 100644 --- a/src/lib/structures/fpa_rounding.mli +++ b/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 diff --git a/src/lib/structures/id.ml b/src/lib/structures/id.ml index b8666d20a..5a7db0144 100644 --- a/src/lib/structures/id.ml +++ b/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 diff --git a/src/lib/structures/symbols.ml b/src/lib/structures/symbols.ml index 87e47fb45..d911c3854 100644 --- a/src/lib/structures/symbols.ml +++ b/src/lib/structures/symbols.ml @@ -25,7 +25,7 @@ (* *) (**************************************************************************) -module DE = Dolmen.Std.Expr +open Alias.Dolmen type builtin = LE | LT (* arithmetic *) diff --git a/src/lib/structures/ty.ml b/src/lib/structures/ty.ml index 31716e50a..0fedc1b8a 100644 --- a/src/lib/structures/ty.ml +++ b/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 = diff --git a/src/lib/structures/typed.ml b/src/lib/structures/typed.ml index 168e7c8a0..4e2260ea5 100644 --- a/src/lib/structures/typed.ml +++ b/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; diff --git a/src/lib/structures/xliteral.ml b/src/lib/structures/xliteral.ml index b108422c2..9d1097db9 100644 --- a/src/lib/structures/xliteral.ml +++ b/src/lib/structures/xliteral.ml @@ -25,7 +25,7 @@ (* *) (**************************************************************************) -module DE = Dolmen.Std.Expr +open Alias.Dolmen type builtin = Symbols.builtin = LE | LT | (* arithmetic *) diff --git a/src/lib/util/alias.ml b/src/lib/util/alias.ml new file mode 100644 index 000000000..8553c7f0d --- /dev/null +++ b/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 diff --git a/src/lib/util/nest.ml b/src/lib/util/nest.ml index 6b84e2ce0..57ba08c39 100644 --- a/src/lib/util/nest.ml +++ b/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 -> diff --git a/src/lib/util/nest.mli b/src/lib/util/nest.mli index 74c03c244..c4eec7a0b 100644 --- a/src/lib/util/nest.mli +++ b/src/lib/util/nest.mli @@ -16,8 +16,6 @@ (* *) (**************************************************************************) -module DE = Dolmen.Std.Expr - (** The purpose of this module is to construct an appropriate total order on constructors of a given ADT to ensure the termination of model generation for this theory. @@ -30,7 +28,7 @@ module DE = Dolmen.Std.Expr val order_tag : int Dolmen.Std.Tag.t -val attach_orders : DE.ty_def list -> unit +val attach_orders : Dolmen.Std.Expr.ty_def list -> unit (** [attach_orders defs] generate and attach orders on the constructors for each ADT of [defs].