doc-src/Codegen/Thy/pictures/architecture.tex
author Walther Neuper <neuper@ist.tugraz.at>
Thu, 12 Aug 2010 15:03:34 +0200
branchisac-from-Isabelle2009-2
changeset 37913 20e3616b2d9c
parent 30836 1344132160bb
child 39048 f50f0802ba99
permissions -rw-r--r--
prepare reactivation of isac-update-Isa09-2
     1 
     2 \documentclass[12pt]{article}
     3 \usepackage{tikz}
     4 \usetikzlibrary{shapes}
     5 \usetikzlibrary{arrows}
     6 
     7 \begin{document}
     8 
     9 \thispagestyle{empty}
    10 \setlength{\fboxrule}{0.01pt}
    11 \setlength{\fboxsep}{4pt}
    12 
    13 \fcolorbox{white}{white}{
    14 
    15 \newcommand{\sys}[1]{\emph{#1}}
    16 
    17 \begin{tikzpicture}[x = 4cm, y = 1cm]
    18   \tikzstyle positive=[color = black, fill = white];
    19   \tikzstyle negative=[color = white, fill = black];
    20   \tikzstyle entity=[rounded corners, draw, thick];
    21   \tikzstyle process=[ellipse, draw, thick];
    22   \tikzstyle arrow=[-stealth, semithick];
    23   \node (spec) at (0, 3) [entity, positive] {specification tools};
    24   \node (user) at (1, 3) [entity, positive] {user proofs};
    25   \node (spec_user_join) at (0.5, 3) [shape=coordinate] {};
    26   \node (raw) at (0.5, 4) [entity, positive] {raw code equations};
    27   \node (pre) at (1.5, 4) [process, positive] {preprocessing};
    28   \node (eqn) at (2.5, 4) [entity, positive] {code equations};
    29   \node (iml) at (0.5, 0) [entity, positive] {intermediate program};
    30   \node (seri) at (1.5, 0) [process, positive] {serialisation};
    31   \node (SML) at (2.5, 3) [entity, positive] {\sys{SML}};
    32   \node (OCaml) at (2.5, 2) [entity, positive] {\sys{OCaml}};
    33   \node (further) at (2.5, 1) [entity, positive] {(\ldots)};
    34   \node (Haskell) at (2.5, 0) [entity, positive] {\sys{Haskell}};
    35   \draw [semithick] (spec) -- (spec_user_join);
    36   \draw [semithick] (user) -- (spec_user_join);
    37   \draw [-diamond, semithick] (spec_user_join) -- (raw);
    38   \draw [arrow] (raw) -- (pre);
    39   \draw [arrow] (pre) -- (eqn);
    40   \draw [arrow] (eqn) -- node (transl) [process, positive] {translation} (iml);
    41   \draw [arrow] (iml) -- (seri);
    42   \draw [arrow] (seri) -- (SML);
    43   \draw [arrow] (seri) -- (OCaml);
    44   \draw [arrow, dashed] (seri) -- (further);
    45   \draw [arrow] (seri) -- (Haskell);
    46 \end{tikzpicture}
    47 
    48 }
    49 
    50 \end{document}