type t = {
  width : int;
  delay : float;
  animate : bool;
  case : Syntax.t;
  started : float;
  mutable last_draw : float;
  mutable last_rows : int;
  mutable title : string;
  mutable fences : Syntax.location list;
  mutable budget : int;
  mutable round : int;
  mutable excluded : int list;
}

let headline text =
  String.split_on_char ' ' text
  |> List.map (fun word ->
    match String.uppercase_ascii word with
    | "SC" | "TSO" | "SMT" | "FIFO" | "CPU" as acronym -> acronym
    | _ -> String.capitalize_ascii word)
  |> String.concat " "

let fit width text =
  if String.length text <= width then text ^ String.make (width - String.length text) ' '
  else String.sub text 0 (max 0 (width - 3)) ^ "..."
let line width = String.make width '-'
let columns width left right =
  let size = (width - 3) / 2 in
  let height = max (List.length left) (List.length right) in
  List.init height (fun i ->
    let at values = if i < List.length values then List.nth values i else "" in
    fit size (at left) ^ " | " ^ fit size (at right))
let label (case : Syntax.t) address = case.names.(address)
let number value = if value >= 0L && value < 1000000L then Int64.to_string value
  else Printf.sprintf "0x%016Lx" value

let instruction (case : Syntax.t) =
  let open Syntax in
  function
  | Store (a, v) -> Printf.sprintf "mov [%s], %s" (label case a) (number v)
  | Load (a, r) -> Printf.sprintf "mov r%d, [%s]" r (label case a)
  | Fence -> "mfence"
  | Move (r, v) -> Printf.sprintf "mov r%d, %s" r (number v)
  | Branch (r, v, target) -> Printf.sprintf "if r%d == %s goto %02d" r (number v) target
  | Enter -> "enter critical section"
  | Leave -> "leave critical section"
  | Exchange (a, r, v) -> Printf.sprintf "xchg [%s], %s -> r%d" (label case a) (number v) r

let registers state t = String.concat "   " (List.init 4 (fun r ->
  Printf.sprintf "r%d=%s" r (number state.Machine.regs.(t).(r))))
let queue case entries = match entries with
  | [] -> "[ empty ]"
  | entries -> String.concat " -> " (List.map (fun (a, v) ->
      Printf.sprintf "[ %s=%s ]" (label case a) (number v)) entries)
let memory case state = String.concat "     " (List.init (Array.length case.Syntax.names) (fun a ->
  Printf.sprintf "[ %s = %s ]" (label case a) (number state.Machine.memory.(a))))

let program case fences state t =
  let pc = state.Machine.pc.(t) in
  let active = if state.critical.(t) then "   Inside Critical Section" else "" in
  let head = [Printf.sprintf "Thread %d   pc=%02d%s" t pc active; registers state t; ""] in
  let code = case.Syntax.threads.(t) in
  let first = max 0 (min (pc - 3) (Array.length code - 9)) in
  head @ List.concat (List.init (min 9 (Array.length code)) (fun offset ->
    let i = first + offset in
    let fence = if not (List.mem (t, i) fences) then [] else
      [Printf.sprintf "     mfence%s" (if i = pc && state.buffers.(t) <> [] then "  < waiting for store buffer" else "")] in
    fence @ [Printf.sprintf "%s %02d  %s" (if i = pc then ">" else " ") i (instruction case code.(i))])) @
  [""; "FIFO Store Buffer   oldest -> newest"; queue case state.buffers.(t)]

let event case before after = function
  | Machine.Idle -> "scheduler idle"
  | Machine.Drain (t, a, v) ->
      Printf.sprintf "T%d drains %s=%s from its FIFO buffer into shared memory" t (label case a) (number v)
  | Machine.Issue (t, _, Syntax.Load (a, r), Some origin) ->
      let source = match origin with Machine.Memory -> "shared memory" | Machine.Buffer -> "its latest buffered write" in
      let stale = List.exists (fun (address, _) -> address = a) before.Machine.buffers.(1 - t) in
      Printf.sprintf "T%d reads %s=%s into r%d from %s%s" t (label case a)
        (number after.Machine.regs.(t).(r)) r source
        (if stale && origin = Machine.Memory then " while the other thread has a pending write" else "")
  | Machine.Issue (t, pc, ins, _) ->
      Printf.sprintf "T%d issues pc=%02d  %s" t pc (instruction case ins)

let timeline actors count =
  let first = max 0 (count - 24) in
  let cells = List.init (count - first) (fun i ->
    let actor = actors.(first + i) in
    match actor with 0 -> "T0" | 1 -> "T1" | 2 -> "F0" | 3 -> "F1" | _ -> "..") in
  ["Schedule    T=Instruction    F=FIFO Drain";
   String.concat " " (List.init (count - first) (fun i -> Printf.sprintf "%02d" (first + i + 1)));
   String.concat " " cells]

let frame ~width (witness : Engine.witness) index =
  let states, events = Engine.replay witness in
  if index < 0 || index >= Array.length states then invalid_arg "trace frame outside execution";
  let state = states.(index) in
  let status = if state.critical.(0) && state.critical.(1) then "Mutual Exclusion Violated"
    else if index = witness.bound then "Requested Outcome Reached" else "Execution in Progress" in
  let description = if index = 0 then "All registers, memory cells and store buffers start empty"
    else event witness.case states.(index - 1) state events.(index - 1) in
  let heading = ["Reorder    " ^ headline witness.case.name;
    Printf.sprintf "model=%s   transition=%02d/%02d   bound=%d   independent replay=passed"
      (Syntax.model_name witness.model) index witness.bound witness.bound;
    line width; status; ""] in
  heading @ columns width (program witness.case witness.fences state 0) (program witness.case witness.fences state 1) @
  [""; line width; "Shared Memory"; memory witness.case state; "";
   "Current Transition"; description; ""] @ timeline witness.actors index

let colour text =
  let paint code text = "\027[" ^ code ^ "m" ^ text ^ "\027[0m" in
  let code =
    if String.contains text '>' && String.starts_with ~prefix:">" (String.trim text) then "1;34"
    else if String.starts_with ~prefix:"Mutual Exclusion Violated" text then "1;31"
    else if String.starts_with ~prefix:"Minimum Repair Verified" text then "1;32"
    else if String.starts_with ~prefix:"Thread 0" text then "1;34"
    else if String.starts_with ~prefix:"Thread 1" text then "1;35"
    else if String.starts_with ~prefix:"Reorder" text then "1" else "30" in
  match String.index_opt text '|' with
  | None -> paint code text
  | Some middle ->
      let left = String.sub text 0 middle in
      let right = String.sub text (middle + 1) (String.length text - middle - 1) in
      paint "34" left ^ paint "30" "|" ^ paint "35" right

let draw view lines =
  let buffer = Buffer.create 16384 in
  let write text =
    let text = fit view.width text in
    let last = ref (String.length text) in
    while !last > 0 && text.[!last - 1] = ' ' do decr last done;
    Buffer.add_string buffer (if view.animate then colour text else String.sub text 0 !last)
  in
  if view.animate then begin
    let rows = Array.of_list lines in
    for row = 0 to max view.last_rows (Array.length rows) - 1 do
      Printf.bprintf buffer "\027[%d;1H\027[2K" (row + 1);
      if row < Array.length rows then write rows.(row)
    done;
    Buffer.add_string buffer "\027[1;1H"
  end else
    List.iter (fun text -> write text; Buffer.add_char buffer '\n') lines;
  output_string stdout (Buffer.contents buffer);
  flush stdout;
  view.last_rows <- List.length lines;
  view.last_draw <- Unix.gettimeofday ()

let create ?(width=140) ?(delay=0.7) ~animate case =
  if width < 78 || width > 180 || not (Float.is_finite delay) || delay < 0. || delay > 10.
  then invalid_arg "invalid display dimensions or delay";
  if animate then begin print_string "\027[2J\027[H\027[?25l"; flush stdout end;
  {width; delay; animate; case; started=Unix.gettimeofday (); last_draw=0.; last_rows=0;
   title="Preparing SMT query"; fences=[]; budget=0; round=0; excluded=[]}

let tick view =
  let now = Unix.gettimeofday () in
  if view.animate && now -. view.last_draw >= 0.35 then begin
    let state = Machine.initial view.case in
    let selected = String.concat "   " (List.map (fun (t, pc) -> Printf.sprintf "T%d@%02d" t pc) view.fences) in
    draw view (["Reorder    " ^ headline view.case.name; line view.width;
      Printf.sprintf "%s   elapsed %.1fs" view.title (now -. view.started);
      Printf.sprintf "verification round %d   fence budget %d   selected %s" view.round view.budget
        (if selected = "" then "none" else selected);
      ""] @ columns view.width (program view.case view.fences state 0) (program view.case view.fences state 1) @
      [""; line view.width;
       "Counterexample Constraints";
       "Lower budgets excluded: " ^ String.concat ", " (List.map string_of_int view.excluded);
       "SMT query running; elapsed time measures actual solver work"])
  end

let finish view =
  if view.animate then begin
    Printf.printf "\027[%d;1H\027[0m\027[?25h" (view.last_rows + 1);
    flush stdout
  end

let phase view title =
  view.title <- title;
  view.last_draw <- 0.;
  tick view

let play view witness =
  let _, events = Engine.replay witness in
  for index = 0 to witness.Engine.bound do
    if index = 0 || index = witness.bound || events.(index - 1) <> Machine.Idle then begin
      draw view (frame ~width:view.width witness index);
      if view.animate then Unix.sleepf view.delay
    end
  done

let notify view = function
  | Engine.Searching (budget, fences) ->
      view.round <- view.round + 1;
      view.budget <- budget;
      view.fences <- fences;
      view.title <- "Searching for a violating execution";
      if view.animate then (view.last_draw <- 0.; tick view)
      else Printf.printf "round %d  budget %d  fences %s\n%!" view.round budget
        (String.concat ", " (List.map (fun (t, pc) -> Printf.sprintf "T%d@%d" t pc) fences))
  | Engine.Counterexample witness ->
      if view.animate then begin
        let faster = {view with delay=min 0.18 view.delay} in
        play faster witness;
        view.last_rows <- faster.last_rows;
        view.last_draw <- faster.last_draw
      end else print_endline "SAT  counterexample replay checked"
  | Engine.Excluded budget ->
      view.excluded <- view.excluded @ [budget];
      if not view.animate then Printf.printf "budget %d excluded\n%!" budget
  | Engine.Refining bound ->
      view.title <- Printf.sprintf "Graph counterexample extends the SMT bound to %d" bound;
      if not view.animate then print_endline view.title
  | Engine.Verified (fences, bound, states) ->
      view.fences <- fences;
      view.title <- "Minimum Repair Verified";
      let state = Machine.initial view.case in
      draw view (["Reorder    " ^ headline view.case.name; line view.width;
        "Minimum Repair Verified";
        Printf.sprintf "%d fences   bound %d   %d actual verification queries"
          (List.length fences) bound view.round;
        Printf.sprintf "Closed graph: %d reachable states, no violating state" states; ""] @
        columns view.width (program view.case fences state 0) (program view.case fences state 1) @
        [""; "Counterexample replay passed; lower-budget SMT certificate is UNSAT"])

let compact case state =
  [Printf.sprintf "T0 pc=%02d  %s" state.Machine.pc.(0)
      (if state.critical.(0) then "Inside" else "Outside"); registers state 0;
   "T0 buffer  " ^ queue case state.buffers.(0); "";
   Printf.sprintf "T1 pc=%02d  %s" state.pc.(1)
      (if state.critical.(1) then "Inside" else "Outside"); registers state 1;
   "T1 buffer  " ^ queue case state.buffers.(1); ""; memory case state;
   ""; if state.critical.(0) && state.critical.(1) then "Overlap" else "No overlap in this state"]

let contrast view (witness : Engine.witness) (repair : Engine.repair) =
  if witness.case <> repair.case then invalid_arg "comparison cases differ";
  let original, _ = Engine.replay witness in
  let fixed = Machine.reschedule witness.case repair.fences witness.actors in
  Engine.validate_schedule witness.case repair.fences fixed;
  let repaired, _ = Machine.replay witness.case Syntax.Tso repair.fences fixed in
  for index = 0 to witness.bound do
    if index = 0 || index = witness.bound || witness.actors.(index - 1) <> 4 then begin
    let prefix = Machine.reschedule witness.case repair.fences (Array.sub witness.actors 0 index) in
    let corrected = repaired.(Array.length prefix) in
    let left = ["Original Execution"; line ((view.width - 3) / 2)] @ compact witness.case original.(index) in
    let right = ["Minimum Fence Repair"; line ((view.width - 3) / 2)] @ compact witness.case corrected in
    draw view (["Reorder    Original and Repaired Executions";
      Printf.sprintf "requested transition %02d/%02d   pending writes drain before fenced instructions" index witness.bound;
      line view.width; ""] @ columns view.width left right @
      [""; line view.width;
       "left: replayed solver counterexample   right: separately SMT-checked repaired execution";
       Printf.sprintf "Minimum repair certificate: %d fences, UNSAT at bound %d"
         (List.length repair.fences) repair.bound]);
    if view.animate then Unix.sleepf view.delay
    end
  done

let outcomes view sc tso =
  let values = List.sort_uniq compare (sc @ tso) in
  let rows = List.map (fun ((left, right) as pair) -> Printf.sprintf "%-12s%-12s%-12s%s"
    (number left) (number right)
    (if List.mem pair sc then "allowed" else "excluded")
    (if List.mem pair tso then "allowed" else "excluded")) values in
  let initial = Machine.initial view.case in
  draw view (["Reorder    Sequential Consistency Versus TSO"; line view.width;
    "Register Outcome Enumeration Complete"; ""] @
    columns view.width (program view.case [] initial 0) (program view.case [] initial 1) @
    [""; line view.width; "Each row is a distinct pair of final register values";
     "T0:r0       T1:r0       SC          TSO"] @ rows)

let graph view fences =
  if view.case.goal <> Syntax.Overlap then invalid_arg "graph view requires a mutual-exclusion property";
  let rows = Array.length view.case.threads.(0) + 1 in
  let cols = Array.length view.case.threads.(1) + 1 in
  let counts = Array.init rows (fun _ -> Array.make cols 0) in
  let unsafe = Array.init rows (fun _ -> Array.make cols false) in
  let occupancy = Array.make 4 0 in
  let depths = Array.init 2 (fun _ -> Array.make 9 0) in
  let render count complete edges violations =
    let grid = ["PC0 vs PC1  " ^ String.concat "" (List.init cols (fun pc -> Printf.sprintf "%6d" pc))] @
      List.init rows (fun row -> Printf.sprintf "%9d  " row ^
        String.concat "" (List.init cols (fun col ->
          if counts.(row).(col) = 0 then "     ."
          else Printf.sprintf "%5d%s" counts.(row).(col) (if unsafe.(row).(col) then "!" else " ")))) in
    let selected = String.concat ", " (List.map (fun (t, pc) -> Printf.sprintf "T%d@%02d" t pc) fences) in
    let occupancy = [""; "Critical Section Occupancy"] @
      List.mapi (fun i name -> Printf.sprintf "%-18s %5d states" name occupancy.(i))
        ["Both Outside"; "T0 Inside"; "T1 Inside"; "Both Inside"] in
    let queues = [""; "FIFO Depth       T0 States    T1 States"] @
      List.init 9 (fun depth -> Printf.sprintf "%10d %12d %12d" depth depths.(0).(depth) depths.(1).(depth)) in
    let programs = ["Fence Placement"] @
      program view.case fences (Machine.initial view.case) 0 @ [""] @
      program view.case fences (Machine.initial view.case) 1 in
    draw view (["Reorder    Finite Execution State Exploration"; line view.width;
      "Program Counter Occupancy   each cell counts distinct reachable machine states";
      "! marks a cell containing a mutual-exclusion violation"; ""] @ columns view.width (grid @ occupancy @ queues) programs @
      [""; line view.width;
       (if complete then Printf.sprintf "Reachable states %d   transitions %d   violating states %d" count edges violations
        else Printf.sprintf "Reachable states %d   transition totals available at graph closure" count);
       "Fences: " ^ (if selected = "" then "none" else selected);
       if complete then "State Graph Closed   every enabled successor is already represented"
       else "Exploring actual enabled instruction and FIFO-drain transitions"])
  in
  let visit state count =
    let row, col = state.Machine.pc.(0), state.pc.(1) in
    counts.(row).(col) <- counts.(row).(col) + 1;
    let active = (if state.critical.(0) then 1 else 0) + (if state.critical.(1) then 2 else 0) in
    occupancy.(active) <- occupancy.(active) + 1;
    for thread = 0 to 1 do
      let depth = List.length state.buffers.(thread) in
      depths.(thread).(depth) <- depths.(thread).(depth) + 1
    done;
    if state.critical.(0) && state.critical.(1) then unsafe.(row).(col) <- true;
    if view.animate && count mod 25 = 0 then begin
      render count false 0 0;
      Unix.sleepf (min 0.12 view.delay)
    end
  in
  let graph = Machine.explore ~visit view.case Syntax.Tso fences in
  render (Array.length graph.states) true graph.edges (List.length graph.violations);
  graph