///|
/// MPST-style Protocol AST MVP for Isochronon W-1.

///|
pub fn package_id() -> String {
  "concord/protocol_ast"
}

///|
pub(all) enum Role {
  Role(String)
} derive(Eq, Debug)

///|
pub fn role(name~ : String) -> Role {
  Role(name)
}

///|
pub fn Role::label(self : Role) -> String {
  match self {
    Role(name) => name
  }
}

///|
pub(all) enum LocalDirection {
  Send
  Receive
} derive(Eq, Debug)

///|
pub fn LocalDirection::label(self : LocalDirection) -> String {
  match self {
    Send => "send"
    Receive => "receive"
  }
}

///|
pub(all) struct ProtocolMessage {
  from : Role
  to : Role
  label : String
  object_id : String
} derive(Eq, Debug)

///|
pub fn ProtocolMessage::make(
  from~ : Role,
  to~ : Role,
  label~ : String,
  object_id~ : String,
) -> ProtocolMessage {
  { from, to, label, object_id }
}

///|
pub(all) struct GlobalProtocol {
  protocol_id : String
  messages : Array[ProtocolMessage]
  terminal_labels : Array[String]
} derive(Debug)

///|
pub fn GlobalProtocol::new(protocol_id~ : String) -> GlobalProtocol {
  { protocol_id, messages: [], terminal_labels: [] }
}

///|
pub fn GlobalProtocol::copy(self : GlobalProtocol) -> GlobalProtocol {
  {
    protocol_id: self.protocol_id,
    messages: copy_messages(self.messages),
    terminal_labels: copy_strings(self.terminal_labels),
  }
}

///|
pub fn GlobalProtocol::send(
  self : GlobalProtocol,
  from~ : Role,
  to~ : Role,
  label~ : String,
  object_id~ : String,
) -> GlobalProtocol {
  let messages = copy_messages(self.messages)
  messages.push(ProtocolMessage::make(from~, to~, label~, object_id~))
  {
    protocol_id: self.protocol_id,
    messages,
    terminal_labels: copy_strings(self.terminal_labels),
  }
}

///|
pub fn GlobalProtocol::with_terminal_label(
  self : GlobalProtocol,
  label~ : String,
) -> GlobalProtocol {
  let terminal_labels = copy_strings(self.terminal_labels)
  terminal_labels.push(label)
  {
    protocol_id: self.protocol_id,
    messages: copy_messages(self.messages),
    terminal_labels,
  }
}

///|
pub(all) struct LocalStep {
  index : Int
  direction : LocalDirection
  label : String
  peer : Role
  object_id : String
} derive(Eq, Debug)

///|
pub(all) struct LocalProtocol {
  protocol_id : String
  role : Role
  steps : Array[LocalStep]
  terminal_labels : Array[String]
} derive(Debug)

///|
pub fn LocalProtocol::copy(self : LocalProtocol) -> LocalProtocol {
  {
    protocol_id: self.protocol_id,
    role: self.role,
    steps: copy_local_steps(self.steps),
    terminal_labels: copy_strings(self.terminal_labels),
  }
}

///|
pub fn GlobalProtocol::project(
  self : GlobalProtocol,
  role : Role,
) -> LocalProtocol {
  let steps : Array[LocalStep] = []
  for index, message in self.messages {
    if message.from == role {
      steps.push({
        index,
        direction: Send,
        label: message.label,
        peer: message.to,
        object_id: message.object_id,
      })
    } else if message.to == role {
      steps.push({
        index,
        direction: Receive,
        label: message.label,
        peer: message.from,
        object_id: message.object_id,
      })
    }
  }
  {
    protocol_id: self.protocol_id,
    role,
    steps,
    terminal_labels: copy_strings(self.terminal_labels),
  }
}

///|
pub(all) struct ProtocolLintIssue {
  protocol_id : String
  step_index : Int?
  message : String
} derive(Eq, Debug)

///|
pub(all) struct ProtocolLintReport {
  issues : Array[ProtocolLintIssue]
} derive(Eq, Debug)

///|
pub fn ProtocolLintReport::passes(self : ProtocolLintReport) -> Bool {
  self.issues.length() == 0
}

///|
pub fn GlobalProtocol::lint(
  self : GlobalProtocol,
  contracts : @isocontract.ContractRegistry,
) -> ProtocolLintReport {
  let issues : Array[ProtocolLintIssue] = []
  if self.protocol_id == "" {
    issues.push({
      protocol_id: self.protocol_id,
      step_index: None,
      message: "protocol_id is empty",
    })
  }
  for index, message in self.messages {
    if message.label == "" {
      issues.push({
        protocol_id: self.protocol_id,
        step_index: Some(index),
        message: "message label is empty",
      })
    }
    if message.from == message.to {
      issues.push({
        protocol_id: self.protocol_id,
        step_index: Some(index),
        message: "self send is not allowed",
      })
    }
    if !contracts.contains_object(message.object_id) {
      issues.push({
        protocol_id: self.protocol_id,
        step_index: Some(index),
        message: "unknown object_id " + message.object_id,
      })
    }
  }
  for label in self.terminal_labels {
    if label == "" {
      issues.push({
        protocol_id: self.protocol_id,
        step_index: None,
        message: "terminal label is empty",
      })
    }
  }
  { issues, }
}

///|
pub(all) struct ProtocolViolation {
  protocol_id : String
  event_id : Int?
  expected_label : String?
  observed_label : String
  reason : String
} derive(Eq, Debug)

///|
pub(all) struct ProtocolMonitorReport {
  matched_steps : Int
  violations : Array[ProtocolViolation]
  last_event_time : @core.VTime?
} derive(Eq, Debug)

///|
pub fn ProtocolMonitorReport::passes(self : ProtocolMonitorReport) -> Bool {
  self.violations.length() == 0
}

///|
pub(all) enum ConformanceFailureSource {
  ObjectContractFailure
  ProtocolContractFailure
} derive(Eq, Debug)

///|
pub fn ConformanceFailureSource::label(
  self : ConformanceFailureSource,
) -> String {
  match self {
    ObjectContractFailure => "object"
    ProtocolContractFailure => "protocol"
  }
}

///|
pub(all) struct ConformanceFailure {
  source : ConformanceFailureSource
  event_id : Int?
  role : Role?
  reason : String
} derive(Eq, Debug)

///|
pub(all) struct RoleProtocolReport {
  role : Role
  matched_steps : Int
  violations : Array[ProtocolViolation]
  last_event_time : @core.VTime?
} derive(Eq, Debug)

///|
pub fn RoleProtocolReport::passes(self : RoleProtocolReport) -> Bool {
  self.violations.length() == 0
}

///|
pub(all) struct ConformanceReport {
  protocol_id : String
  checked_events : Int
  matched_steps : Int
  object_report : @isocontract.ObjectMonitorReport
  protocol_reports : Array[RoleProtocolReport]
  first_failure : ConformanceFailure?
} derive(Eq, Debug)

///|
pub fn ConformanceReport::passes(self : ConformanceReport) -> Bool {
  self.first_failure is None
}

///|
pub(all) struct ObserverBackend {
  registry : @isocontract.ContractRegistry
  protocol : GlobalProtocol
  roles : Array[Role]
} derive(Debug)

///|
pub fn ObserverBackend::new(
  registry~ : @isocontract.ContractRegistry,
  protocol~ : GlobalProtocol,
  roles~ : Array[Role],
) -> ObserverBackend {
  { registry, protocol, roles: copy_roles(roles) }
}

///|
pub fn ObserverBackend::check_trace(
  self : ObserverBackend,
  log : @trace.TraceLog,
) -> ConformanceReport {
  let object_report = @isocontract.ObjectMonitor::new(registry=self.registry).check_trace(
    log,
  )
  let protocol_reports : Array[RoleProtocolReport] = []
  let mut matched_steps = 0
  for role in self.roles {
    let monitor_report = ProtocolMonitor::new(
      local_protocol=self.protocol.project(role),
    ).check_trace(log)
    matched_steps += monitor_report.matched_steps
    protocol_reports.push({
      role,
      matched_steps: monitor_report.matched_steps,
      violations: copy_protocol_violations(monitor_report.violations),
      last_event_time: monitor_report.last_event_time,
    })
  }
  {
    protocol_id: self.protocol.protocol_id,
    checked_events: object_report.checked_events,
    matched_steps,
    object_report,
    protocol_reports,
    first_failure: first_conformance_failure(object_report, protocol_reports),
  }
}

///|
pub(all) struct ProtocolMonitor {
  protocol : LocalProtocol
  trace_node_id : String
} derive(Debug)

///|
pub fn ProtocolMonitor::new(local_protocol~ : LocalProtocol) -> ProtocolMonitor {
  {
    protocol: local_protocol.copy(),
    trace_node_id: local_protocol.role.label(),
  }
}

///|
pub fn ProtocolMonitor::bind_trace_node_id(
  self : ProtocolMonitor,
  trace_node_id : String,
) -> ProtocolMonitor {
  { protocol: self.protocol.copy(), trace_node_id }
}

///|
pub fn ProtocolMonitor::check_trace(
  self : ProtocolMonitor,
  log : @trace.TraceLog,
) -> ProtocolMonitorReport {
  let violations : Array[ProtocolViolation] = []
  let mut cursor = 0
  let mut terminal_seen = false
  let mut last_event_time : @core.VTime? = None
  for event in log.events {
    last_event_time = Some(event.vtime)
    if self.protocol.is_terminal_label(event.label) {
      if event.node_id == self.trace_node_id {
        terminal_seen = true
      } else {
        violations.push({
          protocol_id: self.protocol.protocol_id,
          event_id: Some(event.event_id),
          expected_label: Some(event.label),
          observed_label: event.label,
          reason: "unexpected terminal trace identity",
        })
      }
    } else if self.protocol.knows_label(event.label) {
      if terminal_seen {
        violations.push({
          protocol_id: self.protocol.protocol_id,
          event_id: Some(event.event_id),
          expected_label: None,
          observed_label: event.label,
          reason: "protocol message observed after terminal label",
        })
      } else if cursor >= self.protocol.steps.length() {
        violations.push({
          protocol_id: self.protocol.protocol_id,
          event_id: Some(event.event_id),
          expected_label: None,
          observed_label: event.label,
          reason: "extra protocol message",
        })
      } else {
        let expected = self.protocol.steps[cursor]
        if expected.matches_event(self.trace_node_id, event) {
          cursor += 1
        } else {
          violations.push({
            protocol_id: self.protocol.protocol_id,
            event_id: Some(event.event_id),
            expected_label: Some(expected.label),
            observed_label: event.label,
            reason: "unexpected protocol message",
          })
        }
      }
    }
  }
  if cursor < self.protocol.steps.length() {
    let expected = self.protocol.steps[cursor]
    violations.push({
      protocol_id: self.protocol.protocol_id,
      event_id: None,
      expected_label: Some(expected.label),
      observed_label: "",
      reason: "missing protocol message",
    })
  }
  { matched_steps: cursor, violations, last_event_time }
}

///|
fn LocalProtocol::knows_label(self : LocalProtocol, label : String) -> Bool {
  let mut found = false
  for step in self.steps {
    if step.label == label {
      found = true
    }
  }
  found
}

///|
fn LocalProtocol::is_terminal_label(
  self : LocalProtocol,
  label : String,
) -> Bool {
  let mut found = false
  for terminal in self.terminal_labels {
    if terminal == label {
      found = true
    }
  }
  found
}

///|
fn LocalStep::matches_event(
  self : LocalStep,
  trace_node_id : String,
  event : @trace.TraceEvent,
) -> Bool {
  let role_ok = event.node_id == trace_node_id
  let direction_ok = match self.direction {
    Send => event.direction == @trace.Tx
    Receive => event.direction == @trace.Rx
  }
  self.label == event.label && role_ok && direction_ok
}

///|
fn first_conformance_failure(
  object_report : @isocontract.ObjectMonitorReport,
  protocol_reports : Array[RoleProtocolReport],
) -> ConformanceFailure? {
  match object_report.violations.get(0) {
    Some(violation) =>
      Some({
        source: ObjectContractFailure,
        event_id: violation.event_id,
        role: None,
        reason: violation.reason,
      })
    None => first_protocol_failure(protocol_reports)
  }
}

///|
fn first_protocol_failure(
  protocol_reports : Array[RoleProtocolReport],
) -> ConformanceFailure? {
  let mut found : ConformanceFailure? = None
  for report in protocol_reports {
    if found is None {
      match report.violations.get(0) {
        Some(violation) =>
          found = Some({
            source: ProtocolContractFailure,
            event_id: violation.event_id,
            role: Some(report.role),
            reason: violation.reason,
          })
        None => ()
      }
    }
  }
  found
}

///|
pub fn axis_authority_protocol() -> GlobalProtocol {
  let controller = role(name="controller")
  let drive = role(name="drive")
  GlobalProtocol::new(protocol_id="AxisAuthority")
  .send(
    from=controller,
    to=drive,
    label="axis.lifecycle.enable",
    object_id="axis.lifecycle",
  )
  .send(
    from=drive,
    to=controller,
    label="axis.statusword.ack",
    object_id="axis.statusword",
  )
  .send(
    from=controller,
    to=drive,
    label="axis.target_position.command",
    object_id="axis.target_position",
  )
  .send(
    from=drive,
    to=controller,
    label="axis.actual_position.signal",
    object_id="axis.actual_position",
  )
  .with_terminal_label(label="axis.lifecycle.fault")
}

///|
fn copy_messages(messages : Array[ProtocolMessage]) -> Array[ProtocolMessage] {
  let out : Array[ProtocolMessage] = []
  for message in messages {
    out.push(message)
  }
  out
}

///|
fn copy_local_steps(steps : Array[LocalStep]) -> Array[LocalStep] {
  let out : Array[LocalStep] = []
  for step in steps {
    out.push(step)
  }
  out
}

///|
fn copy_strings(values : Array[String]) -> Array[String] {
  let out : Array[String] = []
  for value in values {
    out.push(value)
  }
  out
}

///|
fn copy_roles(values : Array[Role]) -> Array[Role] {
  let out : Array[Role] = []
  for value in values {
    out.push(value)
  }
  out
}

///|
fn copy_protocol_violations(
  values : Array[ProtocolViolation],
) -> Array[ProtocolViolation] {
  let out : Array[ProtocolViolation] = []
  for value in values {
    out.push(value)
  }
  out
}