Add back the Loc module

In OCamlPro#1284 we replaced custom locations with Dolmen locations explicitly,
which breaks API users such as Owi. This patch makes the `Loc.t` type
abstract and provides a conversion function from Dolmen locations
instead.

Author: bclement-ocp

src/bin/js/worker_js.ml

@@ -102,15 +102,15 @@ let main worker_id filename filecontent =
           | None -> begin
               match Expr.form_view f with
               | Lemma {name=name;loc=loc;_} ->
-                let b,e = Dolmen.Std.Loc.lexing_positions loc in
+                let b,e = Loc.lexing_positions loc in
                 let used =
                   if Options.get_unsat_core () then Worker_interface.Unused
                   else Worker_interface.Unknown in
                 (name,b.Lexing.pos_lnum,e.Lexing.pos_lnum,!nb,used) :: acc
               | _ -> acc
             end
           | Some r ->
-            let b,e = Dolmen.Std.Loc.lexing_positions r.loc in
+            let b,e = Loc.lexing_positions r.loc in
             (r.name,b.Lexing.pos_lnum,e.Lexing.pos_lnum,
              !nb,Worker_interface.Used)
             :: acc

src/lib/dune

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

src/lib/frontend/frontend.ml

@@ -135,7 +135,7 @@ module type S = sig
     mutable expl : Explanation.t
   }
 
-  type 'a process = ?loc : Dolmen.Std.Loc.loc -> 'a -> env -> unit
+  type 'a process = ?loc : Loc.t -> 'a -> env -> unit
 
   val init_env : ?selector_inst:(Expr.t -> bool) -> used_context -> env
 
@@ -221,7 +221,7 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct
     mutable expl : Explanation.t
   }
 
-  type 'a process = ?loc : DStd.Loc.loc -> 'a -> env -> unit
+  type 'a process = ?loc : Loc.t -> 'a -> env -> unit
 
   let init_env ?selector_inst used_context =
     {
@@ -294,20 +294,20 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct
     else Ex.empty
 
   let internal_decl
-      ?(loc = DStd.Loc.dummy) (id : Id.typed) (env : env) : unit =
+      ?(loc = Loc.dummy) (id : Id.typed) (env : env) : unit =
     ignore loc;
     match env.res with
     | `Sat | `Unknown ->
       SAT.declare env.sat_env id
     | `Unsat -> ()
 
-  let internal_push ?(loc = DStd.Loc.dummy) (n : int) (env : env) : unit =
+  let internal_push ?(loc = Loc.dummy) (n : int) (env : env) : unit =
     ignore loc;
     Util.loop ~f:(fun _ res () -> Stack.push res env.consistent_dep_stack)
       ~max:n ~elt:(env.res, env.expl) ~init:();
     Steps.apply_without_step_limit (fun () -> SAT.push env.sat_env n)
 
-  let internal_pop ?(loc = DStd.Loc.dummy) (n : int) (env : env) : unit =
+  let internal_pop ?(loc = Loc.dummy) (n : int) (env : env) : unit =
     ignore loc;
     let res, expl =
       Util.loop ~f:(fun _n () _env -> Stack.pop env.consistent_dep_stack)
@@ -318,7 +318,7 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct
     env.expl <- expl
 
   let internal_assume
-      ?(loc = DStd.Loc.dummy)
+      ?(loc = Loc.dummy)
       ((name, f, mf) : string * E.t * bool)
       (env : env) =
     let is_hyp = try (Char.equal '@' name.[0]) with _ -> false in
@@ -350,13 +350,13 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct
       | `Unsat ->
         env.expl <- expl
 
-  let internal_pred_def ?(loc = DStd.Loc.dummy) (name, f) env =
+  let internal_pred_def ?(loc = Loc.dummy) (name, f) env =
     if not (unused_context name env.used_context) then
       let expl = mk_root_dep name f loc in
       SAT.pred_def env.sat_env f name expl loc;
       env.expl <- expl
 
-  let internal_query ?(loc = DStd.Loc.dummy) (n, f, sort) env =
+  let internal_query ?(loc = Loc.dummy) (n, f, sort) env =
     ignore loc;
     let expl =
       match env.res with
@@ -385,7 +385,7 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct
     env.expl <- expl
 
   let internal_th_assume
-      ?(loc = DStd.Loc.dummy)
+      ?(loc = Loc.dummy)
       ({ Expr.ax_name; Expr.ax_form ; _ } as th_elt)
       env =
     if not (unused_context ax_name env.used_context) then
@@ -396,7 +396,7 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct
         env.expl <- expl
       | `Unsat -> ()
 
-  let internal_optimize ?(loc = DStd.Loc.dummy) fn env =
+  let internal_optimize ?(loc = Loc.dummy) fn env =
     ignore loc;
     match env.res with
     | `Sat | `Unknown ->

src/lib/frontend/frontend.mli

@@ -64,7 +64,7 @@ module type S = sig
       They catch the [Sat], [Unsat] and [I_dont_know] exceptions to update the
       frontend environment, but not the [Timeout] exception which is raised to
       the user. *)
-  type 'a process = ?loc:Dolmen.Std.Loc.loc -> 'a -> env -> unit
+  type 'a process = ?loc:Loc.t -> 'a -> env -> unit
 
   val push : int process
 

src/lib/frontend/translate.ml

@@ -495,7 +495,7 @@ let rec dty_to_ty ?(update = false) ?(is_var = false) dty =
     let vty = aux vty in
     Ty.Tfarray (ity, vty)
   | `Bitv n ->
-    if n <= 0 then Errors.typing_error (NonPositiveBitvType n) DStd.Loc.dummy;
+    if n <= 0 then Errors.typing_error (NonPositiveBitvType n) Loc.dummy;
     Ty.Tbitv n
 
   | `App (`Builtin B.Unit, []) -> Ty.tunit
@@ -763,7 +763,7 @@ let arith_ty = function
    - [lb] is the (optional) lower bound for the variable [var]
    - [ub] is the (optional) upper bound for the variable [var]
 *)
-let parse_semantic_bound ?(loc = DStd.Loc.dummy) ~var b x y =
+let parse_semantic_bound ?(loc = Loc.dummy) ~var b x y =
   let is_main_var { DE.term_descr; _ } =
     match term_descr with
     | DE.Var v -> DE.Id.equal v var
@@ -779,7 +779,7 @@ let parse_semantic_bound ?(loc = DStd.Loc.dummy) ~var b x y =
     | _ ->
       Fmt.failwith
         "%aInternal error: invalid semantic bound"
-        DStd.Loc.fmt loc
+        Loc.report loc
   in
   let sort = arith_ty t in
   let parse_bound_kind { DE.term_descr; _ } =
@@ -790,7 +790,7 @@ let parse_semantic_bound ?(loc = DStd.Loc.dummy) ~var b x y =
     | _ ->
       Fmt.failwith
         "%aInternal error: invalid semantic bound"
-        DStd.Loc.fmt loc
+        Loc.report loc
   in
   (* Parse [main_var `op` b] *)
   let parse_bound ?(flip = false) b =
@@ -869,7 +869,7 @@ let mk_rounding fpar =
     Builds an Alt-Ergo hashconsed expression from a dolmen term
 *)
 let rec mk_expr
-    ?(loc = DStd.Loc.dummy) ?(name_base = "") ?(toplevel = false)
+    ?(loc = Loc.dummy) ?(name_base = "") ?(toplevel = false)
     ~decl_kind dt =
   let name_tag = ref 0 in
   let rec aux_mk_expr ?(toplevel = false)
@@ -984,7 +984,7 @@ let rec mk_expr
               | _ ->
                 Fmt.failwith
                   "%asemantic trigger should have at most one bound variable"
-                  DStd.Loc.fmt loc
+                  Loc.report loc
             in
             semantic_trigger ~loc ?var trigger
 
@@ -1400,7 +1400,7 @@ let rec mk_expr
       res
     | _ -> res
 
-  and semantic_trigger ?var ?(loc = DStd.Loc.dummy) t =
+  and semantic_trigger ?var ?(loc = Loc.dummy) t =
     let cst, args =
       match destruct_app t with
       | Some (cst, args) -> cst, args
@@ -1424,7 +1424,7 @@ let rec mk_expr
         | _ ->
           Fmt.failwith
             "%aMaps_to: expected a variable but got: %a"
-            DStd.Loc.fmt loc DE.Term.print x
+            Loc.report loc DE.Term.print x
       end
 
     (* open-ended in interval *)
@@ -1467,16 +1467,16 @@ let rec mk_expr
           E.mk_term (Sy.mk_in lb ub) [aux_mk_expr main_expr] Ty.Tbool
         | _ ->
           Fmt.failwith "%aInvalid semantic trigger: %a"
-            DStd.Loc.fmt loc DE.Term.print t
+            Loc.report loc DE.Term.print t
       end
 
     | _ ->
       Fmt.failwith "%aInvalid semantic trigger: %a"
-        DStd.Loc.fmt loc DE.Term.print t
+        Loc.report loc DE.Term.print t
 
   in aux_mk_expr ~toplevel dt
 
-and make_trigger ?(loc = DStd.Loc.dummy) ~name_base ~decl_kind
+and make_trigger ?(loc = Loc.dummy) ~name_base ~decl_kind
     ~(in_theory: bool) (name: string) (hyp: E.t list)
     (e, from_user: DE.term * bool) =
   (* Dolmen adds an existential quantifier to bind the '?xxx' variables *)
@@ -1618,11 +1618,12 @@ let rec is_pure_term t =
 
 let make file acc stmt =
   let rec aux acc (stmt: _ Typer_Pipe.stmt) =
-    let st_loc = Dolmen.Std.Loc.loc file stmt.loc in
+    let loc = Dolmen.Std.Loc.loc file stmt.loc in
+    let st_loc = Loc.from_dolmen_loc loc in
     match stmt with
     (* Optimize terms *)
     | { contents = `Optimize (t, is_max); _ } ->
-      let e = mk_expr ~loc:st_loc ~toplevel:true ~decl_kind:Dobjective t in
+      let e = mk_expr t ~loc:st_loc ~toplevel:true ~decl_kind:Dobjective in
       let fn = Objective.Function.mk ~is_max e in
       if not @@ is_pure_term e then
         begin
@@ -1760,7 +1761,7 @@ let make file acc stmt =
         | _ ->
           Fmt.failwith
             "%a: Internal error: multiple theories."
-            DStd.Loc.fmt st_loc
+            DStd.Loc.fmt loc
       in
       let decl_kind, assume =
         match theory with
@@ -1837,7 +1838,7 @@ let make file acc stmt =
                 in
                 let qb = E.mk_eq ~iff:true defn ff in
                 let ff =
-                  E.mk_forall name_base DStd.Loc.dummy binders [] qb
+                  E.mk_forall name_base Loc.dummy binders [] qb
                     ~toplevel:true ~decl_kind
                 in
                 assert (Var.Map.is_empty (E.free_vars ff Var.Map.empty));
@@ -1858,7 +1859,7 @@ let make file acc stmt =
                 let iff = Ty.equal (Expr.type_info defn) (Ty.Tbool) in
                 let qb = E.mk_eq ~iff defn ff in
                 let ff =
-                  E.mk_forall name_base DStd.Loc.dummy binders [] qb
+                  E.mk_forall name_base Loc.dummy binders [] qb
                     ~toplevel:true ~decl_kind
                 in
                 assert (Var.Map.is_empty (E.free_vars ff Var.Map.empty));

src/lib/frontend/translate.mli

@@ -35,7 +35,7 @@ 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.Loc.loc ->
+  Loc.t ->
   decl_kind:Expr.decl_kind ->
   Expr.t
 

src/lib/reasoners/fun_sat.mli

@@ -51,7 +51,7 @@ module Make (_ : Theory.S) : sig
   val assume_th_elt : t -> Expr.th_elt -> Explanation.t -> t
 
   val pred_def :
-    t -> Expr.t -> string -> Explanation.t -> Dolmen.Std.Loc.loc -> t
+    t -> Expr.t -> string -> Explanation.t -> Loc.t -> t
 
   val unsat : t -> Expr.gformula -> Explanation.t
 

src/lib/reasoners/sat_solver_sig.ml

@@ -114,7 +114,7 @@ module type S = sig
     Expr.t ->
     string ->
     Explanation.t ->
-    Dolmen.Std.Loc.loc ->
+    Loc.t ->
     unit
   (** [pred_def env f] assumes a new predicate definition [f] in [env]. *)
 

src/lib/reasoners/sat_solver_sig.mli

@@ -94,7 +94,7 @@ module type S = sig
     Expr.t ->
     string ->
     Explanation.t ->
-    Dolmen.Std.Loc.loc ->
+    Loc.t ->
     unit
   (** [pred_def env f] assumes a new predicate definition [f] in [env]. *)
 

src/lib/structures/commands.ml

@@ -41,7 +41,7 @@ type sat_decl_aux =
   | Pop of int
 
 type sat_tdecl = {
-  st_loc : Dolmen.Std.Loc.loc;
+  st_loc : Loc.t;
   st_decl : sat_decl_aux
 }
 
@@ -68,4 +68,3 @@ let print_aux fmt = function
     Format.fprintf fmt "%s %a" s Expr.print e
 
 let print fmt decl = print_aux fmt decl.st_decl
-