Manual merging of ∑ stuff to version 2.1. Hide tests folder temporarily.

src/main/zipperposition.ml

@@ -1,30 +1,27 @@
-
-(* This file is free software, part of Zipperposition. See file "license" for more details. *)
-
-(** {1 Main file for the prover} *)
-
-(** This module just calls the main {!Phases} runner that processes files
-    passed as arguments on the command line. *)
-
-open Logtk
-open Libzipperposition_phases
-
-let section = Libzipperposition.Const.section
-
-let phases = Phases_impl.main_cli ~setup_gc:true ()
-
-let () =
-  ZProf.setup();
-  begin match Phases.run phases with
-    | CCResult.Error msg ->
-      print_endline msg;
-      exit 1
-    | CCResult.Ok (_, 0) -> ()
-    | CCResult.Ok (_, errcode) -> exit errcode (* failure *)
-  end
-
-let _ =
-  at_exit
-    (fun () ->
-       Util.debugf ~section 1 "run time: %.3f" (fun k->k (Util.total_time_s ()));
-       Signal.send Libzipperposition.Signals.on_exit 0)
+
+(* This file is free software, part of Zipperposition. See file "license" for more details. *)
+
+(** {1 Main file for the prover} *)
+
+(** This module just calls the main {!Phases} runner that processes files
+    passed as arguments on the command line. *)
+
+open Logtk
+open Libzipperposition_phases
+
+let section = Libzipperposition.Const.section
+
+let () =
+  begin match main_cli() with
+    | CCResult.Error msg ->
+      print_endline msg;
+      exit 1
+    | CCResult.Ok 0 -> ()
+    | CCResult.Ok errcode -> exit errcode (* failure *)
+  end
+
+let _ =
+  at_exit
+    (fun () ->
+       Util.debugf ~section 1 "run time: %.3f" (fun k->k (Util.total_time_s ()));
+       Signal.send Libzipperposition.Signals.on_exit 0)

src/prover_phases/libzipperposition_phases.ml

@@ -3,12 +3,61 @@
 
 module Phases = Phases
 module Phases_impl = Phases_impl
+open Libzipperposition
+open Phases.Infix
 
-let main_cli ?setup_gc () =
-  Phases.run (Phases_impl.main_cli ?setup_gc ())
-  |> CCResult.map snd
+(* List the extensions as late in the compilation chain as possible. This lets them access as much functionality as possible without a cyclic dependency. That is here where the command line interface is defined. *)
+let load_extensions =
+  let open Libzipperposition_calculi in
+  Phases.start_phase Phases.LoadExtensions >>= fun () ->
+  let _= List.map Extensions.register [
+    Lazy_cnf.extension;
+    Combinators.extension;
+    Higher_order.extension;
+    Superposition.extension;
+    Bce_pe_fixpoint.extension;
+    Bce.extension;
+    Pred_elim.extension;
+    Qle.extension;
+    Hlt_elim.extension;
+    AC.extension;
+    Heuristics.extension;
+    Libzipperposition_avatar.extension;
+    EnumTypes.extension;
+    Libzipperposition_induction.extension;
+    Rewriting.extension;
+    Ind_types.extension;
+    Fool.extension;
+    Booleans.extension;
+    Lift_lambdas.extension;
+    Pure_literal_elim.extension;
+    Bool_encode.extension;
+    App_encode.extension;
+    Eq_encode.extension;
+    Summation_equality.extension;
+    TypeTests.extension;
+  ] in
+  Phases.return_phase (Extensions.extensions ())
 
-let main ?setup_gc ?params file =
-  Phases.run (Phases_impl.main ?setup_gc ?params file)
-  |> CCResult.map snd
 
+let main_cli ?setup_gc:(gc=true) () =
+  Phases.run(
+    (if gc then Phases_impl.setup_gc else Phases.return ()) >>= fun () ->
+    Phases_impl.setup_signal >>= fun () ->
+    Phases_impl.parse_cli >>= fun (files, params) ->
+    load_extensions >>= fun _ ->
+    Phases_impl.process_files_and_print ~params files >>= fun errcode ->
+    Phases.exit >|= fun () ->
+    errcode
+  ) |> CCResult.map snd
+
+let main ?setup_gc:(gc=true) ?params file =
+  Phases.run(
+    (if gc then Phases_impl.setup_gc else Phases.return ()) >>= fun () ->
+    (* pseudo-parse *)
+    Phases_impl.skip_parse_cli ?params file >>= fun (files, params) ->
+    load_extensions >>= fun _ ->
+    Phases_impl.process_files_and_print ~params files >>= fun errcode ->
+    Phases.exit >|= fun () ->
+    errcode
+  ) |> CCResult.map snd

src/prover_phases/phases_impl.ml

@@ -46,41 +46,6 @@ let print_version ~params =
     exit 0
   )
 
-(* have a list of extensions that should be loaded, and load them
-   in phase Phases.LoadExtension
-   FIXME: still too global? *)
-(* TODO: just use a list, not "register" *)
-let load_extensions =
-  let open Libzipperposition_calculi in
-  Phases.start_phase Phases.LoadExtensions >>= fun () ->
-  Extensions.register Lazy_cnf.extension;
-  Extensions.register Combinators.extension;
-  Extensions.register Higher_order.extension;
-  Extensions.register Superposition.extension;
-  Extensions.register Bce_pe_fixpoint.extension;
-  Extensions.register Bce.extension;
-  Extensions.register Pred_elim.extension;
-  Extensions.register Qle.extension;
-  Extensions.register Hlt_elim.extension;
-  Extensions.register AC.extension;
-  Extensions.register Heuristics.extension;
-  Extensions.register Libzipperposition_avatar.extension;
-  Extensions.register EnumTypes.extension;
-  Extensions.register Libzipperposition_induction.extension;
-  Extensions.register Rewriting.extension;
-  Extensions.register Ind_types.extension;
-  Extensions.register Fool.extension;
-  Extensions.register Booleans.extension;
-  Extensions.register Lift_lambdas.extension;
-  Extensions.register Pure_literal_elim.extension;
-  Extensions.register Bool_encode.extension;
-  Extensions.register App_encode.extension;
-  Extensions.register Eq_encode.extension;
-
-
-  let l = Extensions.extensions () in
-  Phases.return_phase l
-
 (* apply functions of [field e], for each extensions [e], to update
    the current state given some parameter [x]. *)
 let do_extensions ~x ~field =
@@ -636,32 +601,12 @@ let process_files_and_print ?(params=Params.default) files =
   print_stats () >>= fun () ->
   Phases.return r
 
-let main_cli ?setup_gc:(gc=true) () =
-  let open Phases.Infix in
-  (if gc then setup_gc else Phases.return ()) >>= fun () ->
-  setup_signal >>= fun () ->
-  parse_cli >>= fun (files, params) ->
-  load_extensions >>= fun _ ->
-  process_files_and_print ~params files >>= fun errcode ->
-  Phases.exit >|= fun () ->
-  errcode
-
 let skip_parse_cli ?(params=Params.default) file =
   Phases.start_phase Phases.Parse_CLI >>= fun () ->
   CCFormat.set_color_default true;
   Phases.set_key Params.key params >>= fun () ->
   Phases.return_phase ([file], params)
 
-let main ?setup_gc:(gc=true) ?params file =
-  let open Phases.Infix in
-  (if gc then setup_gc else Phases.return ()) >>= fun () ->
-  (* pseudo-parse *)
-  skip_parse_cli ?params file >>= fun (files, params) ->
-  load_extensions >>= fun _ ->
-  process_files_and_print ~params files >>= fun errcode ->
-  Phases.exit >|= fun () ->
-  errcode
-
 let () = 
   let open Libzipperposition in
   Params.add_opts [

src/prover_phases/phases_impl.mli

@@ -11,8 +11,6 @@ val parse_cli :
 (** Parses the file list and parameters, also puts the parameters in
     the state *)
 
-val load_extensions : (Extensions.t list, [`Parse_cli], [`LoadExtensions]) Phases.t
-
 val setup_gc : (unit, [`Init], [`Init]) Phases.t
 
 val setup_signal : (unit, [`Init], [`Init]) Phases.t
@@ -44,18 +42,11 @@ val process_files_and_print :
 
 val print_stats : unit -> (unit, [`Check_proof], [`Print_stats]) Phases.t
 
-val main_cli :
-  ?setup_gc:bool ->
-  unit ->
-  (Phases.errcode, [`Init], [`Exit]) Phases.t
-(** Main for the command-line prover *)
-
-val main :
-  ?setup_gc:bool ->
+val skip_parse_cli :
   ?params:Params.t ->
   string -> (* file *)
-  (Phases.errcode, [`Init], [`Exit]) Phases.t
-(** Main to use from a library *)
+  (string list * Params.t, [`Init], [`Parse_cli]) Phases.t
+(** Advance past the phase Parse_CLI as if its results were the given parameters. *)
 
 (* TODO: finer-grained APIs *)
 val refute_or_saturate :

src/prover_phases/summation_equality.ml

@@ -816,7 +816,7 @@ let extension = RecurrencePolynomial.{
     (* We cannot simply define the KBO weights to be maximal too. Instead they are overriding parameters that we query by polyweight_of_id. *)
     update_weight_rule(fun wf _ id -> get_lazy (fun()-> wf id) (polyweight_of_id id))];
 };;
-(* TODO Setting --int-inf-diff-to-lesseq is vital but Arith_int.ml hides it currently. *)
+
 Options.add_opts[
   "--sum-by-recurrences", Arg.Bool((:=)sum_by_recurrences), " use holonomic sequence method to sums (∑) in algebras";
 ]