Preskeleton.hs

-- Draws preskeletons

-- Copyright (c) 2009 The MITRE Corporation
--
-- This program is free software: you can redistribute it and/or
-- modify it under the terms of the BSD License as published by the
-- University of California.

module CPSA.Graph.Preskeleton (kdraw) where

import CPSA.Lib.CPSA (SExpr, printMsg, printEnv)
import CPSA.Graph.XMLOutput
import CPSA.Graph.Config
import CPSA.Graph.SVG
import CPSA.Graph.Loader
import CPSA.Graph.Layout

showMsg :: Config -> SExpr a -> String
showMsg conf x =
    case notation conf of
      Prefix -> show x
      Infix -> printMsg margin indent x

showEnv :: Config -> SExpr a -> String
showEnv conf x =
    case notation conf of
      Prefix -> show x
      Infix -> printEnv margin indent x

margin :: Int
margin = 1024

indent :: Int
indent = 0

-- Compute a node's position.
npos :: Config -> Rank -> Node -> (Float, Float)
npos conf rank (s, p) =
    (xpos, ypos)
    where
      -- Node x coordinate is determined by its strand
      xpos = mx conf + dx conf * fromIntegral s
      -- Node y coordinate is determined by its rank
      ypos = my conf + dy conf * fromIntegral (rank (s, p) + 1)

-- Dimension of the diagram
dim :: Config -> Int -> Int -> (Float, Float)
dim conf strands maxRank =
    (w, h)
    where
      w = 2 * mx conf + dx conf * fromIntegral (strands - 1)
      h = 2 * my conf + dy conf * fromIntegral (maxRank + 1)

-- Add a cross strand arrow
addEdge :: Config -> Rank -> Vertex -> Float -> Float ->
           [Element] -> Vertex -> [Element]
addEdge conf rank src x1 y1 elements n =
    let (x2, y2) = npos conf rank (vnode n) in
    arrow conf (sameMsg src n) x1 y1 x2 y2 : elements

sameMsg :: Vertex -> Vertex -> Bool
sameMsg src dest =
    msg src == msg dest

-- Add a strand node
addNode :: Config -> Preskel -> Rank -> [Element] -> Vertex -> [Element]
addNode conf k rank elements node =
    let (x, y) = npos conf rank (vnode node)
        color = elem node (maybe [] id (unrealized k))
        bullet = circ conf color x y
        es = tooltip (showMsg conf $ msg node) [bullet] : elements
        es' = foldl (addEdge conf rank node x y) es (succs node) in
    maybe es' (addNode conf k rank es') (next node)

-- Add role above a strand
addRole :: Config -> [Element] -> Vertex -> [Element]
addRole conf es node =
    if null r then
        es
    else
        tooltip (showEnv conf e) [text conf x y r] : es
    where
      r = role node
      e = env node
      (x, y0) = npos conf snd (strand node, 0)
      (_, y1) = npos conf snd (strand node, (-1))
      y = (y0 + y1) / 2

-- Add strand lines
addStrand :: Config -> Rank -> [Element] -> Vertex -> [Element]
addStrand conf rank es n =
    line conf x1 y1 x2 y2 : es
    where
      (x1, y1) = npos conf rank (vnode n)
      (x2, y2) = npos conf rank (vnode (lastVertex n))

-- Add title of diagram
title :: Config -> Preskel -> [Element]
title conf k =
    foldl (addRole conf) [header] (initial k)
    where
      (w, _) = dim conf (strands k) 0
      (_, y) = npos conf snd (0, (-1))
      content = protocol k ++ " " ++ show (label k)
      header = text conf (w / 2) y (content ++ annotation)
      annotation =
          case unrealized k of
            Nothing -> ""
            Just [] -> " (realized)"
            _ -> ""

-- Draw a preskeleton
kdraw :: Config -> Float -> Float -> Preskel -> (Float, Float, Element)
kdraw conf x y k =
    (w, h, ec "svg" attrs (rect conf 0 0 w h : lines))
    where
      attrs = [("id", "k" ++ show (label k)), ("x", showL x),
               ("y", showL y), ("width", showL w), ("height", showL h)] ++
              if compact conf then [("visibility", "hidden")] else []
      (w, h) = dim conf (strands k) (maxRank k rank)
      circs = foldl (addNode conf k rank) (title conf k) (initial k)
      lines = foldl (addStrand conf rank) circs (initial k)
      rank = layout k