Adding first draft of subtyping rules

Summary:
This is a first draft at documenting the main component of the subtyping rule:
`less_or_equal`. We still need `join` and `meet` to have a realistic package.

The style is to write down the rules in the same order as the code. At some
point we might want to change to a style with only "positive rules" (e.g. don't
write anything about Top <= T, because if there is no rule to build it, we
can't prove it). That might evolve in the future

Reviewed By: dkgi

Differential Revision: D16120038

fbshipit-source-id: ddc1ee5df934771e1d3185bf98f3cae04e4f292d

Author: Vincent Siles

docs/formal/.gitignore

@@ -0,0 +1,4 @@
+*.aux
+*.log
+*.pdf
+*.out

docs/formal/DejaVuSansMono.sty

@@ -0,0 +1,38 @@
+\ProvidesPackage{DejaVuSansMono} [2011/06/01 Style file for DejaVuSansMono.]
+%%
+%% Options:
+%%  [scaled]       --> Scale = 0.95
+%%  [scaled=0.9]   --> Scale = 0.90
+%%
+\RequirePackage{keyval}
+\define@key{DejaVuSansMono}{scaled}[0.95]{%
+  \def\DejaVuSansMono@scale{#1}}
+\def\ProcessOptionsWithKV#1{%
+  \let\@tempc\relax
+  \let\DejaVuSansMono@tempa\@empty
+  \@for\CurrentOption:=\@classoptionslist\do{%
+    \@ifundefined{KV@#1@\CurrentOption}%
+    {}%
+    {%
+      \edef\DejaVuSansMono@tempa{\DejaVuSansMono@tempa,\CurrentOption,}%
+      \@expandtwoargs\@removeelement\CurrentOption
+        \@unusedoptionlist\@unusedoptionlist
+    }%
+  }%
+  \edef\DejaVuSansMono@tempa{%
+    \noexpand\setkeys{#1}{%
+      \DejaVuSansMono@tempa\@ptionlist{\@currname.\@currext}%
+    }%
+  }%
+  \DejaVuSansMono@tempa
+  \let\CurrentOption\@empty
+}
+\ProcessOptionsWithKV{DejaVuSansMono}
+\AtEndOfPackage{%
+  \let\@unprocessedoptions\relax
+}
+    
+
+\renewcommand{\ttdefault}{DejaVuSansMono-TLF}
+
+\endinput

docs/formal/Makefile

@@ -0,0 +1,15 @@
+DOC=pyre_sub
+
+all: $(DOC).pdf
+
+$(DOC).pdf: $(DOC).tex
+	rubber -d $^
+
+watch:
+	sh -c "mupdf-gl $(DOC).pdf 2>/dev/null >&2 & jobs -p %1 > .mupdf.pid"
+	fswatch $(DOC).tex | xargs -n1 sh -c 'make && echo "Refreshing..." &&  kill -n 1 `cat .mupdf.pid`'
+
+clean:
+	rm -f *.aux *.dvi *.log
+
+.PHONY: watch clean

docs/formal/lstocaml.sty

@@ -0,0 +1,60 @@
+%%
+% Copyright (c) 2018-present, Facebook, Inc.
+%
+% This source code is licensed under the MIT license found in the
+% LICENSE file in the root directory of this source tree.
+%%
+
+\usepackage{xcolor}
+\definecolor{butter}{HTML}{C4A000}
+\definecolor{orange}{HTML}{CE5C00}
+\definecolor{chocolate}{HTML}{8F5902}
+\definecolor{chameleon}{HTML}{4E9A06}
+\definecolor{skyblue}{HTML}{204A87}
+\definecolor{plum}{HTML}{5C3566}
+\definecolor{scarletred}{HTML}{A40000}
+\definecolor{lightalu}{HTML}{BABDB6}
+\definecolor{darkalu}{HTML}{2E3436}
+
+\newcommand{\kwstyle}{}
+
+\usepackage{listings}
+
+\lstset{
+  basicstyle=\footnotesize\ttfamily,
+  breaklines=true,
+  aboveskip=10pt,
+  belowskip=5pt,
+  xleftmargin=10pt,
+  commentstyle=\color{orange},
+  keywordstyle=\kwstyle,
+  language=Caml,
+  stringstyle=\color{plum},
+  tabsize=2,
+  numberstyle=\tiny\color{gray},
+  escapeinside={(*@}{*)},
+  numbers=left,
+  numbersep=2pt,
+  keywordstyle=[1]\kwstyle\color{chameleon},
+  keywordstyle=[2]\kwstyle\color{scarletred},
+  keywordstyle=[3]\kwstyle\color{skyblue},
+  keywordstyle=[4]\kwstyle\color{butter},
+  keywordstyle=[5]\kwstyle\color{skyblue},
+  keywordstyle=[6]\kwstyle\color{skyblue},
+  keywordstyle=[7]\kwstyle\color{chameleon},
+  keywordstyle=[8]\kwstyle\color{butter},
+  keywordstyle=[9]\kwstyle\color{butter},
+  keywords=[1]{let,val,method,in,and,rec,private,virtual,constraint},
+  keywords=[2]{type,open,class,module,exception,external},
+  keywords=[3]{fun,function,functor,match,try,with},
+  keywords=[4]{as,when,of},
+  keywords=[5]{if,then,else},
+  keywords=[6]{begin,end,object,struct,sig,for,while,do,done,to,downto},
+  keywords=[7]{true,false},
+  keywords=[8]{include,inherit,initializer},
+  keywords=[9]{new,ref,mutable,lazy,assert,raise},
+}
+
+\lstset{literate=
+  {`}{{{\lq}}}1
+}