modal_logic.typ

#import "@preview/fletcher:0.4.2" as fletcher: node, edge

#let prop(w, v) = { 
  for (p, ws) in v {
    if ws.contains(w) {
      (p,)
    } else {
      ()
    }
  }
}

#let nodes(model) = {
  let (frame, v) = model
  for (w, posR) in frame.enumerate() {
    let (pos, R) = posR
    let ps = prop(w, v)
    if ps == () {
      ps = " "
    } else { 
      ps = ps.map(it => { $it$ }).join(", ")
    }
    (node(pos, align(center)[$w_#w$\ #ps], radius: 2em),)
  }
}

#let edges(model) = {
  let (frame, v) = model
  for (w, posR) in frame.enumerate() {
    let (pos, R) = posR
    for (w1, angle) in R {
      let (pos: pos1, R: R1) = frame.at(w1)
      (edge(pos, pos1, "-|>", bend: angle),)
    }
  }
}

#let Prop(p) = (p: p)
#let Box(phi) = (box: phi)
#let Diamond(phi) = (diamond: phi)
#let Not(phi) = (negation: phi)
#let Arrow(phi, psi) = (arrow: (phi, psi))
#let And(phi, psi) = (conjunction: (phi, psi))
#let Or(phi, psi) = (disjunction: (phi, psi))

#let forcing(w, model, phi) = {
  let (frame, v) = model

  let type = phi.keys().first() 
  let inner = phi.values().first() 
  let unary = ("box", "diamond", "negation")

  if type == "p" {
    let props = prop(w, v)
    props.contains(inner)
  } else if unary.contains(type) {
    let Rw = frame.at(w).at("R").map(it => { it.at(0) })
    let psi = inner
    let fs = (
      negation: phi => not forcing(w, model, phi),
      box: phi => Rw.all(w1 => forcing(w1, model, phi)),
      diamond: phi => Rw.any(w1 => forcing(w1, model, phi)),
    )
    let f = fs.at(type)
    f(psi)
  } else {
    let (psi1, psi2) = inner
    let psi1 = forcing(w, model, psi1)
    let psi2 = forcing(w, model, psi2)
    let fs = (
      conjunction: (x, y) => { x and y },
      disjunction: (x, y) => { x or y },
      arrow: (x, y) => { not x or y },
    )
    let f = fs.at(type)
    f(psi1, psi2)
  }
}

#let render(phi) = {
  let type = phi.keys().first() 
  let inner = phi.values().first() 
  let unary = ("box", "diamond", "negation")

  if type == "p" {
    $#inner$
  } else if unary.contains(type) {
    let psi = render(inner)
    let ss = (
      box: $square$,
      diamond: $diamond$,
      negation: $not$
    )
    $#ss.at(type) #psi$
  } else {
    let (psi1, psi2) = inner
    let psi1 = render(psi1)
    let psi2 = render(psi2)
    let ss = (
      arrow: $->$,
      conjunction: $and$,
      disjunction: $or$,
    )
    $(#psi1 #ss.at(type) #psi2)$
  }
}

#let forceRender(w, m, phi) = {
  let rel = if forcing(w, m, phi) { [\u{22A9}] } else { [\u{22AE}] }
  $w_#w rel #render(phi)$
}

#let modelRender(model) = {
  fletcher.diagram(
    node-stroke: .1em,
    spacing: 4em,
    ..nodes(model),
    ..edges(model)
  )
}

#let frameRender(frame) = {
  let model = (frame, (:))
  modelRender(model)
}