Initial set of files.

2 files changed, 213 insertions, 0 deletions

diff --git a/Util/Emacs/dafny-mode.el b/Util/Emacs/dafny-mode.el
new file mode 100644
index 00000000..508ffbaf
--- /dev/null
+++ b/Util/Emacs/dafny-mode.el
@@ -0,0 +1,112 @@
+;; dafny-mode.el - GNU Emacs mode for Dafny

+;; Adapted by Rustan Leino from Jean-Christophe FILLIATRE's GNU Emancs mode for Why

+

+(defvar dafny-mode-hook nil)

+

+(defvar dafny-mode-map nil

+  "Keymap for Dafny major mode")

+

+(if dafny-mode-map nil

+  (setq dafny-mode-map (make-keymap))

+  (define-key dafny-mode-map "\C-c\C-c" 'dafny-run-boogie)

+  (define-key dafny-mode-map [(control return)] 'font-lock-fontify-buffer))

+

+(setq auto-mode-alist

+      (append

+       '(("\\.dfy" . dafny-mode))

+       auto-mode-alist))

+

+;; font-lock

+

+(defun dafny-regexp-opt (l)

+  (concat "\\<" (concat (regexp-opt l t) "\\>")))

+

+(defconst dafny-font-lock-keywords-1

+  (list

+   ; comments have the form /* ... */

+   '("/\\*\\([^*]\\|\\*[^/]\\)*\\*/" . font-lock-comment-face)

+   ; or // ...

+   '("//\\([^

+]\\)*" . font-lock-comment-face)

+

+   `(,(dafny-regexp-opt '(

+        "class" "function" "frame" "var" "method"

+        "returns" "requires" "ensures" "modifies" "reads" "free"

+        "invariant" "decreases"

+        )) . font-lock-builtin-face)

+   `(,(dafny-regexp-opt '(

+        "assert" "assume" "break" "call" "else" "havoc" "if" "label" "return" "while"

+        "old" "forall" "exists" "new" "foreach" "in" "this" "fresh" "use"

+        "false" "true" "null")) . font-lock-keyword-face)

+   `(,(dafny-regexp-opt '("bool" "int" "object" "set" "seq")) . font-lock-type-face)

+   )

+  "Minimal highlighting for Dafny mode")

+

+(defvar dafny-font-lock-keywords dafny-font-lock-keywords-1

+  "Default highlighting for Dafny mode")

+

+;; syntax

+

+(defvar dafny-mode-syntax-table nil

+  "Syntax table for dafny-mode")

+

+(defun dafny-create-syntax-table ()

+  (if dafny-mode-syntax-table

+      ()

+    (setq dafny-mode-syntax-table (make-syntax-table))

+    (set-syntax-table dafny-mode-syntax-table)

+    (modify-syntax-entry ?' "w" dafny-mode-syntax-table)

+    (modify-syntax-entry ?_ "w" dafny-mode-syntax-table)))

+

+;; menu

+

+(require 'easymenu)

+

+(defun dafny-menu ()

+  (easy-menu-define

+   dafny-mode-menu (list dafny-mode-map)

+   "Dafny Mode Menu." 

+   '("Dafny"

+     ["Run Boogie" dafny-run-boogie t]

+     "---"

+     ["Recolor buffer" font-lock-fontify-buffer t]

+     "---"

+     ))

+  (easy-menu-add dafny-mode-menu))

+

+;; commands

+

+(defun dafny-command-line (file)

+  (concat "boogie " file))

+

+(defun dafny-run-boogie ()

+  "run Boogie to check the Dafny program"

+  (interactive)

+  (let ((f (buffer-name)))

+    (compile (dafny-command-line f))))

+

+;; setting the mode

+

+(defun dafny-mode ()

+  "Major mode for editing Dafny programs.

+

+\\{dafny-mode-map}"

+  (interactive)

+  (kill-all-local-variables)

+  (dafny-create-syntax-table)

+  ; hilight

+  (make-local-variable 'font-lock-defaults)

+  (setq font-lock-defaults '(dafny-font-lock-keywords))

+  ; indentation

+  ; (make-local-variable 'indent-line-function)

+  ; (setq indent-line-function 'dafny-indent-line)

+  ; menu

+  ; providing the mode

+  (setq major-mode 'dafny-mode)

+  (setq mode-name "Dafny")

+  (use-local-map dafny-mode-map)

+  (font-lock-mode 1)

+  (dafny-menu)

+  (run-hooks 'dafny-mode-hook))

+

+(provide 'dafny-mode)

diff --git a/Util/latex/dafny.sty b/Util/latex/dafny.sty
new file mode 100644
index 00000000..9f7a76b3
--- /dev/null
+++ b/Util/latex/dafny.sty
@@ -0,0 +1,101 @@
+% dafny.sty

+% Dafny mode for the LaTeX listings package.

+% Rustan Leino, 22 June 2008.

+

+\usepackage{listings}

+

+\lstdefinelanguage{dafny}{

+  morekeywords={class,bool,int,object,set,seq,%

+      function,returns,

+      var,

+      method,in,

+      requires,modifies,ensures,reads,free,

+      % expressions

+      false,true,null,old,fresh,this,

+      % statements

+      assert,assume,new,havoc,call,if,else,while,invariant,break,return,foreach,

+      },

+  literate=%

+    {:}{$\colon$}1

+    {::}{$\bullet$}2

+    {:=}{$:$$=$}2

+    {!}{$\lnot$}1

+    {!!}{$\nparallel$}1

+    {==}{$=$}1

+    {!=}{$\neq$}1

+    {&&}{$\land$}1

+    {||}{$\lor$}1

+    {<=}{$\le$}1

+    {=>}{$\ge$}1

+    {<=set}{$\subseteq$}1

+    {+set}{$\cup$}1

+    {==>}{$\Longrightarrow$}3 

+    {<==>}{$\Longleftrightarrow$}4 

+    {forall}{$\forall$}1

+    {exists}{$\exists$}1

+    {\\in}{$\in$}1

+    % the following isn't actually Dafny, but it gives the option to produce nicer latex

+    {<<}{$\langle$}1

+    {>>}{$\rangle$}1

+    {\\alpha}{$\alpha$}1

+    {\\beta}{$\beta$}1

+    {\\gamma}{$\gamma$}1

+    {\\delta}{$\delta$}1

+    {\\epsilon}{$\epsilon$}1

+    {\\zeta}{$\zeta$}1

+    {\\eta}{$\eta$}1

+    {\\theta}{$\theta$}1

+    {\\iota}{$\iota$}1

+    {\\kappa}{$\kappa$}1

+    {\\lambda}{$\lambda$}1

+    {\\mu}{$\mu$}1

+    {\\nu}{$\nu$}1

+    {\\xi}{$\xi$}1

+    {\\pi}{$\pi$}1

+    {\\rho}{$\rho$}1

+    {\\sigma}{$\sigma$}1

+    {\\tau}{$\tau$}1

+    {\\upsilon}{$\upsilon$}1

+    {\\phi}{$\phi$}1

+    {\\chi}{$\chi$}1

+    {\\psi}{$\psi$}1

+    {\\omega}{$\omega$}1

+    {\\Gamma}{$\Gamma$}1

+    {\\Delta}{$\Delta$}1

+    {\\Theta}{$\Theta$}1

+    {\\Lambda}{$\Lambda$}1

+    {\\Xi}{$\Xi$}1

+    {\\Pi}{$\Pi$}1

+    {\\Sigma}{$\Sigma$}1

+    {\\Upsilon}{$\Upsilon$}1

+    {\\Phi}{$\Phi$}1

+    {\\Psi}{$\Psi$}1

+    {\\Omega}{$\Omega$}1

+    ,

+  sensitive=true,  % case sensitive

+  morecomment=[l]{//},

+  morecomment=[s]{/*}{*/},

+  morestring=[b]",

+  numbers=none,

+  firstnumber=0,

+  numberstyle=\tiny,

+  stepnumber=5,

+  basicstyle=\scriptsize\sffamily,

+  commentstyle=\itshape,

+  keywordstyle=\bfseries,

+  ndkeywordstyle=\bfseries,

+}

+\lstnewenvironment{dafny}[1][]{%

+  \lstset{language=dafny,

+    floatplacement={tbp},captionpos=b,

+    frame=lines,xleftmargin=8pt,xrightmargin=8pt,basicstyle=\ttfamily,#1}}{}

+\lstnewenvironment{dafnyNoLines}[1][]{%

+  \lstset{language=dafny,

+    floatplacement={tbp},captionpos=b,

+    xleftmargin=8pt,xrightmargin=8pt,basicstyle=\ttfamily,#1}}{}

+\def\inlinedafny{%

+    \lstinline[language=dafny,basicstyle=\ttfamily,columns=fixed]}

+\newcommand{\lstfile}[1]{

+  \lstinputlisting[language=dafny,%

+    frame=lines,xleftmargin=8pt,xrightmargin=8pt,basicstyle=\ttfamily,columns=fixed]{#1}

+}