3 files changed, 88 insertions, 1 deletions
diff --git a/lib/arith.sail b/lib/arith.sail
new file mode 100644
index 00000000..f43f2791
--- /dev/null
+++ b/lib/arith.sail
@@ -0,0 +1,49 @@
+$ifndef _ARITH
+$define _ARITH
+
+$include <flow.sail>
+
+// ***** Addition *****
+
+val add_atom = {ocaml: "add_int", lem: "integerAdd"} : forall 'n 'm.
+  (atom('n), atom('m)) -> atom('n + 'm)
+
+val add_int = {ocaml: "add_int", lem: "integerAdd", c: "add_int"} : (int, int) -> int
+
+overload operator + = {add_atom, add_int}
+
+// ***** Subtraction *****
+
+val sub_atom = {ocaml: "sub_int", lem: "integerMinus", c: "sub_int"} : forall 'n 'm.
+  (atom('n), atom('m)) -> atom('n - 'm)
+
+val sub_int = {ocaml: "sub_int", lem: "integerMinus", c: "sub_int"} : (int, int) -> int
+
+overload operator - = {sub_atom, sub_int}
+
+// ***** Negation *****
+
+val negate_atom = {ocaml: "negate", lem: "integerNegate", c: "neg_int"} : forall 'n. atom('n) -> atom(- 'n)
+
+val negate_int = {ocaml: "negate", lem: "integerNegate", c: "neg_int"} : int -> int
+
+overload negate = {negate_atom, negate_int}
+
+// ***** Multiplication *****
+
+val mult_atom = {ocaml: "mult", lem: "integerMult", c: "mult_int"} : forall 'n 'm.
+  (atom('n), atom('m)) -> atom('n * 'm)
+
+val mult_int = {ocaml: "mult", lem: "integerMult", c: "mult_int"} : (int, int) -> int
+
+overload operator * = {mult_atom, mult_int}
+
+val "print_int" : (string, int) -> unit
+
+// ***** Integer shifts *****
+
+val shl_int = "shl_int" : (int, int) -> int
+
+val shr_int = "shr_int" : (int, int) -> int
+
+$endif
diff --git a/lib/flow.sail b/lib/flow.sail
index 9e4c98c1..94019b0a 100644
--- a/lib/flow.sail
+++ b/lib/flow.sail
@@ -27,13 +27,14 @@ val gteq_atom_range = "gteq" : forall 'n 'm 'o. (atom('n), range('m, 'o)) -> boo
 
 val eq_range = {ocaml: "eq_int", lem: "eq", c: "eq_int"} : forall 'n 'm 'o 'p. (range('n, 'm), range('o, 'p)) -> bool
 val eq_int = {ocaml: "eq_int", lem: "eq", c: "eq_int"} : (int, int) -> bool
+val eq_bool = {ocaml: "eq_bool", lem: "eq", c: "eq_bool"} : (bool, bool) -> bool
 
 val lteq_int = "lteq" : (int, int) -> bool
 val gteq_int = "gteq" : (int, int) -> bool
 val lt_int = "lt" : (int, int) -> bool
 val gt_int = "gt" : (int, int) -> bool
 
-overload operator == = {eq_atom, eq_range, eq_int}
+overload operator == = {eq_atom, eq_range, eq_int, eq_bool}
 overload operator | = {or_bool}
 overload operator & = {and_bool}
 
diff --git a/lib/sail.tex b/lib/sail.tex
new file mode 100644
index 00000000..a1ae86c0
--- /dev/null
+++ b/lib/sail.tex
@@ -0,0 +1,37 @@
+\documentclass{report}
+
+\usepackage[svgnames]{xcolor}
+\usepackage{fullpage}
+\usepackage{listings}
+\usepackage[hidelinks]{hyperref}
+
+\lstset{
+  basicstyle=\ttfamily\small,
+  columns=fullflexible,
+  breaklines=true,
+  postbreak=\mbox{\textcolor{red}{$\hookrightarrow$}\space},
+}
+
+\lstdefinelanguage{sail}
+  { morekeywords={val,function,cast,type,forall,overload,operator,enum,union,undefined,exit,and,assert,sizeof
+      scattered,register,inc,dec,if,then,else,effect,let,as,@,in,end,Type,Int,Order,match,clause,struct},
+    keywordstyle={\bf\ttfamily\color{blue}},
+    morestring=[b]",
+    stringstyle={\ttfamily\color{red}},
+    morecomment=[l][\itshape\color{DarkGreen}]{//},
+    morecomment=[s][\itshape\color{DarkGreen}]{/*}{*/},
+    deletestring=[bd]{'},
+    escapechar=\#,
+    emphstyle={\it},
+    literate=
+      {\{|}{{$\{|$}}1
+      {|\}}{{$|\}$}}1
+  }
+
+\lstset{language=sail}
+
+\begin{document}
+
+\include{out}
+
+\end{document}