imandra-ai / imandra-vscode

VSCode extension for developing imandra
Other
2 stars 0 forks source link

bugs in imandra-merlin? #36

Open ignaden opened 3 years ago

ignaden commented 3 years ago

there are errors in the rest of the code, but is this still expected? Screen Shot 2021-01-11 at 1 56 31 PM

ewenmaclean commented 3 years ago

Can you post the code please - it's hard to know from a screenshot what's going on

ignaden commented 3 years ago
(* Generic support modules *)

module Price = struct
  type t = real

  let (>) x y = x >. y
  let (>=) x y = x >=. y
  let (<) x y = x <. y
  let (<=) x y = x <=. y
  let (/) x y = x /. y
  let (+) x y = x +. y
end

let list_sort = List.sort

let p str = ()

module Time = struct

  type t = int

end

module Qty = struct

  type t = int

end

module Id = struct

  type t = int

end

module Book = struct

  type 'a t = {
    buys: 'a list;
    sells: 'a list;
  }

end

(* Custom modules for the specific venue being modeled *)
module Order = struct

  type order_type = LIMIT | MARKET | PEGGED
  type side = BUY | SELL
  type peg = FAR | MID | NEAR
  type tif = DAY | IOC (* Time-in-force *)
  type exec_inst = ACKED | CANCELLED | EXPIRED | FILL

  type t = {

    (* This first block of fields is set by the model upong entry/trading, etc.
       The user cannot modify them directly. *)

    id: Id.t;
    time: Time.t;
    visible_qty: Qty.t;
    hidden_qty: Qty.t;
    filled_qty: Qty.t;
    effective_p: Price.t option;

    processed: bool; (* This is used during matching 
                      - flag for checking that this order has been checked for tradeability *)

    (* The second block, below, is set by the client. *)

    client_id: Id.t;
    side: side;
    order_type: order_type;
    qty: Qty.t;
    maq: Qty.t; (* MAQ - only applies to visible quantity or the
                   full quantity if everything's hidden/visible *)
    iceberg_qty: Qty.t; (* Displayed quantity - this is a setting.
                           Visible Qty is the actual Qty that is
                           currently displayed.  *)
    tif: tif;
    peg: peg option;
    price: Price.t option;
    hidden: bool;
  }

  let is_valid (o : t) : bool =
    o.qty >  0 &&
    o.maq >= 0 && o.maq <= o.qty &&
    o.iceberg_qty >=0 && o.iceberg_qty <= o.qty &&
    ( o.iceberg_qty <> 0 && not o.hidden) &&
    ( match o.price , o.order_type with
    | None   , LIMIT  -> false
    | Some _ , MARKET -> false     
    | Some p , _ -> Price.(p > 0.0)
    | None   , _ -> true 
    ) && (
      (* if it's a pegged order, it needs to have peg level *)
      match o.peg, o.order_type with
      | None, PEGGED -> false
      | _, _ -> true
    )

end

module Public_order = struct

  type t = {
    side: Order.side;
    qty: Qty.t;
    order_type: Order.order_type;
    price: Price.t;
  }

end

module Order_book = struct

  type t = Order.t Book.t

end

module Public_order_book = struct

  type t = Public_order.t Book.t

end

module Fill = struct

  type t = {
    buy_order_id: Id.t;
    buy_client_id: Id.t;
    sell_order_id: Id.t;
    sell_client_id: Id.t;
    qty: Qty.t;
    price: Price.t;
  }

end

module Msg = struct

  type inbound =
    | New_order of new_order_data
    | Modify_order of modify_order_data
    | Cancel_order of cancel_order_data

  and new_order_data = {
    client_id: Id.t;
    side: Order.side;
    order_type: Order.order_type;
    qty: Qty.t;
    maq: Qty.t;
    peg: Order.peg option;
    iceberg_qty: Qty.t;
    price: Price.t option;
    hidden: bool;
  }

  and modify_order_data = {
    client_id: Id.t;
    side: Order.side;
    order_id: Id.t;
    qty: Qty.t;
    maq: Qty.t;
    price: Price.t option;
    shown_qty: Qty.t;
  }

  and cancel_order_data = {
    order_id: Id.t;
    client_id: Id.t;
    side: Order.side;
  }

  type outbound =
    | Reject of {
        client_id: Id.t;
        order_id: Id.t;
      }
    | ExecutionReport of {
        client_id: Id.t;
        order_id: Id.t;
        exec_inst: Order.exec_inst;
        fill_qty: Qty.t option;
        fill_price: Price.t option;
      }

  type t =
    | Inbound of inbound
    | Outbound of outbound

end

module State = struct

  type t = {
    order_id: Id.t;
    time: Time.t;
    book: Order_book.t;
    out_msgs: Msg.outbound list;
    fills: Fill.t list;
  }

end

(* We'll use this to compute the effective prices of pegged orders *)
type bid_offer = {
  bid: Price.t option
  ; offer: Price.t option
}

(* Compute effective order price, relative to the current best bid/offer *)
let calc_effective_price (o : Order.t) (m : bid_offer) =

  (* Calculate the near and far here *)
  let near = if o.side = BUY then m.bid else m.offer in
  let far = if o.side = BUY then m.offer else m.bid in

  (* Market orders use the other type *)
  match o.order_type with
  | MARKET -> if o.side = BUY then m.offer else m.bid
  | _ ->

  (* Now we're handling limit and pegged orders *)
  match o.price with
  | Some p -> (* We could still have a peg *)
    begin
      match o.peg with
      | None -> Some p (* We just have a limit price *)
      | Some Order.NEAR   ->  (* we're pegged to NEAR *)
        begin
          match near with
          | None -> Some p (* No near is available *)
          | Some nearP ->
          if o.side = BUY then Price.( if p > nearP then Some nearP else Some p )
          else Price.( if p < nearP then Some nearP else Some p)
        end
      | Some MID ->
        begin
          match near, far with
          | Some n, Some f ->
            let mid = Price.((n + f) / 2.0) in
            if o.side = BUY then Price.(if p > mid then Some mid else Some p)
            else Price.(if p < mid then Some mid else Some p)
          | _, _ -> Some p
        end
      | Some FAR ->
        begin
          match far with
          | None -> Some p
          | Some farP ->
            if o.side = BUY then Price.(if p > farP then Some farP else Some p)
            else Price.(if p > farP then Some farP else Some p)
        end
    end

  (* In this case, we do not have a price *)
  | None ->
    begin
      match o.peg with
      | None -> None
      | Some NEAR -> near
      | Some FAR -> far
      | Some MID ->
        begin
          match near, far with
          | Some n, Some f -> Some Price.((n + f) / 2.0)
          | _, _ -> None
        end
    end

(* Comparison function - return true if o1 is higher ranked than o2 *)
let order_higher_ranked (s : Order.side) (o1 : Order.t) (o2 : Order.t) =
  let price_better =
    match o1.effective_p, o2.effective_p with
    | Some p1, Some p2 ->
      if s = BUY then (
        if Price.(p1 > p2) then 1 else
        if Price.(p1 < p2) then -1 else
          0
      ) else (
        if Price.(p1 < p2) then 1 else
        if Price.(p1 > p2) then -1 else
          0
      )
    | _, _ -> 0 in
  (* first, we check the effective price *)
  match price_better with
  | 1 -> true
  | -1 -> false
  | _ ->
    if o1.time < o2.time then (
      true
    ) else if o1.time > o2.time then (
      false
    ) else if o1.qty > o2.qty then (
      true
    ) else (
      false
    )

(* Calculate the effective prices *)
let calc_side_effect_price (ords : Order.t list) (mkt : bid_offer) =
  ords |> List.map ( fun x -> 
    { x with Order.effective_p = calc_effective_price x mkt }
  )

(* Reset the book processed flags *)
let reset_book_flags (book : Order_book.t) =
  let reset_ord (x : Order.t) = { x with processed = false } in
  Book.{ 
    buys = List.map reset_ord book.buys
    ; sells = List.map reset_ord book.sells
  }

(*  *)
let sort_side_orders (s : Order.side) (orders : Order.t list) =
  let leq o1 o2 = not @@ order_higher_ranked s o1 o2 in
  list_sort ~leq orders

(* Clean up IOCs from the order book *)
let clean_iocs (v : State.t) =
  let is_ioc (x:Order.t) = x.tif = IOC in
  let is_not_ioc (x:Order.t) = x.tif <> IOC in
  let create_exp_msg (x:Order.t) =
    Msg.ExecutionReport {
      client_id = x.client_id;
      order_id = x.id;
      exec_inst = EXPIRED;
      fill_price = None;
      fill_qty = None;
    } in
  let buy_msgs = List.map create_exp_msg (List.filter is_ioc v.book.buys) in (* TODO: filter_map *)
  let sell_msgs = List.map create_exp_msg (List.filter is_ioc v.book.sells) in
  let (book:Order_book.t) = {
    buys = List.filter is_not_ioc v.book.buys;
    sells = List.filter is_not_ioc v.book.sells
  } in {
    v with
    book;
    out_msgs = buy_msgs @ (sell_msgs @ v.out_msgs)
  }

(* Trade results *)
type trade_res = {
  proc_orders: Order.t list; (* processed orders *)
  fills: Fill.t list; (* generated fills *)
  resid_ord: Order.t option; (* residual order *)
}

(* Replenish the order *)
let replenish_order (x : Order.t) =
  if x.visible_qty < x.iceberg_qty && x.hidden_qty > 0 then
    let new_visible = min x.iceberg_qty (x.visible_qty + x.hidden_qty) in
    let hidden_delta = new_visible - x.visible_qty in
    { x with
      visible_qty = new_visible
      ; hidden_qty = x.hidden_qty - hidden_delta }
  else
    x

(* Helper function   *)
let do_one_on_one_trade (o : Order.t) (o_effective_p : Price.t) (x_effective_p : Price.t) (x : Order.t) (hidden_sweep : bool) (tr : trade_res) =
  (* let's calculate our min and max trades *)
  let min_our_trade = if o.filled_qty > o.maq then 0 else o.maq in
  let max_our_trade = o.qty - o.filled_qty in
  let min_other_trade =
    if hidden_sweep then (
      if x.filled_qty > x.maq then 0 else x.maq
    ) else (
      if x.filled_qty > x.maq then 0 else x.maq
    )
  in
  let max_other_trade =
    if hidden_sweep then (
      x.qty - x.filled_qty
    ) else (
      x.visible_qty
    )
  in
  let trade_qty =
    if max_our_trade < min_other_trade || max_other_trade < min_our_trade then (
      0
    ) else (
      min max_our_trade max_other_trade
    )
  in
  if trade_qty = 0 then (
    (* Nothing to trade here - let's return trade result with the other order added to the list of processed orders *)
    { tr with proc_orders = tr.proc_orders @ [ x ] }
  ) else (
    let trade_price = if x.time < o.time then x_effective_p else o_effective_p in
    let fill = {
      Fill.buy_order_id = if o.side = BUY then o.id else x.id;
      buy_client_id = if o.side = BUY then o.client_id else x.client_id;
      sell_order_id = if o.side = SELL then o.id else x.id;
      sell_client_id = if o.side = SELL then o.client_id else x.client_id;
      qty = trade_qty;
      price = trade_price;
    }
    in
    (* Let's now update the orders that have traded *)
    let x =
      if hidden_sweep then
        begin
          let sub_from_visible = min trade_qty x.visible_qty in
          let sub_from_hidden = trade_qty - sub_from_visible in
        (* We need to first subtract *)
          replenish_order {
            x with
            filled_qty = x.filled_qty + trade_qty
          ; hidden_qty = x.hidden_qty - sub_from_hidden
          ; visible_qty = x.visible_qty - sub_from_visible }
        end
      else
        replenish_order {
          x with
          filled_qty = x.filled_qty + trade_qty
        ; visible_qty = x.visible_qty - trade_qty } in
    let o = { o with filled_qty = o.filled_qty + trade_qty } in
    let processed_orders =
      if x.filled_qty = x.qty then (
        (* we don't need to insert it *)
        tr.proc_orders
      ) else (
        (* Note: we cons on the front, rather than appending to the end.
           (less recursion, and the order doesn't seem to matter) *)
        x :: tr.proc_orders
      ) in
    (* Let's add our fill to the list of fills in trade result *)
    { fills = fill :: tr.fills;
      proc_orders = processed_orders;
      resid_ord = Some o;
    }
  )

(* trade_hidden_side *)
let rec trade_hidden_side (orders : Order.t list) (o : Order.t) (o_effective_p : Price.t) (curr_p : Price.t) (tr : trade_res) = 
  match orders with
  | [] -> { tr with resid_ord = Some o }
  | x::xs ->
    if x.hidden_qty = 0 then (
      (* we can skip this order since it has no hidden quantity *)
      trade_hidden_side xs o o_effective_p curr_p { tr with proc_orders = tr.proc_orders @ [x] }
    ) else (
      match x.effective_p with
      | None ->
        (* we can also skip this order *)
        trade_hidden_side xs o o_effective_p curr_p { tr with proc_orders = tr.proc_orders @ [x] }
      | Some x_effective_p ->
        if x_effective_p <> curr_p then (
          trade_hidden_side xs o o_effective_p curr_p { tr with proc_orders = tr.proc_orders @ [x] }
        ) else (
          let tr = do_one_on_one_trade o o_effective_p x_effective_p x true tr in
          match tr.resid_ord with
          | None -> { tr with proc_orders = tr.proc_orders @ xs } (* we're done *)
          | Some o -> trade_hidden_side xs o o_effective_p curr_p tr
        )
    )

(*
  Iterate through the list of ranked orders and attempt to trade them.
  - orders - list of orders
  - o - the order we're trading
  - tr - trade results that we're accumulating
  - curr_p - price of the orders on the other side that we're currently sweeping
  - hidden_sweep - are we coducting a second sweep. The first sweep prioritizes only
    the visible volume, while second sweep is design to take care of invisible volume.

  The algorithm is:
  - Start with a price level, set curr_p
  - Process orders
  - If curr_p changes, do a hidden sweep of the old curr_p
  - Once get to new curr_p, just exit it (the old way continues)
*)

let rec trade_side (orders : Order.t list) (o : Order.t) (o_effective_p : Price.t) (curr_p : Price.t) (tr : trade_res) =
  match orders with
  | [] -> { tr with resid_ord = Some o; proc_orders = tr.proc_orders @ orders }
  | x::xs ->

    match x.effective_p with
    | None -> (* We can skip this next order *)
      let tr = { tr with proc_orders = tr.proc_orders @ [ x ] } in
      trade_side xs o o_effective_p curr_p tr

    | Some x_effective_p ->

    (* Need to check whether we should go into sweep mode *)
    if x_effective_p <> curr_p then
      begin
        let tr = trade_hidden_side tr.proc_orders o o_effective_p curr_p { tr with proc_orders = [] } in
        match tr.resid_ord with
        | None -> { tr with proc_orders = tr.proc_orders @ xs }
        | Some o -> trade_side xs o o_effective_p x_effective_p tr
      end
    else

    (* Let's check that the prices are still good for us to pursue this... *)
    if (o.side = BUY && Price.(o_effective_p < x_effective_p)) || (o.side = SELL && Price.(o_effective_p > x_effective_p)) then
      (* we stop here... *)
      { tr with resid_ord = Some o; proc_orders = tr.proc_orders @ orders }
    else

    (*  *)
    let tr = do_one_on_one_trade o o_effective_p x_effective_p x false tr in

    match tr.resid_ord with
    | None ->
      (* It has completed traded, we can exit *)
      { tr with proc_orders = tr.proc_orders @ xs }
    | Some o ->
      (* We still have a residual order *)
      trade_side xs o o_effective_p curr_p tr

(* ***** ***** ***** ***** ***** ***** ***** ***** ***** ***** ***** ***** *****  *)

(* Insert order based on ranking - note although we rerank orders because we have Pegged orders,
  we still  *)
let rec insert_order (s : Order.side) (no : Order.t) (orders : Order.t list) =
  match orders with
  | [] -> [ no ]
  | x::xs ->
    if order_higher_ranked s no x then
      no :: orders
    else
      x :: (insert_order s no xs)

(* Compute BBO, assuming the book is sorted *)
let calc_bbo (book : Order_book.t) =
  let rec get_best_order (ords:Order.t list) =
    match ords with
    | [] -> None
    | x::xs ->
      match x.price with
      | None -> get_best_order xs
      | Some _ -> x.price in
  { bid = get_best_order book.buys;
    offer = get_best_order book.sells
  }

(* Convert fills to execution reports *)
let rec fills_to_msgs (fills : Fill.t list) =
  match fills with
  | [] -> []
  | x::xs ->
    begin
      let ex1 = Msg.ExecutionReport {
          client_id = x.buy_client_id;
          order_id = x.buy_order_id;
          exec_inst = FILL;
          fill_qty = Some x.qty;
          fill_price = Some x.price;
      } in
      let ex2 = Msg.ExecutionReport {
          client_id = x.sell_client_id;
          order_id = x.sell_order_id;
          exec_inst = FILL;
          fill_qty = Some x.qty;
          fill_price = Some x.price;
      } in
      ex1 :: (ex2 :: (fills_to_msgs xs))
    end

(* Empty result *)
let emptyTradeRes = {
  proc_orders = [];
  fills = [];
  resid_ord = None;
}

(* List of orders *)
type side_trade_res = {
  tr_unproc_orders : Order.t list
  ; tr_proc_orders : Order.t list
}

(*
  while True:
  - check the best unprocessed buy and sell orders that can trade (price)
    - if there are no more unprocessed orders
      - quit 
    - else
      - pick the best one ():
        - take all of the orders on the other side and process them
          -> remove if some of the orders trade
          -> continue
        - mark this order if it's still there
  - we need to go through the list of 
*)

(* Split a list of orders into processed and unprocessed *)
let split_orders (orders : Order.t list) = {
  tr_unproc_orders = List.filter (fun (x : Order.t) -> x.processed) orders
  ; tr_proc_orders = List.filter (fun (x : Order.t) -> not x.processed) orders
}

(* Remove order from a list *)
let remove_order (o : Order.t) (orders : Order.t list) =
  List.filter (fun (x : Order.t) -> not (x.id = o.id && x.client_id = o.client_id)) orders

(* TODO what's a good way to do this? *)
let rec update_order (o : Order.t) (orders : Order.t list) =
  match orders with
  | [] -> []
  | x::xs ->
    if x.id = o.id && x.client_id = o.client_id then
      o :: xs
    else
      x :: (update_order o xs)

(* let's trade an order against the other side *)
let trade_order_vs_side (s : Order.side) (o : Order.t) (buyPrice : Price.t) (sellPrice : Price.t) (v : State.t) =

  let tr = 
    if s = BUY then
      trade_side v.book.sells o buyPrice sellPrice emptyTradeRes
    else
      trade_side v.book.buys o sellPrice buyPrice emptyTradeRes in

  (* we can say that we've processed the order now *)
  let o = { o with processed = true } in

  let fill_msgs = fills_to_msgs tr.fills in

  let book =
    match tr.resid_ord with
    | None -> 
      begin
        (* Here we remove the order from the list of buys because it is fully traded *)
          if s = BUY then
            Book.{ sells = tr.proc_orders; buys = (remove_order o v.book.buys) }
          else
            Book.{ buys = tr.proc_orders; sells = (remove_order o v.book.sells) }
      end
    | Some res_ord ->
      begin
        if s = BUY then
          Book.{ sells = tr.proc_orders; buys = (update_order o v.book.buys) }
        else
          Book.{ buys = tr.proc_orders; sells = (update_order o v.book.sells) }
      end in

  { v with book;
      out_msgs = v.out_msgs @ fill_msgs;
      fills = tr.fills @ v.fills;
  }

(* *)
let trade_step (v : State.t) =

  (* Let's first figure out what orders have not been processed yet *)
  let buy_splits = split_orders v.book.buys in
  let sell_splits = split_orders v.book.sells in

  (*  *)
  match buy_splits.tr_unproc_orders, sell_splits.tr_unproc_orders with
  | b::bs, s::xs ->
    begin
      match b.effective_p, s.effective_p with
      | Some buyPrice, Some sellPrice ->
        begin
          if Price.(buyPrice >= sellPrice) then
            begin
              if b.time > s.time then
                (trade_order_vs_side BUY b buyPrice sellPrice v)
              else
                (trade_order_vs_side SELL s buyPrice sellPrice v)
            end
          else
            v
        end
      | _, _ -> v
    end
  | [], s::xs ->
      begin
        (* We only have unprocessed sell orders left *)
        match s.effective_p with
        | Some sellPrice -> v
        | None -> v
      end
  | b::bs, [] ->
      begin
        (* we only have unprocessed buy orders left *)
        match b.effective_p with
        | Some buyPrice -> v
        | None -> v
      end
  | _, _ -> v

(* Main trade function *) 
let rec trade (v : State.t) =
  (* Let's check that if we've traded something, we should attempt to trade again *)
  let v' = trade_step v in
  if v' = v then v else trade v'
[@@adm v] [@@no_validate]

(* Reprice and resort the book *)
let resort_book (book : Order_book.t) : Order_book.t =
  (* Find first buy order *)
  let bbo = calc_bbo book in
  let buy_orders = calc_side_effect_price book.buys bbo in
  let buy_orders = sort_side_orders BUY buy_orders in
  let sell_orders = calc_side_effect_price book.sells bbo in
  let sell_orders = sort_side_orders SELL sell_orders in
  { buys = buy_orders; sells = sell_orders }

(* Top level trade function - we always start by sorting the books *)
let try_trading (v : State.t) : State.t option =
  if List.length v.book.buys > 0 && List.length v.book.sells > 0 then
    let book = resort_book v.book in
    (* Now that we have up-to-date books, let's attemp to trade them *)
    Some (trade { v with book })
  else    
    Some v

(*** ***** *** ***** *** ***** *** ***** *** ***** *** ***** *)
(* Message processing functions *)
(*** ***** *** ***** *** ***** *** ***** *** ***** *** ***** *)

let do_new_order (v : State.t) (m : Msg.inbound) : State.t option =
  match m with
  | Msg.Cancel_order _ -> None
  | Msg.Modify_order _ -> None
  | Msg.New_order no ->
    (* Let us create a new order ID *)
    let new_ord_id = v.order_id + 1 in
    let new_ord = Order.{
      client_id = no.client_id;
      id = new_ord_id;
      side = no.side;
      order_type = no.order_type;
      time = v.time;
      qty = no.qty;
      filled_qty = 0;
      maq = no.maq;
      peg = no.peg;
      iceberg_qty = no.iceberg_qty;
      price = no.price;
      effective_p = None;
      hidden = no.hidden;
      tif = DAY;
      visible_qty = if no.iceberg_qty > 0 then no.iceberg_qty else no.qty;
      hidden_qty = if no.iceberg_qty > 0 then no.qty - no.iceberg_qty else 0; (* hidden quantity is what's not displayed *)
      processed = false;  
  } in
  (* If we ended up with an invalid order, let's reject it *)
  if not (Order.is_valid new_ord) then (
    let rej_msg = Msg.Reject { client_id = 0; order_id = 0 } in
    Some { v with out_msgs = rej_msg :: v.out_msgs }
  ) else (
    (* Here we know we have a valid order, so let's insert it *)
    let v' = { v with order_id = new_ord_id } in
    if no.side = BUY then (
      let new_buys = insert_order BUY new_ord v.book.buys in
      let new_book = { v.book with buys = new_buys } in
      let new_ord_ack = Msg.ExecutionReport {
          client_id = new_ord.client_id
        ; order_id = new_ord.id
        ; exec_inst = ACKED
        ; fill_qty = None
        ; fill_price = None
        } in
      Some { v' with
             book = new_book;
             out_msgs = new_ord_ack :: v.out_msgs }
    ) else (
      let new_sells = insert_order SELL new_ord v.book.sells in
      let new_book = { v.book with sells = new_sells } in
      let new_ord_ack = Msg.ExecutionReport {
          client_id = new_ord.client_id
        ; order_id = new_ord.id
        ; exec_inst = ACKED
        ; fill_qty = None
        ; fill_price = None
        } in
      Some { v' with
             book = new_book;
             out_msgs = new_ord_ack :: v.out_msgs }
    )
  )

(* Will perform the actual order modification *)
let rec modify_order_side (s : Order.side) (orders : Order.t list) (proc_orders : Order.t list) (mo : Msg.modify_order_data) (v : State.t) = 
  match orders with
  | [] ->
    begin
      (* We could not find the order, so we need to return the state and send back a rejection message *)
      let rej_msg = Msg.Reject { client_id = mo.client_id; order_id = mo.order_id } in
      { v with out_msgs = rej_msg :: v.out_msgs }
    end
  | x::xs ->
      if x.client_id = mo.client_id && x.id = mo.order_id then (
        (* Let's make the updates heres *)
        let x =
          { x with
            qty = mo.qty;
            maq = mo.maq;
            price = mo.price;
            iceberg_qty = mo.shown_qty
          } in
        let book =
          if s = BUY then
            { Book.buys = proc_orders @ (x::xs); sells = v.book.sells }
          else
            { Book.buys = v.book.buys; sells = proc_orders @ (x::xs) } in
        let mod_msg = Msg.ExecutionReport {
            client_id = mo.client_id
          ; order_id = mo.order_id
          ; exec_inst = ACKED
          ; fill_price = None
          ; fill_qty = None } in
        { v with
          book;
          out_msgs = mod_msg :: v.out_msgs }
      ) else (
        modify_order_side s xs (x :: proc_orders) mo v
      )

let do_modify_order (v : State.t) (m : Msg.inbound) : State.t option =
  match m with
  | Msg.Cancel_order _ -> None
  | Msg.New_order _ -> None
  | Msg.Modify_order mo ->
    if mo.side = BUY then (
      Some (modify_order_side BUY v.book.buys [] mo v)
    ) else (
      Some (modify_order_side SELL v.book.sells [] mo v)
    )

let rec cancel_order_side (s : Order.side) (orders : Order.t list) (proc_orders : Order.t list) (v : State.t) (cl_id : Id.t) (ord_id : Id.t) =
  match orders with
  | [] ->
    begin
      (* We could not find the order, so we need to return the state and send back a rejection message *)
      let rej_msg = Msg.Reject { client_id = cl_id; order_id = ord_id } in
      { v with out_msgs = rej_msg :: v.out_msgs }
    end
  | x::xs ->
    if x.client_id = cl_id && x.id = ord_id then
      begin
        let book =
          if s = BUY then
            { Book.buys = proc_orders @ xs; sells = v.book.sells }
          else
            { buys = v.book.buys; sells = proc_orders @ xs } in
        let can_msg = Msg.ExecutionReport {
            client_id = cl_id
          ; order_id = ord_id
          ; exec_inst = CANCELLED
          ; fill_price = None
          ; fill_qty = None } in
        { v with
          book;
          out_msgs = can_msg :: v.out_msgs }
      end
    else
      cancel_order_side s xs (x :: proc_orders) v cl_id ord_id

let do_cancel_order (v : State.t) (m : Msg.inbound) : State.t option =
  match m with
  | Msg.New_order _ -> None
  | Msg.Modify_order _ -> None
  | Msg.Cancel_order co ->
    if co.side = BUY then (
      Some (cancel_order_side BUY v.book.buys [] v co.client_id co.order_id)
    ) else (
      Some (cancel_order_side SELL v.book.sells [] v co.client_id co.order_id)
    )

let do_time_step (v : State.t) : State.t option =
  Some { v with time = Time.(v.time + 1) }

(*** ***** *** ***** *** ***** *** ***** *** ***** *)

let process_inbound (v : State.t) (m : Msg.inbound) =
  match m with
  | Msg.New_order _ -> do_new_order v m
  | Msg.Modify_order _ -> do_modify_order v m
  | Msg.Cancel_order _ -> do_cancel_order v m

let step (v : State.t) (m : Msg.inbound option) : State.t option =
  match m with
  | None -> try_trading v
  | Some m ->
    begin match process_inbound v m with
      | None -> try_trading v
      | Some v' -> try_trading v'
    end

let init_state : State.t = {
  order_id = 0;
  book = { buys = []; sells = [] };
  time = 0;
  out_msgs = [];
  fills = [];
}

(* predicates *)
let init (s:State.t) = s = init_state

let has_buys (s:State.t) =
  s.book.buys <> []

let has_sells (s:State.t) =
  s.book.sells <> []

let iceberg_sell (s:State.t) =
  match s.book.sells with
  | o :: _ ->
    o.hidden_qty > 0
  | _ -> false

let iceberg_buy (s:State.t) =
  match s.book.buys with
  | o :: _ ->
    o.hidden_qty > 0
  | _ -> false

let fills (s:State.t) =
  s.fills <> []

let reject (s:State.t) =
  match s.out_msgs with
  | Msg.Reject _ :: _ -> true
  | _ -> false

let valid_state (s:State.t) =
  match s.book.buys, s.book.sells with
  | [], []
  | [], _ :: []
  | _ :: [], []
  | _ :: [], _ :: []
  | _ :: [], _ :: _ :: []
    -> true
  | _ -> false
;;