components/tactics/doc/main.tex

   1 \documentclass[a4paper]{article}
   2
   3 \usepackage{a4wide}
   4 \usepackage{pifont}
   5 \usepackage{semantic}
   6 \usepackage{stmaryrd}
   7 \usepackage{graphicx}
   8
   9 \newcommand{\MATITA}{\ding{46}\textsf{\textbf{Matita}}}
  10
  11 \title{Continuationals semantics for \MATITA}
  12 \author{Claudio Sacerdoti Coen \quad Enrico Tassi \quad Stefano Zacchiroli \\
  13 \small Department of Computer Science, University of Bologna \\
  14 \small Mura Anteo Zamboni, 7 -- 40127 Bologna, ITALY \\
  15 \small \{\texttt{sacerdot}, \texttt{tassi}, \texttt{zacchiro}\}\texttt{@cs.unibo.it}}
  16
  17 \newcommand{\MATHIT}[1]{\ensuremath{\mathit{#1}}}
  18 \newcommand{\MATHTT}[1]{\ensuremath{\mathtt{#1}}}
  19
  20 \newcommand{\DOT}{\ensuremath{\mbox{\textbf{.}}}}
  21 \newcommand{\SEMICOLON}{\ensuremath{\mbox{\textbf{;}}}}
  22 \newcommand{\BRANCH}{\ensuremath{\mbox{\textbf{[}}}}
  23 \newcommand{\SHIFT}{\ensuremath{\mbox{\textbf{\textbar}}}}
  24 \newcommand{\POS}[1]{\ensuremath{#1\mbox{\textbf{:}}}}
  25 \newcommand{\MERGE}{\ensuremath{\mbox{\textbf{]}}}}
  26 \newcommand{\FOCUS}[1]{\ensuremath{\mathtt{focus}~#1}}
  27 \newcommand{\UNFOCUS}{\ensuremath{\mathtt{unfocus}}}
  28 \newcommand{\SKIP}{\MATHTT{skip}}
  29 \newcommand{\TACTIC}[1]{\ensuremath{\mathtt{tactic}~#1}}
  30
  31 \newcommand{\APPLY}[1]{\ensuremath{\mathtt{apply}~\mathit{#1}}}
  32
  33 \newcommand{\GOAL}{\MATHIT{goal}}
  34 \newcommand{\SWITCH}{\MATHIT{switch}}
  35 \newcommand{\LIST}{\MATHTT{list}}
  36 \newcommand{\INT}{\MATHTT{int}}
  37 \newcommand{\OPEN}{\MATHTT{Open}}
  38 \newcommand{\CLOSED}{\MATHTT{Closed}}
  39
  40 \newcommand{\SEMOP}[1]{|[#1|]}
  41 \newcommand{\TSEMOP}[1]{{}_t|[#1|]}
  42 \newcommand{\SEM}[3][\xi]{\SEMOP{#2}_{{#1},{#3}}}
  43 \newcommand{\ENTRY}[4]{\langle#1,#2,#3,#4\rangle}
  44 \newcommand{\TSEM}[3]{\TSEMOP{#1}_{#2,#3}}
  45
  46 \newcommand{\GIN}[1][1]{\ensuremath{[l_{#1};\cdots;l_n]}}
  47
  48 \newcommand{\ZEROPOS}{\MATHIT{zero\_pos}}
  49 \newcommand{\INITPOS}{\MATHIT{init\_pos}}
  50 \newcommand{\ISFRESH}{\MATHIT{is\_fresh}}
  51 \newcommand{\FILTER}{\MATHIT{filter}}
  52 \newcommand{\FILTEROPEN}{\MATHIT{filter\_open}}
  53 \newcommand{\ISOPEN}{\MATHIT{is\_open}}
  54 \newcommand{\DEEPCLOSE}{\MATHIT{deep\_close}}
  55 \newcommand{\REMOVEGOALS}{\MATHIT{remove\_goals}}
  56 \newcommand{\GOALS}{\MATHIT{open\_goals}}
  57
  58 \newcommand{\BRANCHTAG}{\ensuremath{\mathtt{B}}}
  59 \newcommand{\FOCUSTAG}{\ensuremath{\mathtt{F}}}
  60
  61 \newlength{\sidecondlen}
  62 \setlength{\sidecondlen}{2cm}
  63
  64 \begin{document}
  65 \maketitle
  66
  67 \input{body.tex}
  68
  69 \end{document}
  70