plumbing to make a pdf version of MIPS Sail spec, using LaTeX lstlistings

3 files changed, 186 insertions, 0 deletions

diff --git a/mips/doc/Makefile b/mips/doc/Makefile
new file mode 100644
index 00000000..0220a4cc
--- /dev/null
+++ b/mips/doc/Makefile
@@ -0,0 +1,7 @@
+all:
+	cat preamble.tex ../mips_prelude.sail ../mips_wrappers.sail ../mips_insts.sail ../mips_epilogue.sail postamble.tex > mips_all.tex
+	pdflatex mips_all.tex
+
+clean:
+	rm -rf *~
+	rm -rf mips_all.*
diff --git a/mips/doc/postamble.tex b/mips/doc/postamble.tex
new file mode 100644
index 00000000..892ef896
--- /dev/null
+++ b/mips/doc/postamble.tex
@@ -0,0 +1,2 @@
+\end{lstlisting}
+\end{document}
diff --git a/mips/doc/preamble.tex b/mips/doc/preamble.tex
new file mode 100644
index 00000000..524ec736
--- /dev/null
+++ b/mips/doc/preamble.tex
@@ -0,0 +1,177 @@
+
+\documentclass[10pt]{article}
+
+\usepackage[margin=1.0in]{geometry}
+\usepackage[T1]{fontenc}
+\usepackage[scaled=0.82]{beramono}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% for Lem listing
+\usepackage[scaled=0.82]{beramono}
+\usepackage{listings}
+
+\newsavebox{\codebox}
+
+\lstdefinelanguage{SailExtraKeywords}
+ {morekeywords= {
+% from the sail lexer
+and,          
+alias,        
+as,           
+bitzero,      
+bitone,       
+bits,         
+by,           
+case,	       
+clause,       
+const,	       
+dec,          
+default,      
+deinfix,      
+effect,       
+Effect,       
+end,          
+enumerate,    
+else,         
+exit,         
+extern,       
+false,        
+forall,       
+foreach,      
+function,     
+if,           
+in,	       
+inc,          
+IN,           
+let,          
+member,       
+Nat,          
+Order,        
+pure,         
+rec,	       
+register,     
+scattered,    
+struct,       
+switch,       
+then,         
+true,         
+Type,         
+typedef,      
+undefined,    
+union,	       
+with,         
+val,          
+div,	       
+mod,	       
+quot,	       
+rem,	       
+barr,         
+rreg,         
+wreg,         
+rmem,         
+wmem,         
+undef,        
+unspec,       
+nondet,       
+bool,unit,vector,range,list,bit,nat, int, uint8,uint16,uint32,uint64,implicit
+}
+}
+
+\lstdefinelanguage{LemExtraKeywords}
+ {morekeywords= {
+% from the lem lexer
+      as,                  
+      fun,                 
+      function,            
+      with,                
+      match,               
+      let,                 
+      and,                 
+      in,                  
+      of,                  
+      rec,                 
+      type,                
+      module,              
+      rename,              
+      struct,              
+      end,                 
+      open,                
+      import,              
+      include,             
+      true,                
+      false,               
+      begin,               
+      if,                  
+      then,                
+      else,                
+      val,                 
+      class,               
+      instance,            
+      default_instance,    
+      indreln,             
+      forall,              
+      exists,              
+      inline,              
+      lem_transform,       
+      IN,                  
+      MEM,                 
+      declare,             
+      infix,               
+      field,              
+      automatic,          
+      manual,             
+      exhaustive,         
+      inexhaustive,       
+      ascii_rep,          
+      compile_message,    
+      set_flag,           
+      termination_argument,
+      pattern_match,      
+      right_assoc,        
+      left_assoc,         
+      non_assoc,          
+      special,            
+      target_rep,         
+      target_type,         
+      target_const,        
+      lemma,               
+      assert,              
+      theorem,             
+      do,                  
+      witness,	     
+      check,
+      % coq notation
+      Inductive,
+      Prop,
+% names of targets,
+  ocaml,
+  html,
+  coq,
+  hol,
+  isabelle,
+% these seem to be used as keywors in indreln?
+  input,
+  output,
+% and more keywords for specific target code that we quote
+  case,
+  definition,
+}
+}
+
+%\lstset{basicstyle=\footnotesize\ttfamily} %
+%\lstset{keywordstyle=\pmb}
+%\lstset{basicstyle=\footnotesize\ttfamily} %
+\lstset{basicstyle=\ttfamily} %
+\lstset{keywordstyle=\bfseries}
+\lstset{language=Caml}
+\lstset{defaultdialect=[Objective]Caml}
+\lstset{alsolanguage=SailExtraKeywords}
+\lstset{mathescape}
+
+\lstset{escapeinside={<@}{@>}}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\begin{document}
+
+\begin{lstlisting}