Ensure that definitions have the same ordering with dolmen (OCamlPro#771

)

The dolmen frontend is adding declarations to the end of the command
queue instead of to the front, causing the final command list to be all
shuffled. This is the cause of at least some of the regressions with the
dolmen frontend, since the solver now processes things in a different
order.

This patch ensures that the definitions are added with the correct
ordering, so that the command queue should be the same with both
frontends, barring additional bugs. This was tested with `-d commands`
on a few benchmarks locally, where it produced the exact same output
with both frontends.

The patch also refactors slightly the [handle_smtt] method in the
solving loop: as part of the debugging for this, I realized that we can
never end up with `Hyp` constructors with local/global hypotheses names
there, because one difference between the Dolmen and legacy frontend is
that the legacy frontend extracts the hypotheses from the goal during
typechecking (so prior to cnf-conversion) while the Dolmen frontend
extracts the hypotheses from the goal during cnf-conversion (i.e. when
we encounter a `Solve`).

src/bin/common/solving_loop.ml

@@ -451,21 +451,17 @@ let main () =
               DStd.Loc.fmt loc
         in
         let stmt = { Typer_Pipe.id; contents; loc ; attrs } in
-        let rev_cnf =
-          D_cnf.make (State.get State.logic_file st).loc l stmt
+        let cnf, is_thm =
+          match D_cnf.make (State.get State.logic_file st).loc l stmt with
+          | { Commands.st_decl = Query (_, _, kind); _ } as cnf :: hyps ->
+            let is_thm =
+              match kind with Ty.Thm | Sat -> true | _ -> false
+            in
+            List.rev (cnf :: hyps), is_thm
+          | _ -> assert false
         in
-        let cnf = List.rev rev_cnf in
         let partial_model = solve all_context (cnf, name) in
-        let rec ng_is_thm rcnf =
-          begin match rcnf with
-            | Commands.{ st_decl = Query (_, _, (Ty.Thm | Ty.Sat)); _ } :: _ ->
-              true
-            | Commands.{ st_decl = Query _; _ } :: _ -> false
-            | _ :: tl -> ng_is_thm tl
-            | _ -> assert false (* unreachable *)
-          end
-        in
-        if ng_is_thm rev_cnf
+        if is_thm
         then
           State.set solver_ctx_key (
             let solver_ctx = State.get solver_ctx_key st in
@@ -479,28 +475,6 @@ let main () =
           ) st
           |> State.set partial_model_key partial_model
 
-      | { id = _; contents = `Hyp _; _ } ->
-        let cnf = D_cnf.make (State.get State.logic_file st).loc [] td in
-        begin match cnf with
-          | [Commands.{ st_decl = Assume (name, _, _); _ } as c]
-            when Ty.is_global_hyp name ->
-            State.set solver_ctx_key (
-              let solver_ctx = State.get solver_ctx_key st in
-              { solver_ctx with global = c :: solver_ctx.global }
-            ) st
-          | [Commands.{ st_decl = Assume (name, _, _); _ } as c]
-            when Ty.is_local_hyp name ->
-            State.set solver_ctx_key (
-              let solver_ctx = State.get solver_ctx_key st in
-              { solver_ctx with local = c :: solver_ctx.local }
-            ) st
-          | _ ->
-            State.set solver_ctx_key (
-              let solver_ctx = State.get solver_ctx_key st in
-              { solver_ctx with ctx = cnf @ solver_ctx.ctx }
-            ) st
-        end
-
       | {contents = `Set_option
              { DStd.Term.term =
                  App ({ term = Symbol { name = Simple name; _ }; _ }, [value]);

src/lib/frontend/d_cnf.ml

@@ -1939,6 +1939,8 @@ let make dloc_file acc stmt =
                here. *)
             assert false
         ) defs;
+      let append xs = List.append xs acc in
+      append @@
       List.filter_map (fun (def : Typer_Pipe.def) ->
           match def with
           | `Term_def ( _, ({ path; tags; _ } as tcst), tyvars, terml, body) ->
@@ -2018,7 +2020,7 @@ let make dloc_file acc stmt =
                polymorphic partially-defined bulitin and should not end up
                here. *)
             assert false
-        ) defs |> List.rev_append acc
+        ) defs
 
     | {contents = `Decls [td]; _ } ->
       begin match td with