tutorial.tex

\documentclass[12pt]{article}

%\usepackage[top=4cm, bottom=4cm, left=4cm, right=4cm]{geometry}
%\usepackage{2in1}
%\usepackage{a4wide}
%\setlength{\columnsep}{1cm}

%\newcommand{\todo}[1]{{\bf \Huge !!!!! #1 !!!!!}}

\usepackage{booktabs}
\usepackage[usenames,dvipsnames]{xcolor}
\usepackage[textsize=footnotesize]{todonotes}
%\usepackage[british]{babel}
\usepackage[utf8]{inputenc}
\usepackage{url}
\usepackage{graphicx}
\usepackage{amssymb}
\usepackage{amsmath}
\usepackage{amsthm}
\usepackage{setspace}
\onehalfspacing
\usepackage{framed}
%\usepackage[usenames,dvipsnames]{color}
\usepackage[titles]{tocloft}
\setlength{\cftbeforesecskip}{0.1ex}
\renewcommand{\cftsecfont}{\rm}
\renewcommand{\cftsubsecfont}{\rm}
\renewcommand{\cftdot}{\ensuremath{\dots}}
\renewcommand{\cftsecdotsep}{3}
\renewcommand{\cftsubsecdotsep}{3}
\renewcommand{\cftsecpagefont}{\sl}
\renewcommand{\cftsubsecpagefont}{\sl}
\usepackage{sectsty}
\sectionfont{\large\it\centering}
\subsectionfont{\normalsize\it\centering}
\usepackage{listings}
%\usepackage{natbib}
\usepackage{fancyvrb}
\usepackage[margin=2cm]{geometry}
\usepackage[titletoc]{appendix}
\usepackage{bcprules}
\usepackage{tikz}
\usepackage{pgf}
\usetikzlibrary{arrows,automata}
\usepackage{tikz-cd}
\usetikzlibrary{positioning}
\usepackage{gensymb} % \degree symbol
% boxes around figs
\usepackage{float}
\floatstyle{boxed}
\restylefloat{figure}


\DefineVerbatimEnvironment{code}{Verbatim}{fontsize=\footnotesize}

% Copilot + formatting for listings
\lstdefinelanguage{Copilot} {
  language = Haskell,
  morekeywords = {arg, Bool, Double, Float, Int8, Int16, Int32, Int64,
                  Word8, Word16, Word32, Word64, Spec, Stream, String,
                  Proof, Universal, Existential,
                  true, false, label, Nothing, Just, arg, constant, drop,
                  trigger, observer, prop, theorem, interpret, reify, local,
                  extern, externB, externI8, externI16, externI32, externI64,
                  externW8, externW16, externW32, externW64, externF, externD,
                  externFun, externArray, externArrayB, externArrayI8,
                  externArrayI16, externArrayI32, externArrayI64, externArrayW8,
                  externArrayW16, externArrayW32, externArrayW64, externArrayF,
                  externArrayD, not, abs, signum, complement, recip, exp, sqrt,
                  log, sin, cos, tan, asin, acos, atan, sinh, cosh, tanh, asin,
                  acosh, atanh, cast, unsafeCast, mod, div, logBase, xor, mux},
  % formatting
  commentstyle = \color{ForestGreen}\it,
  keywordstyle = \color{blue}\bf,
  literate = {+}{{$+$}}1 {/}{{$/$}}1 {*}{{$*$}}1 {=}{{$=$}}1
             {>}{{$>$}}1 {<}{{$<$}}1 {\\}{{${\color{blue}\lambda}$}}1
             {\\\\}{{\char`\\\char`\\}}1
             {\ .}{{$\circ$}}2 {\ .\ }{{$\circ$}}2
             {>>}{{>>}}2 {>>=}{{>>=}}2
             {++}{{${\color{blue}++}$}}2
             {|}{{$\mid$}}1
             {==>}{{${\color{blue}==>}$}}3
}

% A custom version of Haskell for listings
\lstdefinelanguage{Haskell} {
  morekeywords = {as, case, of, class, data, data, family, data, instance,
                  default, deriving, do, forall, foreign, hiding, if, then, else, import,
                  infix, infixl, infixr, let, in, mdo, module, newtype, proc, qualified,
                  rec, type, where},
  morecomment=[l]{--},
  morecomment=[s]{{\{-}{-\}}},
  morestring=[b]",
  literate= {'c}{{$\gamma$}}1
  {'d}{{$\delta$}}1 {'e}{{$\eta$}}1
}

%\lstnewenvironment{code}
%    {\lstset{}%
%      \csname lst@SetFirstLabel\endcsname}
%   {\csname lst@SaveFirstLabel\endcsname}
%\lstnewenvironment{Haskell}
%{
%\lstset{
%    language=Haskell,
%    basicstyle=\small\ttfamily,
%    flexiblecolumns=false,
%    basewidth={0.5em,0.45em}
%}
%}
%{}


\definecolor{mygreen}{rgb}{0,0.6,0}
\definecolor{mygray}{rgb}{0.5,0.5,0.5}
\definecolor{mymauve}{rgb}{0.58,0,0.82}

% Global listings settings
\lstset{
  basewidth={0.5em,0.45em},         % spacing more like verbatim
  basicstyle=\footnotesize\ttfamily,% the size/face of the fonts that are used for the code
  backgroundcolor=\color{white},    % choose the background color; you must add \usepackage{color} or \usepackage{xcolor}
  breakatwhitespace=false,          % sets if automatic breaks should only happen at whitespace
  breaklines=true,                  % sets automatic line breaking
  captionpos=b,                     % sets the caption-position to bottom
  commentstyle=\color{mygreen},     % comment style
  %deletekeywords={ls,xor,conj,reset,gt,input},            % if you want to delete keywords from the given language
  escapeinside={\%*}{*)},           % if you want to add LaTeX within your code
  extendedchars=true,               % lets you use non-ASCII characters; for 8-bits encodings only, does not work with UTF-8
  frame=single,                     % adds a frame around the code
  keepspaces=true,                  % keeps spaces in text, useful for keeping indentation of code (possibly needs columns=flexible)
  keywordstyle=\color{blue},        % keyword style
  rulecolor=\color{black},          % if not set, the frame-color may be changed on line-breaks within not-black text (e.g. comments (green here))
  showspaces=false,                 % show spaces everywhere adding particular underscores; it overrides 'showstringspaces'
  showstringspaces=false,           % underline spaces within strings only
  showtabs=false,                   % show tabs within strings adding particular underscores
  stringstyle=\color{red},          % string literal style
  tabsize=2,                        % sets default tabsize to 2 spaces
}


\newtheoremstyle{example}{\topsep}{\topsep}
     {\normalsize\sl} % Body font.
     {}               % Indent amount (empty = no indent, \parindent = para indent).
     {\small\it}      % Thm head font.
     {:}              % Punctuation after thm head.
     {\newline}       % Space after thm head (\newline = linebreak).
     {\thmname{#1} \thmnumber{#2}\thmnote{#3}} % Thm head spec.
\theoremstyle{example}
\newtheorem{example}{Example}

\newcommand{\hlinepage}{\rule{\textwidth}{0.25pt}}
\newcommand{\HRule}{\rule{\linewidth}{0.25pt}}
\newcommand{\fixme}[1]{\emph{\color{Red}\{!~#1~!\}}}

\begin{document}

\thispagestyle{empty}

\begin{center}

The National Institute of Aerospace / Galois Inc. / NASA LaRC

\vspace{0.1cm}

\HRule

\vspace{0.6cm}

{\Huge \bfseries
An Introduction to Copilot
}\\
A tutorial to Copilot 3.0
\HRule

\vspace{1cm}

\begin{minipage}{0.3\textwidth}
\large
\begin{center}
Frank Dedden\\
\small{
dev@dedden.net\\
}
\end{center}
\end{minipage}
%
\begin{minipage}{0.3\textwidth}
\large
\begin{center}
Alwyn Goodloe\\
\small{
a.goodloe@nasa.gov\\
}
\end{center}
\end{minipage}

\vspace{1cm}

\begin{minipage}{0.3\textwidth}
\large
\begin{center}
Ivan Perez\\
\small{
ivan.perezdominguez@nasa.gov\\
}
\end{center}
\end{minipage}
%
\begin{minipage}{0.3\textwidth}
\large
\begin{center}
Will Pogge\\
\small{
will.d.pogge@ama-inc.com\\
}
\end{center}
\end{minipage}

\vspace{1cm}

\begin{minipage}{0.3\textwidth}
\large
\begin{center}
Macallan Cruff\\
\end{center}
\end{minipage}
%
\begin{minipage}{0.3\textwidth}
\large
\begin{center}
Nis N. Wegmann\\
\end{center}
\end{minipage}

\vspace{1cm}

\begin{minipage}{0.3\textwidth}
\large
\begin{center}
Lee Pike\\
\end{center}
\end{minipage}
%
\begin{minipage}{0.3\textwidth}
\large
\begin{center}
Chris Hathhorn \\
\end{center}
\end{minipage}

\vspace{1cm}

\begin{minipage}{0.3\textwidth}
\large
\begin{center}
Sebastian Niller\\
\end{center}
\end{minipage}
%
\begin{minipage}{0.3\textwidth}
\large
\begin{center}
Lauren Pick\\
\end{center}
\end{minipage}

\vspace{1cm}

\begin{minipage}{0.3\textwidth}
\large
\begin{center}
Georges-Axel Jaloyan \\
\end{center}
\end{minipage}

\vspace{1cm}

{\large
Hampton, Virginia, United States, \today
}

%\begin{tabular}{cc}
%\hspace{0.5cm}\includegraphics[width=0.18\textwidth]{figures/nia}\hspace{0.5cm}  &
%\hspace{0.5cm}\includegraphics[width=0.2\textwidth]{figures/galois}\hspace{0.5cm} &
%\hspace{0.5cm}\includegraphics[width=0.2\textwidth]{figures/nasa}\hspace{0.5cm} \\
%\textsc{\large NIA} &
%\textsc{\large Galois Inc.} &
%\textsc{\large NASA LaRC} \\
%\end{tabular}

\let\thefootnote\relax\footnotetext{
This research is supported by NASA Contract NNL08AD13T, 80LARC17C0004 and
NNL09AA00A.
}

\end{center}

\vspace{0.25cm}

\section*{Abstract}

{
\small
This document contains a tutorial on Copilot and its accompanying tools.
We do not attempt to give a complete, formal description of Copilot
(references are provided in the bibliography), rather we aim at
demonstrating the fundamental concepts of the language by using idiomatic
expositions and examples.
}

{
\small
\setcounter{tocdepth}{2}
\tableofcontents
}

\newpage
\addcontentsline{toc}{section}{Acknowledgement}
\section*{Acknowledgement}

The authors are grateful for NASA Contract NNL08AD13T to Galois Inc. and the
National Institute of Aerospace, which partially supported this work.
Thanks to Lars Kuhtz, Benedetto Di~Vito,  Robin Morisset, Kaveh
Darafsheh.

{


\input{introduction}
\input{Interpret}
\input{Language}
\input{example}
\addcontentsline{toc}{section}{References}
\bibliographystyle{alpha}
\bibliography{mybib}
}

\end{document}