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
haftmann@30734
     1
haftmann@30734
     2
\documentclass[12pt]{article}
haftmann@30734
     3
\usepackage{tikz}
haftmann@30836
     4
\usetikzlibrary{shapes}
haftmann@30836
     5
\usetikzlibrary{arrows}
haftmann@30734
     6
haftmann@30734
     7
\begin{document}
haftmann@30734
     8
haftmann@30754
     9
\thispagestyle{empty}
haftmann@30754
    10
\setlength{\fboxrule}{0.01pt}
haftmann@30754
    11
\setlength{\fboxsep}{4pt}
haftmann@30754
    12
haftmann@30836
    13
\fcolorbox{white}{white}{
haftmann@30754
    14
haftmann@30836
    15
\newcommand{\sys}[1]{\emph{#1}}
haftmann@30836
    16
haftmann@30836
    17
\begin{tikzpicture}[x = 4cm, y = 1cm]
haftmann@30836
    18
  \tikzstyle positive=[color = black, fill = white];
haftmann@30836
    19
  \tikzstyle negative=[color = white, fill = black];
haftmann@30836
    20
  \tikzstyle entity=[rounded corners, draw, thick];
haftmann@30836
    21
  \tikzstyle process=[ellipse, draw, thick];
haftmann@30836
    22
  \tikzstyle arrow=[-stealth, semithick];
haftmann@30836
    23
  \node (spec) at (0, 3) [entity, positive] {specification tools};
haftmann@30836
    24
  \node (user) at (1, 3) [entity, positive] {user proofs};
haftmann@30836
    25
  \node (spec_user_join) at (0.5, 3) [shape=coordinate] {};
haftmann@30836
    26
  \node (raw) at (0.5, 4) [entity, positive] {raw code equations};
haftmann@30836
    27
  \node (pre) at (1.5, 4) [process, positive] {preprocessing};
haftmann@30836
    28
  \node (eqn) at (2.5, 4) [entity, positive] {code equations};
haftmann@30836
    29
  \node (iml) at (0.5, 0) [entity, positive] {intermediate program};
haftmann@30836
    30
  \node (seri) at (1.5, 0) [process, positive] {serialisation};
haftmann@30836
    31
  \node (SML) at (2.5, 3) [entity, positive] {\sys{SML}};
haftmann@30836
    32
  \node (OCaml) at (2.5, 2) [entity, positive] {\sys{OCaml}};
haftmann@30836
    33
  \node (further) at (2.5, 1) [entity, positive] {(\ldots)};
haftmann@30836
    34
  \node (Haskell) at (2.5, 0) [entity, positive] {\sys{Haskell}};
haftmann@30836
    35
  \draw [semithick] (spec) -- (spec_user_join);
haftmann@30836
    36
  \draw [semithick] (user) -- (spec_user_join);
haftmann@30836
    37
  \draw [-diamond, semithick] (spec_user_join) -- (raw);
haftmann@30836
    38
  \draw [arrow] (raw) -- (pre);
haftmann@30836
    39
  \draw [arrow] (pre) -- (eqn);
haftmann@30836
    40
  \draw [arrow] (eqn) -- node (transl) [process, positive] {translation} (iml);
haftmann@30836
    41
  \draw [arrow] (iml) -- (seri);
haftmann@30836
    42
  \draw [arrow] (seri) -- (SML);
haftmann@30836
    43
  \draw [arrow] (seri) -- (OCaml);
haftmann@30836
    44
  \draw [arrow, dashed] (seri) -- (further);
haftmann@30836
    45
  \draw [arrow] (seri) -- (Haskell);
haftmann@30734
    46
\end{tikzpicture}
haftmann@30734
    47
haftmann@30754
    48
}
haftmann@30754
    49
haftmann@30734
    50
\end{document}