[dolmen] Add support for theory extensions

This patch is an updated version of OCamlPro#652 to be compatible with the new
API in Dolmen for accessing the [in] semantic triggers.

In addition, the patch also adds proper support for theory extensions,
which were previously ignored by the dolmen frontend. There are also
some simple tests to ensure that theory extensions and semantic triggers
work.

It requires that Gbury/dolmen#162 and Gbury/dolmen#165 be merged to
work. It also includes OCamlPro#660 because it touches on similar codes and
there would be conflicts otherwise.

src/bin/common/solving_loop.ml

@@ -200,11 +200,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
@@ -370,12 +445,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 } ->
@@ -411,7 +486,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
@@ -527,7 +602,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))