diff options
| author | Thomas Bauereiss | 2019-01-29 16:55:26 +0000 |
|---|---|---|
| committer | Thomas Bauereiss | 2019-01-29 16:58:47 +0000 |
| commit | 06b4141e3a06aaf74449d062d85cffb68f566b6b (patch) | |
| tree | 97cd44c6a17bb7d5bd205be6f2565941cbef9ba8 | |
| parent | 1f2c21b684be664e8ffffda2fd3c8d34edaba807 (diff) | |
| parent | 60164a9a221ed6566f1067100dbea2ec828b47d2 (diff) | |
Merge branch 'sail2' into asl_flow2
38 files changed, 595 insertions, 2319 deletions
@@ -3,7 +3,7 @@ Installing Sail on Ubuntu and macOS This note lists the commands needed to get Sail and all dependencies working on a new Ubuntu install or macOS. We have recently (2018-02-17) tested these -on Xubuntu 16.04 LTS in a virtual machine and on macOS Sierre 10.12.6, so they should +on Xubuntu 16.04 LTS in a virtual machine and on macOS Sierra 10.12.6, so they should work. Hopefully this will be useful as a reference. Basics @@ -21,6 +21,8 @@ install: mkdir -p $(INSTALL_DIR)/bin cp src/isail.native $(INSTALL_DIR)/bin/sail mkdir -p $(SHARE_DIR) + make -C lib/isabelle all + make -C lib/hol all-scripts cp -r lib $(SHARE_DIR) mkdir -p $(SHARE_DIR)/src cp src/elf_loader.ml $(SHARE_DIR)/src @@ -44,9 +46,6 @@ archs: $(MAKE) -C "$$arch" || exit;\ done -isabelle-lib: - $(MAKE) -C isabelle-lib - apply_header: $(MAKE) clean headache -c etc/headache_config -h etc/mips_header `ls mips/*.sail` @@ -77,4 +76,4 @@ clean: for subdir in src arm ; do\ $(MAKE) -C "$$subdir" clean;\ done - -rm sail + rm -f sail @@ -82,10 +82,9 @@ with all the required dependencies. Emacs Mode ========== -[editors/sail2-mode.el](editors/sail2-mode.el) contains an Emacs mode +[editors/sail-mode.el](editors/sail-mode.el) contains an Emacs mode for the most recent version of Sail which provides some basic syntax -highlighting. [editors/sail-mode.el](editors/sail-mode.el) contains an -emacs mode for previous versions of the language. +highlighting. Licensing ========= @@ -109,4 +108,4 @@ the headers of those files. The POWER model in power/ is distributed under the 2-clause BSD licence in the headers of those files. -The models in separate repositories are licensed as described in each.
\ No newline at end of file +The models in separate repositories are licensed as described in each. diff --git a/doc/Makefile b/doc/Makefile index ae542571..981463ca 100644 --- a/doc/Makefile +++ b/doc/Makefile @@ -52,14 +52,18 @@ ifeq ($(shell which sail),) $(error Cannot find sail executable, make sure it is in PATH) endif +SAIL_RISCV=../../sail-riscv + +all: manual.pdf + .PHONY: clean -code_riscv.tex: ../riscv/prelude.sail ../riscv/riscv_duopod.sail - sail -o code_riscv -latex ../riscv/prelude.sail ../riscv/riscv_duopod.sail +code_riscv.tex: ${SAIL_RISCV}/model/prelude.sail ${SAIL_RISCV}/model/riscv_duopod.sail + sail -o code_riscv -latex -latex_full_valspecs ${SAIL_RISCV}/model/prelude.sail ${SAIL_RISCV}/model/riscv_duopod.sail cp code_riscv/commands.tex code_riscv.tex code_myreplicatebits.tex: examples/my_replicate_bits.sail - sail -o code_myreplicatebits -latex -latex_prefix mrb examples/my_replicate_bits.sail + sail -o code_myreplicatebits -latex -latex_full_valspecs -latex_prefix mrb examples/my_replicate_bits.sail cp code_myreplicatebits/commands.tex code_myreplicatebits.tex grammar.tex: ../language/sail.ott diff --git a/doc/manual.tex b/doc/manual.tex index d731ecd3..1cab3afa 100644 --- a/doc/manual.tex +++ b/doc/manual.tex @@ -1,5 +1,6 @@ \documentclass[a4paper]{article} +\usepackage{etoolbox} \usepackage[nounderscore]{syntax} \usepackage{amsmath,amssymb} \usepackage[svgnames]{xcolor} @@ -25,7 +26,7 @@ \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, - foreach,from,to,by,infix,infixl,infixr,bitfield,default,try,catch,throw}, + foreach,from,to,by,infix,infixl,infixr,bitfield,default,try,catch,throw,constraint}, keywordstyle={\bf\ttfamily\color{blue}}, morestring=[b]", stringstyle={\ttfamily\color{red}}, @@ -44,6 +45,22 @@ \def\sail{\trivlist \item\relax} \def\endsail{\endtrivlist} +\newcommand{\saildocval}[2]{ +#1 #2 +} +\newcommand{\saildocfcl}[2]{ +#1 #2 +} +\newcommand{\saildoctype}[2]{ +#1 #2 +} +\newcommand{\saildocfn}[2]{ +#1 #2 +} +\newcommand{\saildocoverload}[2]{ +#1 #2 +} + \renewcommand{\ll}[1]{\lstinline{#1}} \newcommand{\riscv}{RISC-V} diff --git a/doc/riscv.tex b/doc/riscv.tex index 299a7bdd..586efdf4 100644 --- a/doc/riscv.tex +++ b/doc/riscv.tex @@ -25,11 +25,11 @@ that the constraint on the \ll{regno} type synonym is satisfied, we return an existentially quantified type \ll{\{'n, 0 <= 'n < 32. regno('n)\}}. -\sailxlent -\sailregno -\sailregbits -\sailregbitstoregno -\sailfnregbitstoregno +\sailtype{xlen_t} +\sailtype{regno} +\sailtype{regbits} +\sailval{regbits_to_regno} +\sailfn{regbits_to_regno} We now set up some basic architectural state. First creating a register of type \ll{xlen_t} for both the program counter \ll{PC}, and @@ -54,13 +54,14 @@ register nextPC : xlen_t register Xs : vector(32, dec, xlen_t) \end{lstlisting} -\sailrX -\sailfnrX -\sailfnrXA +\sailval{rX} +% TODO: Fix funcl commands +\sailfclrX +\sailfclMMMrX -\sailwX -\sailfnwX -\sailX +\sailval{wX} +\sailfn{wX} +\sailoverloadHHX We also give a function \ll{MEMr} for reading memory, this function just points at a builtin we have defined elsewhere. Note that @@ -71,8 +72,8 @@ well as a host of other concurrency model related effects. They also indicate whether a function throws exceptions or has other non-local control flow (the escape effect). -\sailMEMr -\sailfnMEMr +\sailval{MEMr} +\sailfn{MEMr} It's common when defining architecture specifications to break instruction semantics down into separate functions that handle @@ -85,7 +86,7 @@ architecture reference manual. To support this Sail supports decode functions, and declare them as scattered functions, as well as the \ll{ast} union. -\sailiop +\sailtype{iop} \begin{lstlisting} scattered union ast @@ -110,8 +111,8 @@ its argument. union clause ast = ITYPE : (bits(12), regbits, regbits, iop) \end{lstlisting} -\sailfndecodeSomeITYPE -\sailfnexecuteITYPE +%\sailfndecodeSomeITYPE +%\sailfnexecuteITYPE \noindent Now we do the same thing for the load-double instruction: @@ -119,15 +120,15 @@ union clause ast = ITYPE : (bits(12), regbits, regbits, iop) union clause ast = LOAD : (bits(12), regbits, regbits) \end{lstlisting} -\sailfndecodeSomeLOAD -\sailfnexecuteLOAD +%\sailfndecodeSomeLOAD +%\sailfnexecuteLOAD Finally we define the fallthrough case for the decode function, and end all our scattered definitions. Note that the clauses in a scattered function will be matched in the order they appear in the file. -\sailfndecodeNone +%\sailfndecodeNone \begin{lstlisting} end ast diff --git a/doc/tutorial.tex b/doc/tutorial.tex index 5a362c28..dcac1c13 100644 --- a/doc/tutorial.tex +++ b/doc/tutorial.tex @@ -12,14 +12,14 @@ Subsection, we will write our own version of the \ll{replicate_bits} function from the Sail library. This function takes a number $n$ and a bitvector, and copies that bitvector $n$ times. -\mrbmyreplicatebits +\mrbval{my_replicate_bits} \noindent The general syntax for a function type in Sail is as follows: \begin{center} \ll{val} \textit{name} \ll{:} \ll{forall} \textit{type variables} \ll{,} \textit{constraint} \ll{. (} \textit{type$_1$} \ll{,} $\ldots$ \ll{,} \textit{type$_2$} \ll{)} \ll{->} \textit{return type} \end{center} An implementation for the \ll{replicate_bits} function would be -follows \mrbfnmyreplicatebits +follows \mrbfn{my_replicate_bits} The general syntax for a function declaration is: \begin{center} @@ -36,7 +36,7 @@ above function, and eventually return the result \verb|0xAAA|. Typing to be evaluated fully, rather than stepping through the execution. Sail allows type variables to be used directly within expressions, so -the above could be re-written as \mrbfnmyreplicatebitstwo This +the above could be re-written as \mrbfn{my_replicate_bits_two} This notation can be succinct, but should be used with caution. What happens is that Sail will try to re-write the type variables using expressions of the appropriate size that are available within the @@ -48,8 +48,8 @@ however very useful for implementing functions with implicit parameters, e.g. we can implement a zero extension function that implicitly picks up its result length from the calling context as follows: -\mrbextzz -\mrbfnextzz +\mrbval{extz} +\mrbfn{extz} Notice that we annotated the \ll{val} declaration as a \ll{cast}---this means that the type checker is allowed to @@ -58,32 +58,32 @@ check. This is another feature that must be used carefully, because too many implicit casts can quickly result in unreadable code. Sail does not make any distinction between expressions and statements, so since there is only a single line of code within the foreach block, we -can drop it and simply write: \mrbfnmyreplicatebitsthree - -\subsection{External Bindings} - -Rather than defining functions within Sail itself, they can be mapped -onto function definitions within the various backend targets supported -by Sail. This is primarily used to setup the primitive functions -defined in the Sail library. These declarations work much like FFI -bindings in many programming languages---in Sail we provide the -\ll{val} declaration, except rather than giving a function body we -supply a string used to identify the external operator in each -backend. For example, we could link the \ll{<<} operator with the -\verb|shiftl| primitive as \mrbzeightoperatorzzerozIzIznine If the -external function has the same name as the sail function, such as -\ll{shiftl = "shiftl"}, then we can use the shorthand syntax -\mrbshiftl - -We can map onto differently-named operations for different targets by -using a JSON-like \ll{key: "value"} notation, for example: -\mrbzeightoperatorzzerozKzKznine We can also omit backends---in which -case those targets will expect a definition written in Sail. Note that -no checking is done to ensure that the definition in the target -matches the type of the Sail function. Finally, the \ll{_} key used -above is a wildcard that will be used for any backend not otherwise -included. If we use the wildcard key, then we cannot omit specific -backends to force them to use a definition in Sail. +can drop it and simply write: \mrbfn{my_replicate_bits_three} + +%\subsection{External Bindings} + +%Rather than defining functions within Sail itself, they can be mapped +%onto function definitions within the various backend targets supported +%by Sail. This is primarily used to setup the primitive functions +%defined in the Sail library. These declarations work much like FFI +%bindings in many programming languages---in Sail we provide the +%\ll{val} declaration, except rather than giving a function body we +%supply a string used to identify the external operator in each +%backend. For example, we could link the \ll{<<} operator with the +%\verb|shiftl| primitive as \mrbzeightoperatorzzerozIzIznine If the +%external function has the same name as the sail function, such as +%\ll{shiftl = "shiftl"}, then we can use the shorthand syntax +%\mrbshiftl + +%We can map onto differently-named operations for different targets by +%using a JSON-like \ll{key: "value"} notation, for example: +%\mrbzeightoperatorzzerozKzKznine We can also omit backends---in which +%case those targets will expect a definition written in Sail. Note that +%no checking is done to ensure that the definition in the target +%matches the type of the Sail function. Finally, the \ll{_} key used +%above is a wildcard that will be used for any backend not otherwise +%included. If we use the wildcard key, then we cannot omit specific +%backends to force them to use a definition in Sail. \subsection{Numeric Types} \label{sec:numeric} @@ -265,10 +265,10 @@ Pattern matching can be used to destructure lists, see Section~\ref{sec:pat}. Sail also has a \ll{string} type, and a \ll{real} type. The \ll{real} type is used to model arbitrary real numbers, so floating point -instructions could be specified by saying that they are equivalent to -mapping the floating point inputs to real numbers, performing the -arithmetic operation on the real numbers, and then mapping back to a -floating point value of the appropriate precision. +instructions could be specified by mapping the floating point inputs +to real numbers, performing the arithmetic operation on the real +numbers, and then mapping back to a floating point value of the +appropriate precision. \subsection{Pattern Matching} \label{sec:pat} @@ -473,8 +473,8 @@ If we were to write \end{lstlisting} instead, then \textit{pattern} would only be bound within $\textit{expression}_1$ and not any further expressions. In general -the block-form of let statements terminated with a semicolon should be -preferred within blocks. +the block-form of let statements terminated with a semicolon should +always be preferred within blocks. Variables bound within function arguments, match statement, and let-bindings are always immutable, but Sail also allows mutable diff --git a/doc/usage.tex b/doc/usage.tex index d4f87393..2711fff5 100644 --- a/doc/usage.tex +++ b/doc/usage.tex @@ -147,7 +147,7 @@ files. call the \ll{cycle_count} function for this to work. \end{itemize} -\subsection{Lem and Isabelle} +\subsection{Lem, Isabelle \& HOL4} We have a separate document detailing how to generate Isabelle theories from Sail models, and how to work with those models in @@ -191,6 +191,68 @@ mode, a list of commands can be accessed by typing \verb+:commands+, while \verb+:help+ can be used to provide some documentation for each command. +\subsection{\LaTeX\ Generation} + +Sail can be used to generate latex for inclusion in documentation as: +\begin{verbatim} +sail -o DIRECTORY -latex FILES +\end{verbatim} +The list of \verb+FILES+ is a list of Sail files to produce latex for, +and \verb+DIRECTORY+ is the directory where the generated latex will +be placed. The list of files must be a valid type-checkable series of +Sail files. The intention behind this latex generation is for it to be +included within existing ISA manuals written in Latex, as such the +latex output generates a list of commands for each top-level Sail +declaration in \verb+DIRECTORY/commands.tex+. The rest of this section +discusses the stable features of the latex generation process---there +are additional features for including markdown doc-comments in Sail +code and formatting them into latex for inclusion id documentation, +among other things, but these features are not completely stable +yet. This manual itself makes use of the Sail latex generation, so +\verb+doc/manual.tex+, and \verb+doc/Makefile+ can be used to see how +the process is set up. + + +\paragraph{Requirements} The generated latex uses the \emph{listings} package for formatting +source code, uses the macros in the \emph{etoolbox} package for the +generated commands, and relies on the \emph{hyperref} package for +cross-referencing. These packages are available in most TeX +distributions, and are available as part of thetexlive packages for +Ubuntu. + +\paragraph{Usage} Due to the oddities of latex verbatim environments each Sail +declaration must be placed in it's own file then the command in +\verb+commands.tex+ includes in with \verb+\lstinputlisting+. To +include the generated Sail in a document one would do something like: +\begin{lstlisting}[language=TeX] + \input{commands.tex} + \sailval{my_function} + \sailfn{my_function} +\end{lstlisting} +which would enclude the type declaration (\verb+\sailval+) for +\verb+my_function+ as well as type body of that function +(\verb+\sailfn+). + +It is sometimes useful to include multiple versions of the same Sail +definitions in a latex document. In this case the \verb+-latex_prefix+ +option can be used. For example if we used \verb+-latex_prefix prefix+ +then the above example would become: +\begin{lstlisting}[language=TeX] + \input{commands.tex} + \prefixval{my_function} + \prefixfn{my_function} +\end{lstlisting} + +The generated definitions are created wrapped in customisable macros +that can be overridden to change the formatting of the Sail code. For +\verb+\sailfn+ there is a macro \verb+\saildocfn+ that must be defined, +and similarly for the other Sail toplevel types. + +\paragraph{Cross-referencing} For each macro \verb+\sail+\emph{X}\verb+{id}+ there is a macro +\verb+\sailref+\emph{X}\verb+{id}{text}+ which creates a +hyper-reference to the original definition. This requires the +hyper-ref package. + \subsection{Other options} Here we summarize most of the other options available for diff --git a/editors/sail-mode.el b/editors/sail-mode.el index 28a109b0..6dae0761 100644 --- a/editors/sail-mode.el +++ b/editors/sail-mode.el @@ -1,2099 +1,67 @@ -;;; sail.el --- Sail mode for Emacs. -;;; based on tuareg.el which was - ;; Copyright (C) 1997-2006 Albert Cohen, all rights reserved. - ;; Copyright (C) 2009-2010 Jane Street Holding, LLC. - ;; Licensed under the GNU General Public License. - ;; Author: Albert Cohen <Albert.Cohen@inria.fr> - ;; Sam Steingold <sds@gnu.org> - ;; Christophe Troestler <Christophe.Troestler@umons.ac.be> - ;; Till Varoquaux <till@pps.jussieu.fr> - ;; Sean McLaughlin <seanmcl@gmail.com> - ;; Created: 8 Jan 1997 - ;; Version: 2.0.5 - ;; URL: http://forge.ocamlcore.org/projects/tuareg/ - ;; EmacsWiki: TuaregMode - -(eval-when-compile (require 'cl)) -(require 'easymenu) - -(defalias 'sail-match-string - (if (fboundp 'match-string-no-properties) - 'match-string-no-properties - 'match-string)) - - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; User customizable variables - -;; Use the standard `customize' interface or `sail-mode-hook' to -;; Configure these variables - -(require 'custom) - -(defgroup sail nil - "Support for the Sail language." - :group 'languages) - -;; Comments - -(defcustom sail-indent-leading-comments t - "*If true, indent leading comment lines (starting with `(*') like others." - :group 'sail :type 'boolean) - -(defcustom sail-indent-comments t - "*If true, automatically align multi-line comments." - :group 'sail :type 'boolean) - -(defcustom sail-comment-end-extra-indent 0 - "*How many spaces to indent a leading comment end `*)'. -If you expect comments to be indented like - (* - ... - *) -even without leading `*', use `sail-comment-end-extra-indent' = 1." - :group 'sail - :type '(radio :extra-offset 8 - :format "%{Comment End Extra Indent%}: - Comment alignment:\n%v" - (const :tag "align with `(' in comment opening" 0) - (const :tag "align with `*' in comment opening" 1) - (integer :tag "custom alignment" 0))) - -(defcustom sail-support-leading-star-comments t - "*Enable automatic intentation of comments of the form - (* - * ... - *) -Documentation comments (** *) are not concerned by this variable -unless `sail-leading-star-in-doc' is also set. - -If you do not set this variable and still expect comments to be -indented like - (* - ... - *) -\(without leading `*'), set `sail-comment-end-extra-indent' to 1." - :group 'sail :type 'boolean) - -(defcustom sail-leading-star-in-doc nil - "*Enable automatic intentation of documentation comments of the form - (** - * ... - *)" - :group 'sail :type 'boolean) - -;; Indentation defaults - -(defcustom sail-default-indent 2 - "*Default indentation. - -Global indentation variable (large values may lead to indentation overflows). -When no governing keyword is found, this value is used to indent the line -if it has to." - :group 'sail :type 'integer) - -(defcustom sail-let-always-indent t - "*If true, enforce indentation is at least `sail-let-indent' after a `let'. - -As an example, set it to false when you have `sail-with-indent' set to 0, -and you want `let x = match ... with' and `match ... with' indent the -same way." - :group 'sail :type 'boolean) - -(defcustom sail-case-extra-unindent sail-default-indent - "*Extra backward indent for Sail lines starting with the `case' operator. - -It is NOT the variable controlling the indentation of the `case' itself: -this value is automatically added to `switch' to leave enough space for `case' backward -indentation." - - :group 'sail :type 'integer) - -(defcustom sail-enum-indent sail-default-indent - "*How many spaces to indent from an `enumerate' keyword." - :group 'sail :type 'integer) - -(defcustom sail-struct-struct-indent sail-default-indent - "*How many spaces to indent from a `struct' keyword." - :group 'sail :type 'integer) - -(defcustom sail-foreach-indent sail-default-indent - "*How many spaces to indent from a `foreach' keyword." - :group 'sail :type 'integer) - -(defcustom sail-function-indent sail-default-indent - "*How many spaces to indent from a `function' keyword." - :group 'sail :type 'integer) - -(defcustom sail-if-then-else-indent sail-default-indent - "*How many spaces to indent from an `if', `then' or `else' keyword." - :group 'sail :type 'integer) - -(defcustom sail-let-indent sail-default-indent - "*How many spaces to indent from a `let' keyword." - :group 'sail :type 'integer) - -(defcustom sail-in-indent sail-default-indent - "*How many spaces to indent from a `in' keyword." - :group 'sail :type 'integer) - -(defcustom sail-switch-indent sail-default-indent - "*How many spaces to indent from a `switch' keyword." - :group 'sail :type 'integer) - -(defcustom sail-with-indent sail-default-indent - "*How many spaces to indent from a `with' keyword." - :group 'sail :type 'integer) - -(defcustom sail-typedef-indent sail-default-indent - "*How many spaces to indent from a `typedef' keyword." - :group 'sail :type 'integer) - -(defcustom sail-val-indent sail-default-indent - "*How many spaces to indent from a `val' keyword." - :group 'sail :type 'integer) - -;; Automatic indentation -;; Using abbrev-mode and electric keys - -(defcustom sail-use-abbrev-mode t - "*Non-nil means electrically indent lines starting with leading keywords. -It makes use of `abbrev-mode'. - -Many people find eletric keywords irritating, so you can disable them by -setting this variable to nil." - :group 'sail :type 'boolean - :set '(lambda (var val) - (setq sail-use-abbrev-mode val) - (abbrev-mode val))) - -(defcustom sail-electric-indent t - "*Non-nil means electrically indent lines starting with `|]', '||]', '>', `)', `]' or `}'. - -Many people find eletric keys irritating, so you can disable them in -setting this variable to nil." - :group 'sail :type 'boolean) - -(defcustom sail-electric-close-range t - "*Non-nil means electrically insert `|' before a list-closing `]'. - -Many people find eletric keys irritating, so you can disable them in -setting this variable to nil. You should probably have this on, -though, if you also have `sail-electric-indent' on." - :group 'sail :type 'boolean) - -(defcustom sail-electric-close-block t -"*Non-nil means electrically insert `}'" - :group 'sail :type 'boolean) - - -(defvar sail-options-list - '(("Automatic indentation of leading keywords" . 'sail-use-abbrev-mode) - ("Automatic indentation of ), ], |], ||], >, and }" . 'sail-electric-indent) - ("Automatic matching of [|" . 'sail-electric-close-range) - "---" - ("Indent body of comments" . 'sail-indent-comments) - ("Indent first line of comments" . 'sail-indent-leading-comments) - ("Leading-`*' comment style" . 'sail-support-leading-star-comments)) - "*List of menu-configurable Sail options.") - -(eval-and-compile - (defconst sail-use-syntax-ppss (fboundp 'syntax-ppss) - "*If nil, use our own parsing and caching.")) - -(defgroup sail-faces nil - "Special faces for the Sail mode." - :group 'sail) - -(defconst sail-faces-inherit-p - (and (boundp 'face-attribute-name-alist) - (assq :inherit face-attribute-name-alist))) - -(defface sail-font-lock-governing-face - '((((background light)) (:foreground "blue" :bold t)) - (t (:foreground "orange" :bold t))) - "Face description for governing/leading keywords." - :group 'sail-faces) -(defvar sail-font-lock-governing-face - 'sail-font-lock-governing-face) - -(defface sail-font-lock-operator-face - '((((background light)) (:foreground "brown")) - (t (:foreground "khaki"))) - "Face description for all operators." - :group 'sail-faces) -(defvar sail-font-lock-operator-face - 'sail-font-lock-operator-face) - -(defface sail-font-lock-error-face - '((t (:foreground "yellow" :background "red" :bold t))) - "Face description for all errors reported to the source." - :group 'sail-faces) -(defvar sail-font-lock-error-face - 'sail-font-lock-error-face) - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; Support definitions - -(defun sail-leading-star-p () - (and sail-support-leading-star-comments - (save-excursion ; this function does not make sense outside of a comment - (sail-beginning-of-literal-or-comment) - (and (or sail-leading-star-in-doc - (not (looking-at "(\\*[Tt][Ee][Xx]\\|(\\*\\*"))) - (progn - (forward-line 1) - (back-to-indentation) - (looking-at "\\*[^)]")))))) - -(defun sail-auto-fill-insert-leading-star (&optional leading-star) - (let ((point-leading-comment (looking-at "(\\*")) (return-leading nil)) - (save-excursion - (back-to-indentation) - (when sail-electric-indent - (when (and (sail-in-comment-p) - (or leading-star - (sail-leading-star-p))) - (unless (looking-at "(?\\*") - (insert-before-markers "* ")) - (setq return-leading t)) - (unless point-leading-comment - ;; Use optional argument to break recursion - (sail-indent-command t)))) - return-leading)) - -(defun sail-auto-fill-function () - (unless (sail-in-literal-p) - (let ((leading-star - (and (not (char-equal ?\n last-command-event)) - (sail-auto-fill-insert-leading-star)))) - (do-auto-fill) - (unless (char-equal ?\n last-command-event) - (sail-auto-fill-insert-leading-star leading-star))))) - -;; these two functions are different from the standard -;; in that they do NOT signal errors beginning-of-buffer and end-of-buffer -(defun sail-forward-char (&optional step) - (if step (goto-char (+ (point) step)) - (goto-char (1+ (point))))) - -(defun sail-backward-char (&optional step) - (if step (goto-char (- (point) step)) - (goto-char (1- (point))))) - -(defun sail-in-indentation-p () - "Return non-nil if all chars between beginning of line and point are blanks." - (save-excursion - (skip-chars-backward " \t") - (bolp))) - -(defvar sail-cache-stop (point-min)) -(make-variable-buffer-local 'sail-cache-stop) -(defvar sail-cache nil) -(make-variable-buffer-local 'sail-cache) -(defvar sail-cache-local nil) -(make-variable-buffer-local 'sail-cache-local) -(defvar sail-cache-last-local nil) -(make-variable-buffer-local 'sail-cache-last-local) -(defvar sail-last-loc (cons nil nil)) - -;; PPSS definitions -(defun sail-ppss-in-literal-or-comment () (error "sail uses PPSS")) -(defun sail-ppss-fontify (beg end) (error "sail uses PPSS")) -(defun sail-ppss-in-literal-p () - "Returns non-nil if point is inside a Sail literal." - (nth 3 (syntax-ppss))) -(defun sail-ppss-in-comment-p () - "Returns non-nil if point is inside or right before a Sail comment." - (or (nth 4 (syntax-ppss)) - (looking-at "[ \t]*(\\*"))) -(defun sail-ppss-in-literal-or-comment-p () - "Returns non-nil if point is inside a Sail literal or comment." - (nth 8 (syntax-ppss))) -(defun sail-ppss-beginning-of-literal-or-comment () - "Skips to the beginning of the current literal or comment (or buffer)." - (interactive) - (goto-char (or (nth 8 (syntax-ppss)) (point)))) -(defun sail-ppss-beginning-of-literal-or-comment-fast () - (goto-char (or (nth 8 (syntax-ppss)) (point-min)))) -;; FIXME: not clear if moving out of a string/comment counts as 1 or no. -(defalias 'sail-backward-up-list 'backward-up-list) - -;; non-PPSS definitions -(defun sail-!ppss-in-literal-p () - "Return non-nil if point is inside a Sail literal." - (car (sail-in-literal-or-comment))) -(defun sail-!ppss-in-comment-p () - "Return non-nil if point is inside a Sail comment." - (cdr (sail-in-literal-or-comment))) -(defun sail-!ppss-in-literal-or-comment-p () - "Return non-nil if point is inside a Sail literal or comment." - (sail-in-literal-or-comment) - (or (car sail-last-loc) (cdr sail-last-loc))) -(defun sail-!ppss-in-literal-or-comment () - "Return the pair `((sail-in-literal-p) . (sail-in-comment-p))'." - (if (and (<= (point) sail-cache-stop) sail-cache) - (progn - (if (or (not sail-cache-local) (not sail-cache-last-local) - (and (>= (point) (caar sail-cache-last-local)))) - (setq sail-cache-local sail-cache)) - (while (and sail-cache-local (< (point) (caar sail-cache-local))) - (setq sail-cache-last-local sail-cache-local - sail-cache-local (cdr sail-cache-local))) - (setq sail-last-loc - (if sail-cache-local - (cons (eq (cadar sail-cache-local) 'b) - (> (cddar sail-cache-local) 0)) - (cons nil nil)))) - (let ((flag t) (op (point)) (mp (min (point) (1- (point-max)))) - (balance 0) (end-of-comment nil)) - (while (and sail-cache (<= sail-cache-stop (caar sail-cache))) - (setq sail-cache (cdr sail-cache))) - (if sail-cache - (if (eq (cadar sail-cache) 'b) - (progn - (setq sail-cache-stop (1- (caar sail-cache))) - (goto-char sail-cache-stop) - (setq balance (cddar sail-cache)) - (setq sail-cache (cdr sail-cache))) - (setq balance (cddar sail-cache)) - (setq sail-cache-stop (caar sail-cache)) - (goto-char sail-cache-stop) - (skip-chars-forward "(")) - (goto-char (point-min))) - (skip-chars-backward "\\\\*") - (while flag - (if end-of-comment (setq balance 0 end-of-comment nil)) - (skip-chars-forward "^\\\\'`\"(\\*") - (cond - ((looking-at "\\\\") - (sail-forward-char 2)) - ((looking-at "'\\([^\n\\']\\|\\\\[^ \t\n][^ \t\n]?[^ \t\n]?\\)'") - (setq sail-cache (cons (cons (1+ (point)) (cons 'b balance)) - sail-cache)) - (goto-char (match-end 0)) - (setq sail-cache (cons (cons (point) (cons 'e balance)) - sail-cache))) - ((looking-at "\"") - (sail-forward-char) - (setq sail-cache (cons (cons (point) (cons 'b balance)) - sail-cache)) - (skip-chars-forward "^\\\\\"") - (while (looking-at "\\\\") - (sail-forward-char 2) (skip-chars-forward "^\\\\\"")) - (sail-forward-char) - (setq sail-cache (cons (cons (point) (cons 'e balance)) - sail-cache))) - ((looking-at "(\\*") - (setq balance (1+ balance)) - (setq sail-cache (cons (cons (point) (cons nil balance)) - sail-cache)) - (sail-forward-char 2)) - ((looking-at "\\*)") - (sail-forward-char 2) - (if (> balance 1) - (progn - (setq balance (1- balance)) - (setq sail-cache (cons (cons (point) (cons nil balance)) - sail-cache))) - (setq end-of-comment t) - (setq sail-cache (cons (cons (point) (cons nil 0)) - sail-cache)))) - (t (sail-forward-char))) - (setq flag (<= (point) mp))) - (setq sail-cache-local sail-cache - sail-cache-stop (point)) - (goto-char op) - (if sail-cache (sail-in-literal-or-comment) - (setq sail-last-loc (cons nil nil)) - sail-last-loc)))) -(defun sail-!ppss-beginning-of-literal-or-comment () - "Skips to the beginning of the current literal or comment (or buffer)." - (interactive) - (when (sail-in-literal-or-comment-p) - (sail-beginning-of-literal-or-comment-fast))) - -(defun sail-!ppss-beginning-of-literal-or-comment-fast () - (while (and sail-cache-local - (or (eq 'b (cadar sail-cache-local)) - (> (cddar sail-cache-local) 0))) - (setq sail-cache-last-local sail-cache-local - sail-cache-local (cdr sail-cache-local))) - (if sail-cache-last-local - (goto-char (caar sail-cache-last-local)) - (goto-char (point-min))) - (when (eq 'b (cadar sail-cache-last-local)) (sail-backward-char))) - -(defun sail-!ppss-backward-up-list () - "Safe up-list regarding comments, literals and errors." - (let ((balance 1) (op (point)) (oc nil)) - (sail-in-literal-or-comment) - (while (and (> (point) (point-min)) (> balance 0)) - (setq oc (if sail-cache-local (caar sail-cache-local) (point-min))) - (condition-case nil (up-list -1) (error (goto-char (point-min)))) - (if (>= (point) oc) (setq balance (1- balance)) - (goto-char op) - (skip-chars-backward "^[]{}()<>") (sail-backward-char) - (cond ((sail-in-literal-or-comment-p) - (sail-beginning-of-literal-or-comment-fast)) - ((looking-at "[[{(<]") - (setq balance (1- balance))) - ((looking-at "[]})>]") - (setq balance (1+ balance))))) - (setq op (point))))) - -(defalias 'sail-in-literal-or-comment - (eval-and-compile (if sail-use-syntax-ppss - 'sail-ppss-in-literal-or-comment - 'sail-!ppss-in-literal-or-comment))) -(defalias 'sail-fontify - (eval-and-compile (if sail-use-syntax-ppss - 'sail-ppss-fontify - 'sail-!ppss-fontify))) -(defalias 'sail-in-literal-p - (eval-and-compile (if sail-use-syntax-ppss - 'sail-ppss-in-literal-p - 'sail-!ppss-in-literal-p))) -(defalias 'sail-in-comment-p - (eval-and-compile (if sail-use-syntax-ppss - 'sail-ppss-in-comment-p - 'sail-!ppss-in-comment-p))) -(defalias 'sail-in-literal-or-comment-p - (eval-and-compile (if sail-use-syntax-ppss - 'sail-ppss-in-literal-or-comment-p - 'sail-!ppss-in-literal-or-comment-p))) -(defalias 'sail-beginning-of-literal-or-comment - (eval-and-compile (if sail-use-syntax-ppss - 'sail-ppss-beginning-of-literal-or-comment - 'sail-!ppss-beginning-of-literal-or-comment))) -(defalias 'sail-beginning-of-literal-or-comment-fast - (eval-and-compile (if sail-use-syntax-ppss - 'sail-ppss-beginning-of-literal-or-comment-fast - 'sail-!ppss-beginning-of-literal-or-comment-fast))) -(defalias 'sail-backward-up-list - ;; FIXME: not clear if moving out of a string/comment counts as 1 or no. - (eval-and-compile (if sail-use-syntax-ppss - 'backward-up-list - 'sail-!ppss-backward-up-list))) - -(defun sail-false-=-p () - "Is the underlying `=' the first/second letter of an operator?" - (or (memq (preceding-char) '(?: ?> ?< ?=)) - (char-equal ?= (char-after (1+ (point)))))) - -(defun sail-at-phrase-break-p () - "Is the underlying `;' a phrase break?" - (and (char-equal ?\; (following-char)) - (or (and (not (eobp)) - (char-equal ?\; (char-after (1+ (point))))) - (char-equal ?\; (preceding-char))))) - -(defvar sail-mode-syntax-table +(defvar sail2-mode-hook nil) + +(add-to-list 'auto-mode-alist '("\\.sail\\'" . sail2-mode)) + +(defconst sail2-keywords + '("val" "function" "type" "struct" "union" "enum" "let" "var" "if" "then" "by" + "else" "match" "in" "return" "register" "ref" "forall" "operator" "effect" + "overload" "cast" "sizeof" "constant" "constraint" "default" "assert" "newtype" "from" + "pure" "infixl" "infixr" "infix" "scattered" "end" "try" "catch" "and" "to" + "throw" "clause" "as" "repeat" "until" "while" "do" "foreach" "bitfield" + "mapping" "where" "with")) + +(defconst sail2-kinds + '("Int" "Type" "Order" "Bool" "inc" "dec" + "barr" "depend" "rreg" "wreg" "rmem" "rmemt" "wmv" "wmvt" "eamem" "wmem" + "exmem" "undef" "unspec" "nondet" "escape" "configuration")) + +(defconst sail2-types + '("vector" "int" "nat" "atom" "range" "unit" "bit" "real" "list" "bool" "string" "bits" "option" + "uint64_t" "int64_t" "bv_t" "mpz_t")) + +(defconst sail2-special + '("_prove" "_not_prove" "create" "kill" "convert" "undefined" + "$define" "$include" "$ifdef" "$ifndef" "$else" "$endif" "$option" "$optimize" "$latex")) + +(defconst sail2-font-lock-keywords + `((,(regexp-opt sail2-keywords 'symbols) . font-lock-keyword-face) + (,(regexp-opt sail2-kinds 'symbols) . font-lock-builtin-face) + (,(regexp-opt sail2-types 'symbols) . font-lock-type-face) + (,(regexp-opt sail2-special 'symbols) . font-lock-preprocessor-face) + ("~" . font-lock-negation-char-face) + ("\\(::\\)<" 1 font-lock-keyword-face) + ("@" . font-lock-preprocessor-face) + ("<->" . font-lock-negation-char-face) + ("\'[a-zA-Z0-9_]+" . font-lock-variable-name-face) + ("\\([a-zA-Z0-9_]+\\)(" 1 font-lock-function-name-face) + ("function \\([a-zA-Z0-9_]+\\)" 1 font-lock-function-name-face) + ("val \\([a-zA-Z0-9_]+\\)" 1 font-lock-function-name-face) + ("\\_<\\([0-9]+\\|0b[0-9_]+\\|0x[0-9a-fA-F_]+\\|true\\|false\\|bitone\\|bitzero\\)\\_>\\|()" . font-lock-constant-face))) + +(defconst sail2-mode-syntax-table (let ((st (make-syntax-table))) - (modify-syntax-entry ?_ "_" st) - (modify-syntax-entry ?? ". p" st) - (modify-syntax-entry ?~ ". p" st) - (modify-syntax-entry ?: "." st) - (modify-syntax-entry ?' "w" st) ; ' is part of words (for primes). - (modify-syntax-entry ?\" "\"" st) ; " is a string delimiter - (modify-syntax-entry ?\\ "\\" st) - (modify-syntax-entry ?* ". 23" st) - (condition-case nil - (progn - (modify-syntax-entry ?\( "()1n" st) - (modify-syntax-entry ?\) ")(4n" st)) - (error ;XEmacs signals an error instead of ignoring `n'. - (modify-syntax-entry ?\( "()1" st) - (modify-syntax-entry ?\) ")(4" st))) + (modify-syntax-entry ?> "." st) + (modify-syntax-entry ?_ "w" st) + (modify-syntax-entry ?' "w" st) + (modify-syntax-entry ?* ". 23" st) + (modify-syntax-entry ?/ ". 124b" st) + (modify-syntax-entry ?\n "> b" st) st) - "Syntax table in use in Sail mode buffers.") - -(defmacro sail-with-internal-syntax (&rest body) - `(progn - ;; Switch to a modified internal syntax. - (modify-syntax-entry ?. "w" sail-mode-syntax-table) - (modify-syntax-entry ?_ "w" sail-mode-syntax-table) - (unwind-protect (progn ,@body) - ;; Switch back to the interactive syntax. - (modify-syntax-entry ?. "." sail-mode-syntax-table) - (modify-syntax-entry ?_ "_" sail-mode-syntax-table)))) - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; Font-Lock - -(defvar sail-doc-face 'font-lock-doc-face) - -(unless sail-use-syntax-ppss - - (defun sail-fontify-buffer () - (font-lock-default-fontify-buffer) - (sail-fontify (point-min) (point-max))) - - (defun sail-fontify-region (begin end &optional verbose) - (font-lock-default-fontify-region begin end verbose) - (sail-fontify begin end)) - - (defun sail-fontify (begin end) - (when (eq major-mode 'sail-mode) - (save-excursion - (sail-with-internal-syntax - - (let ((case-fold-search nil) - (modified (buffer-modified-p))) ; Emacs hack (see below) - (goto-char begin) - (setq begin (line-beginning-position)) - (goto-char (1- end)) - (end-of-line) - ;; Dirty hack to trick `font-lock-default-unfontify-region' - (forward-line 2) - (setq end (point)) - - (while (> end begin) - (goto-char (1- end)) - (sail-in-literal-or-comment) - (cond - ((cdr sail-last-loc) - (sail-beginning-of-literal-or-comment) - (put-text-property (max begin (point)) end 'face - (if (looking-at - "(\\*[Tt][Ee][Xx]\\|(\\*\\*[^*]") - sail-doc-face - 'font-lock-comment-face)) - (setq end (1- (point)))) - ((car sail-last-loc) - (sail-beginning-of-literal-or-comment) - (put-text-property (max begin (point)) end 'face - 'font-lock-string-face) - (setq end (point))) - (t (while (and sail-cache-local - (or (> (caar sail-cache-local) end) - (eq 'b (cadar sail-cache-local)))) - (setq sail-cache-local (cdr sail-cache-local))) - (setq end (if sail-cache-local - (caar sail-cache-local) begin))))) - (unless modified (set-buffer-modified-p nil))) - )))) - ) ;; end sail-use-syntax-ppss - -(defconst sail-font-lock-syntactic-keywords - ;; Char constants start with ' but ' can also appear in identifiers. - ;; Beware not to match things like '*)hel' or '"hel' since the first ' - ;; might be inside a string or comment. - '(("\\<\\('\\)\\([^'\\\n]\\|\\\\.[^\\'\n \")]*\\)\\('\\)" - (1 '(7)) (3 '(7))))) - -(defun sail-font-lock-syntactic-face-function (state) - (if (nth 3 state) font-lock-string-face - (let ((start (nth 8 state))) - (if (and (> (point-max) (+ start 2)) - (eq (char-after (+ start 2)) ?*) - (not (eq (char-after (+ start 3)) ?*))) - ;; This is a documentation comment - sail-doc-face - font-lock-comment-face)))) - -;; Initially empty, set in `sail-install-font-lock' -(defvar sail-font-lock-keywords () - "Font-Lock patterns for Sail mode.") - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; Keymap - -(defvar sail-mode-map - (let ((map (make-sparse-keymap))) - ;(define-key map "|]" 'sail-electric-piperb) - (define-key map ")" 'sail-electric-rp) - (define-key map "}" 'sail-electric-rc) - ;(define-key map "]" 'sail-electric-rb) - (define-key map ">" 'sail-electric-lt) - (define-key map "\M-q" 'sail-indent-phrase) - (define-key map "\C-c\C-q" 'sail-indent-phrase) - (define-key map "\M-\C-\\" 'indent-region) - (define-key map "\C-c\C-a" 'sail-find-alternate-file) - (define-key map "\C-c\C-c" 'compile) - (define-key map "\C-xnd" 'sail-narrow-to-phrase) - (define-key map "\C-c\C-n" 'sail-next-phrase) - (define-key map "\C-c\C-p" 'sail-previous-phrase) - (define-key map [(backspace)] 'backward-delete-char-untabify) - (define-key map [(control c) (control down)] 'sail-next-phrase) - (define-key map [(control c) (control up)] 'sail-previous-phrase) - (define-key map [(meta control down)] 'sail-next-phrase) - (define-key map [(meta control up)] 'sail-previous-phrase) - (define-key map [(meta control n)] 'sail-next-phrase) - (define-key map [(meta control p)] 'sail-previous-phrase) - (define-key map [(meta control h)] 'sail-mark-phrase) - map) - "Keymap used in Sail mode.") - -(defconst sail-font-lock-syntax - `((?_ . "w") (?` . ".") - ,@(unless sail-use-syntax-ppss - '((?\" . ".") (?\( . ".") (?\) . ".") (?* . ".")))) - "Syntax changes for Font-Lock.") - -(defvar sail-mode-abbrev-table () - "Abbrev table used for Sail mode buffers.") -(defun sail-define-abbrev (keyword) - (define-abbrev sail-mode-abbrev-table keyword keyword 'sail-abbrev-hook)) -(if sail-mode-abbrev-table () - (setq sail-mode-abbrev-table (make-abbrev-table)) - (mapc 'sail-define-abbrev - '("scattered" "function" "typedef" "let" "default" "val" "register" - "alias" "union" "member" "clause" "extern" "cast" "effect" - "rec" "and" "switch" "case" "when" "exit" "foreach" "from" "else" - "to" "end" "downto" "in" "then" "with" "if" "nondet" "as" - "undefined" "const" "struct" "IN" "deinfix" "return" "constraint" "sizeof")) - (setq abbrevs-changed nil)) - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; The major mode + "Syntax table for Sail2 mode") -;;;###autoload (add-to-list 'auto-mode-alist '("\\.sail?" . sail-mode)) - -;;;###autoload -(defun sail-mode () - "Major mode for editing Sail code. - -Based on Tuareg mode. See Tuareg mode for usage" +(defun sail2-mode () + "Major mode for editing Sail Language files" (interactive) (kill-all-local-variables) - (setq major-mode 'sail-mode) - (setq mode-name "Sail") - (use-local-map sail-mode-map) - (set-syntax-table sail-mode-syntax-table) - (setq local-abbrev-sail sail-mode-abbrev-table) - - ;; Initialize the Sail menu - (sail-build-menu) - - ;; Initialize indentation regexps - (sail-make-indentation-regexps) - - (make-local-variable 'paragraph-start) - (setq paragraph-start (concat "^[ \t]*$\\|\\*)$\\|" page-delimiter)) - (make-local-variable 'paragraph-separate) - (setq paragraph-separate paragraph-start) - (make-local-variable 'require-final-newline) - (setq require-final-newline t) - (make-local-variable 'comment-start) - (setq comment-start "(* ") - (make-local-variable 'comment-end) - (setq comment-end " *)") - (make-local-variable 'comment-column) - (setq comment-column 40) - (make-local-variable 'comment-start-skip) - (setq comment-start-skip "(\\*+[ \t]*") - (make-local-variable 'comment-multi-line) - (setq comment-multi-line t) - (make-local-variable 'parse-sexp-ignore-comments) - (setq parse-sexp-ignore-comments nil) - ;; (make-local-variable 'indent-line-function) - ;; setq indent-line-function 'sail-indent-command) - (unless sail-use-syntax-ppss - (add-hook 'before-change-functions 'sail-before-change-function nil t)) - (make-local-variable 'normal-auto-fill-function) - (setq normal-auto-fill-function 'sail-auto-fill-function) - - (when (featurep 'imenu) - (setq imenu-prev-index-position-function 'sail-imenu-prev-index-position - imenu-extract-index-name-function 'sail-imenu-extract-index-name)) - - ;; Hooks for sail-mode, use them for sail-mode configuration - (sail-install-font-lock) - (run-hooks 'sail-mode-hook) - (when sail-use-abbrev-mode (abbrev-mode 1)) - (message nil)) - -(defun sail-install-font-lock () - (setq - sail-font-lock-keywords - `(("\\<\\(extern\\|cast\\|overload\\|deinfix\\|function\\|scattered\\|clause\\|effect\\|default\\|struct\\|const\\|union\\|val\\|typedef\\|let\\|rec\\|and\\|end\\|register\\|alias\\|member\\|enumerate\\)\\>" - 0 sail-font-lock-governing-face nil nil) - ("\\<\\(_prove\\)\\>" - 0 font-lock-preprocessor-face nil nil) - ("\\<\\(false\\|true\\|bitzero\\|bitone\\|0x[:xdigit:]\\|[:digit:]\\)\\>" 0 font-lock-constant-face nil nil) - ("\\<\\(as\\|downto\\|else\\|foreach\\|while\\|do\\|repeat\\|until\\|try\\|catch\\|throw\\|if\\|t\\(hen\\|o\\)\\|when\\|in\\|switch\\|with\\|case\\|when\\|exit\\|constraint\\|sizeof\\|nondet\\|from\\|by\\|return\\)\\>" - 0 font-lock-keyword-face nil nil) - ("\\<\\(clause\\)\\>[ \t\n]*\\(\\(\\w\\|[_ \t()*,]\\)+\\)" - 2 font-lock-variable-name-face keep nil) - ("\\<\\(typedef\\|union\\)\\>[ \t\n]*\\(\\(\\w\\|[_ \t()*,]\\)+\\)" - 2 font-lock-type-face keep nil) - ("\\<\\(Type\\|Nat\\|Num\\|Order\\|Effect\\|inc\\|dec\\|implicit\\|vector\\|rreg\\|wreg\\|rmem\\|wmem\\|wmv\\|eamem\\|barr\\|undef\\|escape\\|unspec\\|nondet\\|pure\\|effect\\|IN\\|forall\\|exist\\|bit\\|unit\\|bool\\|nat\\|real\\|int\\)\\>" - 0 font-lock-type-face keep nil) - ("\\<\\(val\\|extern\\|clause\\|and\\||let\\|rec\\>[ \t\n]*\\(\\(\\w\\|[_,?~.]\\)*\\)" - 2 font-lock-variable-name-face keep nil) - ("\\<\\(val\\|and\\|let\\>[ \t\n]*\\(\\(\\w\\|[_,?~.]\\)*\\)\\>\\(\\(\\w\\|[->_ \t,?~.]\\|(\\(\\w\\|[--->_ \t,?~.=]\\)*)\\)*\\)" - 6 font-lock-variable-name-face keep nil) - ("\\<\\([?~]?[_[:alpha:]]\\w*\\)[ \t\n]*:[^:>=]" - 0 font-lock-variable-name-face keep nil) - ("^#\\w+\\>" 0 font-lock-preprocessor-face t nil) - )) - (setq font-lock-defaults - (list* - 'sail-font-lock-keywords (not sail-use-syntax-ppss) nil - sail-font-lock-syntax nil - '(font-lock-syntactic-keywords - . sail-font-lock-syntactic-keywords) - '(parse-sexp-lookup-properties - . t) - '(font-lock-syntactic-face-function - . sail-font-lock-syntactic-face-function) - (unless sail-use-syntax-ppss - '((font-lock-fontify-region-function - . sail-fontify-region))))) - (when (and (boundp 'font-lock-fontify-region-function) - (not sail-use-syntax-ppss)) - (make-local-variable 'font-lock-fontify-region-function) - (setq font-lock-fontify-region-function 'sail-fontify-region))) - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; Indentation stuff - -(eval-and-compile - (defconst sail-no-more-code-this-line-regexp "[ \t]*" - "Regexp matching lines which have no more code: - blanks + (maybe) comment start.")) - -(defmacro sail-no-code-after (rex) - `(eval-when-compile (concat ,rex sail-no-more-code-this-line-regexp))) - -(defconst sail-no-code-this-line-regexp - (concat "^" sail-no-more-code-this-line-regexp)) - -(defun sail-ro (&rest words) (concat "\\<" (regexp-opt words t) "\\>")) - -(defconst sail-extra-unindent-regexp - (concat "\\(" (sail-ro "function") - "\\[" sail-no-more-code-this-line-regexp "\\)") - "Regexp for keywords needing extra indentation to compensate for case matches.") - -(defun sail-give-extra-unindent-regexp () - sail-extra-unindent-regexp) - -(defconst sail-keyword-regexp - (concat (sail-ro "scattered" "function" "typedef" "let" "overload" "default" "val" "register" - "alias" "union" "member" "clause" "cast" "extern" "effect" - "rec" "and" "switch" "case" "exit" "return" "foreach" "from" "else" - "to" "end" "downto" "in" "then" "with" "if" "nondet" "as" - "undefined" "const" "struct" "IN" "deinfix" "sizeof") - "\\|->\\|[;,|]") - "Regexp for all recognized keywords.") - -(defun sail-give-keyword-regexp () sail-keyword-regexp) - -(defconst sail-operator-regexp "[---+*/=<>@^&|]\\|:>\\|::\\|\\<\\(or\\|l\\(and\\|x?or\\|s[lr]\\)\\|as[lr]\\|mod\\)\\>" - "Regexp for all operators.") - -(defconst sail-matching-keyword-regexp - (sail-ro "and" "then" "else" "in") - "Regexp matching Sail keywords which act as end block delimiters.") - -(defun sail-give-matching-keyword-regexp () sail-matching-keyword-regexp) - -(defconst sail-matching-kwop-regexp - (concat sail-matching-keyword-regexp - "\\|\\<with\\>\\|[|>]?\\]\\|>?}\\|[|)]\\|;;") - "Regexp matching Sail keywords or operators which act as end block -delimiters.") - -(defun sail-give-matching-kwop-regexp () sail-matching-kwop-regexp) - -(defconst sail-block-regexp - (concat (sail-ro "foreach" "nondet" "if" "clause" "switch" "case") - "\\|[][(){}]\\|\\*)")) - -(defconst sail-find-kwop-regexp - (concat sail-matching-keyword-regexp "" sail-block-regexp)) - -(defun sail-give-find-kwop-regexp () sail-find-kwop-regexp) - -(defconst sail-governing-phrase-regexp - (sail-ro "val" "typedef" "function" "scattered" "default" "union" "member" - "end" "extern" "let") - "Regexp matching Sail phrase delimitors.") - -(defconst sail-keyword-alist - '(("end" . sail-default-indent) - ("foreach" . sail-foreach-indent) - ("val" . sail-val-indent) - ("function" . sail-fun-indent) - ("if" . sail-if-then-else-indent) - ("then" . sail-if-then-else-indent) - ("else" . sail-if-then-else-indent) - ("let" . sail-let-indent) - ("switch" . sail-match-indent) - - ;; Case match keywords - ("case" . sail-case-indent) - - ;; Assume default indentation for other keywords and operators - ) - "Association list of indentation values based on governing keywords.") - -(defconst sail-leading-kwop-alist - '(("}" . sail-find-match) - (">" . sail-find-match) - (")" . sail-find-match) - ("]" . sail-find-match) - ("|]" . sail-find-match) - ("||]" . sail-find-match) - ("in" . sail-find-in-match) - ("else" . sail-find-else-match) - ("then" . sail-find-then-match) - ("to" . sail-find-match) - ("downto" . sail-find-match) - ("by" . sail-find-match) - ("and" . sail-find-and-match)) - "Association list used in Sail mode for skipping back over nested blocks.") - -(defun sail-find-leading-kwop-match (kwop) - (funcall (cdr (assoc kwop sail-leading-kwop-alist)))) - -(defconst sail-binding-regexp "\\(\\<and\\>\\|(*\\<let\\>\\)") - -(defun sail-assoc-indent (kwop &optional look-for-let-or-and) - "Return relative indentation of the keyword given in argument." - (let ((ind (or (symbol-value (cdr (assoc kwop sail-keyword-alist))) - sail-default-indent)) - (looking-let-or-and (and look-for-let-or-and - (looking-at sail-binding-regexp)))) - (if (string-match (sail-give-extra-unindent-regexp) kwop) - (if (and sail-let-always-indent - looking-let-or-and (< ind sail-let-indent)) - sail-let-indent ind) - ind))) - -(defconst sail-meaningful-word-regexp - "[^ \t\n_[:alnum:]]\\|\\<\\(\\w\\|_\\)+\\>\\|\\*)") -(defun sail-find-meaningful-word () - "Look back for a word, skipping comments and blanks. -Returns the actual text of the word, if found." - (let ((found nil) (kwop nil) (pt (point))) - (while (and (not found) - (re-search-backward sail-meaningful-word-regexp - (point-min) t)) - (setq kwop (sail-match-string 0)) - (cond ((or (string= kwop "=") (string= kwop ">")) - (backward-char 2) - (setq kwop (concat ">>" kwop))) - ((and (string= kwop ">") (char-equal ?- (char-before))) - (backward-char) - (setq kwop "->"))) - (when (= pt (point)) - (error "sail-find-meaningful-word: inf loop at %d, kwop=%s" pt kwop)) - (setq pt (point)) - (if kwop - (if (sail-in-comment-p) - (sail-beginning-of-literal-or-comment-fast) - (setq found t)) - (setq found t))) - (if found kwop (goto-char (point-min)) nil))) - -(defun sail-make-find-kwop-regexp (kwop-regexp) - "Make a custom indentation regexp." - (concat (sail-give-find-kwop-regexp) "\\|" kwop-regexp)) - -;; Static regexps -(defconst sail-find-and-match-regexp - (concat (sail-ro "else" "in" "then" "downto" "by" "from" - "foreach" "if" "function" - "let" "in" "typedef" "val" "end") - "\\|[][(){}]\\|\\*)")) -(defconst sail-find-phrase-beginning-regexp - (concat (sail-ro "end" "typedef" "let") - "\\|^#[ \t]*[a-z][_a-z]*\\>\\|;;")) -(defconst sail-find-phrase-beginning-and-regexp - (concat "\\<\\(and\\)\\>\\|" sail-find-phrase-beginning-regexp)) -(defconst sail-back-to-paren-or-indentation-regexp - "[][(){}]\\|\\.<\\|>\\.\\|\\*)\\|^[ \t]*\\(.\\|\n\\)") - -(defun sail-make-indentation-regexps () - "Initialisation of specific indentation regexp. -Gathered here for memoization and dynamic reconfiguration purposes." - (setq - sail-find-comma-match-regexp - (sail-make-find-kwop-regexp - (concat (sail-ro "and" "switch" "else" "then" "function" "let" "foreach") - "\\|->\\|[[{(]")) - sail-find-with-match-regexp - (sail-make-find-kwop-regexp - (concat (sail-ro "switch" "case" "typedef") - "\\|[[{(]")) - sail-find-in-match-regexp - (sail-make-find-kwop-regexp (sail-ro "let" "function")) - sail-find-else-match-regexp - (sail-make-find-kwop-regexp ";") - sail-find-do-match-regexp - (sail-make-find-kwop-regexp "->") - sail-find-=-match-regexp - (sail-make-find-kwop-regexp - (concat (sail-ro "val" "let" "function" "typedef" "if" "in") - "\\|=")) - sail-find-arrow-match-regexp - (sail-make-find-kwop-regexp - (concat (sail-ro "extern" "typedef" "val" "function" "let") - "\\|[|;]")) - sail-find-semicolon-match-regexp - (sail-make-find-kwop-regexp - (concat ";" sail-no-more-code-this-line-regexp "\\|->\\|" - (sail-ro "let"))) - sail-find-phrase-indentation-regexp - (sail-make-find-kwop-regexp - (concat sail-governing-phrase-regexp "\\|" (sail-ro "and"))) - sail-find-phrase-indentation-break-regexp - (concat sail-find-phrase-indentation-regexp "\\|;") - sail-compute-argument-indent-regexp - (sail-make-find-kwop-regexp - (concat (sail-give-keyword-regexp) "\\|=")) - sail-compute-normal-indent-regexp - (concat sail-compute-argument-indent-regexp "\\|^.[ \t]*") - sail-find-monadic-match-regexp - (concat sail-block-regexp "\\|\\([;=]\\)\\|\\(->\\)\\|" - (sail-ro "val" "let" "function" "typedef" "if" "in" "end")))) - -(defun sail-strip-trailing-whitespace (string) - (if (string-match "[ \t]*\\'" string) - (substring string 0 (match-beginning 0)) - string)) - -(defun sail-find-kwop-pos (kr do-not-skip-regexp may-terminate-early) - "Look back for a keyword or operator matching KR (short for kwop regexp). -Skips blocks etc... - -Ignore occurences inside literals and comments. -If found, return the actual text of the keyword or operator." - (let ((found nil) - (kwop nil) pos - (kwop-regexp kr)) - (while (and (not found) - (setq pos (re-search-backward kwop-regexp (point-min) t)) - (setq kwop (sail-strip-trailing-whitespace - ;; for trailing blanks after a semicolon - (sail-match-string 0)))) - (cond - ((sail-in-literal-or-comment-p) - (sail-beginning-of-literal-or-comment-fast)) - ((looking-at "[>]})]") - (sail-backward-up-list)) - ((sail-at-phrase-break-p) - (setq found t)) - ((and do-not-skip-regexp (looking-at do-not-skip-regexp)) - (if (and (string= kwop "|") (char-equal ?| (preceding-char))) - (backward-char) - (setq found t))) - ((looking-at (sail-give-matching-keyword-regexp)) - (let ((mkwop (sail-find-leading-kwop-match (sail-match-string 0)))) - (when (and may-terminate-early (string-match kwop-regexp mkwop)) - (setq found t)))) - (t - (setq found t)))) - (if found (list kwop pos) (goto-char (point-min)) nil))) - -(defun sail-find-kwop (kr &optional do-not-skip-regexp) - (car (sail-find-kwop-pos kr do-not-skip-regexp nil))) - -(defun sail-find-match () - (let ((kwop (sail-find-kwop (sail-give-find-kwop-regexp)))) - (when (string= kwop "then") - (sail-find-then-match) - (sail-find-match)) - kwop)) - -(defun sail-find-comma-match () - (car (sail-find-kwop-pos sail-find-comma-match-regexp nil t))) - -(defun sail-find-in-match () - (let ((kwop (sail-find-kwop sail-find-in-match-regexp "\\<and\\>"))) - (cond - ((string= kwop "and") - (sail-find-in-match)) - (t - kwop)))) - -(defconst sail-find-then-match-regexp - (sail-make-find-kwop-regexp "\\(->\\)")) -(defun sail-find-then-kwop () - (sail-find-kwop sail-find-then-match-regexp "\\(->\\)")) -(defun sail-find-then-match () - (let ((kwop (sail-find-then-kwop))) - (cond ((string= kwop "if") - (let ((back (point))) - (sail-back-to-paren-or-indentation) - (if (looking-at "else[ \t]*\\((\\*.*\\*)\\)*[ \t]*if") - "else if" - (goto-char back) - kwop))) - (t kwop)))) - -(defun sail-find-then-else-match () - (let ((kwop (sail-find-then-kwop))) - (cond - ((string= kwop "if") - (let ((pos (point))) - (if (and (not (sail-in-indentation-p)) - (string= "else" (sail-find-meaningful-word))) - "else" - (goto-char pos) - kwop))) - (t - kwop)))) - -(defun sail-find-else-match () - (let ((kwop (sail-find-kwop sail-find-else-match-regexp - "\\<then\\>"))) - (cond - ((string= kwop "then") - (sail-find-then-else-match)) - ((string= kwop ";") - (sail-find-semicolon-match) - (sail-find-else-match))))) - - -(defconst sail-done-match-stop-regexp (sail-ro "and")) -(defun sail-find-done-match () - (let ((kwop (sail-find-kwop (sail-give-find-kwop-regexp) - sail-done-match-stop-regexp))) - (cond - ((string= kwop "and") - (sail-find-and-match)) - (t - kwop)))) - -(defun sail-find-and-match () - (let* ((kwop (sail-find-kwop - sail-find-and-match-regexp - (sail-give-and-stop-regexp))) - (old-point (point))) - (cond - ((string= kwop "typedef") - (let ((kwop2 (sail-find-meaningful-word))) - (cond ((string= kwop2 "and") - (sail-find-and-match)) - ((and (string= kwop "function") - (string= kwop2 "let")) - kwop2) - (t (goto-char old-point) kwop)))) - (t kwop)))) - -(defconst sail-=-stop-regexp (concat (sail-ro "and" "in" "function") "\\|=")) -(defun sail-give-=-stop-regexp () sail-=-stop-regexp) - -(defun sail-find-=-match () - (let ((kwop (sail-find-kwop - sail-find-=-match-regexp - (sail-give-=-stop-regexp)))) - (cond - ((string= kwop "and") - (sail-find-and-match)) - ((and (string= kwop "=") - (not (sail-false-=-p))) - (while (and (string= kwop "=") - (not (sail-false-=-p))) - (setq kwop (sail-find-=-match))) - kwop) - (t kwop)))) - -(defconst sail-captive-regexp - (sail-ro "let" "if" "typedef")) -(defun sail-captive-= () - (save-excursion - (sail-find-=-match) - (looking-at sail-captive-regexp))) - - -(defun sail-find-arrow-match () - (let ((kwop (sail-find-kwop (sail-give-find-arrow-match-regexp) - "\\<with\\>"))) - (cond - ((string= kwop "function") - (let ((pos (point))) - (progn (goto-char pos) kwop))) - ((not (string= kwop ":")) - kwop) - ;; If we get this far, we know we're looking at a colon. - ((or (char-equal (char-before) ?:) - (char-equal (char-after (1+ (point))) ?:) - (char-equal (char-after (1+ (point))) ?>)) - (sail-find-arrow-match)) - ;; Patch by T. Freeman - (t - (let ((oldpoint (point)) - (match (sail-find-arrow-match))) - (if (looking-at ":") - match - (progn - ;; Go back to where we were before the recursive call. - (goto-char oldpoint) - kwop))))))) - -(defconst sail-semicolon-match-stop-regexp - (sail-ro "and" "end" "in")) -(defconst sail-no-code-after-paren-regexp - (sail-no-code-after "[[{(][|<]?")) -(defun sail-semicolon-indent-kwop-point (&optional leading-semi-colon) - ;; return (kwop kwop-point indentation) - (let ((kwop (sail-find-kwop sail-find-semicolon-match-regexp - sail-semicolon-match-stop-regexp)) - (point (point))) - ;; We don't need to find the keyword matching `and' since we know it's `let'! - (list - (cond - ((string= kwop ";") - (forward-line 1) - (while (or (sail-in-comment-p) - (looking-at sail-no-code-this-line-regexp)) - (forward-line 1)) - (back-to-indentation) - (current-column)) - ((and leading-semi-colon - (looking-at "\\((\\|\\[[<|]?\\|{<?\\)[ \t]*[^ \t\n]") - (not (looking-at sail-no-code-after-paren-regexp))) - (current-column)) - ;; ((looking-at (tuareg-no-code-after "\\((\\|\\[[<|]?\\|{<?\\)")) - ;; (+ (current-column) tuareg-default-indent)) - ((looking-at "\\(\\.<\\|(\\|\\[[<|]?\\|{<?\\)") ; paren with subsequent text - (sail-search-forward-paren) - (current-column)) - ((string= kwop "->") - (if (save-excursion - (sail-find-arrow-match) - (or (looking-at "\\<function\\>\\||") - (looking-at (sail-give-extra-unindent-regexp)))) - (sail-paren-or-indentation-indent) - (sail-find-semicolon-match))) - ((string= kwop "in") - (sail-find-in-match) - (+ (current-column) sail-in-indent)) - ((string= kwop "let") - (+ (current-column) sail-let-indent)) - (t (sail-paren-or-indentation-indent))) - kwop point))) - -(defun sail-find-semicolon-match (&optional leading-semi-colon) - (car (sail-semicolon-indent-kwop-point leading-semi-colon))) - -(defmacro sail-reset-and-kwop (kwop) - `(when (and ,kwop (string= ,kwop "and")) - (setq ,kwop (sail-find-and-match)))) - -(defconst sail-phrase-regexp-1 (sail-ro "typedef" "end")) -(defconst sail-phrase-regexp-2 (sail-ro "and" "let" "function" "case")) -(defconst sail-phrase-regexp-3 - (sail-ro "and" "in")) -(defun sail-find-phrase-indentation (&optional phrase-break) - (if (and (looking-at sail-phrase-regexp-1) (> (point) (point-min)) - (save-excursion - (sail-find-meaningful-word) - (looking-at sail-phrase-regexp-2))) - (progn - (sail-find-meaningful-word) - (+ (current-column) sail-default-indent)) - (let ((looking-at-and (looking-at "\\<and\\>")) - (kwop (sail-find-kwop - (if phrase-break - sail-find-phrase-indentation-break-regexp - sail-find-phrase-indentation-regexp) - sail-phrase-regexp-3)) - (tmpkwop nil) (curr nil)) - (sail-reset-and-kwop kwop) - (cond ((not kwop) (current-column)) - ((and (string= kwop "in") - (not (save-excursion - (setq tmpkwop (sail-find-in-match)) - (sail-reset-and-kwop tmpkwop) - (setq curr (point)) - (and (string= tmpkwop "let") - (not (sail-looking-at-internal-let)))))) - (goto-char curr) - (sail-find-phrase-indentation phrase-break)) - ((sail-at-phrase-break-p) - (end-of-line) - (sail-skip-blank-and-comments) - (current-column)) - ((string= kwop "let") - (if (sail-looking-at-internal-let) - (sail-find-phrase-indentation phrase-break) - (current-column))) - ((string= kwop "in") - (sail-find-in-match) - (current-column)) - ((looking-at "\\(\\.<\\|(\\|\\[[<|]?\\|{<?\\)[ \t]*[^ \t\n]") - (sail-search-forward-paren) - (current-column)) - (t (current-column)))))) - -(defconst sail-paren-or-indentation-stop-regexp - (sail-ro "and" "in")) -(defun sail-back-to-paren-or-indentation () - "Search backwards for the first open paren in line, or skip to indentation. -Returns t iff skipped to indentation." - (if (or (bolp) (sail-in-indentation-p)) - (progn (back-to-indentation) t) - (let ((kwop (sail-find-kwop - sail-back-to-paren-or-indentation-regexp - sail-paren-or-indentation-stop-regexp)) - (retval)) - (setq retval - (cond - ((string= kwop "in") - (sail-in-indentation-p)) -; ((looking-at "[[{(]") (tuareg-search-forward-paren) nil) -; ((looking-at "\\.<") -; (if tuareg-support-metaocaml -; (progn -; (tuareg-search-forward-paren) nil) -; (tuareg-back-to-paren-or-indentation))) - (t (back-to-indentation) t))) - (cond - ; ((looking-at "|[^|]") - ; (re-search-forward "|[^|][ \t]*") nil) - ((string= kwop "in") - (sail-find-in-match) - (sail-back-to-paren-or-indentation) - (if (looking-at "\\<\\(let\\|and\\)\\>") - (forward-char sail-in-indent)) nil) - (t retval))))) - -(defun sail-paren-or-indentation-column () - (sail-back-to-paren-or-indentation) - (current-column)) - -(defun sail-paren-or-indentation-indent () - (+ (sail-paren-or-indentation-column) sail-default-indent)) - -(defun sail-search-forward-paren () - (re-search-forward "\\(\\.<\\|(\\|\\[[<|]?\\|{|<\\)[ \t]*")) - -(defun sail-add-default-indent (leading-operator) - (if leading-operator 0 sail-default-indent)) - -(defconst sail-internal-let-regexp - (concat "[[({;=]\\|" - (sail-ro "if" "in" "then" "else" "switch"))) -(defun sail-looking-at-internal-let () - (save-excursion - (sail-find-meaningful-word) - (and (not (sail-at-phrase-break-p)) - (or (looking-at sail-internal-let-regexp) - (looking-at sail-operator-regexp))))) - -(defun sail-looking-at-in-let () - (save-excursion - (string= (sail-find-meaningful-word) "in"))) - -(defun sail-indent-from-previous-kwop () - (let* ((start-pos (point)) - (kwop (sail-find-argument-kwop-non-blank t)) - (captive= (and (string= kwop "=") (sail-captive-=))) - (kwop-pos (point))) - (forward-char (length kwop)) - (sail-skip-blank-and-comments) - (cond ((or (not captive=) - (/= (point) start-pos)) ; code between paren and kwop - (goto-char start-pos) - (sail-paren-or-indentation-indent)) - (t - (goto-char kwop-pos) - (when (string= kwop "=") - (setq kwop (sail-find-=-match))) - (+ sail-default-indent - (if (assoc kwop sail-leading-kwop-alist) - (sail-compute-kwop-indent kwop) - (current-column))))))) - -(defun sail-indent-from-paren (leading-operator start-pos) - (cond - ((looking-at (sail-no-code-after "\\(\\(\\.<\\|(\\|\\[[<|]?\\|{\\|<\\)\\)")) - (cond ((sail-in-indentation-p) - (+ sail-default-indent - (current-column))) - (t (sail-indent-from-previous-kwop)))) - ((looking-at "([ \t]*\\(\\w\\)") - (goto-char (match-beginning 1)) - (current-column)) - (t - (+ (sail-add-default-indent leading-operator) - (current-column))))) - -(defun sail-skip-to-next-form (old-point) - (while (and (not (looking-at sail-no-more-code-this-line-regexp)) - (< (point) old-point)) ; do not go beyond old-point - (forward-sexp 1)) - (sail-skip-blank-and-comments) - (sail-back-to-paren-or-indentation)) - -(defun sail-find-argument-kwop (leading-operator) - (sail-find-kwop (if leading-operator - sail-compute-argument-indent-regexp - sail-compute-normal-indent-regexp) - (sail-give-keyword-regexp))) - -(defun sail-find-argument-kwop-clean (leading-operator) - (let (kwop) - (while (or (progn (setq kwop (sail-find-argument-kwop leading-operator)) - (sail-reset-and-kwop kwop) - nil) - (and (string= kwop "=") (sail-false-=-p)) - (and (looking-at sail-no-code-this-line-regexp) - (not (= (point) (point-min)))))) - kwop)) - -(defun sail-find-argument-kwop-non-blank (leading-operator) - (let ((kwop "") (point (1+ (point)))) - (while (and (> point (point)) (string= "" kwop)) - (setq point (point) - kwop (sail-find-argument-kwop-clean leading-operator))) - kwop)) - -(defun sail-compute-argument-indent (leading-operator) - (let* ((old-point (line-beginning-position)) - (kwop (sail-find-argument-kwop-non-blank leading-operator)) - (match-end-point (+ (point) (length kwop)))) ; match-end is invalid! - (cond - ((let (matching-kwop matching-pos) - (save-excursion - (setq matching-kwop (sail-find-arrow-match)) - (setq matching-pos (point))) - (cond - ((or (string= matching-kwop "val") (string= matching-kwop "let") (string= matching-kwop "function")) - (+ (current-column) sail-val-indent)) - (t - (+ (sail-paren-or-indentation-column) - (sail-add-default-indent leading-operator)))))) - ((string= kwop "function") - (+ (sail-paren-or-indentation-column) - (sail-add-default-indent leading-operator) - (sail-assoc-indent kwop))) - ((<= old-point (point)) - (+ (sail-add-default-indent leading-operator) - (current-column))) - (t - (goto-char match-end-point) ; skip kwop == (forward-char (length kwop)) - (sail-skip-to-next-form old-point) - (+ (sail-add-default-indent - (if (save-excursion (goto-char match-end-point) - (looking-at sail-no-more-code-this-line-regexp)) - (or leading-operator (string= kwop "{") - (looking-at (sail-no-code-after "[[:upper:]].*\\."))) - (not (looking-at sail-operator-regexp)))) - (current-column)))))) - -(defun sail-compute-arrow-indent (start-pos) - (let (kwop pos) - (save-excursion (setq kwop (sail-find-arrow-match) pos (point))) - (cond ((or (string= kwop "val") - (string= kwop "let")) - (goto-char pos) - (+ (current-column) sail-val-indent)) - ((string= kwop "typedef") - (goto-char pos) - (+ (current-column) sail-type-indent - sail-default-indent)) - ((string= kwop "(") - (goto-char pos) - (sail-indent-after-next-char)) - ((or (string= kwop "{") - (string= kwop ";")) - (if (and (looking-at "->") - (search-backward ":" pos t)) - (sail-indent-after-next-char) - (sail-back-to-paren-or-indentation) - (current-column))) - (t (sail-paren-or-indentation-indent))))) - -(defun sail-compute-keyword-indent (kwop leading-operator start-pos) - (cond ((string= kwop ";") - (if (looking-at (sail-no-code-after ";")) - (let* ((pos (point)) (indent (sail-find-semicolon-match))) - (if (looking-at sail-phrase-regexp-1) - (progn - (goto-char start-pos) - (if (search-backward ":" pos t) - (sail-indent-after-next-char) - indent)) - indent)) - (sail-paren-or-indentation-indent))) - ((string= kwop ",") - (if (looking-at (sail-no-code-after ",")) - (let ((mkwop (sail-find-comma-match))) - (cond ((or (string= mkwop "[") - (string= mkwop "{") - (string= mkwop "(") - (string= mkwop "<") - (string- mkwop "[|")) - (forward-char 1) (skip-syntax-forward " ") - (current-column)) - ((looking-at "[[{(]\\|\\<") - (sail-indent-from-paren t start-pos)) - ((or (and (looking-at "[<|]") - (char-equal ?\[ (preceding-char))) - (and (looking-at "<") - (char-equal ?\{ (preceding-char)))) - (sail-backward-char) - (sail-indent-from-paren t start-pos)) - ((and (looking-at "\\<let\\>") (string= mkwop "in")) - (+ (current-column) sail-in-indent)) - (t (+ (sail-paren-or-indentation-column) - (sail-assoc-indent mkwop))))) - (sail-paren-or-indentation-indent))) - ((or (string= kwop "function") (string= kwop "and")) - (sail-back-to-paren-or-indentation) - (+ (sail-paren-or-indentation-indent) - (sail-assoc-indent kwop t))) - ((string-match "\\<\\(function\\)\\>" kwop) - (+ (sail-paren-or-indentation-column) - (sail-add-default-indent leading-operator) - (sail-assoc-indent kwop t))) - ((string-match (sail-give-extra-unindent-regexp) kwop) - (+ (sail-paren-or-indentation-column) - (sail-assoc-indent kwop t))) - ((string= kwop "in") - (when (looking-at (sail-no-code-after "\\<in\\>")) - (sail-find-in-match)) - (+ (current-column) - sail-in-indent)) - ((string-match (sail-give-matching-kwop-regexp) kwop) - (sail-find-leading-kwop-match kwop) - (if (sail-in-indentation-p) - (+ (current-column) - (sail-assoc-indent kwop t)) - (sail-back-to-paren-or-indentation) - (+ (sail-paren-or-indentation-indent) - (sail-assoc-indent kwop t)))) - (t (+ (if (sail-in-indentation-p) - (current-column) - (sail-paren-or-indentation-indent)) - (sail-assoc-indent kwop t))))) - -(defconst sail-=-indent-regexp-1 - (sail-ro "val" "let" "function" "scattered" "foreach" "if")) - -(defun sail-compute-=-indent (start-pos) - (let ((current-column-module-type nil) (kwop1 (sail-find-=-match)) - (next-pos (point))) - (+ (save-excursion - (sail-reset-and-kwop kwop1) - (cond ((string= kwop1 "typedef") - (sail-find-meaningful-word) - (cond (t (goto-char start-pos) - (beginning-of-line) - (+ (sail-add-default-indent - (looking-at "[ \t]*[\[|]")) - sail-type-indent)))) - ((looking-at sail-=-indent-regexp-1) - (let ((matched-string (sail-match-string 0))) - (setq current-column-module-type (current-column)) - (sail-assoc-indent matched-string))) - ((looking-at sail-no-code-after-paren-regexp) - (setq current-column-module-type - (sail-indent-from-paren nil next-pos)) - sail-default-indent) - (t (setq current-column-module-type - (sail-paren-or-indentation-indent)) - sail-default-indent))) - (or current-column-module-type - (current-column))))) - -(defun sail-indent-after-next-char () - (forward-char 1) - (sail-skip-blank-and-comments) - (current-column)) - -(defconst sail-definitions-regexp - (sail-ro "and" "val" "typedef" "scattered" "function" "default" "register" "let") - "Regexp matching definition phrases.") - -(defun sail-compute-normal-indent () - (let ((leading-operator (looking-at sail-operator-regexp))) - (beginning-of-line) - (save-excursion - (let ((start-pos (point)) - (kwop (sail-find-argument-kwop-clean leading-operator))) - (cond - ((not kwop) (current-column)) - ((sail-at-phrase-break-p) - (sail-find-phrase-indentation t)) - ((or (looking-at "[[{(<]") - (and (looking-at "[<|]") - (char-equal ?\[ (preceding-char)) - (progn (sail-backward-char) t)) - (and (looking-at "<") - (char-equal ?\{ (preceding-char)) - (progn (sail-backward-char) t))) - (cond ((looking-at "{ *[A-Z]") - (forward-char 1) (skip-syntax-forward " ") - (current-column)) - ((looking-at (sail-no-code-after "[[{(][<|]?")) - (sail-indent-from-paren leading-operator start-pos)) - ((and leading-operator (string= kwop "(")) - (sail-indent-after-next-char)) - (t (+ sail-default-indent - (sail-indent-from-paren leading-operator start-pos))))) - ((looking-at (sail-give-keyword-regexp)) - (sail-compute-keyword-indent kwop leading-operator start-pos)) - ((and (string= kwop "=") (not (sail-false-=-p)) - (or (null leading-operator) - ;; defining "=", not testing for equality - (string-match sail-definitions-regexp - (save-excursion - (sail-find-argument-kwop-clean t))))) - (sail-compute-=-indent start-pos)) - (nil 0) - (t (sail-compute-argument-indent leading-operator))))))) - -(defun sail-compute-paren-indent (paren-match-p old-point) - (unless paren-match-p - (sail-search-forward-paren)) - (let ((looking-at-paren (char-equal ?\( (char-after))) (start-pos (point))) - (when (or looking-at-paren - (looking-at (sail-no-code-after "\\(\{\\(.*with[ \t]*\\([[:upper:]].*\\.\\)?\\)?\\|\\[\\)"))) - (if (sail-in-indentation-p) - (sail-back-to-paren-or-indentation) - (sail-indent-from-previous-kwop)) - (when looking-at-paren - (skip-chars-forward "( \t" start-pos)) - (while (and (looking-at "[([{]") - (> (scan-sexps (point) 1) - (save-excursion (goto-char old-point) - (line-end-position)))) - (forward-char 1) - (skip-syntax-forward " ")))) - (current-column)) - -(defun sail-compute-kwop-indent-general (kwop matching-kwop) - (let* ((looking-at-matching (looking-at matching-kwop)) - (extra-unindent ; non-paren code before matching-kwop - (unless (save-excursion - (skip-chars-backward "( \t" (line-beginning-position)) - (bolp)) - (sail-back-to-paren-or-indentation) - t))) - (+ (current-column) - (sail-add-default-indent - (or (not (string= kwop "then")) - looking-at-matching))))) - -(defun sail-compute-kwop-indent (kwop) - (when (string= kwop "rec") - (setq kwop "and")) - (let* ((old-point (point)) - (paren-match-p (looking-at "[|>]?[]})]\\|>\\.")) - (real-pipe (looking-at "|\\([^|]\\|$\\)")) - (matching-kwop (sail-find-leading-kwop-match kwop))) - (cond ((looking-at "[[{(][<|]?\\|\\.<") - (sail-compute-paren-indent paren-match-p old-point)) - ((string= kwop "and") - (if (sail-in-indentation-p) - (current-column) - (sail-paren-or-indentation-column))) - ((string= kwop "in") - (+ (current-column) - (sail-add-default-indent (string= matching-kwop "let")))) - ((not (string= kwop "and")) ; pretty general case - (sail-compute-kwop-indent-general kwop matching-kwop)) - (t (sail-paren-or-indentation-column))))) - -(defun sail-indent-to-code (beg-pos match) - (unless (and (string= match "(") - (search-forward "->" beg-pos t)) - (forward-char (length match))) - (sail-skip-blank-and-comments) - (current-column)) - -(defun sail-indent-command (&optional from-leading-star) - "Indent the current line in Sail mode. - -Compute new indentation based on Sail syntax." - (interactive "*") - (unless from-leading-star - (sail-auto-fill-insert-leading-star)) - (let ((case-fold-search nil)) - (sail-with-internal-syntax - (save-excursion - (back-to-indentation) - (indent-line-to (max 0 (sail-compute-indent)))) - (when (sail-in-indentation-p) (back-to-indentation))))) - -(defun sail-compute-indent () - (save-excursion - (cond - ((sail-in-comment-p) - (cond - ((looking-at "(\\*") - (if sail-indent-leading-comments - (save-excursion - (sail-skip-blank-and-comments) - (back-to-indentation) - (current-column)) - (current-column))) - ((looking-at "\\*\\**)") - (sail-beginning-of-literal-or-comment-fast) - (if (sail-leading-star-p) - (+ (current-column) - (if (save-excursion - (forward-line 1) - (back-to-indentation) - (looking-at "*")) 1 - sail-comment-end-extra-indent)) - (+ (current-column) sail-comment-end-extra-indent))) - (sail-indent-comments - (let ((star (and (sail-leading-star-p) - (looking-at "\\*")))) - (sail-beginning-of-literal-or-comment-fast) - (if star (re-search-forward "(") (re-search-forward "(\\*+[ \t]*")) - (current-column))) - (t (current-column)))) - ((sail-in-literal-p) - (current-column)) - ((looking-at "\\<let\\>") - (if (sail-looking-at-internal-let) - (if (sail-looking-at-in-let) - (progn - (sail-find-meaningful-word) - (sail-find-in-match) - (current-column)) - (sail-compute-normal-indent)) - (sail-find-phrase-indentation))) - ((or (looking-at sail-governing-phrase-regexp) - (looking-at ";")) - (sail-find-phrase-indentation)) - ((looking-at ";") - (sail-find-semicolon-match t)) - ((or (looking-at (sail-give-matching-kwop-regexp)) - (looking-at "\\<rec\\>")) - (sail-compute-kwop-indent (sail-match-string 0))) - (t (sail-compute-normal-indent))))) - -(defun sail-split-string () - "Called whenever a line is broken inside an Sail string literal." - (insert-before-markers "\\ ") - (sail-backward-char)) - -(defadvice newline-and-indent (around - sail-newline-and-indent - activate) - "Handle multi-line strings in Sail mode." - (let ((hooked (and (eq major-mode 'sail-mode) (sail-in-literal-p))) - (split-mark)) - (when hooked - (setq split-mark (set-marker (make-marker) (point))) - (sail-split-string)) - ad-do-it - (when hooked - (goto-char split-mark) - (set-marker split-mark nil)))) - -(defun sail-electric-rp () - "If inserting a ) operator or a comment-end at beginning of line, -reindent the line." - (interactive "*") - (let ((electric (and sail-electric-indent - (or (sail-in-indentation-p) - (char-equal ?* (preceding-char))) - (not (sail-in-literal-p)) - (or (not (sail-in-comment-p)) - (save-excursion - (back-to-indentation) - (looking-at "\\*")))))) - (self-insert-command 1) - (and electric - (indent-according-to-mode)))) - -(defun sail-electric-lt () - "If inserting a > operator or a comment-end at beginning of line, -reindent the line." - (interactive "*") - (let ((electric (and sail-electric-indent - (or (sail-in-indentation-p) - (char-equal ?* (preceding-char))) - (not (sail-in-literal-p)) - (or (not (sail-in-comment-p)) - (save-excursion - (back-to-indentation) - (looking-at "\\*")))))) - (self-insert-command 1) - (and electric - (indent-according-to-mode)))) - -(defun sail-electric-rc () - "If inserting a } operator at beginning of line, reindent the line." - (interactive "*") - (let* ((prec (preceding-char)) - (look-bra (and sail-electric-close-range - (not (sail-in-literal-or-comment-p)) - (not (char-equal ?> prec)))) - (electric (and sail-electric-indent - (or (sail-in-indentation-p) - (and (char-equal ?> prec) - (save-excursion (sail-backward-char) - (sail-in-indentation-p)))) - (not (sail-in-literal-or-comment-p))))) - (self-insert-command 1) - (when look-bra - (save-excursion - (let ((inserted-char - (save-excursion - (sail-backward-char) - (sail-backward-up-list) - (cond ((looking-at "{<") ">") - (t ""))))) - (sail-backward-char) - (insert inserted-char)))) - (when electric (indent-according-to-mode)))) - -(defun sail-electric-rb () - "If inserting a ] operator at beginning of line, reindent the line. - -Reindent also if ] is inserted after a | operator at beginning of line. -Also, if the matching [ is followed by a | and this ] is not preceded -by |, insert one |." - (interactive "*") - (let* ((prec (preceding-char)) - (look-pipe-or-bra (and sail-electric-close-range - (not (sail-in-literal-or-comment-p)) - (not (and (char-equal ?| prec) - (not (char-equal - (save-excursion - (sail-backward-char) - (preceding-char)) ?\[)))))) - (electric (and sail-electric-indent - (or (sail-in-indentation-p) - (and (char-equal ?| prec) - (save-excursion (sail-backward-char) - (sail-in-indentation-p)))) - (not (sail-in-literal-or-comment-p))))) - (self-insert-command 1) - (when look-pipe-or-bra - (save-excursion - (let ((inserted-char - (save-excursion - (sail-backward-char) - (sail-backward-up-list) - (cond ((looking-at "\\[|") "\\|") - (t ""))))) - (sail-backward-char) - (insert inserted-char)))) - (when electric (indent-according-to-mode)))) - -(defun sail-abbrev-hook () - "If inserting a leading keyword at beginning of line, reindent the line." - (unless (sail-in-literal-or-comment-p) - (let* ((bol (line-beginning-position)) - (kw (save-excursion - (and (re-search-backward "^[ \t]*\\(\\w\\|_\\)+\\=" bol t) - (sail-match-string 1))))) - (when kw - (insert " ") - (indent-according-to-mode) - (backward-delete-char-untabify 1))))) - -(defun sail-skip-to-end-of-phrase () - (let ((old-point (point))) - (when (and (string= (sail-find-meaningful-word) ";") - (char-equal (preceding-char) ?\;)) - (setq old-point (1- (point)))) - (goto-char old-point) - (let ((kwop (sail-find-meaningful-word))) - (goto-char (+ (point) (length kwop)))))) - -(defun sail-skip-blank-and-comments () - (skip-syntax-forward " ") - (while (and (not (eobp)) (sail-in-comment-p) - (search-forward "*)" nil t)) - (skip-syntax-forward " "))) - -(defun sail-skip-back-blank-and-comments () - (skip-syntax-backward " ") - (while (save-excursion (sail-backward-char) - (and (> (point) (point-min)) (sail-in-comment-p))) - (sail-backward-char) - (sail-beginning-of-literal-or-comment) (skip-syntax-backward " "))) - -(defun sail-find-phrase-beginning (&optional stop-at-and) - "Find `real' phrase beginning and return point." - (beginning-of-line) - (sail-skip-blank-and-comments) - (end-of-line) - (sail-skip-to-end-of-phrase) - (let ((old-point (point)) (pt (point))) - (if stop-at-and - (sail-find-kwop sail-find-phrase-beginning-and-regexp "and") - (sail-find-kwop sail-find-phrase-beginning-regexp)) - (while (and (> (point) (point-min)) (< (point) old-point) - (or (not (looking-at sail-find-phrase-beginning-and-regexp)) - (and (looking-at "\\<let\\>") - (sail-looking-at-internal-let)) - (and (looking-at "\\<and\\>") - (save-excursion - (sail-find-and-match) - (sail-looking-at-internal-let))) - ) - (when (= pt (point)) - (error "sail-find-phrase-beginning: inf loop at %d" pt)) - (setq pt (point)) - (if (looking-at "\\<end\\>") - (sail-find-match) - (unless (bolp) (sail-backward-char)) - (setq old-point (point)) - (if stop-at-and - (sail-find-kwop sail-find-phrase-beginning-and-regexp "and") - (sail-find-kwop sail-find-phrase-beginning-regexp)))) - (when (sail-at-phrase-break-p) - (end-of-line) (sail-skip-blank-and-comments)) - (back-to-indentation) - (point)))) - -(defun sail-imenu-prev-index-position () - "The default value for `imenu-prev-index-position-function'." - (let ((pos (point)) ret) - (while (and (<= 0 pos) - (<= pos (setq ret (sail-find-phrase-beginning t)))) - (setq pos (goto-char (1- pos)))) - (and (<= 0 pos) ret))) - -(defun sail-imenu-extract-index-name () - "The default value for `imenu-extract-index-name-function'." - (forward-sexp 1) - (skip-syntax-forward " ") - (buffer-substring-no-properties (point) (scan-sexps (point) 1))) - -(defun sail-mark-phrase () - "Put mark at end of this Sail phrase, point at beginning. -The Sail phrase is the phrase just before the point." - (interactive) - (let ((pair (sail-discover-phrase))) - (goto-char (nth 1 pair)) (push-mark (nth 0 pair) t t))) - -(defun sail-next-phrase (&optional quiet stop-at-and) - "Skip to the beginning of the next phrase." - (interactive "i") - (goto-char (save-excursion - (nth 2 (sail-discover-phrase quiet stop-at-and)))) - (cond - ((looking-at "}") - (forward-char 1) - (sail-skip-blank-and-comments)) - ((looking-at ")") - (forward-char 1) - (sail-skip-blank-and-comments)) - ((looking-at ";") - (forward-char 1) - (sail-skip-blank-and-comments)))) - -(defun sail-previous-phrase () - "Skip to the beginning of the previous phrase." - (interactive) - (beginning-of-line) - (sail-skip-to-end-of-phrase) - (sail-discover-phrase)) - -(defun sail-indent-phrase () - "Depending of the context: justify and indent a comment, -or indent all lines in the current phrase." - (interactive) - (save-excursion - (back-to-indentation) - (if (sail-in-comment-p) - (let* ((cobpoint (save-excursion - (sail-beginning-of-literal-or-comment) - (point))) - (begpoint (save-excursion - (while (and (> (point) cobpoint) - (sail-in-comment-p) - (not (looking-at "^[ \t]*$"))) - (forward-line -1)) - (max cobpoint (point)))) - (coepoint (save-excursion - (while (sail-in-comment-p) - (re-search-forward "\\*)" nil 'end)) - (point))) - (endpoint (save-excursion - (re-search-forward "^[ \t]*$" coepoint 'end) - (line-beginning-position 2))) - (leading-star (sail-leading-star-p))) - (goto-char begpoint) - (while (and leading-star - (< (point) endpoint) - (not (looking-at "^[ \t]*$"))) - (forward-line 1) - (back-to-indentation) - (when (looking-at "\\*\\**\\([^)]$\\)") - (delete-char 1) - (setq endpoint (1- endpoint)))) - (goto-char (min (point) endpoint)) - (fill-region begpoint endpoint) - (re-search-forward "\\*)" nil 'end) - (setq endpoint (point)) - (when leading-star - (goto-char begpoint) - (forward-line 1) - (if (< (point) endpoint) - (sail-auto-fill-insert-leading-star t))) - (indent-region begpoint endpoint nil)) - (let ((pair (sail-discover-phrase))) - (indent-region (nth 0 pair) (nth 1 pair) nil))))) - -(defun sail-complete (arg) - "Completes qualified Sail identifiers." - (interactive "p") - (modify-syntax-entry ?_ "w" sail-mode-syntax-table) - (caml-complete arg) - (modify-syntax-entry ?_ "_" sail-mode-syntax-table)) - -(defun sail-ensure-space () - (let ((prec (preceding-char))) - (when (and prec (not (char-equal ?\ (char-syntax prec)))) - (insert " ")))) - -(defun sail-insert-if-form () - "Insert a nicely formatted if-then-else form, leaving a mark after else." - (interactive "*") - (sail-ensure-space) - (let ((old (point))) - (insert "if\n\nthen\n\nelse\n") - (end-of-line) - (indent-region old (point) nil) - (indent-according-to-mode) - (push-mark) - (forward-line -2) - (indent-according-to-mode) - (forward-line -2) - (indent-according-to-mode))) - -(defun sail-insert-let-form () - "Insert a nicely formatted let-in form, leaving a mark after in." - (interactive "*") - (sail-ensure-space) - (let ((old (point))) - (insert "let in\n") - (end-of-line) - (indent-region old (point) nil) - (indent-according-to-mode) - (push-mark) - (beginning-of-line) - (backward-char 4) - (indent-according-to-mode))) - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; Menu support - -(defun sail-about () - (interactive) - (describe-variable 'sail-mode-version)) - -(defun sail-short-cuts () - "Short cuts for the sail mode: -\\{sail-mode-map} - -" - (interactive) - (describe-function 'sail-short-cuts)) - -(defun sail-help () - (interactive) - (describe-function 'sail-mode)) - -(defvar sail-definitions-menu (list ["Scan..." sail-list-definitions t]) - "Initial content of the definitions menu.") -(make-variable-buffer-local 'sail-definitions-menu) - -(defvar sail-definitions-menu-last-buffer nil) -(defvar sail-definitions-keymaps nil) - -(defun sail-build-menu () - (easy-menu-define - sail-mode-menu (list sail-mode-map) - "Sail Mode Menu." - '("Sail" - ("Sail Forms" - ["let .. in .." sail-insert-let-form t] - ["if .. then .. else .." sail-insert-if-form t]) - "---" - ["Customize Sail Mode..." (customize-group 'sail) t] - ("Sail Options" ["Dummy" nil t]) - "---" - ["About" sail-about t] - ["Short Cuts" sail-short-cuts] - ["Help" sail-help t])) - (easy-menu-add sail-mode-menu) - (sail-update-options-menu) - ;; Save and update definitions menu - (when (functionp 'easy-menu-create-menu) - ;; Patch for Emacs - (add-hook 'menu-bar-update-hook - 'sail-with-emacs-update-definitions-menu) - (make-local-variable 'sail-definitions-keymaps) - (setq sail-definitions-keymaps - (cdr (easy-menu-create-menu - "Definitions" sail-definitions-menu))) - (setq sail-definitions-menu-last-buffer nil))) - -(defun sail-update-definitions-menu () - (when (eq major-mode 'sail-mode) - (easy-menu-change - '("Sail") "Definitions" - sail-definitions-menu))) - -(defun sail-with-emacs-update-definitions-menu () - (when (current-local-map) - (let ((keymap - (lookup-key (current-local-map) [menu-bar Sail Definitions]))) - (if (and - (keymapp keymap) - (not (eq sail-definitions-menu-last-buffer (current-buffer)))) - (setcdr keymap sail-definitions-keymaps) - (setq sail-definitions-menu-last-buffer (current-buffer)))))) - -(defun sail-toggle-option (symbol) - (interactive) - (set symbol (not (symbol-value symbol))) - (when (eq 'sail-use-abbrev-mode symbol) - (abbrev-mode sail-use-abbrev-mode)) ; toggle abbrev minor mode - (sail-update-options-menu)) - -(defun sail-update-options-menu () - (easy-menu-change - '("Sail") "Sail Options" - (mapcar (lambda (pair) - (if (consp pair) - (vector (car pair) - (list 'sail-toggle-option (cdr pair)) - ':style 'toggle - ':selected (nth 1 (cdr pair)) - ':active t) - pair)) sail-options-list)) - ) - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; Definitions List - -;; Designed from original code by M. Quercia - -(defconst sail--id-regexp "[[:alpha:]][_'[:alnum:]]*") - -(defconst sail-definitions-bind-skip-regexp - (concat (sail-ro "rec" "typedef" "function") "\\'" - sail--id-regexp "\\|('.*)") - "Regexp matching stuff to ignore after a binding keyword.") - -(defconst sail-identifier-regexp (concat "\\<" sail--id-regexp "\\>")) - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; Hooks and Exit - -(eval-when-compile - (autoload 'speedbar-add-supported-extension "speedbar")) -(when (require 'speedbar nil t) - (speedbar-add-supported-extension - '(".sail"))) - -(defvar sail-load-hook nil - "This hook is run when Sail is loaded in. It is a good place to put -key-bindings or hack Font-Lock keywords...") - -(run-hooks 'sail-load-hook) + (set-syntax-table sail2-mode-syntax-table) + (setq font-lock-defaults '(sail2-font-lock-keywords)) + (setq comment-start-skip "\\(//+\\|/\\*+\\)\\s *") + (setq comment-start "/*") + (setq comment-end "*/") + (setq major-mode 'sail2-mode) + (setq mode-name "Sail2") + (run-hooks 'sail2-mode-hook)) -(provide 'sail-mode) +(provide 'sail2-mode) -;;; sail.el ends here diff --git a/editors/sail2-mode.el b/editors/sail2-mode.el deleted file mode 100644 index 54973aa4..00000000 --- a/editors/sail2-mode.el +++ /dev/null @@ -1,67 +0,0 @@ - -(defvar sail2-mode-hook nil) - -(add-to-list 'auto-mode-alist '("\\.sail\\'" . sail2-mode)) - -(defconst sail2-keywords - '("val" "function" "type" "struct" "union" "enum" "let" "var" "if" "then" "by" - "else" "match" "in" "return" "register" "ref" "forall" "operator" "effect" - "overload" "cast" "sizeof" "constant" "constraint" "default" "assert" "newtype" "from" - "pure" "infixl" "infixr" "infix" "scattered" "end" "try" "catch" "and" "to" - "throw" "clause" "as" "repeat" "until" "while" "do" "foreach" "bitfield" - "mapping" "where" "with")) - -(defconst sail2-kinds - '("Int" "Type" "Order" "Bool" "inc" "dec" - "barr" "depend" "rreg" "wreg" "rmem" "rmemt" "wmv" "wmvt" "eamem" "wmem" - "exmem" "undef" "unspec" "nondet" "escape" "configuration")) - -(defconst sail2-types - '("vector" "int" "nat" "atom" "range" "unit" "bit" "real" "list" "bool" "string" "bits" "option" - "uint64_t" "int64_t" "bv_t" "mpz_t")) - -(defconst sail2-special - '("_prove" "_not_prove" "_check" "_not_check" "create" "kill" "convert" "undefined" - "$define" "$include" "$ifdef" "$ifndef" "$else" "$endif" "$option" "$latex")) - -(defconst sail2-font-lock-keywords - `((,(regexp-opt sail2-keywords 'symbols) . font-lock-keyword-face) - (,(regexp-opt sail2-kinds 'symbols) . font-lock-builtin-face) - (,(regexp-opt sail2-types 'symbols) . font-lock-type-face) - (,(regexp-opt sail2-special 'symbols) . font-lock-preprocessor-face) - ("~" . font-lock-negation-char-face) - ("\\(::\\)<" 1 font-lock-keyword-face) - ("@" . font-lock-preprocessor-face) - ("<->" . font-lock-negation-char-face) - ("\'[a-zA-Z0-9_]+" . font-lock-variable-name-face) - ("\\([a-zA-Z0-9_]+\\)(" 1 font-lock-function-name-face) - ("function \\([a-zA-Z0-9_]+\\)" 1 font-lock-function-name-face) - ("val \\([a-zA-Z0-9_]+\\)" 1 font-lock-function-name-face) - ("\\_<\\([0-9]+\\|0b[0-9_]+\\|0x[0-9a-fA-F_]+\\|true\\|false\\|bitone\\|bitzero\\)\\_>\\|()" . font-lock-constant-face))) - -(defconst sail2-mode-syntax-table - (let ((st (make-syntax-table))) - (modify-syntax-entry ?> "." st) - (modify-syntax-entry ?_ "w" st) - (modify-syntax-entry ?' "w" st) - (modify-syntax-entry ?* ". 23" st) - (modify-syntax-entry ?/ ". 124b" st) - (modify-syntax-entry ?\n "> b" st) - st) - "Syntax table for Sail2 mode") - -(defun sail2-mode () - "Major mode for editing Sail Language files" - (interactive) - (kill-all-local-variables) - (set-syntax-table sail2-mode-syntax-table) - (setq font-lock-defaults '(sail2-font-lock-keywords)) - (setq comment-start-skip "\\(//+\\|/\\*+\\)\\s *") - (setq comment-start "/*") - (setq comment-end "*/") - (setq major-mode 'sail2-mode) - (setq mode-name "Sail2") - (run-hooks 'sail2-mode-hook)) - -(provide 'sail2-mode) - diff --git a/lib/coq/Makefile b/lib/coq/Makefile index a5f2874b..6dd962d1 100644 --- a/lib/coq/Makefile +++ b/lib/coq/Makefile @@ -1,8 +1,8 @@ -BBV_DIR=../../../bbv/theories +BBV_DIR?=../../../bbv SRC=Sail2_prompt_monad.v Sail2_prompt.v Sail2_impl_base.v Sail2_instr_kinds.v Sail2_operators_bitlists.v Sail2_operators_mwords.v Sail2_operators.v Sail2_values.v Sail2_state_monad.v Sail2_state.v Sail2_string.v Sail2_real.v -COQ_LIBS = -R . Sail -R "$(BBV_DIR)" bbv +COQ_LIBS = -R . Sail -R "$(BBV_DIR)/theories" bbv TARGETS=$(SRC:.v=.vo) diff --git a/lib/isabelle/Makefile b/lib/isabelle/Makefile index 57459b82..039a81f1 100644 --- a/lib/isabelle/Makefile +++ b/lib/isabelle/Makefile @@ -7,7 +7,9 @@ EXTRA_THYS = Sail2_state_monad_lemmas.thy Sail2_state_lemmas.thy \ Sail2_prompt_monad_lemmas.thy \ Sail2_operators_mwords_lemmas.thy Hoare.thy -RISCV_DIR = ../../riscv +LEM_ISA_LIB?=$(shell opam config var lem:share)/isabelle-lib + +SAIL_RISCV ?= ../../../sail-riscv .PHONY: all heap-img clean @@ -16,16 +18,15 @@ all: thys thys: $(THYS) heap-img: thys $(EXTRA_THYS) ROOT - @echo '*** To build a heap image with the Sail library, please' - @echo '*** add this directory to your ROOTS file' - @echo '*** (e.g. $$HOME/.isabelle/Isabelle<version>/ROOTS)' - @echo '*** and add the isabelle binary to your PATH.' - isabelle build -b Sail +ifeq ($(wildcard $(LEM_ISA_LIB)/ROOT),) + $(error isabelle-lib directory of Lem not found. Please set the LEM_ISA_LIB environment variable) +endif + isabelle build -d $(LEM_ISA_LIB) -D . manual: heap-img manual/Manual.thy manual/ROOT manual/document/root.tex cp output/document/session_graph.pdf manual/document/Sail_session_graph.pdf - make -C $(RISCV_DIR) Riscv_duopod.thy - isabelle build -d manual -d $(RISCV_DIR) Sail-Manual + make -C $(SAIL_RISCV) riscv_duopod + isabelle build -d $(LEM_ISA_LIB) -d . -d $(SAIL_RISCV)/generated_definitions/isabelle -D manual Sail2_instr_kinds.thy: ../../src/lem_interp/sail2_instr_kinds.lem lem -isa -outdir . -auxiliary_level none -lib ../../src/lem_interp -lib ../../src/gen_lib $< @@ -238,6 +238,21 @@ bool write_ram(const mpz_t addr_size, // Either 32 or 64 return true; } +sbits fast_read_ram(const int64_t data_size, + const uint64_t addr) +{ + uint64_t r = 0; + + uint64_t byte; + for(uint64_t i = (uint64_t) data_size; i > 0; --i) { + byte = read_mem(addr + (i - 1)); + r = r << 8; + r = r + byte; + } + sbits res = {.len = data_size * 8, .bits = r }; + return res; +} + void read_ram(lbits *data, const mpz_t addr_size, const mpz_t data_size_mpz, @@ -65,6 +65,9 @@ void read_ram(lbits *data, const lbits hex_ram, const lbits addr_bv); +sbits fast_read_ram(const int64_t data_size, + const uint64_t addr_bv); + unit write_tag_bool(const fbits, const bool); bool read_tag_bool(const fbits); @@ -1,6 +1,6 @@ opam-version: "1.2" name: "sail" -version: "0.6" +version: "0.7.1" maintainer: "Sail Devs <cl-sail-dev@lists.cam.ac.uk>" authors: [ "Alasdair Armstrong" diff --git a/src/ast_util.ml b/src/ast_util.ml index c0e9fe02..26c6b9df 100644 --- a/src/ast_util.ml +++ b/src/ast_util.ml @@ -165,7 +165,7 @@ module Kind = struct | K_type, _ -> 1 | _, K_type -> -1 | K_order, _ -> 1 | _, K_order -> -1 end - + module KOpt = struct type t = kinded_id let compare kopt1 kopt2 = @@ -1362,6 +1362,9 @@ let is_fundef id = function | DEF_fundef (FD_aux (FD_function (_, _, _, FCL_aux (FCL_Funcl (id', _), _) :: _), _)) when Id.compare id' id = 0 -> true | _ -> false +let rename_valspec id (VS_aux (VS_val_spec (typschm, _, externs, is_cast), annot)) = + VS_aux (VS_val_spec (typschm, id, externs, is_cast), annot) + let rename_funcl id (FCL_aux (FCL_Funcl (_, pexp), annot)) = FCL_aux (FCL_Funcl (id, pexp), annot) let rename_fundef id (FD_aux (FD_function (ropt, topt, eopt, funcls), annot)) = @@ -1498,7 +1501,7 @@ let locate_id f (Id_aux (name, l)) = Id_aux (name, f l) let locate_kid f (Kid_aux (name, l)) = Kid_aux (name, f l) let locate_kind f (K_aux (kind, l)) = K_aux (kind, f l) - + let locate_kinded_id f (KOpt_aux (KOpt_kind (k, kid), l)) = KOpt_aux (KOpt_kind (locate_kind f k, locate_kid f kid), f l) diff --git a/src/ast_util.mli b/src/ast_util.mli index 8787dbff..d9b0110a 100644 --- a/src/ast_util.mli +++ b/src/ast_util.mli @@ -385,6 +385,8 @@ val is_valspec : id -> 'a def -> bool val is_fundef : id -> 'a def -> bool +val rename_valspec : id -> 'a val_spec -> 'a val_spec + val rename_fundef : id -> 'a fundef -> 'a fundef val split_defs : ('a def -> bool) -> 'a defs -> ('a defs * 'a def * 'a defs) option diff --git a/src/c_backend.ml b/src/c_backend.ml index 6e21dab6..5e600918 100644 --- a/src/c_backend.ml +++ b/src/c_backend.ml @@ -1399,9 +1399,11 @@ let compile_type_def ctx (TD_aux (type_def, _)) = CTD_struct (id, Bindings.bindings ctors), { ctx with records = Bindings.add id ctors ctx.records } - | TD_variant (id, _, tus, _) -> + | TD_variant (id, typq, tus, _) -> let compile_tu = function - | Tu_aux (Tu_ty_id (typ, id), _) -> ctyp_of_typ ctx typ, id + | Tu_aux (Tu_ty_id (typ, id), _) -> + let ctx = { ctx with local_env = add_typquant (id_loc id) typq ctx.local_env } in + ctyp_of_typ ctx typ, id in let ctus = List.fold_left (fun ctus (ctyp, id) -> Bindings.add id ctyp ctus) Bindings.empty (List.map compile_tu tus) in CTD_variant (id, Bindings.bindings ctus), @@ -1763,6 +1765,9 @@ let rec compile_def n total ctx = function (* Only the parser and sail pretty printer care about this. *) | DEF_fixity _ -> [], ctx + (* We just ignore any pragmas we don't want to deal with. *) + | DEF_pragma _ -> [], ctx + | DEF_internal_mutrec fundefs -> let defs = List.map (fun fdef -> DEF_fundef fdef) fundefs in List.fold_left (fun (cdefs, ctx) def -> let cdefs', ctx = compile_def n total ctx def in (cdefs @ cdefs', ctx)) ([], ctx) defs diff --git a/src/constraint.ml b/src/constraint.ml index af024ce3..b7fa50c3 100644 --- a/src/constraint.ml +++ b/src/constraint.ml @@ -133,16 +133,17 @@ let to_smt l vars constr = | _ -> raise (Reporting.err_unreachable l __POS__ "Tried to pass Type or Order kind to SMT function") in - var_decs l vars, smt_constraint constr + var_decs l vars, smt_constraint constr, smt_var -let smtlib_of_constraints ?get_model:(get_model=false) l vars constr : string = - let variables, problem = to_smt l vars constr in +let smtlib_of_constraints ?get_model:(get_model=false) l vars constr : string * (kid -> sexpr) = + let variables, problem, var_map = to_smt l vars constr in "(push)\n" ^ variables ^ "\n" ^ pp_sexpr (sfun "define-fun" [Atom "constraint"; List []; Atom "Bool"; problem]) ^ "\n(assert constraint)\n(check-sat)" ^ (if get_model then "\n(get-model)" else "") - ^ "\n(pop)" + ^ "\n(pop)", + var_map type smt_result = Unknown | Sat | Unsat @@ -185,7 +186,7 @@ let save_digests () = let call_z3' l vars constraints : smt_result = let problems = [constraints] in - let z3_file = smtlib_of_constraints l vars constraints in + let z3_file, _ = smtlib_of_constraints l vars constraints in if !opt_smt_verbose then prerr_endline (Printf.sprintf "SMTLIB2 constraints are: \n%s%!" z3_file) @@ -243,9 +244,11 @@ let call_z3 l vars constraints = result let rec solve_z3 l vars constraints var = - let z3_file = smtlib_of_constraints ~get_model:true l vars constraints in + let z3_file, smt_var = smtlib_of_constraints ~get_model:true l vars constraints in + let z3_var = pp_sexpr (smt_var var) in - (* prerr_endline (Printf.sprintf "SMTLIB2 constraints are: \n%s%!" z3_file); *) + (* prerr_endline (Printf.sprintf "SMTLIB2 constraints are: \n%s%!" z3_file); + prerr_endline ("Solving for " ^ z3_var); *) let rec input_all chan = try @@ -270,7 +273,7 @@ let rec solve_z3 l vars constraints var = raise (Reporting.err_general l ("Got error when calling z3: " ^ Printexc.to_string exn)) in Sys.remove input_file; - let regexp = {|(define-fun v|} ^ Util.zencode_string (string_of_kid var) ^ {| () Int[ ]+\([0-9]+\))|} in + let regexp = {|(define-fun |} ^ z3_var ^ {| () Int[ ]+\([0-9]+\))|} in try let _ = Str.search_forward (Str.regexp regexp) z3_output 0 in let result = Big_int.of_string (Str.matched_group 1 z3_output) in diff --git a/src/latex.ml b/src/latex.ml index 2f578f2c..a0660daa 100644 --- a/src/latex.ml +++ b/src/latex.ml @@ -57,6 +57,7 @@ module StringSet = Set.Make(String);; let opt_prefix = ref "sail" let opt_directory = ref "sail_latex" +let opt_simple_val = ref true let rec unique_postfix n = if n < 0 then @@ -97,13 +98,13 @@ let rec unique_postfix n = type id_category = | Function | Val - | Overload + | Overload of int | FunclCtor of id * int | FunclNum of int | FunclApp of string + | Type -let replace_numbers str = - let replacements = +let number_replacements = [ ("0", "Zero"); ("1", "One"); ("2", "Two"); @@ -114,16 +115,28 @@ let replace_numbers str = ("7", "Seven"); ("8", "Eight"); ("9", "Nine") ] - in + +(* add to this as needed *) +let other_replacements = + [ ("_", "Underscore") ] + +let char_replace str replacements = List.fold_left (fun str (from, into) -> Str.global_replace (Str.regexp_string from) into str) str replacements +let replace_numbers str = + char_replace str number_replacements + +let replace_others str = + char_replace str other_replacements + let category_name = function | Function -> "fn" | Val -> "val" - | Overload -> "overload" + | Type -> "type" + | Overload n -> "overload" ^ unique_postfix n | FunclNum n -> "fcl" ^ unique_postfix n | FunclCtor (id, n) -> - let str = replace_numbers (Util.zencode_string (string_of_id id)) in + let str = replace_others (replace_numbers (Util.zencode_string (string_of_id id))) in "fcl" ^ String.sub str 1 (String.length str - 1) ^ unique_postfix n | FunclApp str -> "fcl" ^ str @@ -134,7 +147,8 @@ let category_name_val = function let category_name_simple = function | Function -> "fn" | Val -> "val" - | Overload -> "overload" + | Type -> "type" + | Overload n -> "overload" | FunclNum _ -> "fcl" | FunclCtor (_, _) -> "fcl" | FunclApp _ -> "fcl" @@ -162,8 +176,8 @@ let latex_id id = (* If we have any other weird symbols in the id, remove them using Util.zencode_string (removing the z prefix) *) let str = Util.zencode_string str in let str = String.sub str 1 (String.length str - 1) in - (* Latex only allows letters in identifiers, so replace all numbers *) - let str = replace_numbers str in + (* Latex only allows letters in identifiers, so replace all numbers and other characters *) + let str = replace_others (replace_numbers str) in let generated = state.generated_names |> Bindings.bindings |> List.map snd |> StringSet.of_list in @@ -290,10 +304,10 @@ let latex_loc no_loc l = let commands = ref StringSet.empty -let doc_spec_simple (VS_val_spec(ts,id,ext,is_cast)) = - Pretty_print_sail.doc_id id ^^ space - ^^ colon ^^ space - ^^ Pretty_print_sail.doc_typschm ~simple:true ts +let doc_spec_simple (VS_aux (VS_val_spec (ts, id, ext, is_cast), _)) = + Pretty_print_sail.doc_id id ^^ space + ^^ colon ^^ space + ^^ Pretty_print_sail.doc_typschm ~simple:true ts let rec latex_command cat id no_loc ((l, _) as annot) = state.this <- Some id; @@ -309,7 +323,7 @@ let rec latex_command cat id no_loc ((l, _) as annot) = output_string chan (Pretty_print_sail.to_string doc); close_out chan; - ksprintf string "\\newcommand{\\sail%s%s}{\\phantomsection%s\\saildoc%s{" (category_name cat) (latex_id id) labelling (category_name_simple cat) + ksprintf string "\\newcommand{\\%s%s%s}{\\phantomsection%s\\saildoc%s{" !opt_prefix (category_name cat) (latex_id id) labelling (category_name_simple cat) ^^ docstring l ^^ string "}{" ^^ ksprintf string "\\lstinputlisting[language=sail]{%s}}}" (Filename.concat !opt_directory code_file) @@ -381,30 +395,47 @@ let process_pragma l command = Util.warn (Printf.sprintf "Bad latex pragma %s" (Reporting.loc_to_string l)); None +let tdef_id = function + | TD_abbrev (id, _, _) -> id + | TD_record (id, _, _, _) -> id + | TD_variant (id, _, _, _) -> id + | TD_enum (id, _, _) -> id + | TD_bitfield (id, _, _) -> id + let defs (Defs defs) = reset_state state; + let overload_counter = ref 0 in + let valspecs = ref IdSet.empty in let fundefs = ref IdSet.empty in + let typedefs = ref IdSet.empty in let latex_def def = match def with - | DEF_overload (id, ids) -> None - (* + | DEF_overload (id, ids) -> let doc = string (Printf.sprintf "overload %s = {%s}" (string_of_id id) (Util.string_of_list ", " string_of_id ids)) in - Some (latex_command Overload id doc (id_loc id, None)) - *) + incr overload_counter; + Some (latex_command (Overload !overload_counter) id doc (id_loc id, None)) - | DEF_spec (VS_aux (VS_val_spec (_, id, _, _) as vs, annot)) as def -> + | DEF_spec (VS_aux (VS_val_spec (_, id, _, _), annot) as vs) as def -> valspecs := IdSet.add id !valspecs; - Some (latex_command Val id (doc_spec_simple vs) annot) + if !opt_simple_val then + Some (latex_command Val id (doc_spec_simple vs) annot) + else + Some (latex_command Val id (Pretty_print_sail.doc_spec ~comment:false vs) annot) | DEF_fundef (FD_aux (FD_function (_, _, _, [FCL_aux (FCL_Funcl (id, _), _)]), annot)) as def -> fundefs := IdSet.add id !fundefs; Some (latex_command Function id (Pretty_print_sail.doc_def def) annot) + | DEF_type (TD_aux (tdef, annot)) as def -> + let id = tdef_id tdef in + typedefs := IdSet.add id !typedefs; + Some (latex_command Type id (Pretty_print_sail.doc_def def) annot) + | DEF_fundef (FD_aux (FD_function (_, _, _, funcls), annot)) as def -> Some (latex_funcls def funcls) @@ -432,7 +463,7 @@ let defs (Defs defs) = identifiers then outputs the correct mangled command. *) let id_command cat ids = sprintf "\\newcommand{\\%s%s}[1]{\n " !opt_prefix (category_name cat) - ^ Util.string_of_list "%\n " (fun id -> sprintf "\\ifstrequal{#1}{%s}{\\sail%s%s}{}" (string_of_id id) (category_name cat) (latex_id id)) + ^ Util.string_of_list "%\n " (fun id -> sprintf "\\ifstrequal{#1}{%s}{\\%s%s%s}{}" (string_of_id id) !opt_prefix (category_name cat) (latex_id id)) (IdSet.elements ids) ^ "}" |> string @@ -449,5 +480,7 @@ let defs (Defs defs) = ^^ separate (twice hardline) [id_command Val !valspecs; ref_command Val !valspecs; id_command Function !fundefs; - ref_command Function !fundefs] + ref_command Function !fundefs; + id_command Type !typedefs; + ref_command Type !typedefs] ^^ hardline diff --git a/src/monomorphise.ml b/src/monomorphise.ml index 1b7fb3b4..2124c11e 100644 --- a/src/monomorphise.ml +++ b/src/monomorphise.ml @@ -3424,7 +3424,7 @@ let rec sets_from_assert e = match e with | E_app (Id_aux (Id "or_bool",_),[e1;e2]) -> aux e1 @ aux e2 - | E_app (Id_aux (Id "eq_atom",_), + | E_app (Id_aux (Id "eq_int",_), [E_aux (E_sizeof (Nexp_aux (Nexp_var kid,_)),_); E_aux (E_lit (L_aux (L_num i,_)),_)]) -> (check_kid kid; [i]) @@ -4040,7 +4040,7 @@ let rec extract_value_from_guard var (E_aux (e,_)) = match e with | E_app (op, ([E_aux (E_id var',_); E_aux (E_lit (L_aux (L_num i,_)),_)] | [E_aux (E_lit (L_aux (L_num i,_)),_); E_aux (E_id var',_)])) - when string_of_id op = "eq_atom" && Id.compare var var' == 0 -> + when string_of_id op = "eq_int" && Id.compare var var' == 0 -> Some i | E_app (op, [e1;e2]) when string_of_id op = "and_bool" -> (match extract_value_from_guard var e1 with @@ -4053,7 +4053,8 @@ let fill_in_type env typ = let subst = KidSet.fold (fun kid subst -> match Env.get_typ_var kid env with | K_type - | K_order -> subst + | K_order + | K_bool -> subst | K_int -> (match solve env (nvar kid) with | None -> subst @@ -4108,7 +4109,7 @@ let add_bitvector_casts (Defs defs) = | E_app (op, ([E_aux (E_sizeof (Nexp_aux (Nexp_var kid,_)),_); y] | [y; E_aux (E_sizeof (Nexp_aux (Nexp_var kid,_)),_)])) - when string_of_id op = "eq_atom" -> + when string_of_id op = "eq_int" -> (match destruct_atom_nexp (env_of y) (typ_of y) with | Some (Nexp_aux (Nexp_constant i,_)) -> [(kid,i)] | _ -> []) diff --git a/src/optimize.ml b/src/optimize.ml new file mode 100644 index 00000000..a372abf4 --- /dev/null +++ b/src/optimize.ml @@ -0,0 +1,100 @@ +(**************************************************************************) +(* Sail *) +(* *) +(* Copyright (c) 2013-2017 *) +(* Kathyrn Gray *) +(* Shaked Flur *) +(* Stephen Kell *) +(* Gabriel Kerneis *) +(* Robert Norton-Wright *) +(* Christopher Pulte *) +(* Peter Sewell *) +(* Alasdair Armstrong *) +(* Brian Campbell *) +(* Thomas Bauereiss *) +(* Anthony Fox *) +(* Jon French *) +(* Dominic Mulligan *) +(* Stephen Kell *) +(* Mark Wassell *) +(* *) +(* All rights reserved. *) +(* *) +(* This software was developed by the University of Cambridge Computer *) +(* Laboratory as part of the Rigorous Engineering of Mainstream Systems *) +(* (REMS) project, funded by EPSRC grant EP/K008528/1. *) +(* *) +(* Redistribution and use in source and binary forms, with or without *) +(* modification, are permitted provided that the following conditions *) +(* are met: *) +(* 1. Redistributions of source code must retain the above copyright *) +(* notice, this list of conditions and the following disclaimer. *) +(* 2. Redistributions in binary form must reproduce the above copyright *) +(* notice, this list of conditions and the following disclaimer in *) +(* the documentation and/or other materials provided with the *) +(* distribution. *) +(* *) +(* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' *) +(* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED *) +(* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A *) +(* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR *) +(* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, *) +(* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT *) +(* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF *) +(* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND *) +(* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, *) +(* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT *) +(* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF *) +(* SUCH DAMAGE. *) +(**************************************************************************) + +open Ast +open Ast_util +open Rewriter + +let recheck (Defs defs) = + let defs = Type_check.check_with_envs Type_check.initial_env defs in + + let rec find_optimizations = function + | ([DEF_pragma ("optimize", pragma, p_l)], env) + :: ([DEF_spec vs as def1], _) + :: ([DEF_fundef fdef as def2], _) + :: defs -> + let id = id_of_val_spec vs in + let args = Str.split (Str.regexp " +") (String.trim pragma) in + begin match args with + | ["unroll"; n]-> + let n = int_of_string n in + + let rw_app subst (fn, args) = + if Id.compare id fn = 0 then E_app (subst, args) else E_app (fn, args) + in + let rw_exp subst = { id_exp_alg with e_app = rw_app subst } in + let rw_defs subst = { rewriters_base with rewrite_exp = (fun _ -> fold_exp (rw_exp subst)) } in + + let specs = ref [def1] in + let bodies = ref [rewrite_def (rw_defs (append_id id "_unroll_1")) def2] in + + for i = 1 to n do + let current_id = append_id id ("_unroll_" ^ string_of_int i) in + let next_id = if i = n then current_id else append_id id ("_unroll_" ^ string_of_int (i + 1)) in + (* Create a valspec for the new unrolled function *) + specs := !specs @ [DEF_spec (rename_valspec current_id vs)]; + (* Then duplicate it's function body and make it call the next unrolled function *) + bodies := !bodies @ [rewrite_def (rw_defs next_id) (DEF_fundef (rename_fundef current_id fdef))] + done; + + !specs @ !bodies @ find_optimizations defs + + | _ -> + Util.warn ("Unrecognised optimize pragma in this context: " ^ pragma); + def1 :: def2 :: find_optimizations defs + end + + | (defs, _) :: defs' -> + defs @ find_optimizations defs' + + | [] -> [] + in + + Defs (find_optimizations defs) diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml index 169bd824..8cef3529 100644 --- a/src/pretty_print_lem.ml +++ b/src/pretty_print_lem.ml @@ -359,14 +359,14 @@ let replace_typ_size ctxt env (Typ_aux (t,a)) = let mk_typ nexp = Some (Typ_aux (Typ_app (id, [A_aux (A_nexp nexp,Parse_ast.Unknown);ord;typ']),a)) in - match Type_check.solve env size with - | Some n -> mk_typ (nconstant n) - | None -> - let is_equal nexp = - prove __POS__ env (NC_aux (NC_equal (size,nexp),Parse_ast.Unknown)) - in match List.find is_equal (NexpSet.elements ctxt.bound_nexps) with - | nexp -> mk_typ nexp - | exception Not_found -> None + let is_equal nexp = + prove __POS__ env (NC_aux (NC_equal (size,nexp),Parse_ast.Unknown)) + in match List.find is_equal (NexpSet.elements ctxt.bound_nexps) with + | nexp -> mk_typ nexp + | exception Not_found -> + match Type_check.solve env size with + | Some n -> mk_typ (nconstant n) + | None -> None end | _ -> None diff --git a/src/process_file.ml b/src/process_file.ml index ed34238b..00013775 100644 --- a/src/process_file.ml +++ b/src/process_file.ml @@ -51,6 +51,10 @@ open PPrint open Pretty_print_common +let opt_lem_output_dir = ref None +let opt_isa_output_dir = ref None +let opt_coq_output_dir = ref None + type out_type = | Lem_out of string list | Coq_out of string list @@ -254,19 +258,24 @@ let check_ast (env : Type_check.Env.t) (defs : unit Ast.defs) : Type_check.tanno (ast, env) -let open_output_with_check file_name = +let open_output_with_check opt_dir file_name = let (temp_file_name, o) = Filename.open_temp_file "ll_temp" "" in let o' = Format.formatter_of_out_channel o in - (o', (o, temp_file_name, file_name)) + (o', (o, temp_file_name, opt_dir, file_name)) -let open_output_with_check_unformatted file_name = +let open_output_with_check_unformatted opt_dir file_name = let (temp_file_name, o) = Filename.open_temp_file "ll_temp" "" in - (o, temp_file_name, file_name) + (o, temp_file_name, opt_dir, file_name) let always_replace_files = ref true -let close_output_with_check (o, temp_file_name, file_name) = +let close_output_with_check (o, temp_file_name, opt_dir, file_name) = let _ = close_out o in + let file_name = match opt_dir with + | None -> file_name + | Some dir -> if Sys.file_exists dir then () + else Unix.mkdir dir 0o775; + Filename.concat dir file_name in let do_replace = !always_replace_files || (not (Util.same_content_files temp_file_name file_name)) in let _ = if (not do_replace) then Sys.remove temp_file_name else Util.move_file temp_file_name file_name in @@ -308,22 +317,22 @@ let output_lem filename libs type_env defs = string "end" ] ^^ hardline in - let ((ot,_, _) as ext_ot) = - open_output_with_check_unformatted (filename ^ "_types" ^ ".lem") in - let ((o,_, _) as ext_o) = - open_output_with_check_unformatted (filename ^ ".lem") in + let ((ot,_,_,_) as ext_ot) = + open_output_with_check_unformatted !opt_lem_output_dir (filename ^ "_types" ^ ".lem") in + let ((o,_,_,_) as ext_o) = + open_output_with_check_unformatted !opt_lem_output_dir (filename ^ ".lem") in (Pretty_print.pp_defs_lem (ot, base_imports) (o, base_imports @ (String.capitalize_ascii types_module :: libs)) type_env defs generated_line); close_output_with_check ext_ot; close_output_with_check ext_o; - let ((ol, _, _) as ext_ol) = - open_output_with_check_unformatted (isa_thy_name ^ ".thy") in + let ((ol,_,_,_) as ext_ol) = + open_output_with_check_unformatted !opt_isa_output_dir (isa_thy_name ^ ".thy") in print ol isa_lemmas; close_output_with_check ext_ol -let output_coq filename libs defs = +let output_coq opt_dir filename libs defs = let generated_line = generated_line filename in let types_module = (filename ^ "_types") in let monad_modules = ["Sail2_prompt_monad"; "Sail2_prompt"; "Sail2_state"] in @@ -336,10 +345,10 @@ let output_coq filename libs defs = operators_module ] @ monad_modules in - let ((ot,_, _) as ext_ot) = - open_output_with_check_unformatted (filename ^ "_types" ^ ".v") in - let ((o,_, _) as ext_o) = - open_output_with_check_unformatted (filename ^ ".v") in + let ((ot,_,_,_) as ext_ot) = + open_output_with_check_unformatted opt_dir (filename ^ "_types" ^ ".v") in + let ((o,_,_,_) as ext_o) = + open_output_with_check_unformatted opt_dir (filename ^ ".v") in (Pretty_print_coq.pp_defs_coq (ot, base_imports) (o, base_imports @ (types_module :: libs)) @@ -357,7 +366,7 @@ let output1 libpath out_arg filename type_env defs = | Lem_out libs -> output_lem f' libs type_env defs | Coq_out libs -> - output_coq f' libs defs + output_coq !opt_coq_output_dir f' libs defs let output libpath out_arg files = List.iter @@ -374,7 +383,7 @@ let rewrite_step n total defs (name, rewriter) = begin let filename = f ^ "_rewrite_" ^ string_of_int i ^ "_" ^ name ^ ".sail" in (* output "" Lem_ast_out [filename, defs]; *) - let ((ot,_, _) as ext_ot) = open_output_with_check_unformatted filename in + let ((ot,_,_,_) as ext_ot) = open_output_with_check_unformatted None filename in Pretty_print_sail.pp_defs ot defs; close_output_with_check ext_ot; opt_ddump_rewrite_ast := Some (f, i + 1) diff --git a/src/process_file.mli b/src/process_file.mli index 181443fb..74d847a5 100644 --- a/src/process_file.mli +++ b/src/process_file.mli @@ -71,6 +71,10 @@ val opt_ddump_tc_ast : bool ref val opt_ddump_rewrite_ast : ((string * int) option) ref val opt_dno_cast : bool ref +val opt_lem_output_dir : (string option) ref +val opt_isa_output_dir : (string option) ref +val opt_coq_output_dir : (string option) ref + type out_type = | Lem_out of string list (* If present, the strings are files to open in the lem backend*) | Coq_out of string list (* If present, the strings are files to open in the coq backend*) diff --git a/src/rewrites.ml b/src/rewrites.ml index 19ec6db7..67b6518f 100644 --- a/src/rewrites.ml +++ b/src/rewrites.ml @@ -5162,7 +5162,7 @@ let rewrite_defs_c = [ ("trivial_sizeof", rewrite_trivial_sizeof); ("sizeof", rewrite_sizeof); ("merge_function_clauses", merge_funcls); - ("recheck_defs", recheck_defs) + ("recheck_defs", Optimize.recheck) ] let rewrite_defs_interpreter = [ diff --git a/src/sail.ml b/src/sail.ml index 6e5e7556..be2a6198 100644 --- a/src/sail.ml +++ b/src/sail.ml @@ -111,6 +111,9 @@ let options = Arg.align ([ ( "-latex", Arg.Tuple [Arg.Set opt_print_latex; Arg.Clear Type_check.opt_expand_valspec ], " pretty print the input to latex"); + ( "-latex_full_valspecs", + Arg.Clear Latex.opt_simple_val, + " print full valspecs in latex output latex"); ( "-c", Arg.Tuple [Arg.Set opt_print_c; Arg.Set Initial_check.opt_undefined_gen], " output a C translated version of the input"); @@ -149,6 +152,12 @@ let options = Arg.align ([ ( "-lem", Arg.Set opt_print_lem, " output a Lem translated version of the input"); + ( "-lem_output_dir", + Arg.String (fun dir -> Process_file.opt_lem_output_dir := Some dir), + " set a custom directory to output generated Lem"); + ( "-isa_output_dir", + Arg.String (fun dir -> Process_file.opt_isa_output_dir := Some dir), + " set a custom directory to output generated Isabelle auxiliary theories"); ( "-lem_lib", Arg.String (fun l -> opt_libs_lem := l::!opt_libs_lem), "<filename> provide additional library to open in Lem output"); @@ -161,6 +170,9 @@ let options = Arg.align ([ ( "-coq", Arg.Set opt_print_coq, " output a Coq translated version of the input"); + ( "-coq_output_dir", + Arg.String (fun dir -> Process_file.opt_coq_output_dir := Some dir), + " set a custom directory to output generated Coq"); ( "-coq_lib", Arg.String (fun l -> opt_libs_coq := l::!opt_libs_coq), "<filename> provide additional library to open in Coq output"); diff --git a/src/sail_lib.ml b/src/sail_lib.ml index c0bf80fa..d1a21b73 100644 --- a/src/sail_lib.ml +++ b/src/sail_lib.ml @@ -508,6 +508,13 @@ let read_ram (addr_size, data_size, hex_ram, addr) = Bytes.iter (fun byte -> vector := (byte_of_int (int_of_char byte)) @ !vector) bytes; !vector +let fast_read_ram (data_size, addr) = + let addr = uint addr in + let bytes = read_mem_bytes addr (Big_int.to_int data_size) in + let vector = ref [] in + Bytes.iter (fun byte -> vector := (byte_of_int (int_of_char byte)) @ !vector) bytes; + !vector + let tag_ram = (ref Mem.empty : (bool Mem.t) ref);; let write_tag_bool (addr, tag) = diff --git a/src/state.ml b/src/state.ml index fb065440..74bc97b2 100644 --- a/src/state.ml +++ b/src/state.ml @@ -135,20 +135,20 @@ let generate_initial_regstate defs = let typ_subst_typquant tq args typ = List.fold_left2 typ_subst_quant_item typ (quant_items tq) args in - let add_typ_init_val vals = function + let add_typ_init_val (defs', vals) = function | TD_enum (id, id1 :: _, _) -> (* Choose the first value of an enumeration type as default *) - Bindings.add id (fun _ -> string_of_id id1) vals + (defs', Bindings.add id (fun _ -> string_of_id id1) vals) | TD_variant (id, tq, (Tu_aux (Tu_ty_id (typ1, id1), _)) :: _, _) -> (* Choose the first variant of a union type as default *) let init_val args = let typ1 = typ_subst_typquant tq args typ1 in string_of_id id1 ^ " (" ^ lookup_init_val vals typ1 ^ ")" in - Bindings.add id init_val vals + (defs', Bindings.add id init_val vals) | TD_abbrev (id, tq, A_aux (A_typ typ, _)) -> let init_val args = lookup_init_val vals (typ_subst_typquant tq args typ) in - Bindings.add id init_val vals + (defs', Bindings.add id init_val vals) | TD_record (id, tq, fields, _) -> let init_val args = let init_field (typ, id) = @@ -157,16 +157,21 @@ let generate_initial_regstate defs = in "struct { " ^ (String.concat ", " (List.map init_field fields)) ^ " }" in - Bindings.add id init_val vals + let def_name = "initial_" ^ string_of_id id in + if quant_items tq = [] && not (is_defined defs def_name) then + (defs' @ ["let " ^ def_name ^ " : " ^ string_of_id id ^ " = " ^ init_val []], + Bindings.add id (fun _ -> def_name) vals) + else (defs', Bindings.add id init_val vals) | TD_bitfield (id, typ, _) -> - Bindings.add id (fun _ -> lookup_init_val vals typ) vals - | _ -> vals + (defs', Bindings.add id (fun _ -> lookup_init_val vals typ) vals) + | _ -> (defs', vals) in - let init_vals = List.fold_left (fun vals def -> match def with - | DEF_type (TD_aux (td, _)) -> add_typ_init_val vals td - | _ -> vals) Bindings.empty defs + let (init_defs, init_vals) = List.fold_left (fun inits def -> match def with + | DEF_type (TD_aux (td, _)) -> add_typ_init_val inits td + | _ -> inits) ([], Bindings.empty) defs in let init_reg (typ, id) = string_of_id id ^ " = " ^ lookup_init_val init_vals typ in + init_defs @ ["let initial_regstate : regstate = struct { " ^ (String.concat ", " (List.map init_reg registers)) ^ " }"] with | _ -> [] (* Do not generate an initial register state if anything goes wrong *) diff --git a/src/type_check.ml b/src/type_check.ml index 11d5e6a0..0da7bb8e 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -4448,14 +4448,18 @@ let check_val_spec env (VS_aux (vs, (l, _))) = typ_print (lazy (Util.("Check val spec " |> cyan |> clear) ^ string_of_id id ^ " : " ^ string_of_typschm typschm)); let env = Env.add_extern id ext_opt env in let env = if is_cast then Env.add_cast id env else env in + let typq', typ' = expand_bind_synonyms ts_l env (typq, typ) in + (* !opt_expand_valspec controls whether the actual valspec in + the AST is expanded, the val_spec type stored in the + environment is always expanded and uses typq' and typ' *) let typq, typ = if !opt_expand_valspec then - expand_bind_synonyms ts_l env (typq, typ) + (typq', typ') else (typq, typ) in let vs = VS_val_spec (TypSchm_aux (TypSchm_ts (typq, typ), ts_l), id, ext_opt, is_cast) in - (vs, id, typq, typ, env) + (vs, id, typq', typ', env) in let eff = match typ with @@ -4635,6 +4639,14 @@ and check_defs : 'a. int -> int -> Env.t -> 'a def list -> tannot defs * Env.t = and check : 'a. Env.t -> 'a defs -> tannot defs * Env.t = fun env (Defs defs) -> let total = List.length defs in check_defs 1 total env defs +and check_with_envs : 'a. Env.t -> 'a def list -> (tannot def list * Env.t) list = + fun env defs -> + match defs with + | [] -> [] + | def :: defs -> + let def, env = check_def env def in + (def, env) :: check_with_envs env defs + let initial_env = Env.empty |> Env.add_prover (prove __POS__) diff --git a/src/type_check.mli b/src/type_check.mli index 522074b3..2663c1c7 100644 --- a/src/type_check.mli +++ b/src/type_check.mli @@ -417,5 +417,9 @@ Some invariants that will hold of a fully checked AST are: Type_error.check *) val check : Env.t -> 'a defs -> tannot defs * Env.t +(** The same as [check], but exposes the intermediate type-checking + environments so we don't have to always re-check the entire AST *) +val check_with_envs : Env.t -> 'a def list -> (tannot def list * Env.t) list + (** The initial type checking environment *) val initial_env : Env.t diff --git a/test/c/nonexistent_pragma.expect b/test/c/nonexistent_pragma.expect new file mode 100644 index 00000000..9daeafb9 --- /dev/null +++ b/test/c/nonexistent_pragma.expect @@ -0,0 +1 @@ +test diff --git a/test/c/nonexistent_pragma.sail b/test/c/nonexistent_pragma.sail new file mode 100644 index 00000000..da4b99f7 --- /dev/null +++ b/test/c/nonexistent_pragma.sail @@ -0,0 +1,12 @@ +default Order dec + +$include <prelude.sail> + +$not_a_valid_pragma test + +val "print_endline" : string -> unit + +function main((): unit) -> unit = { + print_endline("test") +} + diff --git a/test/c/unroll.expect b/test/c/unroll.expect new file mode 100644 index 00000000..355943c1 --- /dev/null +++ b/test/c/unroll.expect @@ -0,0 +1,6 @@ +fac(4) = 24 +fac(5) = 120 +fac(6) = 720 +fac2(4) = 24 +fac2(5) = 120 +fac2(6) = 720 diff --git a/test/c/unroll.sail b/test/c/unroll.sail new file mode 100644 index 00000000..c68bb49d --- /dev/null +++ b/test/c/unroll.sail @@ -0,0 +1,37 @@ +default Order dec + +$include <prelude.sail> + +/* It's hard to test that this optimization does the right thing, but +we can at least test that it doesn't do the wrong thing. */ + +$optimize unroll 20 +val fac : forall 'n, 'n >= 0. int('n) -> int +function fac(n) = { + if n == 0 then { + 1 + } else { + n * fac(n - 1) + } +} + +$optimize unroll 2 +val fac2 : forall 'n, 'n >= 0. int('n) -> int +function fac2(n) = { + if n == 0 then { + 1 + } else { + n * fac2(n - 1) + } +} + +val "print_int" : (string, int) -> unit + +function main((): unit) -> unit = { + print_int("fac(4) = ", fac(4)); + print_int("fac(5) = ", fac(5)); + print_int("fac(6) = ", fac(6)); + print_int("fac2(4) = ", fac2(4)); + print_int("fac2(5) = ", fac2(5)); + print_int("fac2(6) = ", fac2(6)) +}
\ No newline at end of file diff --git a/test/isabelle/Makefile b/test/isabelle/Makefile index 43028fed..1f488db1 100644 --- a/test/isabelle/Makefile +++ b/test/isabelle/Makefile @@ -1,7 +1,13 @@ -CHERI_DIR = ../../cheri -AARCH64_DIR = ../../aarch64 +LEM_ISA_LIB?=$(shell opam config var lem:share)/isabelle-lib +ifeq ($(wildcard $(LEM_ISA_LIB)/ROOT),) +$(error isabelle-lib directory of Lem not found. Please set the LEM_ISA_LIB environment variable) +endif + +SAIL_ISA_LIB = ../../lib/isabelle +CHERI_DIR ?= ../../../sail-cheri-mips/cheri +AARCH64_DIR ?= ../../aarch64 TGTS = run_cheri.native run_aarch64.native -SESSION_DIRS = -d $(CHERI_DIR) -d $(AARCH64_DIR) -d . +SESSION_DIRS = -d $(LEM_ISA_LIB) -d $(SAIL_ISA_LIB) -d $(CHERI_DIR) -d $(AARCH64_DIR) -d . .PHONY: all clean diff --git a/test/typecheck/pass/nonexistent_pragma.sail b/test/typecheck/pass/nonexistent_pragma.sail new file mode 100644 index 00000000..da4b99f7 --- /dev/null +++ b/test/typecheck/pass/nonexistent_pragma.sail @@ -0,0 +1,12 @@ +default Order dec + +$include <prelude.sail> + +$not_a_valid_pragma test + +val "print_endline" : string -> unit + +function main((): unit) -> unit = { + print_endline("test") +} + |