marxup-3.0.0: MarXup/DerivationTrees.hs

{-# LANGUAGE DisambiguateRecordFields, NamedFieldPuns, RecordWildCards, PostfixOperators, LiberalTypeSynonyms, TypeOperators, OverloadedStrings, PackageImports #-}

module MarXup.DerivationTrees (
-- * Basics
module Data.Monoid,
module Data.LabeledTree,

-- * Derivation' building
-- axiom, rule, etc, aborted, 
emptyDrv, haltDrv, haltDrv', delayPre,
dummy, rule, Derivation, Premise, Rule(..), 

-- * Links
LineStyle,defaultLink,Link(..),

-- * Engine
derivationTree, derivationTreeD

) where

-- import DerivationTrees.Basics
import Data.List
import Control.Monad.Writer 
import Control.Applicative 
import Data.LabeledTree
import Data.Monoid
import MarXup (element)
import MarXup.Tex hiding (label)
import MarXup.MultiRef
import MarXup.Diagram as D
import qualified Data.Tree as T
------------------
--- Basics

type LineStyle = PathOptions -> PathOptions

data Link = Link {label :: Tex (), linkStyle :: LineStyle, steps :: Int}  -- ^ Regular link
          | Delayed -- ^ automatic delaying

defaultLink :: Link
defaultLink = Link mempty (denselyDotted . outline "black")  0


-------------------

data Rule = Rule {ruleStyle :: LineStyle, delimiter :: Tex (), ruleLabel :: Tex (), conclusion :: Tex ()}
--  deriving Show

type Premise = Link ::> Derivation
type Derivation = Tree Link Rule

--------------------------------------------------
-- Delay

depth (Link{steps} ::> Node _ ps) = 1 + steps + maximum (0 : map depth ps)

isDelayed :: Premise -> Bool
isDelayed (Delayed{} ::> _) = True
isDelayed _ = False

delayPre s (Link {..} ::> j) = Link {steps = s, ..} ::> j

delayD :: Derivation -> Derivation
delayD (Node r ps0) = Node r (map delayP ps)
    where ps = fmap (fmap delayD) ps0
          ps' = filter (not . isDelayed) ps
          delayP (Delayed{..} ::> d) = defaultLink {steps = 1 + maximum (0 : map depth ps')} ::> d
          delayP p = p

----------------------------------------------------------
-- TeXify
  
-- | Render a derivation tree without using metapost drv package (links will not be rendered properly)
derivationTree :: Derivation -> TeX
derivationTree = stringizeTex

stringizeTex :: Derivation -> TeX
stringizeTex (Node Rule {..} premises) = braces $ do
  cmd0 "displaystyle" -- so that the text does not get smaller
  cmdn "frac" [mconcat $
               intersperse (cmd0 "quad")
               [ stringizeTex v | _ ::> v <- premises]
              ,conclusion]
  braces $ do cmd0 "small"
              ruleLabel

----------------------------------------------------------
-- Tikzify

derivationTreeD :: Derivation -> Tex ()
derivationTreeD d = element $ derivationTreeDiag $ delayD d

derivationTreeDiag :: Derivation -> Diagram ()
derivationTreeDiag d = do
  [h] <- newVars [ContVar] -- the height of a layer in the tree.
  minimize h
  h >== 1
  tree@(T.Node (_,n,_) _) <- toDiagram h d
  forM_ (T.levels tree) $ \ls ->
    case ls of
      [] -> return ()
      (_:ls') -> forM_ (zip ls ls') $ \((_,_,l),(r,_,_)) ->
        (l + Point 10 0) `westOf` r
  let leftFringe = map head nonNilLevs
      rightFringe = map last nonNilLevs
      nonNilLevs = filter (not . null) $ T.levels tree
  [leftMost,rightMost] <- newVars [ContVar,ContVar]
  forM_ leftFringe $ \(p,_,_) ->
    leftMost <== xpart p
  forM_ rightFringe $ \(_,_,p) ->
    xpart p <== rightMost
  minimize $ 10 *- (rightMost - leftMost)
  n # Center .=. Point 0 0

toDiagPart :: Expr -> Premise -> Diagram (T.Tree (Point,Anchorage,Point))
toDiagPart layerHeight (Link{..} ::> rul)
  | steps == 0 = toDiagram layerHeight rul
  | otherwise = do
    above@(T.Node (_,concl,_) _) <- toDiagram layerHeight rul
    ptObj <- vrule
    let pt = ptObj # S
    pt `eastOf` (concl # W)
    pt `westOf` (concl # E)
    xpart pt =~= xpart (concl # Center)
    let top = ypart (concl # S)
    ypart pt + (fromIntegral steps *- layerHeight) === top
    using linkStyle $ path $ polyline [ptObj # Base,Point (xpart pt) top]
    let embedPt 1 x = T.Node (concl # W,ptObj,concl # E) [x]
        embedPt n x = T.Node (pt,ptObj,pt) [embedPt (n-1) x]
    return $ embedPt steps above

-- | @chainBases distance objects@
-- - Ensures that all the objects have the same baseline.
-- - Separates the objects by the given distance
-- - Returns an object encompassing the group, with a the baseline set correctly.
-- - Returns the average distance between the objects
   
chainBases :: Expr -> [Anchorage] -> Diagram (Anchorage,Expr)
chainBases _ [] = do
  o <- box
  return (o,0)
chainBases spacing ls = do
  grp <- box
  forM_ [Base,N,S] $ \ anch -> do
    D.align ypart $ map (# anch) (grp:ls)
  dxs <- forM (zip ls (tail ls)) $ \(x,y) -> do
    let dx = xdiff (x # E) (y # W)
    dx >== spacing
    return dx
  D.align xpart [grp # W,head ls # W]
  D.align xpart [grp # E,last ls # E]
  return (grp,avg dxs)

-- | Make an horizontally flexible box of glue.
mkHGlue :: Expr -> Expr -> Diagram Anchorage
mkHGlue minimumWidth preferredWidth = do
  g <- box
  width g >== minimumWidth
  width g =~= preferredWidth
  return g

-- | Put object in a box of the same vertical extent, and baseline,
-- but whose height can be bigger.
relaxHeight o = do
  b <- box
  -- using (outline "green")$ traceBounds o
  D.align xpart [b#W,o#W]
  D.align xpart [b#E,o#E]
  D.align ypart [b#Base,o#Base]
  o `fitsVerticallyIn` b
  return b

toDiagram :: Expr -> Derivation -> Diagram (T.Tree (Point,Anchorage,Point))
toDiagram layerHeight (Node Rule{..} premises) = do
  ps <- mapM (toDiagPart layerHeight) premises
  concl <- relaxHeight =<< extend 1.5 <$> texBox conclusion
  -- using (outline "red")$ traceBounds concl
  lab <- texBox ruleLabel

  -- Grouping
  (psGrp,premisesDist) <- chainBases 10 [p | T.Node (_,p,_) _ <- ps]
  -- using (outline "blue" . denselyDotted) $ traceBounds psGrp
  height psGrp === layerHeight

  -- Sepaartion rule
  separ <- hrule
  separ # N .=. psGrp # S
  align ypart [concl # N,separ # S]
  minimize $ width separ
  psGrp `fitsHorizontallyIn` separ
  concl `fitsHorizontallyIn` separ

  -- rule label
  lab # BaseW .=. separ # E + Point 3 (negate 1)


  -- layout hints (not necessary for "correctness")
  let xd = xdiff (separ # W) (psGrp # W)
  xd   === xdiff (psGrp # E) (separ # E) 
  relax 2 $ (2 *- xd) =~= premisesDist
  -- centering of conclusion
  xd' <- absoluteValue $ xdiff (separ # Center) (concl # Center)
  relax 3 $ minimize xd'

  -- draw the rule.
  localPathOptions ruleStyle $ path $ polyline [separ # W,separ # E]
  return $ T.Node (separ # W, concl, lab # E) ps

-----------------------


rule ruleLabel conclusion = Rule {delimiter = mempty, ruleStyle = outline "black", ..}

dummy :: Rule
dummy = (rule mempty mempty) {ruleStyle = const defaultPathOptions}
emptyDrv = Node dummy []

-- abortDrv (Node Rule {..} _) = Node Rule {ruleStyle = Waved, ..} []

-- | Used when the rest of the derivation is known.
haltDrv' :: Tex () -> Derivation -> Derivation
haltDrv' tex (Node r _) = Node r {ruleStyle = noOutline}
     [defaultLink {steps = 1, label = tex} ::> emptyDrv]

-- | More compact variant
haltDrv :: Tex () -> Derivation -> Derivation
haltDrv t (Node r _) = Node r [defaultLink ::> Node dummy {conclusion = cmd "vdots" nil >> cmd "hspace" (tex "2pt") >> t} []]