[dolmen] Add support for theory extensions

This patch adds support for theory extensions in the Dolmen frontend.
It uses Gbury/dolmen#165 and hence requires that to be merged in Dolmen
to work.

It also includes OCamlPro#660 because it touches similar parts of the code and
there would be conflicts otherwise.

alt-ergo-lib.opam.template

@@ -17,14 +17,14 @@ build: [
 pin-depends: [
   [
   "dolmen.dev"
-  "git+https://github.com/Gbury/dolmen.git#master"
+  "git+https://github.com/Gbury/dolmen.git#theory_attrs"
   ]
   [
   "dolmen_loop.dev"
-  "git+https://github.com/Gbury/dolmen.git#master"
+  "git+https://github.com/Gbury/dolmen.git#theory_attrs"
   ]
   [
   "dolmen_type.dev"
-  "git+https://github.com/Gbury/dolmen.git#master"
+  "git+https://github.com/Gbury/dolmen.git#theory_attrs"
   ]
 ]

src/bin/common/solving_loop.ml

@@ -231,11 +231,86 @@ let main () =
     else
       st, `Continue c
   in
-  let debug_typed_pipe st stmt =
+  let typecheck st (stmt : DStd.Statement.t) =
+    let file_loc = (State.get State.logic_file st).loc in
+    let dloc = DStd.Loc.(loc file_loc stmt.loc) in
+    let aloc = DStd.Loc.lexing_positions dloc in
+    (* Dolmen adds information about theory extensions and case splits in the
+       [attrs] field of the parsed statements. [attrs] can be arbitrary terms,
+       where the information we care about is encoded as a [Colon]-list of
+       symbols.
+
+       The few helper functions below are used to extract the information from
+       the [attrs]. More specifically:
+
+       - "case split" statements have the [DStd.Id.case_split] symbol as an
+          attribute
+
+       - Theory elements have a 3-length list of symbols as an attribute, of
+          the form [theory_decl; name; extends], where [theory_decl] is the
+          symbol [DStd.Id.theory_decl] and [name] and [extends] are the theory
+          extension name and the base theory name, respectively.
+    *)
+    let rec symbols = function
+      | DStd.Term. { term = Colon ({ term = Symbol sy; _ }, xs); _ } ->
+        Option.bind (symbols xs) @@ fun sys ->
+        Some (sy :: sys)
+      | { term = Symbol sy; _ } -> Some [sy]
+      | _ -> None
+    in
+    let sy_attrs = List.filter_map symbols stmt.DStd.Statement.attrs in
+    let is_case_split =
+      let is_case_split = function
+        | [ sy ] when DStd.Id.(equal sy case_split) -> true
+        | _ -> false
+      in
+      List.exists is_case_split sy_attrs
+    in
+    let theory =
+      let theory =
+        let open DStd.Id in
+        function
+        | [ td; name; extends] when DStd.Id.(equal td theory_decl) ->
+          let name = match name.name with
+            | Simple name -> name
+            | _ ->
+              Util.failwith
+                "Internal error: invalid theory extension: %a"
+                print name
+          in
+          let extends = match extends.name with
+            | Simple name ->
+              begin match Util.th_ext_of_string name with
+                | Some extends -> extends
+                | None ->
+                  Errors.typing_error (ThExtError name) aloc
+              end
+            | _ ->
+              Util.failwith
+                "Internal error: invalid base theory name: %a"
+                print extends
+          in
+          Some (name, extends)
+        | _ -> None
+      in
+      match List.filter_map theory sy_attrs with
+      | [] -> None
+      | [name, extends] -> Some (name, extends)
+      | _ ->
+        Util.failwith
+          "%a: Internal error: multiple theories."
+          DStd.Loc.fmt dloc
+    in
+    let st, c = Typer_Pipe.typecheck st stmt in
+    match c with
+    | `Continue stmt -> st, `Continue { stmt ; theory; is_case_split}
+    | `Done () -> st, `Done ()
+  in
+  let debug_typed_pipe st (stmt : _ D_loop.stmt) =
     if State.get State.debug st then
       Format.eprintf "[logic][typed][%a] @[<hov>%a@]@\n@."
-        Dolmen.Std.Loc.print_compact stmt.Typer_Pipe.loc
-        Typer_Pipe.print stmt;
+        Dolmen.Std.Loc.print_compact stmt.stmt.Typer_Pipe.loc
+        Typer_Pipe.print stmt.stmt;
     if get_type_only () then
       st, `Done ()
     else
@@ -411,12 +486,12 @@ let main () =
 
   let handle_stmt :
     FE.used_context -> State.t ->
-    _ D_loop.Typer_Pipe.stmt -> State.t =
+    _ D_loop.stmt -> State.t =
     let goal_cnt = ref 0 in
     fun all_context st td ->
       let file_loc = (State.get State.logic_file st).loc in
       let solver_ctx = State.get solver_ctx_key st in
-      match td with
+      match td.stmt with
       (* When the next statement is a goal, the solver is called and provided
          the goal and the current context *)
       | { id; contents = (`Solve _ as contents); loc } ->
@@ -452,7 +527,7 @@ let main () =
         in
         let stmt = { Typer_Pipe.id; contents; loc } in
         let rev_cnf =
-          D_cnf.make (State.get State.logic_file st).loc l stmt
+          D_cnf.make (State.get State.logic_file st).loc l { td with stmt }
         in
         let cnf = List.rev rev_cnf in
         let partial_model = solve all_context (cnf, name) in
@@ -577,7 +652,7 @@ let main () =
           (fix
              (op ~name:"expand" Parser.expand)
              (op ~name:"debug_pre" debug_parsed_pipe
-              @>|> op ~name:"typecheck" Typer_Pipe.typecheck
+              @>|> op ~name:"typecheck" typecheck
               @>|> op ~name:"debug_post" debug_typed_pipe
               @>|> op_i (handle_stmt all_used_context)
               @>>> _end))

src/lib/frontend/d_cnf.ml

@@ -1481,7 +1481,7 @@ let make_form name_base f loc ~decl_kind =
   else
     E.mk_forall name_base loc SM.empty [] ff ~toplevel:true ~decl_kind
 
-let make dloc_file acc stmt =
+let make dloc_file acc { stmt ; theory; is_case_split }=
   let rec aux acc (stmt: _ Typer_Pipe.stmt) =
     match stmt with
 
@@ -1536,10 +1536,29 @@ let make dloc_file acc stmt =
       C.{st_decl; st_loc} :: List.rev_append (List.rev rev_hyps_c) acc
 
     (* Axiom definitions *)
-    | { id = Id.{name = Simple name; _}; contents = `Hyp t; loc; } ->
+    | { id = Id.{name = Simple name; _}; contents = `Hyp t; loc } ->
+      let decl_kind, assume =
+        match theory with
+        | Some (th_name, extends) ->
+          let axiom_kind =
+            if is_case_split then Util.Default else Util.Propagator
+          in
+          let th_assume name e =
+            let th_elt = {
+              Expr.th_name;
+              axiom_kind;
+              extends;
+              ax_form = e;
+              ax_name = name;
+            } in
+            C.ThAssume th_elt
+          in
+          E.Dtheory, th_assume
+        | None -> E.Daxiom, fun name e -> C.Assume (name, e, true)
+      in
       let st_loc = dl_to_ael dloc_file loc in
-      let e = make_form name t st_loc ~decl_kind:E.Daxiom in
-      let st_decl = C.Assume (name, e, true) in
+      let e = make_form name t st_loc ~decl_kind in
+      let st_decl = assume name e in
       C.{ st_decl; st_loc } :: acc
 
     (* Function and predicate definitions *)

src/lib/frontend/d_cnf.mli

@@ -37,7 +37,7 @@ val make :
   [< D_loop.Typer_Pipe.typechecked
   | `Goal  of Dolmen.Std.Expr.term
   | `Check of Dolmen.Std.Expr.term
-         > `Hyp ] D_loop.Typer_Pipe.stmt ->
+         > `Hyp ] D_loop.stmt ->
   Commands.sat_tdecl list
 (** [make acc stmt] Makes one or more [Commands.sat_tdecl] from the
     type-checked statement [stmt] and appends them to [acc].

src/lib/frontend/d_loop.ml

@@ -39,3 +39,17 @@ 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)
+
+(** A wrapper around Dolmen's type of typed statements with additional
+    information relevant to Alt-Ergo. *)
+type +!'a stmt = {
+  stmt : 'a Typer_Pipe.stmt ;
+  (** The underlying Dolmen statement. *)
+  theory : (string * Util.theories_extensions) option ;
+  (** Information about the theory extension that this statement is part
+      of, if any *)
+  is_case_split : bool ;
+  (** Indicates that this statement is a "case-split" axiom. Case-split
+      axioms are specific axioms in theory extensions that are used to perform
+      case analysis. *)
+}