Source file resumptions.ml

open UtilsLib

module Log = Xlog.Make (struct
  let name = "Resumptions"
end)

module type Resumptions_sig =
  sig
    type 'a resumptions
    type 'a computation
    type w
    val empty : alt_max:int -> 'a resumptions
        
    val regular_sorting : 'a resumptions -> bool
      
    val is_empty : 'a resumptions -> bool
      
    val extend_resumptions : computation:'a computation ->
      weight:w -> 'a resumptions -> 'a resumptions
        
    val pp : Format.formatter -> 'a resumptions -> unit
      
    val swap: ?current_computation:'a computation * w ->
      'a resumptions -> 'a computation * w * 'a resumptions
  end


module Make(W : Weight.Weight_sig)(C:sig type 'a computation end) =
struct
  exception Empty
  type 'a computation = 'a C.computation
  type w = W.w
  type 'a resumptions = { resumptions : 'a C.computation W.WMap.t;
                          (* a map from weights to states for resuming *)
                          alt_max : int ;
                          (* the threshold beyong which sorting stop
                             being regular *)
                          alt_number : int ;
                          (* the number of alternatives still to be processed *)
                          regular_sorting : bool ;
                          (* This field is used to indicate whether
                             regular sorting is used or if switching
                             to higher stages was necessary. *)
                          unordered_resumptions : ('a C.computation * w) list ;
                          (* when [regular_sorting] is false, populate
                             this list instead of the map. Should be
                             faster.
                             
                          *)
                          unordered_number : int;
                        }

  (* [pow a n] returns [a^n] *)
  let rec pow a = function
    | 0 -> 1
    | 1 -> a
    | n -> 
      let b = pow a (n / 2) in
      b * b * (if n mod 2 = 0 then 1 else a)

  
  let empty ~alt_max =
    let alt_max = max 0 alt_max in
    {
      resumptions = W.WMap.empty;
      alt_max = pow 10 alt_max ;
      alt_number = 0 ;
      regular_sorting = true;
      unordered_resumptions = [];
      unordered_number = 0;}

  let regular_sorting res = res.regular_sorting

  let is_empty res = 
    match W.WMap.optimum res.resumptions, res.unordered_resumptions with
    | None, [] ->
      let () = assert (res.alt_number = 0) in
      let () = assert (res.unordered_number = 0) in
      true
    | Some _, _ -> false
    | None, _ :: _ -> false
  
  let extend_resumptions ~computation ~weight resumptions =
    if
      resumptions.alt_number <= resumptions.alt_max &&
      resumptions.regular_sorting then
      { resumptions with
        resumptions = W.WMap.add weight computation resumptions.resumptions ;
        alt_number = resumptions.alt_number + 1 }
    else
      let () = if resumptions.regular_sorting then
          Logs.warn
            (fun m -> m "The@ grammar@ is@ too@ ambiguous.@ \
                         Breaking@ regular@ sorting@ is@ needed@ in@ \
                         order@ to@ avoid@ stack@ overflow") in
      { resumptions with
        alt_number = resumptions.alt_number + 1 ;
        regular_sorting = false;
        unordered_resumptions = (computation, weight) :: resumptions.unordered_resumptions;
        unordered_number = resumptions.unordered_number + 1}
      
  let pp fmt { resumptions ;
               alt_number;
               alt_max;
               regular_sorting = _;
               unordered_resumptions = _;
               unordered_number = _;} =
    Format.fprintf
      fmt
      "Current resumption is as follow:@ @[%d alternatives (max is %d).@ @[%a@]@]"
      alt_number
      alt_max
      W.WMap.pp
      resumptions[@@warning "-32"]

  (** [swap ~current_computation resumptions] returns [(alternative_states,
     new_resumption)] where [alternative_states] correspond to the
     optimal binding of the resumption, and [new_resumption] the new
     resumption when the optimal one has been removed. If
     [current_computation] is provided, it is taken into account to check
     the optimal binding, except if sorting is not regular in which
     case it is directly returned (in order to stop swapping).

  *)
  let rec swap
      ?current_computation
      (* When present, the [current_computation] parameter specifies the
         current computation and its weight when asking for swapping. The
         aim is to keep the current computation within the working stage
         without adding it with [extend_resumptions] that could put it
         in a secondary stage.*)
      ({ resumptions=resumption_map ;
         alt_number ;
         alt_max=_ ;
         regular_sorting ;
         unordered_resumptions;
         unordered_number;} as resumptions) =
    match regular_sorting,
          current_computation,
          W.WMap.optimum resumption_map,
          unordered_resumptions with
    | true, _, _ , _ :: _ ->
      failwith "Bug: the unorderd_resumptions should be empty when \
                regular sorting is true"
    | true, Some (computation, w), None, [] -> computation, w, resumptions
    | true, Some (computation, w), Some opt, _ when (W.is_better w opt || W.is_equal w opt) ->
      computation, w, resumptions
    | true, Some (computation, w), Some _, _  ->
      let new_resumptions =
        extend_resumptions
          ~computation:computation
          ~weight:w
          resumptions in
      swap new_resumptions
    | true, None, None, [] -> raise Empty
    | false, Some (computation, w), _, _ :: _ ->
      computation, w, resumptions
    | false, Some (computation, w), _, [] ->
      let () = Logs.warn (fun m -> m "Back@ to@ normal@ sorting") in
      computation, w, {resumptions with regular_sorting = true}
    | false, None, None, [] -> raise Empty
    | false, None, _, (computation, w) :: tl ->
      computation,
      w,
      {resumptions with
       unordered_resumptions = tl;
       unordered_number = unordered_number - 1;
      }
    | _, None, Some _, []  ->
      let opt_computation, opt_w, new_map =
        match W.WMap.pop_optimum resumption_map with
        | None -> failwith "Bug: the optimume should not be set to None"
        | Some res -> res in
      opt_computation,
      opt_w,
      { resumptions with
        resumptions = new_map ;
        alt_number = alt_number - 1 ;
        regular_sorting = true ;
      }
      

  
end