diff --git a/Agda.cabal b/Agda.cabal --- a/Agda.cabal +++ b/Agda.cabal @@ -1,6 +1,6 @@ name: Agda -version: 2.2.0 -cabal-version: >= 1.4 && < 2 +version: 2.2.2 +cabal-version: >= 1.6 && < 2 build-type: Simple license: OtherLicense license-file: LICENSE @@ -18,18 +18,33 @@ Emacs interface (the type checker can assist in the development of your code). . - Agda is a proof assistant: It is an interactive system for writing - and checking proofs. Agda is based on intuitionistic type theory, a - foundational system for constructive mathematics developed by the - Swedish logician Per Martin-Löf. It has many similarities with other - proof assistants based on dependent types, such as Coq, Epigram and - NuPRL. -tested-with: GHC == 6.8.3 && == 6.10.1 + Agda is also a proof assistant: It is an interactive system for + writing and checking proofs. Agda is based on intuitionistic type + theory, a foundational system for constructive mathematics developed + by the Swedish logician Per Martin-Löf. It has many similarities + with other proof assistants based on dependent types, such as Coq, + Epigram and NuPRL. + . + Note that if you want to use the command-line program (agda), then + you should also install the Agda-executable package. This package + includes an Emacs mode for Agda, but you need to set up the Emacs + mode yourself (see the README). +tested-with: GHC == 6.8.3 && == 6.10.2 extra-source-files: src/full/Agda/undefined.h README -data-dir: src/data -data-files: Agda.css +data-dir: src/data +data-files: Agda.css + emacs-mode/*.el +source-repository head + type: darcs + location: http://code.haskell.org/Agda/ + +source-repository this + type: darcs + location: http://code.haskell.org/Agda/ + tag: 2.2.2 + library hs-source-dirs: src/full build-depends: base >= 3 && < 4, @@ -43,7 +58,7 @@ old-time >= 1 && < 2, bytestring >= 0.9.0.1 && < 1, array >= 0.1 && < 1, - binary >= 0.4.4 && < 0.5, + binary >= 0.4.4 && < 0.6, zlib >= 0.4.0.1 && < 1, filepath >= 1.1 && < 2, process >= 1.0.1.0 && < 2, @@ -227,3 +242,12 @@ if impl(ghc >= 6.10) ghc-options: -fwarn-warnings-deprecations -fwarn-deprecated-flags -fwarn-dodgy-foreign-imports + +executable agda-mode + hs-source-dirs: src/agda-mode + main-is: Main.hs + other-modules: Paths_Agda + build-depends: base >= 3 && < 4, + filepath >= 1.1 && < 2, + process >= 1.0.1.0 && < 2, + utf8-string >= 0.3 && < 0.4 diff --git a/README b/README --- a/README +++ b/README @@ -1,259 +1,275 @@ -README ------- +======================================================================== +Agda 2 +======================================================================== -We recommend that you install Agda 2 using a binary package. To -install Agda 2 from source, proceed as follows: +Table of contents: -(An appendix below lists a partial installation script for Ubuntu -Linux.) +* Installing Agda +* Configuring the Emacs mode +* Prerequisites +* Installing a suitable version of Emacs under Windows +* Installation script for (at least) Ubuntu -0) Install prerequisites (recent versions of GHC, Alex, Happy and - cabal-install, and perhaps also darcs, Emacs and haskell-mode). +------------------------------------------------------------------------ +Installing Agda +------------------------------------------------------------------------ - GHC: http://www.haskell.org/ghc/ - Alex: http://www.haskell.org/alex/ - Happy: http://www.haskell.org/happy/ - cabal-install: http://www.haskell.org/cabal/ - darcs: http://darcs.net/ - GNU Emacs: http://www.gnu.org/software/emacs/ - haskell-mode: http://haskell.org/haskell-mode/ (version 2.1 or later) +There are several ways to install Agda. - Note: If you are downloading a source tar-ball, then you do not - need Alex, Happy or darcs. +* Using a binary package, prepared for your platform. - For non-Windows users: - The development files for the C library zlib have to be installed - (see http://zlib.net). Your package manager may be able to - install these files for you. For instance, on Debian or Ubuntu - it should suffice to run - apt-get install zlib1g-dev - as root to get the correct files installed. + Recommended if such a package exists. See the Agda Wiki. -1) Download Agda 2, perhaps as follows: +* Using stable packages available from Hackage. - darcs get --partial http://code.haskell.org/Agda - cd Agda + Install the prerequisites mentioned below, then run the following + commands: -2) If your system is Unix-like you can now hopefully install the - Agda 2 library, batch-mode tool and Emacs mode by running + cabal install Agda-executable + agda-mode setup - make install PREFIX= + The second command tries to set up Emacs for use with Agda. As an + alternative you can copy the following text to your .emacs file: - (the PREFIX=<...> part can be omitted if the default location is OK - for you). + (load-file (let ((coding-system-for-read 'utf-8)) + (shell-command-to-string "agda-mode locate"))) - If your system is not sufficiently Unix-like, or you want to have - more control, continue reading below. +* Using the source tar balls available from the Agda Wiki, or the + development version of the code available from our darcs repository. -3) Build and install the Agda 2 library. If you want to install it in - the default location (you may need root privileges for this), use - the following command in the root of the Agda source tree: + 1) Install the prerequisites mentioned below. - cabal install + 2a) If your system is Unix-like you can now hopefully install the + Agda 2 library, batch-mode tool and Emacs mode by running - You can select another location for the installation of the library - by using the following command: + make install PREFIX= - cabal install --prefix= + (the PREFIX=<...> part can be omitted if the default location is + OK for you). - You can also give other options to the installer, see the built-in - documentation of cabal-install: + If your system is not sufficiently Unix-like, or you want to have + more control, follow 2b instead. - cabal install --help + 2b) Run the following commands in the top-level directory of the + Agda source tree: -4) If you want to use the Emacs mode (recommended), build and install - it (see below). + cabal install + agda-mode setup + cd src/main + cabal clean # To ensure recompilation when upgrading. + cabal install -5) If you want to use the batch-mode Agda tool (not necessary), go to - the src/main directory and run the following commands: + The second command tries to set up Emacs for use with Agda. As + an alternative you can copy the following text to your .emacs + file: - cabal clean # To ensure recompilation when upgrading. - cabal install + (load-file (let ((coding-system-for-read 'utf-8)) + (shell-command-to-string "agda-mode locate"))) - (You can give options to cabal-install just as under step 2.) + If you want to have more control over where files are installed + then you can give various flags to cabal install, see + cabal install --help. - When upgrading Agda, note that the batch-mode tool also needs to be - rebuilt. + A section below lists an installation script which should work under + the Ubuntu distribution of GNU/Linux, assuming that your + configuration is reasonably standard. ------------------------------------------------------------------------ -To use the Agda 2 Emacs mode: +Configuring the Emacs mode +------------------------------------------------------------------------ --1. Install Emacs. +If you want to you can customise the Emacs mode. Just start Emacs and +type the following: - (For non-Windows - jump down to **END OF "Under Windows ...") - **Under Windows you may want to follow the following procedure: + M-x load-library RET agda2-mode RET + M-x customize-group RET agda2 RET - 1. Install NTEmacs 22. +This is useful if you want to change the Agda search path, in which +case you should change the agda2-include-dirs variable. - Download from - http://ntemacs.sourceforge.net/ - the self-extracting executable - ntemacs22-bin-20070819.exe +If you want some specific settings for the Emacs mode you can add them +to agda2-mode-hook. For instance, if you do not want to use the Agda +input method (for writing various symbols like ∀≥ℕ→π⟦⟧) you can add +the following to your .emacs: - When executed, it asks where to extract itself. This can be - anywhere you like, but here we write the top directory for ntemacs as - c:/pkg/ntemacs - in the following. +(add-hook 'agda2-mode-hook + '(lambda () + ; If you do not want to use any input method: + (inactivate-input-method) + ; If you want to use the X input method: + (set-input-method "X") + )) - What follows is tested only on this version. Other versions may - work but you have to figure out yourself how to use Unicode fonts - on your version. +Note that, on some systems, the Emacs mode changes the default font of +the current frame in order to enable many Unicode symbols to be +displayed. This only works if the right fonts are available, though. +If you want to turn off this feature, then you should customise the +agda2-fontset-name variable. - 2. Install ucs-fonts and mule-fonts for emacs. +------------------------------------------------------------------------ +Prerequisites +------------------------------------------------------------------------ - Download from - http://www.cl.cam.ac.uk/~mgk25/ucs-fonts.html - the tar file - http://www.cl.cam.ac.uk/~mgk25/download/ucs-fonts.tar.gz - Let us write the top directory of extracted files as - c:/pkg/ucs-fonts - Next we create some derived fonts. - cd c:/pkg/ucs-fonts/submission - make all-bdfs - This gives an error message about missing fonts, but ignore it. +For stable packages you need recent versions of the following +programs/libraries: - Download from - http://www.meadowy.org/ - the tar file - http://www.meadowy.org/meadow/dists/3.00/packages/mule-fonts-1.0-4-pkg.tar.bz2 - The untarred top directory is named "packages", but we are only - interested in the subdirectory "packages/fonts". Let us assume - we moved this subdirectory to - c:/pkg/mule-fonts + GHC: http://www.haskell.org/ghc/ + cabal-install: http://www.haskell.org/cabal/ + GNU Emacs: http://www.gnu.org/software/emacs/ + haskell-mode: http://haskell.org/haskell-mode/ (version 2.1 or later) - Add the following to your .emacs +You should also make sure that programs installed by cabal-install are +on your shell's search path. - ;;;;;;;;; start of quoted elisp code +For instructions on installing a suitable version of Emacs under +Windows, see below. - (setq bdf-directory-list - '( - "c:/pkg/ucs-fonts/submission" - "c:/pkg/mule-fonts/intlfonts" - "c:/pkg/mule-fonts/efonts" - "c:/pkg/mule-fonts/bitmap" - "c:/pkg/mule-fonts/CDAC" - "c:/pkg/mule-fonts/AkrutiFreeFonts" - )) +Non-Windows users need to ensure that the development files for the C +library zlib are installed (see http://zlib.net). Your package manager +may be able to install these files for you. For instance, on Debian or +Ubuntu it should suffice to run - (setq w32-bdf-filename-alist - (w32-find-bdf-fonts bdf-directory-list)) + apt-get install zlib1g-dev - (create-fontset-from-fontset-spec - "-*-fixed-Medium-r-Normal-*-15-*-*-*-c-*-fontset-bdf, - ascii:-Misc-Fixed-Medium-R-Normal--15-140-75-75-C-90-ISO8859-1, - latin-iso8859-2:-*-Fixed-*-r-*-*-15-*-*-*-c-*-iso8859-2, - latin-iso8859-3:-*-Fixed-*-r-*-*-15-*-*-*-c-*-iso8859-3, - latin-iso8859-4:-*-Fixed-*-r-*-*-15-*-*-*-c-*-iso8859-4, - cyrillic-iso8859-5:-*-Fixed-*-r-*-*-15-*-*-*-c-*-iso8859-5, - greek-iso8859-7:-*-Fixed-*-r-*-*-15-*-*-*-c-*-iso8859-7, - latin-iso8859-9:-*-Fixed-*-r-*-*-15-*-*-*-c-*-iso8859-9, - mule-unicode-0100-24ff:-Misc-Fixed-Medium-R-Normal--15-140-75-75-C-90-ISO10646-1, - mule-unicode-2500-33ff:-Misc-Fixed-Medium-R-Normal--15-140-75-75-C-90-ISO10646-1, - mule-unicode-e000-ffff:-Misc-Fixed-Medium-R-Normal--15-140-75-75-C-90-ISO10646-1, - japanese-jisx0208:-JIS-Fixed-Medium-R-Normal--16-150-75-75-C-160-JISX0208.1983-0, - japanese-jisx0208-1978:-Misc-Fixed-Medium-R-Normal--16-150-75-75-C-160-JISC6226.1978-0, - japanese-jisx0212:-Misc-Fixed-Medium-R-Normal--16-150-75-75-C-160-JISX0212.1990-0, - latin-jisx0201:-*-*-medium-r-normal-*-16-*-*-*-c-*-jisx0201*-*, - katakana-jisx0201:-Sony-Fixed-Medium-R-Normal--16-120-100-100-C-80-JISX0201.1976-0, - thai-tis620:-Misc-Fixed-Medium-R-Normal--24-240-72-72-C-120-TIS620.2529-1, - lao:-Misc-Fixed-Medium-R-Normal--24-240-72-72-C-120-MuleLao-1, - tibetan:-TibMdXA-fixed-medium-r-normal--16-160-72-72-m-160-MuleTibetan-0, - tibetan-1-column:-TibMdXA-fixed-medium-r-normal--16-160-72-72-m-80-MuleTibetan-1, - korean-ksc5601:-Daewoo-Mincho-Medium-R-Normal--16-120-100-100-C-160-KSC5601.1987-0, - chinese-gb2312:-ISAS-Fangsong ti-Medium-R-Normal--16-160-72-72-c-160-GB2312.1980-0, - chinese-cns11643-1:-HKU-Fixed-Medium-R-Normal--16-160-72-72-C-160-CNS11643.1992.1-0, - chinese-big5-1:-ETen-Fixed-Medium-R-Normal--16-150-75-75-C-160-Big5.ETen-0, - chinese-big5-2:-ETen-Fixed-Medium-R-Normal--16-150-75-75-C-160-Big5.ETen-0 - " t) +as root to get the correct files installed. - (setq font-encoding-alist - (append '( - ("JISX0208" (japanese-jisx0208 . 0)) - ("JISX0212" (japanese-jisx0212 . 0)) - ("CNS11643.1992.1-0" (chinese-cns11643-1 . 0)) - ("GB2312" (chinese-gb2312 . 0)) - ("KSC5601" (korean-ksc5601 . 0)) - ("VISCII" (vietnamese-viscii-lower . 0)) - ("MuleArabic-0" (arabic-digit . 0)) - ("MuleArabic-1" (arabic-1-column . 0)) - ("MuleArabic-2" (arabic-2-column . 0)) - ("muleindian-1" (indian-1-column . 0)) - ("muleindian-2" (indian-2-column . 0)) - ("MuleTibetan-0" (tibetan . 0)) - ("MuleTibetan-1" (tibetan-1-column . 0)) - ) font-encoding-alist)) +For the development version of Agda you also need recent versions of +the following programs: - ;;;;;;; end of quoted elisp code + Alex: http://www.haskell.org/alex/ + Happy: http://www.haskell.org/happy/ - To test the fonts, try +------------------------------------------------------------------------ +Installing a suitable version of Emacs under Windows +------------------------------------------------------------------------ - M-x eval-expression RET - (set-default-font "fontset-bdf") RET - M-x view-hello-file +Note that Agda code often uses mathematical and other symbols +available from the Unicode character set. In order to be able to +display these characters you may want to follow the procedure below +when installing Emacs under Windows. - You should see all the characters without white-boxes. - **END OF "Under Windows ..." +1. Install NTEmacs 22. -1. Install Agda 2. (See above.) + Download from + http://ntemacs.sourceforge.net/ + the self-extracting executable + ntemacs22-bin-20070819.exe -2. Copy the .el files in src/emacs-mode to some directory - . Example installation: + When executed, it asks where to extract itself. This can be + anywhere you like, but here we write the top directory for ntemacs as + c:/pkg/ntemacs + in the following. - mkdir - cp src/emacs-mode/*.el + What follows is tested only on this version. Other versions may + work but you have to figure out yourself how to use Unicode fonts + on your version. -3. Add the following to your .emacs: +2. Install ucs-fonts and mule-fonts for emacs. - (add-to-list 'load-path "") - (require 'agda2) + Download from + http://www.cl.cam.ac.uk/~mgk25/ucs-fonts.html + the tar file + http://www.cl.cam.ac.uk/~mgk25/download/ucs-fonts.tar.gz + Let us write the top directory of extracted files as + c:/pkg/ucs-fonts + Next we create some derived fonts. + cd c:/pkg/ucs-fonts/submission + make all-bdfs + This gives an error message about missing fonts, but ignore it. - If you have already set up the suffix .agda for use with some other - mode you may need to remove or alter that setting. You are - encouraged to use the suffix .alfa for Agda 1 files. + Download from + http://www.meadowy.org/ + the tar file + http://www.meadowy.org/meadow/dists/3.00/packages/mule-fonts-1.0-4-pkg.tar.bz2 + The untarred top directory is named "packages", but we are only + interested in the subdirectory "packages/fonts". Let us assume + we moved this subdirectory to + c:/pkg/mule-fonts - Now, if you open a file named XXX.agda the buffer will use - agda2-mode. It may take 5 or 10 seconds before you see anything in - the buffer, but that is normal. + Add the following to your .emacs -4. If you want to you can customise some settings. Just start Emacs - and type the following: +;;;;;;;;; start of quoted elisp code - M-x load-library RET agda2-mode RET - M-x customize-group RET agda2 RET +(setq bdf-directory-list + '( + "c:/pkg/ucs-fonts/submission" + "c:/pkg/mule-fonts/intlfonts" + "c:/pkg/mule-fonts/efonts" + "c:/pkg/mule-fonts/bitmap" + "c:/pkg/mule-fonts/CDAC" + "c:/pkg/mule-fonts/AkrutiFreeFonts" + )) - This is useful if you want to change the Agda search path, in which - case you should change the agda2-include-dirs variable. +(setq w32-bdf-filename-alist + (w32-find-bdf-fonts bdf-directory-list)) -5. If you want some specific settings for the Emacs mode you can add - them to agda2-mode-hook. For instance, if you do not want to use - the Agda input method (for writing various symbols like ∀≥ℕ→π⟦⟧) - you can add the following to your .emacs: +(create-fontset-from-fontset-spec + "-*-fixed-Medium-r-Normal-*-15-*-*-*-c-*-fontset-bdf, + ascii:-Misc-Fixed-Medium-R-Normal--15-140-75-75-C-90-ISO8859-1, + latin-iso8859-2:-*-Fixed-*-r-*-*-15-*-*-*-c-*-iso8859-2, + latin-iso8859-3:-*-Fixed-*-r-*-*-15-*-*-*-c-*-iso8859-3, + latin-iso8859-4:-*-Fixed-*-r-*-*-15-*-*-*-c-*-iso8859-4, + cyrillic-iso8859-5:-*-Fixed-*-r-*-*-15-*-*-*-c-*-iso8859-5, + greek-iso8859-7:-*-Fixed-*-r-*-*-15-*-*-*-c-*-iso8859-7, + latin-iso8859-9:-*-Fixed-*-r-*-*-15-*-*-*-c-*-iso8859-9, + mule-unicode-0100-24ff:-Misc-Fixed-Medium-R-Normal--15-140-75-75-C-90-ISO10646-1, + mule-unicode-2500-33ff:-Misc-Fixed-Medium-R-Normal--15-140-75-75-C-90-ISO10646-1, + mule-unicode-e000-ffff:-Misc-Fixed-Medium-R-Normal--15-140-75-75-C-90-ISO10646-1, + japanese-jisx0208:-JIS-Fixed-Medium-R-Normal--16-150-75-75-C-160-JISX0208.1983-0, + japanese-jisx0208-1978:-Misc-Fixed-Medium-R-Normal--16-150-75-75-C-160-JISC6226.1978-0, + japanese-jisx0212:-Misc-Fixed-Medium-R-Normal--16-150-75-75-C-160-JISX0212.1990-0, + latin-jisx0201:-*-*-medium-r-normal-*-16-*-*-*-c-*-jisx0201*-*, + katakana-jisx0201:-Sony-Fixed-Medium-R-Normal--16-120-100-100-C-80-JISX0201.1976-0, + thai-tis620:-Misc-Fixed-Medium-R-Normal--24-240-72-72-C-120-TIS620.2529-1, + lao:-Misc-Fixed-Medium-R-Normal--24-240-72-72-C-120-MuleLao-1, + tibetan:-TibMdXA-fixed-medium-r-normal--16-160-72-72-m-160-MuleTibetan-0, + tibetan-1-column:-TibMdXA-fixed-medium-r-normal--16-160-72-72-m-80-MuleTibetan-1, + korean-ksc5601:-Daewoo-Mincho-Medium-R-Normal--16-120-100-100-C-160-KSC5601.1987-0, + chinese-gb2312:-ISAS-Fangsong ti-Medium-R-Normal--16-160-72-72-c-160-GB2312.1980-0, + chinese-cns11643-1:-HKU-Fixed-Medium-R-Normal--16-160-72-72-C-160-CNS11643.1992.1-0, + chinese-big5-1:-ETen-Fixed-Medium-R-Normal--16-150-75-75-C-160-Big5.ETen-0, + chinese-big5-2:-ETen-Fixed-Medium-R-Normal--16-150-75-75-C-160-Big5.ETen-0 + " t) - (add-hook 'agda2-mode-hook - '(lambda () - ; If you do not want to use any input method: - (inactivate-input-method) - ; If you want to use the X input method: - (set-input-method "X") - )) +(setq font-encoding-alist + (append '( + ("JISX0208" (japanese-jisx0208 . 0)) + ("JISX0212" (japanese-jisx0212 . 0)) + ("CNS11643.1992.1-0" (chinese-cns11643-1 . 0)) + ("GB2312" (chinese-gb2312 . 0)) + ("KSC5601" (korean-ksc5601 . 0)) + ("VISCII" (vietnamese-viscii-lower . 0)) + ("MuleArabic-0" (arabic-digit . 0)) + ("MuleArabic-1" (arabic-1-column . 0)) + ("MuleArabic-2" (arabic-2-column . 0)) + ("muleindian-1" (indian-1-column . 0)) + ("muleindian-2" (indian-2-column . 0)) + ("MuleTibetan-0" (tibetan . 0)) + ("MuleTibetan-1" (tibetan-1-column . 0)) + ) font-encoding-alist)) - A side note: In order to display Unicode characters you need to use - a font which contains the glyphs in question. If such a font is not - enabled by default (empty boxes are displayed instead of proper - characters) you need to select another font. Do this by running - M-x customize-face RET agda2-fontset-spec RET - in Emacs (after you have started the Agda mode) and change the - setting to a suitable font. +;;;;;;; end of quoted elisp code ------------------------------------------------------------------- -Appendix: Partial installation script for (at least) Ubuntu Linux + To test the fonts, try -sudo apt-get install ghc6 happy alex darcs emacs haskell-mode zlib1g-dev -wget http://www.haskell.org/cabal/release/cabal-install-0.6.0.tar.gz -tar xzf cabal-install-0.6.0.tar.gz -cd cabal-install-0.6.0 -. bootstrap.sh -cd .. -darcs get --partial http://code.haskell.org/Agda -cd Agda -sudo make install + M-x eval-expression RET + (set-default-font "fontset-bdf") RET + M-x view-hello-file + + You should see all the characters without white-boxes. + +------------------------------------------------------------------------ +Installation script for (at least) Ubuntu +------------------------------------------------------------------------ + +Installs the development version. + + sudo apt-get install ghc6 happy alex darcs emacs haskell-mode zlib1g-dev + wget http://www.haskell.org/cabal/release/cabal-install-0.6.0.tar.gz + tar xzf cabal-install-0.6.0.tar.gz + cd cabal-install-0.6.0 + . bootstrap.sh + cd .. + darcs get --partial http://code.haskell.org/Agda + cd Agda + sudo make install diff --git a/src/agda-mode/Main.hs b/src/agda-mode/Main.hs new file mode 100644 --- /dev/null +++ b/src/agda-mode/Main.hs @@ -0,0 +1,190 @@ +-- | A program which either tries to add setup code for Agda's Emacs +-- mode to the users .emacs file, or provides information to Emacs +-- about where the Emacs mode is installed. + +module Main (main) where + +import Control.Exception +import Control.Monad +import Data.Char +import Data.List +import Data.Version +import Numeric +import System.Directory +import System.Environment +import System.Exit +import System.FilePath +import System.IO +import qualified System.IO.UTF8 as UTF8 +import System.Process + +import Paths_Agda (getDataDir, version) + +-- | The program. + +main :: IO () +main = do + prog <- getProgName + args <- getArgs + case args of + [arg] | arg == locateFlag -> printEmacsModeFile + | arg == setupFlag -> do + dotEmacs <- findDotEmacs + setupDotEmacs (Files { thisProgram = prog + , dotEmacs = dotEmacs + }) + _ -> do inform usage + exitFailure + +-- Command line options. + +setupFlag = "setup" +locateFlag = "locate" + +-- | Usage information. + +usage :: String +usage = unlines + [ "This program, which is part of Agda version " ++ ver ++ ", can be run" + , "in two modes, depending on which option it is invoked with:" + , "" + , setupFlag + , "" + , " The program tries to add setup code for Agda's Emacs mode to the" + , " current user's .emacs file. It is assumed that the .emacs file" + , " uses ASCII or some other character encoding which ASCII is" + , " compatible with (like Latin-1 or UTF-8)." + , "" + , locateFlag + , "" + , " The path to the Emacs mode's main file is printed on standard" + , " output (using the UTF-8 character encoding and no trailing" + , " newline)." + ] + +-- | The current version of Agda. + +ver :: String +ver = intercalate "." $ map show $ + versionBranch version + +------------------------------------------------------------------------ +-- Locating the Agda mode + +-- | Prints out the path to the Agda mode's main file (using UTF-8 and +-- without any trailing newline). + +printEmacsModeFile :: IO () +printEmacsModeFile = do + dataDir <- getDataDir + UTF8.putStr $ dataDir "emacs-mode" "agda2.el" + +------------------------------------------------------------------------ +-- Setting up the .emacs file + +data Files = Files { dotEmacs :: FilePath + -- ^ The .emacs file. + , thisProgram :: FilePath + -- ^ The name of the current program. + } + +-- | Tries to set up the Agda mode in the given .emacs file. + +setupDotEmacs :: Files -> IO () +setupDotEmacs files = do + informLn $ "The .emacs file used: " ++ dotEmacs files + + already <- alreadyInstalled files + if already then + informLn "It seems as if setup has already been performed." + else do + + appendFile (dotEmacs files) (setupString files) + inform $ unlines $ + [ "Setup done. Try to (re)start Emacs and open an Agda file." + , "The following text was appended to the .emacs file:" + ] ++ lines (setupString files) + +-- | Tries to find the user's .emacs file by querying Emacs. + +findDotEmacs :: IO FilePath +findDotEmacs = askEmacs "(insert (expand-file-name user-init-file))" + +-- | Has the Agda mode already been set up? + +alreadyInstalled :: Files -> IO Bool +alreadyInstalled files = do + exists <- doesFileExist (dotEmacs files) + if not exists then return False else + withFile (dotEmacs files) ReadMode $ \h -> + evaluate . (identifier files `isInfixOf`) =<< hGetContents h + -- Uses evaluate to ensure that the file is not closed + -- prematurely. + +-- | If this string occurs in the .emacs file, then it is assumed that +-- setup has already been performed. + +identifier :: Files -> String +identifier files = + takeFileName (thisProgram files) ++ " " ++ locateFlag + +-- | The string appended to the end of the .emacs file. It is assumed +-- that the .emacs file uses ASCII or some other character encoding +-- which ASCII is compatible with (like Latin-1 or UTF-8). + +setupString :: Files -> String +setupString files = unlines + [ "" + , "(load-file (let ((coding-system-for-read 'utf-8))" + , " (shell-command-to-string \"" + ++ identifier files ++ "\")))" + ] + +------------------------------------------------------------------------ +-- Querying Emacs + +-- | Evaluates the given Elisp command using Emacs. The output of the +-- command (whatever was written into the current buffer) is returned. +-- +-- Note: The input is not checked. The input is assumed to come from a +-- trusted source. + +askEmacs :: String -> IO String +askEmacs query = do + tempDir <- getTemporaryDirectory + bracket (openTempFile tempDir "askEmacs") + (removeFile . fst) $ \(file, h) -> do + hClose h + exit <- rawSystem "emacs" + [ "--eval" + , "(with-temp-file " ++ escape file ++ " " + ++ query ++ ")" + , "--kill" + ] + unless (exit == ExitSuccess) $ do + informLn "Unable to query Emacs." + exitFailure + withFile file ReadMode $ \h -> do + result <- hGetContents h + evaluate (length result) + -- Uses evaluate to ensure that the file is not closed + -- prematurely. + return result + +-- | Escapes the string so that Emacs can parse it as an Elisp string. + +escape :: FilePath -> FilePath +escape s = "\"" ++ concatMap esc s ++ "\"" + where + esc c | c `elem` ['\\', '"'] = '\\' : [c] + | isAscii c && isPrint c = [c] + | otherwise = "\\x" ++ showHex (fromEnum c) "\\ " + +------------------------------------------------------------------------ +-- Helper functions + +-- These functions inform the user about something by printing on +-- stderr. + +inform = hPutStr stderr +informLn = hPutStrLn stderr diff --git a/src/data/emacs-mode/agda-input.el b/src/data/emacs-mode/agda-input.el new file mode 100644 --- /dev/null +++ b/src/data/emacs-mode/agda-input.el @@ -0,0 +1,817 @@ +;;; agda-input.el --- The Agda input method + +;;; Commentary: + +;; A highly customisable input method which can inherit from other +;; Quail input methods. By default the input method is geared towards +;; the input of mathematical and other symbols in Agda programs. +;; +;; Use M-x customize-group agda-input to customise this input method. +;; Note that the functions defined under "Functions used to tweak +;; translation pairs" below can be used to tweak both the key +;; translations inherited from other input methods as well as the +;; ones added specifically for this one. +;; +;; Use agda-input-show-translations to see all the characters which +;; can be typed using this input method (except for those +;; corresponding to ASCII characters). + +;;; Code: + +(require 'quail) +(require 'cl) + +;; Quail is quite stateful, so be careful when editing this code. Note +;; that with-temp-buffer is used below whenever buffer-local state is +;; modified. + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Utility functions + +(defun agda-input-concat-map (f xs) + "Concat (map F XS)." + (apply 'append (mapcar f xs))) + +(defun agda-input-to-string-list (s) + "Convert a string S to a list of one-character strings, after +removing all space and newline characters." + (agda-input-concat-map + (lambda (c) (if (member c (string-to-list " \n")) + nil + (list (string c)))) + (string-to-list s))) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Functions used to tweak translation pairs + +;; lexical-let is used since Elisp lacks lexical scoping. + +(defun agda-input-compose (f g) + "\x -> concatMap F (G x)" + (lexical-let ((f1 f) (g1 g)) + (lambda (x) (agda-input-concat-map f1 (funcall g1 x))))) + +(defun agda-input-or (f g) + "\x -> F x ++ G x" + (lexical-let ((f1 f) (g1 g)) + (lambda (x) (append (funcall f1 x) (funcall g1 x))))) + +(defun agda-input-nonempty () + "Only keep pairs with a non-empty first component." + (lambda (x) (if (> (length (car x)) 0) (list x)))) + +(defun agda-input-prepend (prefix) + "Prepend PREFIX to all key sequences." + (lexical-let ((prefix1 prefix)) + (lambda (x) `((,(concat prefix1 (car x)) . ,(cdr x)))))) + +(defun agda-input-prefix (prefix) + "Only keep pairs whose key sequence starts with PREFIX." + (lexical-let ((prefix1 prefix)) + (lambda (x) + (if (equal (substring (car x) 0 (length prefix1)) prefix1) + (list x))))) + +(defun agda-input-suffix (suffix) + "Only keep pairs whose key sequence ends with SUFFIX." + (lexical-let ((suffix1 suffix)) + (lambda (x) + (if (equal (substring (car x) + (- (length (car x)) (length suffix1))) + suffix1) + (list x))))) + +(defun agda-input-drop (ss) + "Drop pairs matching one of the given key sequences. +SS should be a list of strings." + (lexical-let ((ss1 ss)) + (lambda (x) (unless (member (car x) ss1) (list x))))) + +(defun agda-input-drop-beginning (n) + "Drop N characters from the beginning of each key sequence." + (lexical-let ((n1 n)) + (lambda (x) `((,(substring (car x) n1) . ,(cdr x)))))) + +(defun agda-input-drop-end (n) + "Drop N characters from the end of each key sequence." + (lexical-let ((n1 n)) + (lambda (x) + `((,(substring (car x) 0 (- (length (car x)) n1)) . + ,(cdr x)))))) + +(defun agda-input-drop-prefix (prefix) + "Only keep pairs whose key sequence starts with PREFIX. +This prefix is dropped." + (agda-input-compose + (agda-input-drop-beginning (length prefix)) + (agda-input-prefix prefix))) + +(defun agda-input-drop-suffix (suffix) + "Only keep pairs whose key sequence ends with SUFFIX. +This suffix is dropped." + (lexical-let ((suffix1 suffix)) + (agda-input-compose + (agda-input-drop-end (length suffix1)) + (agda-input-suffix suffix1)))) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Customization + +;; The :set keyword is set to 'agda-input-incorporate-changed-setting +;; so that the input method gets updated immediately when users +;; customize it. However, the setup functions cannot be run before all +;; variables have been defined. Hence the :initialize keyword is set to +;; 'custom-initialize-default to ensure that the setup is not performed +;; until agda-input-setup is called at the end of this file. + +(defgroup agda-input nil + "The Agda 2 input method. +After tweaking these settings you may want to inspect the resulting +translations using `agda-input-show-translations'." + :group 'agda2 + :group 'leim) + +(defcustom agda-input-tweak-all + '(agda-input-compose + (agda-input-prepend "\\") + (agda-input-nonempty)) + "An expression yielding a function which can be used to tweak +all translations before they are included in the input method. +The resulting function (if non-nil) is applied to every +\(KEY-SEQUENCE . TRANSLATION) pair and should return a list of such +pairs. (Note that the translations can be anything accepted by +`quail-defrule'.) + +If you change this setting manually (without using the +customization buffer) you need to call `agda-input-setup' in +order for the change to take effect." + :group 'agda-input + :set 'agda-input-incorporate-changed-setting + :initialize 'custom-initialize-default + :type 'sexp) + +(defcustom agda-input-inherit + `(("TeX" . (agda-input-compose + (agda-input-drop '("geq" "leq" "bullet" "qed")) + (agda-input-or + (agda-input-drop-prefix "\\") + (agda-input-or + (agda-input-compose + (agda-input-drop '("^o")) + (agda-input-prefix "^")) + (agda-input-prefix "_"))))) + ) + "A list of Quail input methods whose translations should be +inherited by the Agda input method (with the exception of +translations corresponding to ASCII characters). + +The list consists of pairs (qp . tweak), where qp is the name of +a Quail package, and tweak is an expression of the same kind as +`agda-input-tweak-all' which is used to tweak the translation +pairs of the input method. + +If you change this setting manually (without using the +customization buffer) you need to call `agda-input-setup' in +order for the change to take effect." + :group 'agda-input + :set 'agda-input-incorporate-changed-setting + :initialize 'custom-initialize-default + :type '(repeat (cons (string :tag "Quail package") + (sexp :tag "Tweaking function")))) + +(defcustom agda-input-translations + (let ((max-lisp-eval-depth 2800)) `( + + ;; Equality and similar symbols. + + ("eq" . ,(agda-input-to-string-list "=∼∽≈≋∻∾∿≀≃⋍≂≅ ≌≊≡≣≐≑≒≓≔≕≖≗≘≙≚≛≜≝≞≟≍≎≏≬⋕")) + ("eqn" . ,(agda-input-to-string-list "≠≁ ≉ ≄ ≇≆ ≢ ≭ ")) + + ("=n" . ("≠")) + ("~" . ("∼")) ("~n" . ("≁")) + ("~~" . ("≈")) ("~~n" . ("≉")) + ("~~~" . ("≋")) + (":~" . ("∻")) + ("~-" . ("≃")) ("~-n" . ("≄")) + ("-~" . ("≂")) + ("~=" . ("≅")) ("~=n" . ("≇")) + ("~~-" . ("≊")) + ("==" . ("≡")) ("==n" . ("≢")) + ("===" . ("≣")) + (".=" . ("≐")) (".=." . ("≑")) + (":=" . ("≔")) ("=:" . ("≕")) + ("=o" . ("≗")) + ("(=" . ("≘")) + ("and=" . ("≙")) ("or=" . ("≚")) + ("*=" . ("≛")) + ("t=" . ("≜")) + ("def=" . ("≝")) + ("m=" . ("≞")) + ("?=" . ("≟")) + + ;; Inequality and similar symbols. + + ("leq" . ,(agda-input-to-string-list "<≪⋘≤≦≲ ≶≺≼≾⊂⊆ ⋐⊏⊑ ⊰⊲⊴⋖⋚⋜⋞")) + ("leqn" . ,(agda-input-to-string-list "≮ ≰≨≴⋦≸⊀ ⋨⊄⊈⊊ ⋢⋤ ⋪⋬ ⋠")) + ("geq" . ,(agda-input-to-string-list ">≫⋙≥≧≳ ≷≻≽≿⊃⊇ ⋑⊐⊒ ⊱⊳⊵⋗⋛⋝⋟")) + ("geqn" . ,(agda-input-to-string-list "≯ ≱≩≵⋧≹⊁ ⋩⊅⊉⊋ ⋣⋥ ⋫⋭ ⋡")) + + ("<=" . ("≤")) (">=" . ("≥")) + ("<=n" . ("≰")) (">=n" . ("≱")) + ("len" . ("≰")) ("gen" . ("≱")) + ("n" . ("≯")) + ("<~" . ("≲")) (">~" . ("≳")) + ("<~n" . ("⋦")) (">~n" . ("⋧")) + ("<~nn" . ("≴")) (">~nn" . ("≵")) + + ("sub" . ("⊂")) ("sup" . ("⊃")) + ("subn" . ("⊄")) ("supn" . ("⊅")) + ("sub=" . ("⊆")) ("sup=" . ("⊇")) + ("sub=n" . ("⊈")) ("sup=n" . ("⊉")) + + ("squb" . ("⊏")) ("squp" . ("⊐")) + ("squb=" . ("⊑")) ("squp=" . ("⊒")) + ("squb=n" . ("⋢")) ("squp=n" . ("⋣")) + + ;; Set membership etc. + + ("member" . ,(agda-input-to-string-list "∈∉∊∋∌∍⋲⋳⋴⋵⋶⋷⋸⋹⋺⋻⋼⋽⋾⋿")) + + ("inn" . ("∉")) + ("nin" . ("∌")) + + ;; Intersections, unions etc. + + ("intersection" . ,(agda-input-to-string-list "∩⋂∧⋀⋏⨇⊓⨅⋒∏ ⊼ ⨉")) + ("union" . ,(agda-input-to-string-list "∪⋃∨⋁⋎⨈⊔⨆⋓∐⨿⊽⊻⊍⨃⊎⨄⊌∑⅀")) + + ("and" . ("∧")) ("or" . ("∨")) + ("And" . ("⋀")) ("Or" . ("⋁")) + ("i" . ("∩")) ("un" . ("∪")) ("u+" . ("⊎")) ("u." . ("⊍")) + ("I" . ("⋂")) ("Un" . ("⋃")) ("U+" . ("⨄")) ("U." . ("⨃")) + ("glb" . ("⊓")) ("lub" . ("⊔")) + ("Glb" . ("⨅")) ("Lub" . ("⨆")) + + ;; Entailment etc. + + ("entails" . ,(agda-input-to-string-list "⊢⊣⊤⊥⊦⊧⊨⊩⊪⊫⊬⊭⊮⊯")) + + ("|-" . ("⊢")) ("|-n" . ("⊬")) + ("-|" . ("⊣")) + ("|=" . ("⊨")) ("|=n" . ("⊭")) + + ;; Divisibility, parallelity. + + ("|" . ("∣")) ("|n" . ("∤")) + ("||" . ("∥")) ("||n" . ("∦")) + + ;; Some symbols from logic and set theory. + + ("all" . ("∀")) + ("ex" . ("∃")) + ("exn" . ("∄")) + ("0" . ("∅")) + ("C" . ("∁")) + + ;; Corners, ceilings and floors. + + ("c" . ,(agda-input-to-string-list "⌜⌝⌞⌟⌈⌉⌊⌋")) + ("cu" . ,(agda-input-to-string-list "⌜⌝ ⌈⌉ ")) + ("cl" . ,(agda-input-to-string-list " ⌞⌟ ⌊⌋")) + + ("cul" . ("⌜")) ("cuL" . ("⌈")) + ("cur" . ("⌝")) ("cuR" . ("⌉")) + ("cll" . ("⌞")) ("clL" . ("⌊")) + ("clr" . ("⌟")) ("clR" . ("⌋")) + + ;; Various operators/symbols. + + ,@(if (>= emacs-major-version 23) + '(("pm" . ("±")) + ("cdot" . ("·")) + ("times" . ("×")) + ("div" . ("÷")) + ("neg" . ("¬")))) + + ("qed" . ("∎")) + ("x" . ("×")) + ("o" . ("∘")) + ("comp" . ("∘")) + ("." . ("∙")) + ("*" . ("⋆")) + (".+" . ("∔")) + (".-" . ("∸")) + (":" . ("∶")) + ("::" . ("∷")) + ("::-" . ("∺")) + ("-:" . ("∹")) + ("+ " . ("⊹")) + ("surd3" . ("∛")) + ("surd4" . ("∜")) + ("increment" . ("∆")) + ("inf" . ("∞")) + + ;; Circled operators. + + ("o+" . ("⊕")) + ("o--" . ("⊖")) + ("ox" . ("⊗")) + ("o/" . ("⊘")) + ("o." . ("⊙")) + ("oo" . ("⊚")) + ("o*" . ("⊛")) + ("o=" . ("⊜")) + ("o-" . ("⊝")) + + ("O+" . ("⨁")) + ("Ox" . ("⨂")) + ("O." . ("⨀")) + ("O*" . ("⍟")) + + ;; Boxed operators. + + ("b+" . ("⊞")) + ("b-" . ("⊟")) + ("bx" . ("⊠")) + ("b." . ("⊡")) + + ;; Various symbols. + + ("integral" . ,(agda-input-to-string-list "∫∬∭∮∯∰∱∲∳")) + ("angle" . ,(agda-input-to-string-list "∟∡∢⊾⊿")) + ("join" . ,(agda-input-to-string-list "⋈⋉⋊⋋⋌⨝⟕⟖⟗")) + + ;; Arrows. + + ("l" . ,(agda-input-to-string-list "←⇐⇚⇇⇆↤⇦↞↼↽⇠⇺↜⇽⟵⟸↚⇍⇷ ↹ ↢↩↫⇋⇜⇤⟻⟽⤆↶↺⟲ ")) + ("r" . ,(agda-input-to-string-list "→⇒⇛⇉⇄↦⇨↠⇀⇁⇢⇻↝⇾⟶⟹↛⇏⇸⇶ ↴ ↣↪↬⇌⇝⇥⟼⟾⤇↷↻⟳⇰⇴⟴⟿ ➵➸➙➔➛➜➝➞➟➠➡➢➣➤➧➨➩➪➫➬➭➮➯➱➲➳➺➻➼➽➾")) + ("u" . ,(agda-input-to-string-list "↑⇑⟰⇈⇅↥⇧↟↿↾⇡⇞ ↰↱➦ ⇪⇫⇬⇭⇮⇯ ")) + ("d" . ,(agda-input-to-string-list "↓⇓⟱⇊⇵↧⇩↡⇃⇂⇣⇟ ↵↲↳➥ ↯ ")) + ("ud" . ,(agda-input-to-string-list "↕⇕ ↨⇳ ")) + ("lr" . ,(agda-input-to-string-list "↔⇔ ⇼↭⇿⟷⟺↮⇎⇹ ")) + ("ul" . ,(agda-input-to-string-list "↖⇖ ⇱↸ ")) + ("ur" . ,(agda-input-to-string-list "↗⇗ ➶➹➚ ")) + ("dr" . ,(agda-input-to-string-list "↘⇘ ⇲ ➴➷➘ ")) + ("dl" . ,(agda-input-to-string-list "↙⇙ ")) + + ("l-" . ("←")) ("<-" . ("←")) ("l=" . ("⇐")) + ("r-" . ("→")) ("->" . ("→")) ("r=" . ("⇒")) ("=>" . ("⇒")) + ("u-" . ("↑")) ("u=" . ("⇑")) + ("d-" . ("↓")) ("d=" . ("⇓")) + ("ud-" . ("↕")) ("ud=" . ("⇕")) + ("lr-" . ("↔")) ("<->" . ("↔")) ("lr=" . ("⇔")) ("<=>" . ("⇔")) + ("ul-" . ("↖")) ("ul=" . ("⇖")) + ("ur-" . ("↗")) ("ur=" . ("⇗")) + ("dr-" . ("↘")) ("dr=" . ("⇘")) + ("dl-" . ("↙")) ("dl=" . ("⇙")) + + ("l==" . ("⇚")) ("l-2" . ("⇇")) ("l-r-" . ("⇆")) + ("r==" . ("⇛")) ("r-2" . ("⇉")) ("r-3" . ("⇶")) ("r-l-" . ("⇄")) + ("u==" . ("⟰")) ("u-2" . ("⇈")) ("u-d-" . ("⇅")) + ("d==" . ("⟱")) ("d-2" . ("⇊")) ("d-u-" . ("⇵")) + + ("l--" . ("⟵")) ("<--" . ("⟵")) ("l~" . ("↜" "⇜")) + ("r--" . ("⟶")) ("-->" . ("⟶")) ("r~" . ("↝" "⇝" "⟿")) + ("lr--" . ("⟷")) ("<-->" . ("⟷")) ("lr~" . ("↭")) + + ("l-n" . ("↚")) ("<-n" . ("↚")) ("l=n" . ("⇍")) + ("r-n" . ("↛")) ("->n" . ("↛")) ("r=n" . ("⇏")) ("=>n" . ("⇏")) + ("lr-n" . ("↮")) ("<->n" . ("↮")) ("lr=n" . ("⇎")) ("<=>n" . ("⇎")) + + ("l-|" . ("↤")) ("ll-" . ("↞")) + ("r-|" . ("↦")) ("rr-" . ("↠")) + ("u-|" . ("↥")) ("uu-" . ("↟")) + ("d-|" . ("↧")) ("dd-" . ("↡")) + ("ud-|" . ("↨")) + + ("dz" . ("↯")) + + ;; Ellipsis. + + ("..." . ,(agda-input-to-string-list "⋯⋮⋰⋱")) + + ;; Box-drawing characters. + + ("---" . ,(agda-input-to-string-list "─│┌┐└┘├┤┬┼┴╴╵╶╷╭╮╯╰╱╲╳")) + ("--=" . ,(agda-input-to-string-list "═║╔╗╚╝╠╣╦╬╩ ╒╕╘╛╞╡╤╪╧ ╓╖╙╜╟╢╥╫╨")) + ("--_" . ,(agda-input-to-string-list "━┃┏┓┗┛┣┫┳╋┻╸╹╺╻ + ┍┯┑┕┷┙┝┿┥┎┰┒┖┸┚┠╂┨┞╀┦┟╁┧┢╈┪┡╇┩ + ┮┭┶┵┾┽┲┱┺┹╊╉╆╅╄╃ ╿╽╼╾")) + ("--." . ,(agda-input-to-string-list "╌╎┄┆┈┊ + ╍╏┅┇┉┋")) + + ;; Triangles. + + ;; Big/small, black/white. + + ("t" . ,(agda-input-to-string-list "◂◃◄◅▸▹►▻▴▵▾▿◢◿◣◺◤◸◥◹")) + ("T" . ,(agda-input-to-string-list "◀◁▶▷▲△▼▽◬◭◮")) + + ("tb" . ,(agda-input-to-string-list "◂▸▴▾◄►◢◣◤◥")) + ("tw" . ,(agda-input-to-string-list "◃▹▵▿◅▻◿◺◸◹")) + + ("Tb" . ,(agda-input-to-string-list "◀▶▲▼")) + ("Tw" . ,(agda-input-to-string-list "◁▷△▽")) + + ;; Squares. + + ("sq" . ,(agda-input-to-string-list "■□◼◻◾◽▣▢▤▥▦▧▨▩◧◨◩◪◫◰◱◲◳")) + ("sqb" . ,(agda-input-to-string-list "■◼◾")) + ("sqw" . ,(agda-input-to-string-list "□◻◽")) + ("sq." . ("▣")) + ("sqo" . ("▢")) + + ;; Rectangles. + + ("re" . ,(agda-input-to-string-list "▬▭▮▯")) + ("reb" . ,(agda-input-to-string-list "▬▮")) + ("rew" . ,(agda-input-to-string-list "▭▯")) + + ;; Parallelograms. + + ("pa" . ,(agda-input-to-string-list "▰▱")) + ("pab" . ("▰")) + ("paw" . ("▱")) + + ;; Diamonds. + + ("di" . ,(agda-input-to-string-list "◆◇◈")) + ("dib" . ("◆")) + ("diw" . ("◇")) + ("di." . ("◈")) + + ;; Circles. + + ("ci" . ,(agda-input-to-string-list "●○◎◌◯◍◐◑◒◓◔◕◖◗◠◡◴◵◶◷⚆⚇⚈⚉")) + ("cib" . ("●")) + ("ciw" . ("○")) + ("ci." . ("◎")) + ("ci.." . ("◌")) + ("ciO" . ("◯")) + + ;; Stars. + + ("st" . ,(agda-input-to-string-list "⋆✦✧✶✴✹ ★☆✪✫✯✰✵✷✸")) + ("st4" . ,(agda-input-to-string-list "✦✧")) + ("st6" . ("✶")) + ("st8" . ("✴")) + ("st12" . ("✹")) + + ;; Blackboard bold letters. + + ("bn" . ("ℕ")) + ("bz" . ("ℤ")) + ("bq" . ("ℚ")) + ("br" . ("ℝ")) + ("bc" . ("ℂ")) + ("bp" . ("ℙ")) + ("bsum" . ("⅀")) + + ;; Parentheses. + + ("(" . ,(agda-input-to-string-list "([{⁅⁽₍〈⎴⟦⟨⟪〈《「『【〔〖〚︵︷︹︻︽︿﹁﹃﹙﹛﹝（［｛｢")) + (")" . ,(agda-input-to-string-list ")]}⁆⁾₎〉⎵⟧⟩⟫〉》」』】〕〗〛︶︸︺︼︾﹀﹂﹄﹚﹜﹞）］｝｣")) + + ("[[" . ("⟦")) + ("]]" . ("⟧")) + ("<" . ("⟨")) + (">" . ("⟩")) + ("<<" . ("⟪")) + (">>" . ("⟫")) + + ;; Primes. + + ("'" . ,(agda-input-to-string-list "′″‴⁗")) + ("`" . ,(agda-input-to-string-list "‵‶‷")) + + ;; Fractions. + + ("frac" . ,(agda-input-to-string-list "¼½¾⅓⅔⅕⅖⅗⅘⅙⅚⅛⅜⅝⅞⅟")) + + ;; Bullets. + + ("bu" . ,(agda-input-to-string-list "•◦‣⁌⁍")) + ("bub" . ("•")) + ("buw" . ("◦")) + ("but" . ("‣")) + + ;; Musical symbols. + + ("note" . ,(agda-input-to-string-list "♩♪♫♬")) + ("b" . ("♭")) + ("#" . ("♯")) + + ;; Other punctuation and symbols. + + ("\\" . ("\\")) + ("en" . ("–")) + ("em" . ("—")) + ("^i" . ("ⁱ")) + ("!!" . ("‼")) + ("??" . ("⁇")) + ("?!" . ("‽" "⁈")) + ("!?" . ("⁉")) + ("die" . ,(agda-input-to-string-list "⚀⚁⚂⚃⚄⚅")) + ("asterisk" . ,(agda-input-to-string-list "⁎⁑⁂✢✣✤✥✱✲✳✺✻✼✽❃❉❊❋")) + ("8<" . ("✂" "✄")) + ("tie" . ("⁀")) + ("undertie" . ("‿")) + ("apl" . ,(agda-input-to-string-list "⌶⌷⌸⌹⌺⌻⌼⌽⌾⌿⍀⍁⍂⍃⍄⍅⍆⍇⍈ + ⍉⍊⍋⍌⍍⍎⍏⍐⍑⍒⍓⍔⍕⍖⍗⍘⍙⍚⍛ + ⍜⍝⍞⍟⍠⍡⍢⍣⍤⍥⍦⍧⍨⍩⍪⍫⍬⍭⍮ + ⍯⍰⍱⍲⍳⍴⍵⍶⍷⍸⍹⍺⎕")) + + ;; Shorter forms of many greek letters. + + ("Ga" . ("α")) ("GA" . ("Α")) + ("Gb" . ("β")) ("GB" . ("Β")) + ("Gg" . ("γ")) ("GG" . ("Γ")) + ("Gd" . ("δ")) ("GD" . ("Δ")) + ("Ge" . ("ε")) ("GE" . ("Ε")) + ("Gz" . ("ζ")) ("GZ" . ("Ζ")) + ;; \eta \Eta + ("Gth" . ("θ")) ("GTH" . ("θ")) + ("Gi" . ("ι")) ("GI" . ("Ι")) + ("Gk" . ("κ")) ("GK" . ("Κ")) + ("Gl" . ("λ")) ("GL" . ("Λ")) + ("Gm" . ("μ")) ("GM" . ("Μ")) + ("Gn" . ("ν")) ("GN" . ("Ν")) + ("Gx" . ("ξ")) ("GX" . ("Ξ")) + ;; \omicron \Omicron + ;; \pi \Pi + ("Gr" . ("ρ")) ("GR" . ("Ρ")) + ("Gs" . ("σ")) ("GS" . ("Σ")) + ("Gt" . ("τ")) ("GT" . ("Τ")) + ("Gu" . ("υ")) ("GU" . ("Υ")) + ("Gf" . ("φ")) ("GF" . ("Φ")) + ("Gc" . ("χ")) ("GC" . ("Χ")) + ("Gp" . ("ψ")) ("GP" . ("Ψ")) + ("Go" . ("ω")) ("GO" . ("Ω")) + + ;; Some ISO8859-1 characters. + + (" " . (" ")) + ("!" . ("¡")) + ("cent" . ("¢")) + ("brokenbar" . ("¦")) + ("degree" . ("°")) + ("?" . ("¿")) + ("^a_" . ("ª")) + ("^o_" . ("º")) + + ,@(if (>= emacs-major-version 23) + '(("pounds" . ("£")) + ("currency" . ("¤")) + ("yen" . ("¥")) + ("S" . ("§")) + ("\"{}" . ("¨")) + ("copyright" . ("©")) + ("flqq" . ("«")) + ("\"<" . ("«")) + ("-" . ("­")) + ("registered" . ("®")) + ("={}" . ("¯")) + ("^2" . ("²")) + ("^3" . ("³")) + ("'{}" . ("´")) + ("micro" . ("µ")) + ("P" . ("¶")) + ("c{}" . ("¸")) + ("^1" . ("¹")) + ("frqq" . ("»")) + ("\">" . ("»")) + ("frac14" . ("¼")) + ("frac12" . ("½")) + ("frac34" . ("¾")) + ("`A" . ("À")) + ("'A" . ("Á")) + ("^A" . ("Â")) + ("~A" . ("Ã")) + ("\"A" . ("Ä")) + ("AA" . ("Å")) + ("AE" . ("Æ")) + ("cC" . ("Ç")) + ("`E" . ("È")) + ("'E" . ("É")) + ("^E" . ("Ê")) + ("\"E" . ("Ë")) + ("`I" . ("Ì")) + ("'I" . ("Í")) + ("^I" . ("Î")) + ("\"I" . ("Ï")) + ("DH" . ("Ð")) + ("~N" . ("Ñ")) + ("`O" . ("Ò")) + ("'O" . ("Ó")) + ("^O" . ("Ô")) + ("~O" . ("Õ")) + ("\"O" . ("Ö")) + ("O" . ("Ø")) + ("`U" . ("Ù")) + ("'U" . ("Ú")) + ("^U" . ("Û")) + ("\"U" . ("Ü")) + ("'Y" . ("Ý")) + ("TH" . ("Þ")) + ("ss" . ("ß")) + ("`a" . ("à")) + ("'a" . ("á")) + ("^a" . ("â")) + ("~a" . ("ã")) + ("\"a" . ("ä")) + ("aa" . ("å")) + ("ae" . ("æ")) + ("cc" . ("ç")) + ("`e" . ("è")) + ("'e" . ("é")) + ("^e" . ("ê")) + ("\"e" . ("ë")) + ("`i" . ("ì")) + ("'i" . ("í")) + ("^i" . ("î")) + ("\"i" . ("ï")) + ("dh" . ("ð")) + ("~n" . ("ñ")) + ("`o" . ("ò")) + ("'o" . ("ó")) + ("^o" . ("ô")) + ("~o" . ("õ")) + ("\"o" . ("ö")) + ("o" . ("ø")) + ("`u" . ("ù")) + ("'u" . ("ú")) + ("^u" . ("û")) + ("\"u" . ("ü")) + ("'y" . ("ý")) + ("th" . ("þ")) + ("\"y" . ("ÿ")))) + + ;; Circled, parenthesised etc. numbers and letters. + + ( "(0)" . ,(agda-input-to-string-list " ⓪")) + ( "(1)" . ,(agda-input-to-string-list "⑴①⒈❶➀➊")) + ( "(2)" . ,(agda-input-to-string-list "⑵②⒉❷➁➋")) + ( "(3)" . ,(agda-input-to-string-list "⑶③⒊❸➂➌")) + ( "(4)" . ,(agda-input-to-string-list "⑷④⒋❹➃➍")) + ( "(5)" . ,(agda-input-to-string-list "⑸⑤⒌❺➄➎")) + ( "(6)" . ,(agda-input-to-string-list "⑹⑥⒍❻➅➏")) + ( "(7)" . ,(agda-input-to-string-list "⑺⑦⒎❼➆➐")) + ( "(8)" . ,(agda-input-to-string-list "⑻⑧⒏❽➇➑")) + ( "(9)" . ,(agda-input-to-string-list "⑼⑨⒐❾➈➒")) + ("(10)" . ,(agda-input-to-string-list "⑽⑩⒑❿➉➓")) + ("(11)" . ,(agda-input-to-string-list "⑾⑪⒒")) + ("(12)" . ,(agda-input-to-string-list "⑿⑫⒓")) + ("(13)" . ,(agda-input-to-string-list "⒀⑬⒔")) + ("(14)" . ,(agda-input-to-string-list "⒁⑭⒕")) + ("(15)" . ,(agda-input-to-string-list "⒂⑮⒖")) + ("(16)" . ,(agda-input-to-string-list "⒃⑯⒗")) + ("(17)" . ,(agda-input-to-string-list "⒄⑰⒘")) + ("(18)" . ,(agda-input-to-string-list "⒅⑱⒙")) + ("(19)" . ,(agda-input-to-string-list "⒆⑲⒚")) + ("(20)" . ,(agda-input-to-string-list "⒇⑳⒛")) + + ("(a)" . ,(agda-input-to-string-list "⒜Ⓐⓐ")) + ("(b)" . ,(agda-input-to-string-list "⒝Ⓑⓑ")) + ("(c)" . ,(agda-input-to-string-list "⒞Ⓒⓒ")) + ("(d)" . ,(agda-input-to-string-list "⒟Ⓓⓓ")) + ("(e)" . ,(agda-input-to-string-list "⒠Ⓔⓔ")) + ("(f)" . ,(agda-input-to-string-list "⒡Ⓕⓕ")) + ("(g)" . ,(agda-input-to-string-list "⒢Ⓖⓖ")) + ("(h)" . ,(agda-input-to-string-list "⒣Ⓗⓗ")) + ("(i)" . ,(agda-input-to-string-list "⒤Ⓘⓘ")) + ("(j)" . ,(agda-input-to-string-list "⒥Ⓙⓙ")) + ("(k)" . ,(agda-input-to-string-list "⒦Ⓚⓚ")) + ("(l)" . ,(agda-input-to-string-list "⒧Ⓛⓛ")) + ("(m)" . ,(agda-input-to-string-list "⒨Ⓜⓜ")) + ("(n)" . ,(agda-input-to-string-list "⒩Ⓝⓝ")) + ("(o)" . ,(agda-input-to-string-list "⒪Ⓞⓞ")) + ("(p)" . ,(agda-input-to-string-list "⒫Ⓟⓟ")) + ("(q)" . ,(agda-input-to-string-list "⒬Ⓠⓠ")) + ("(r)" . ,(agda-input-to-string-list "⒭Ⓡⓡ")) + ("(s)" . ,(agda-input-to-string-list "⒮Ⓢⓢ")) + ("(t)" . ,(agda-input-to-string-list "⒯Ⓣⓣ")) + ("(u)" . ,(agda-input-to-string-list "⒰Ⓤⓤ")) + ("(v)" . ,(agda-input-to-string-list "⒱Ⓥⓥ")) + ("(w)" . ,(agda-input-to-string-list "⒲Ⓦⓦ")) + ("(x)" . ,(agda-input-to-string-list "⒳Ⓧⓧ")) + ("(y)" . ,(agda-input-to-string-list "⒴Ⓨⓨ")) + ("(z)" . ,(agda-input-to-string-list "⒵Ⓩⓩ")) + + )) + "A list of translations specific to the Agda input method. +Each element is a pair (KEY-SEQUENCE-STRING . LIST-OF-TRANSLATION-STRINGS). +All the translation strings are possible translations +of the given key sequence; if there is more than one you can choose +between them using the arrow keys. + +Note that if you customize this setting you will not +automatically benefit (or suffer) from modifications to its +default value when the library is updated. If you just want to +add some bindings it is probably a better idea to customize +`agda-input-user-translations'. + +If you change this setting manually (without using the +customization buffer) you need to call `agda-input-setup' in +order for the change to take effect." + :group 'agda-input + :set 'agda-input-incorporate-changed-setting + :initialize 'custom-initialize-default + :type '(repeat (cons (string :tag "Key sequence") + (repeat :tag "Translations" string)))) + + +(defcustom agda-input-user-translations nil + "Like `agda-input-translations', but more suitable for user +customizations since by default it is empty." + :group 'agda-input + :set 'agda-input-incorporate-changed-setting + :initialize 'custom-initialize-default + :type '(repeat (cons (string :tag "Key sequence") + (repeat :tag "Translations" string)))) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Inspecting and modifying translation maps + +(defun agda-input-get-translations (qp) + "Return a list containing all translations from the Quail +package QP (except for those corresponding to ASCII). +Each pair in the list has the form (KEY-SEQUENCE . TRANSLATION)." + (with-temp-buffer + (activate-input-method qp) ; To make sure that the package is loaded. + (unless (quail-package qp) + (error "%s is not a Quail package." qp)) + (let ((decode-map (list 'decode-map))) + (quail-build-decode-map (list (quail-map)) "" decode-map 0) + (cdr decode-map)))) + +(defun agda-input-show-translations (qp) + "Display all translations used by the Quail package QP (a string). +\(Except for those corresponding to ASCII)." + (interactive (list (read-input-method-name + "Quail input method (default %s): " "Agda"))) + (let ((buf (concat "*" qp " input method translations*"))) + (with-output-to-temp-buffer buf + (with-current-buffer buf + (quail-insert-decode-map + (cons 'decode-map (agda-input-get-translations qp))))))) + +(defun agda-input-add-translations (trans) + "Add the given translations TRANS to the Agda input method. +TRANS is a list of pairs (KEY-SEQUENCE . TRANSLATION)." + (with-temp-buffer + (dolist (tr (agda-input-concat-map (eval agda-input-tweak-all) trans)) + (quail-defrule (car tr) (cdr tr) "Agda" t)))) + +(defun agda-input-inherit-package (qp &optional fun) + "Let the Agda input method inherit the translations from the +Quail package QP (except for those corresponding to ASCII). + +The optional function FUN can be used to modify the translations. +It is given a pair (KEY-SEQUENCE . TRANSLATION) and should return +a list of such pairs." + (let ((trans (agda-input-get-translations qp))) + (agda-input-add-translations + (if fun (agda-input-concat-map fun trans) + trans)))) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Setting up the input method + +(defun agda-input-setup () + "Set up the Agda input method based on the customisable +variables and underlying input methods." + + ;; Create (or reset) the input method. + (with-temp-buffer + (quail-define-package "Agda" "UTF-8" "∏" t ; guidance + "Agda input method. +The purpose of this input method is to edit Agda programs, but +since it is highly customisable it can be made useful for other +tasks as well." + nil nil nil nil nil nil t ; maximum-shortest + )) + + (agda-input-add-translations + (mapcar (lambda (tr) (cons (car tr) (vconcat (cdr tr)))) + (append agda-input-user-translations + agda-input-translations))) + (dolist (def agda-input-inherit) + (agda-input-inherit-package (car def) + (eval (cdr def))))) + +(defun agda-input-incorporate-changed-setting (sym val) + "Update the Agda input method based on the customisable +variables and underlying input methods. +Suitable for use in the :set field of `defcustom'." + (set-default sym val) + (agda-input-setup)) + +;; Set up the input method. + +(agda-input-setup) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Administrative details + +(provide 'agda-input) +;;; agda-input.el ends here diff --git a/src/data/emacs-mode/agda2-abbrevs.el b/src/data/emacs-mode/agda2-abbrevs.el new file mode 100644 --- /dev/null +++ b/src/data/emacs-mode/agda2-abbrevs.el @@ -0,0 +1,105 @@ +;; agda2-abbrevs.el --- Default Agda abbrevs + +;;; Commentary: + +;;; Code: + +;; Skeletons + +(require 'skeleton) + +(define-skeleton agda2-abbrevs-module + "Inserts a module header template." + nil + "module " _ " where\n") + +(define-skeleton agda2-abbrevs-data + "Inserts a data template." + nil + "data " _ " : Set where\n") + +(define-skeleton agda2-abbrevs-codata + "Inserts a codata template." + nil + "codata " _ " : Set where\n") + +(define-skeleton agda2-abbrevs-record + "Inserts a record type template." + nil + "record " _ " : Set where\n" + " field\n") + +(define-skeleton agda2-abbrevs-record-value + "Inserts a record value template." + nil + "record {" _ "}") + +(define-skeleton agda2-abbrevs-using + "Inserts a using template." + nil + "using (" _ ")") + +(define-skeleton agda2-abbrevs-hiding + "Inserts a hiding template." + nil + "hiding (" _ ")") + +(define-skeleton agda2-abbrevs-renaming + "Inserts a renaming template." + nil + "renaming (" _ " to " _ ")") + +(define-skeleton agda2-abbrevs-forall + "Inserts a forall template." + nil + "∀ {" _ "} ") + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Abbrevs + +(defvar agda2-abbrevs-defaults '( + ("m" "" agda2-abbrevs-module) + ("d" "" agda2-abbrevs-data) + ("c" "" agda2-abbrevs-codata) + ("re" "" agda2-abbrevs-record) + ("rv" "" agda2-abbrevs-record-value) + ("u" "" agda2-abbrevs-using) + ("h" "" agda2-abbrevs-hiding) + ("r" "" agda2-abbrevs-renaming) + ("w" "where\n") + ("po" "postulate") + ("a" "abstract\n") + ("pr" "private\n") + ("pu" "public") + ("mu" "mutual\n") + ("f" "" agda2-abbrevs-forall) + ("oi" "open import ")) + "Abbreviations defined by default in the Agda mode.") + +(defcustom agda2-mode-abbrevs-use-defaults t + "If non-nil include the default Agda mode abbrevs in `agda2-mode-abbrev-table'. +The abbrevs are designed to be expanded explicitly, so users of `abbrev-mode' +probably do not want to include them. + +Restart Emacs in order for this change to take effect." + :group 'agda2 + :type '(choice (const :tag "Yes" t) + (const :tag "No" nil))) + +(defvar agda2-mode-abbrev-table nil + "Agda mode abbrev table.") + +(define-abbrev-table + 'agda2-mode-abbrev-table + (if agda2-mode-abbrevs-use-defaults + (mapcar (lambda (abbrev) + (append abbrev + (make-list (- 4 (length abbrev)) nil) + '((:system t)))) + agda2-abbrevs-defaults))) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Administrative details + +(provide 'agda2-abbrevs) +;;; agda2-abbrevs.el ends here diff --git a/src/data/emacs-mode/agda2-highlight.el b/src/data/emacs-mode/agda2-highlight.el new file mode 100644 --- /dev/null +++ b/src/data/emacs-mode/agda2-highlight.el @@ -0,0 +1,314 @@ +;;; agda2-highlight.el --- Syntax highlighting for Agda (version ≥ 2) + +;;; Commentary: + +;; Code to apply syntactic highlighting to Agda source code. This uses +;; Agda's own annotations to figure out what is what, so the parsing +;; is always done correctly, but highlighting is not done on the fly. + +;;; Code: + +(require 'annotation) +(require 'font-lock) + +(defgroup agda2-highlight nil + "Syntax highlighting for Agda." + :group 'agda2) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Functions for setting faces + +(defun agda2-highlight-set-face-attribute (face attrs) + "Reset (globally) all attributes of the face FACE according to ATTRS. +If the face does not exist, then it is created first." + (make-face face) + (set-face-attribute face nil + :family 'unspecified + :width 'unspecified + :height 'unspecified + :weight 'unspecified + :slant 'unspecified + :foreground 'unspecified + :background 'unspecified + :inverse-video 'unspecified + :stipple 'unspecified + :underline 'unspecified + :overline 'unspecified + :strike-through 'unspecified + :inherit 'unspecified + :box 'unspecified + :font 'unspecified) + (eval `(set-face-attribute face nil ,@attrs))) + +(defun agda2-highlight-set-faces (variable group) + "Set all Agda faces according to the value of GROUP. +Also sets the default value of VARIABLE to GROUP." + (set-default variable group) + (mapc (lambda (face-and-attrs) + (agda2-highlight-set-face-attribute + (car face-and-attrs) (cdr face-and-attrs))) + (cond + ((equal group 'conor) + '((agda2-highlight-keyword-face + :underline t) + (agda2-highlight-string-face) + (agda2-highlight-number-face) + (agda2-highlight-symbol-face) + (agda2-highlight-primitive-type-face + :foreground "blue") + (agda2-highlight-bound-variable-face + :foreground "purple") + (agda2-highlight-inductive-constructor-face + :foreground "dark red") + (agda2-highlight-coinductive-constructor-face + :foreground "dark red") + (agda2-highlight-datatype-face + :foreground "blue") + (agda2-highlight-field-face + :foreground "dark red") + (agda2-highlight-function-face + :foreground "dark green") + (agda2-highlight-module-face + :foreground "dark green") + (agda2-highlight-postulate-face + :foreground "dark green") + (agda2-highlight-primitive-face + :foreground "dark green") + (agda2-highlight-record-face + :foreground "blue") + (agda2-highlight-dotted-face) + (agda2-highlight-error-face + :foreground "black" + :background "sandy brown") + (agda2-highlight-unsolved-meta-face + :foreground "black" + :background "gold") + (agda2-highlight-termination-problem-face + :foreground "black" + :background "red") + (agda2-highlight-incomplete-pattern-face + :foreground "black" + :background "purple")))))) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Faces + +(defcustom agda2-highlight-face-groups nil + "Colour scheme to use for agda2 highlight faces. +Note that changing this option does not remove the customisations +below; you can get them back by resetting this option and +restarting Emacs." + :type '(choice + (const :tag "Use the settings below." nil) + (const :tag "Use an approximation of Conor McBride's colour scheme." + conor)) + :group 'agda2-highlight + :set 'agda2-highlight-set-faces) + +(defface agda2-highlight-keyword-face + '((t (:foreground "DarkOrange3"))) + "The face used for keywords." + :group 'agda2-highlight) + +(defface agda2-highlight-string-face + '((t (:foreground "firebrick"))) + "The face used for strings." + :group 'agda2-highlight) + +(defface agda2-highlight-number-face + '((t (:foreground "purple"))) + "The face used for numbers." + :group 'agda2-highlight) + +(defface agda2-highlight-symbol-face + '((((background light)) + (:foreground "gray25")) + (((background dark)) + (:foreground "gray75"))) + "The face used for symbols like forall, =, ->, etc." + :group 'agda2-highlight) + +(defface agda2-highlight-primitive-type-face + '((t (:foreground "medium blue"))) + "The face used for primitive types (like Set and Prop)." + :group 'agda2-highlight) + +(defface agda2-highlight-bound-variable-face + '((t nil)) + "The face used for bound variables." + :group 'agda2-highlight) + +(defface agda2-highlight-inductive-constructor-face + '((t (:foreground "green4"))) + "The face used for inductive constructors." + :group 'agda2-highlight) + +(defface agda2-highlight-coinductive-constructor-face + '((t (:foreground "gold4"))) + "The face used for coinductive constructors." + :group 'agda2-highlight) + +(defface agda2-highlight-datatype-face + '((t (:foreground "medium blue"))) + "The face used for datatypes." + :group 'agda2-highlight) + +(defface agda2-highlight-field-face + '((t (:foreground "DeepPink2"))) + "The face used for record fields." + :group 'agda2-highlight) + +(defface agda2-highlight-function-face + '((t (:foreground "medium blue"))) + "The face used for functions." + :group 'agda2-highlight) + +(defface agda2-highlight-module-face + '((t (:foreground "purple"))) + "The face used for module names." + :group 'agda2-highlight) + +(defface agda2-highlight-postulate-face + '((t (:foreground "medium blue"))) + "The face used for postulates." + :group 'agda2-highlight) + +(defface agda2-highlight-primitive-face + '((t (:foreground "medium blue"))) + "The face used for primitive functions." + :group 'agda2-highlight) + +(defface agda2-highlight-record-face + '((t (:foreground "medium blue"))) + "The face used for record types." + :group 'agda2-highlight) + +(defface agda2-highlight-dotted-face + '((t nil)) + "The face used for dotted patterns." + :group 'agda2-highlight) + +(defface agda2-highlight-operator-face + '((t nil)) + "The face used for operators." + :group 'agda2-highlight) + +(defface agda2-highlight-error-face + '((t (:foreground "red" :underline t))) + "The face used for errors." + :group 'agda2-highlight) + +(defface agda2-highlight-unsolved-meta-face + '((t (:background "yellow" + :foreground "black"))) + "The face used for unsolved meta variables." + :group 'agda2-highlight) + +(defface agda2-highlight-termination-problem-face + '((t (:background "light salmon" + :foreground "black"))) + "The face used for termination problems." + :group 'agda2-highlight) + +(defface agda2-highlight-incomplete-pattern-face + '((t (:background "wheat" + :foreground "black"))) + "The face used for incomplete patterns. (Currently unused.)" + :group 'agda2-highlight) + +(defvar agda2-highlight-faces + '((keyword . agda2-highlight-keyword-face) + (string . agda2-highlight-string-face) + (number . agda2-highlight-number-face) + (symbol . agda2-highlight-symbol-face) + (primitivetype . agda2-highlight-primitive-type-face) + (bound . agda2-highlight-bound-variable-face) + (inductiveconstructor . agda2-highlight-inductive-constructor-face) + (coinductiveconstructor . agda2-highlight-coinductive-constructor-face) + (datatype . agda2-highlight-datatype-face) + (field . agda2-highlight-field-face) + (function . agda2-highlight-function-face) + (module . agda2-highlight-module-face) + (postulate . agda2-highlight-postulate-face) + (primitive . agda2-highlight-primitive-face) + (record . agda2-highlight-record-face) + (dotted . agda2-highlight-dotted-face) + (operator . agda2-highlight-operator-face) + (error . agda2-highlight-error-face) + (unsolvedmeta . agda2-highlight-unsolved-meta-face) + (terminationproblem . agda2-highlight-termination-problem-face) + (incompletepattern . agda2-highlight-incomplete-pattern-face)) + "Alist mapping code aspects to the face used when displaying them. + +The aspects currently recognised are the following: + +`bound' Bound variables. +`coinductiveconstructor' Coinductive constructors. +`datatype' Data types. +`dotted' Dotted patterns. +`error' Errors. +`field' Record fields. +`function' Functions. +`incompletepattern' Incomplete patterns. +`inductiveconstructor' Inductive constructors. +`keyword' Keywords. +`module' Module names. +`number' Numbers. +`operator' Operators. +`postulate' Postulates. +`primitive' Primitive functions. +`primitivetype' Primitive types (like Set and Prop). +`record' Record types. +`string' Strings. +`symbol' Symbols like forall, =, ->, etc. +`terminationproblem' Termination problems. +`unsolvedmeta' Unsolved meta variables. + +The following aspect is ignored: + +`comment' Comments. + +Comments are handled by Font Lock mode (which uses the syntax +table). The face `font-lock-comment-face' is used for comments.") + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Functions + +(defun agda2-highlight-reload nil + "Reload current buffer's syntax information from the syntax file." + (interactive) + (let* ((dir (file-name-directory buffer-file-name)) + (name (file-name-nondirectory buffer-file-name)) + (file (concat dir "." name ".el")) + (inhibit-read-only t)) + ;; Ignore read-only status, otherwise this function may fail. + (annotation-load-file + file + ;; Do not remove the old annotations if all the new ones + ;; correspond to errors, or if there are no new ones. + (lambda (anns) (not (member anns '((error) nil))))))) + +(defun agda2-highlight-setup nil + "Set up the `annotation' library for use with `agda2-mode'." + (font-lock-mode 0) + (setq annotation-bindings agda2-highlight-faces)) + +(defun agda2-highlight-clear nil + "Remove all syntax highlighting added by `agda2-highlight-reload'." + (interactive) + (let ((inhibit-read-only t)) + ; Ignore read-only status, otherwise this function may fail. + (annotation-remove-annotations))) + +(defun agda2-highlight-reload-or-clear (&optional arg) + "Reload syntax highlighting information. +With prefix argument ARG: Remove syntax highlighting." + (interactive "P") + (if arg (agda2-highlight-clear) + (agda2-highlight-reload))) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Administrative details + +(provide 'agda2-highlight) +;;; agda2-highlight.el ends here diff --git a/src/data/emacs-mode/agda2-mode.el b/src/data/emacs-mode/agda2-mode.el new file mode 100644 --- /dev/null +++ b/src/data/emacs-mode/agda2-mode.el @@ -0,0 +1,1004 @@ +;;; agda2-mode.el --- Major mode for Agda2 + +;;; Commentary: + +;; + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;;; Dependency + + +;;; Code: + +(defvar agda2-version "2.2.2" + "The version of the Agda mode. +Note that, by default, the same version of the underlying Haskell +library is used (see `agda2-ghci-options').") + +(require 'cl) ; haskell-indent requires it anyway. +(set (make-local-variable 'lisp-indent-function) + 'common-lisp-indent-function) +(require 'comint) +(require 'pp) +(require 'eri) +(require 'annotation) +(require 'agda-input) +(require 'agda2-highlight) +(require 'agda2-abbrevs) +(require 'haskell-indent) +(require 'haskell-ghci) +;; due to a bug in haskell-mode-2.1 +(setq haskell-ghci-mode-map (copy-keymap comint-mode-map)) +;; Load filladapt, if it is installed. +(condition-case nil + (require 'filladapt) + (error nil)) +(unless (fboundp 'overlays-in) (load "overlay")) ; for Xemacs +(unless (fboundp 'propertize) ; for Xemacs 21.4 + (defun propertize (string &rest properties) + "Return a copy of STRING with text properties added. +First argument is the string to copy. +Remaining arguments form a sequence of PROPERTY VALUE pairs for text +properties to add to the result." + (let ((str (copy-sequence string))) + (add-text-properties 0 (length str) properties str) + str))) +(unless (fboundp 'run-mode-hooks) + (fset 'run-mode-hooks 'run-hooks)) ; For Emacs versions < 21. + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;;; Programming utilities + +(defmacro agda2-protect (form &optional default) + "Expands to (condition-case nil FORM (error DEFAULT))." + `(condition-case nil ,form (error ,default))) +(put 'agda2-protect 'lisp-indent-function 0) + +(defmacro agda2-let (varbind funcbind &rest body) + "Expands to (let* VARBIND (labels FUNCBIND BODY...))." + `(let* ,varbind (labels ,funcbind ,@body))) +(put 'agda2-let 'lisp-indent-function 2) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;;; User options + +(defgroup agda2 nil + "Major mode for interactively developing Agda programs." + :group 'languages) + +(defcustom agda2-include-dirs + '(".") + "The directories Agda uses to search for files. +The directory names should be relative to the root of the current project." + :type '(repeat directory) + :group 'agda2) + +(defcustom agda2-ghci-options + (list (concat "-package Agda-" agda2-version)) + "Options set in GHCi before loading `agda2-toplevel-module'. +Note that only dynamic options can be set using this variable." + :type '(repeat string) + :group 'agda2) + +(defcustom agda2-toplevel-module "Agda.Interaction.GhciTop" + "The name of the Agda2 toplevel module." + :type 'string :group 'agda2) + +(defcustom agda2-mode-hook + '(agda2-fix-ghci-for-windows) + "Hooks for `agda2-mode'." + :type 'hook :group 'agda2) + +(defcustom agda2-indentation + 'eri + "*The kind of indentation used in `agda2-mode'." + :type '(choice (const :tag "Haskell" haskell) + (const :tag "Extended relative" eri) + (const :tag "None" nil)) + :group 'agda2) + +(defcustom agda2-information-window-max-height + 0.35 + "*The maximum height of the information window. +A multiple of the frame height." + :type 'number + :group 'agda2) + +(defcustom agda2-fontset-name + (unless (eq window-system 'mac) "fontset-agda2") + "Default font to use in the selected frame when activating the Agda2 mode. +This is only used if it's non-nil and Emacs is not running in a terminal. +It is also ignored in Emacs 23 and up, where the improved font handling makes +it unnecessary. + +Note that this setting (if non-nil) affects non-Agda buffers as +well, and that you have to restart Emacs if you want settings to +this variable to take effect." + :type '(choice (string :tag "Fontset name") + (const :tag "Do not change the font" nil)) + :group 'agda2) + +(defcustom agda2-fontset-spec-of-fontset-agda2 + "-*-fixed-Medium-r-Normal-*-18-*-*-*-c-*-fontset-agda2, + ascii:-Misc-Fixed-Medium-R-Normal--18-120-100-100-C-90-ISO8859-1, + latin-iso8859-2:-*-Fixed-*-r-*-*-18-*-*-*-c-*-iso8859-2, + latin-iso8859-3:-*-Fixed-*-r-*-*-18-*-*-*-c-*-iso8859-3, + latin-iso8859-4:-*-Fixed-*-r-*-*-18-*-*-*-c-*-iso8859-4, + cyrillic-iso8859-5:-*-Fixed-*-r-*-*-18-*-*-*-c-*-iso8859-5, + greek-iso8859-7:-*-Fixed-*-r-*-*-18-*-*-*-c-*-iso8859-7, + latin-iso8859-9:-*-Fixed-*-r-*-*-18-*-*-*-c-*-iso8859-9, + mule-unicode-0100-24ff:-Misc-Fixed-Medium-R-Normal--18-120-100-100-C-90-ISO10646-1, + mule-unicode-2500-33ff:-Misc-Fixed-Medium-R-Normal--18-120-100-100-C-90-ISO10646-1, + mule-unicode-e000-ffff:-Misc-Fixed-Medium-R-Normal--18-120-100-100-C-90-ISO10646-1, + japanese-jisx0208:-Misc-Fixed-Medium-R-Normal-ja-18-*-*-*-C-*-JISX0208.1990-0, + japanese-jisx0212:-Misc-Fixed-Medium-R-Normal-ja-18-*-*-*-C-*-JISX0212.1990-0, + thai-tis620:-Misc-Fixed-Medium-R-Normal--24-240-72-72-C-120-TIS620.2529-1, + lao:-Misc-Fixed-Medium-R-Normal--24-240-72-72-C-120-MuleLao-1, + tibetan:-TibMdXA-fixed-medium-r-normal--16-160-72-72-m-160-MuleTibetan-0, + tibetan-1-column:-TibMdXA-fixed-medium-r-normal--16-160-72-72-m-80-MuleTibetan-1, + korean-ksc5601:-Daewoo-Mincho-Medium-R-Normal--16-120-100-100-C-160-KSC5601.1987-0, + chinese-gb2312:-ISAS-Fangsong ti-Medium-R-Normal--16-160-72-72-c-160-GB2312.1980-0, + chinese-cns11643-1:-HKU-Fixed-Medium-R-Normal--16-160-72-72-C-160-CNS11643.1992.1-0, + chinese-big5-1:-ETen-Fixed-Medium-R-Normal--16-150-75-75-C-160-Big5.ETen-0, + chinese-big5-2:-ETen-Fixed-Medium-R-Normal--16-150-75-75-C-160-Big5.ETen-0" + "Specification of the \"fontset-agda2\" fontset. +The \"fontset-agda2\" is the standard setting for `agda2-fontset-name'. +If `agda2-fontset-name' is nil, or Emacs is +run in a terminal, then \"fontset-agda2\" is not created. + +Note that the text \"fontset-agda2\" has to be part of the +string (in a certain way; see the default setting) in order for the +agda2 fontset to be created properly. + +Note also that the default setting may not work unless suitable +fonts are installed on your system. Refer to the README file +accompanying the Agda distribution for details. + +Note finally that you have to restart Emacs if you want settings +to this variable to take effect." + :group 'agda2 + :type 'string) + +(if (and agda2-fontset-name window-system) + (create-fontset-from-fontset-spec agda2-fontset-spec-of-fontset-agda2 t t)) + +(defun agda2-fix-ghci-for-windows () + (if (string-match "windows" system-configuration) + (setq haskell-ghci-program-name "ghc" + haskell-ghci-program-args '("--interactive")))) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;;; Global and buffer-local vars, initialization + +(defvar agda2-mode-syntax-table + (let ((tbl (make-syntax-table))) + ;; Set the syntax of every char to "w" except for those whose default + ;; syntax in `standard-syntax-table' is `paren' or `whitespace'. + (map-char-table (lambda (keys val) + ;; `keys' here can be a normal char, a generic char + ;; (Emacs<23), or a char range (Emacs>=23). + (unless (memq (car val) + (eval-when-compile + (mapcar 'car + (list (string-to-syntax "(") + (string-to-syntax ")") + (string-to-syntax " "))))) + (modify-syntax-entry keys "w" tbl))) + (standard-syntax-table)) + ;; Then override the remaining special cases. + (dolist (cs '((?{ . "(}1n") (?} . "){4n") (?- . "w 123b") (?\n . "> b") + (?. . ".") (?\; . ".") (?_ . ".") (?! . "."))) + (modify-syntax-entry (car cs) (cdr cs) tbl)) + tbl) + "Syntax table used by the Agda 2 mode: + +{} | Comment characters, matching parentheses. +- | Comment character, word constituent. +\n | Comment ender. +.;_! | Punctuation. + +Remaining characters inherit their syntax classes from the +standard syntax table if that table treats them as matching +parentheses or whitespace. Otherwise they are treated as word +constituents.") + +(defconst agda2-command-table + `( + (agda2-load "\C-c\C-l" (global) "Load") + (agda2-load "\C-c\C-x\C-l") + (agda2-compile "\C-c\C-x\C-c" (global) "Compile") + (agda2-text-state "\C-c\C-x\C-d" (global) "Deactivate Agda") + (agda2-quit "\C-c\C-x\C-q" (global) "Quit") + (agda2-restart "\C-c\C-x\C-r" (global) "Restart") + (agda2-display-implicit-arguments "\C-c\C-x\C-h" (global) "Toggle display of hidden arguments") + (agda2-highlight-reload-or-clear "\C-c\C-x\C-s" (global) "Reload syntax highlighting information") + (agda2-show-constraints ,(kbd "C-c C-=") (global) "Show constraints") + (agda2-solveAll ,(kbd "C-c C-s") (global) "Solve constraints") + (agda2-show-goals ,(kbd "C-c C-?") (global) "Show goals") + (agda2-next-goal "\C-c\C-f" (global) "Next goal") ; Forward. + (agda2-previous-goal "\C-c\C-b" (global) "Previous goal") ; Back. + (agda2-give ,(kbd "C-c C-SPC") (local) "Give") + (agda2-refine "\C-c\C-r" (local) "Refine") + (agda2-make-case "\C-c\C-c" (local) "Case") + (agda2-goal-type "\C-c\C-t" (local) "Goal type") + (agda2-show-context "\C-c\C-e" (local) "Context (environment)") + (agda2-infer-type-maybe-toplevel "\C-c\C-d" (local global) "Infer (deduce) type") + (agda2-goal-and-context ,(kbd "C-c C-,") (local) "Goal type and context") + (agda2-goal-and-context-and-inferred ,(kbd "C-c C-.") (local) "Goal type, context and inferred type") + (agda2-compute-normalised-maybe-toplevel "\C-c\C-n" (local global) "Evaluate term to normal form") + (agda2-indent ,(kbd "TAB")) + (agda2-indent-reverse [S-iso-lefttab]) + (agda2-indent-reverse [S-lefttab]) + (agda2-indent-reverse [S-tab]) + (agda2-goto-definition-mouse [mouse-2]) + (agda2-goto-definition-keyboard "\M-.") + (agda2-go-back "\M-*") + ) + "Table of commands, used to build keymaps and menus. +Each element has the form (CMD KEY &optional NAME GOAL-NAME) +Where NAME is the name to use in the main Agda2 menu +and GOAL-NAME is for the Agda goal menu.") + +(defvar agda2-mode-map + (let ((map (make-sparse-keymap "Agda mode"))) + (define-key map [menu-bar Agda2] + (cons "Agda2" (make-sparse-keymap "Agda2"))) + (define-key map [down-mouse-3] 'agda2-popup-menu-3) + (dolist (d (reverse agda2-command-table)) + (destructuring-bind (f &optional keys kinds desc) d + (if keys (define-key map keys f)) + (if (member 'global kinds) + (define-key map + (vector 'menu-bar 'Agda2 (intern desc)) (cons desc f))))) + map) + "Keymap for `agda2-mode'.") + +(defvar agda2-goal-map + (let ((map (make-sparse-keymap "Agda goal"))) + (dolist (d (reverse agda2-command-table)) + (destructuring-bind (f &optional keys kinds desc) d + (if (member 'local kinds) + (define-key map + (vector (intern desc)) (cons desc f))))) + map) + "Keymap for agda2 goal menu.") + +(defvar agda2-buffer nil "Agda subprocess buffer. Set in `agda2-restart'.") +(defvar agda2-process nil "Agda subprocess. Set in `agda2-restart'.") + +;; Some buffer locals +(defvar agda2-buffer-external-status "" + "External status of an `agda2-mode' buffer (dictated by the Haskell side).") +(make-variable-buffer-local 'agda2-buffer-external-status) + +(defconst agda2-help-address + "" + "Address accepting submissions of bug reports and questions.") + +;; Annotation for a goal +;; {! .... !} +;; ---------- overlay: agda2-gn num, face highlight, after-string num, +;; modification-hooks (agda2-protect-goal-markers) +;; - text-props: category agda2-delim1 +;; - text-props: category agda2-delim2 +;; - text-props: category agda2-delim3 +;; - text-props: category agda2-delim4 +;; +;; Char categories for {! ... !} +(defvar agda2-open-brace "{") +(defvar agda2-close-brace " }") +(setplist 'agda2-delim1 `(display ,agda2-open-brace)) +(setplist 'agda2-delim2 `(display ,agda2-open-brace rear-nonsticky t + agda2-delim2 t)) +(setplist 'agda2-delim3 `(display ,agda2-close-brace agda2-delim3 t)) +(setplist 'agda2-delim4 `(display ,agda2-close-brace rear-nonsticky t)) + +;; Note that strings used with the display property are compared by +;; reference. If the agda2-*-brace definitions were inlined, then +;; goals would be displayed as "{{ }}n" instead of "{ }n". + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;;; agda2-mode + +;;;###autoload +(add-to-list 'auto-mode-alist '("\\.l?agda\\'" . agda2-mode)) +;;;###autoload +(modify-coding-system-alist 'file "\\.l?agda\\'" 'utf-8) +;;;###autoload +(define-derived-mode agda2-mode nil "Agda2" + "Major mode for agda2 files. + +Note that when this mode is activated the default font of the +current frame is changed to the fontset `agda2-fontset-name'. +The reason is that Agda programs often use mathematical symbols +and other Unicode characters, so we try to provide a suitable +default font setting, which can display many of the characters +encountered. If you prefer to use your own settings, set +`agda2-fontset-name' to nil. + +Special commands: +\\{agda2-mode-map}" + (setq local-abbrev-table agda2-mode-abbrev-table + indent-tabs-mode nil + mode-line-process + '((:eval (unless (eq 0 (length agda2-buffer-external-status)) + (concat ":" agda2-buffer-external-status))))) + (let ((l '(max-specpdl-size 2600 + max-lisp-eval-depth 2800))) + (while l (set (make-local-variable (pop l)) (pop l)))) + (if (and window-system agda2-fontset-name + ;; Emacs-23 uses a revamped font engine which should make + ;; agda2-fontset-name unnecessary in most cases. And if it turns out + ;; to be necessary, we should probably use face-remapping-alist + ;; rather than set-frame-font so the special font only applies to + ;; Agda buffers, and so it applies in all frames where Agda + ;; buffers are displayed. + (not (boundp 'face-remapping-alist))) + (condition-case nil + (set-frame-font agda2-fontset-name) + (error (error "Unable to change the font; change agda2-fontset-name or tweak agda2-fontset-spec-fontset-agda2")))) + (agda2-indent-setup) + (agda2-highlight-setup) + (agda2-highlight-reload) + (agda2-comments-and-paragraphs-setup) + (force-mode-line-update) + (set-input-method "Agda")) + +(defun agda2-restart () + "Kill and restart the *ghci* buffer and load `agda2-toplevel-module'." + (interactive) + (save-excursion (let ((agda2-bufname "*ghci*") + (ignore-dot-ghci "-ignore-dot-ghci")) + (agda2-protect (kill-buffer agda2-bufname)) + ;; Make sure that the user's .ghci is not read. + ;; Users can override this by adding + ;; "-read-dot-ghci" to + ;; `haskell-ghci-program-args'. + (unless (equal (car-safe haskell-ghci-program-args) + ignore-dot-ghci) + (set (make-local-variable 'haskell-ghci-program-args) + (cons ignore-dot-ghci haskell-ghci-program-args))) + (haskell-ghci-start-process nil) + (setq agda2-process haskell-ghci-process + agda2-buffer haskell-ghci-process-buffer + mode-name "Agda2 GHCi") + (set-buffer-file-coding-system 'utf-8) + (set-buffer-process-coding-system 'utf-8 'utf-8) + (rename-buffer agda2-bufname))) + (apply 'agda2-go ":set" agda2-ghci-options) + (agda2-go ":mod +" agda2-toplevel-module) + (agda2-text-state)) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;;; Communicating with Agda2 + +(defun agda2-go (&rest args) + "Send the list ARGS of strings to ghci, then +wait for output and execute responses, if any" + (interactive) + (unless (eq 'run (agda2-process-status)) + ;; Try restarting automatically, but only once, in case there is + ;; some major problem. + (agda2-restart) + (unless (eq 'run (agda2-process-status)) + (error "Problem encountered. The *ghci* buffer can perhaps explain why."))) + (save-excursion + (haskell-ghci-go (apply 'concat (agda2-intersperse " " args)) nil)) + ;;(display-buffer agda2-buffer 'not-tihs-window) + (let (response) + (with-current-buffer haskell-ghci-process-buffer + (haskell-ghci-wait-for-output) + ;; Note that the following code may be prone to race conditions + ;; (make-temp-file returns a filename, not an open file). This is + ;; not likely to be a problem, though. + (let ((tempfile (make-temp-file "agda2-mode"))) + (unwind-protect + (progn + (comint-write-output tempfile) + (with-temp-buffer + (insert-file-contents tempfile) + (setq response (buffer-substring-no-properties + (point-min) (point-max))))) + (delete-file tempfile)))) + (agda2-respond response))) + +(defun agda2-goal-cmd (cmd &optional want ask &rest args) + "When in a goal, send CMD, goal num and range, and strings ARGS to agda2. +WANT is an optional prompt. When ASK is non-nil, use minibuffer." + (multiple-value-bind (o g) (agda2-goal-at (point)) + (unless g (error "For this command, please place the cursor in a goal")) + (let ((txt (buffer-substring-no-properties (+ (overlay-start o) 2) + (- (overlay-end o) 2)))) + (if (not want) (setq txt "") + (when (or ask (string-match "\\`\\s *\\'" txt)) + (setq txt (read-string (concat want ": ") txt)))) + (apply 'agda2-go cmd + (format "%d" g) + (agda2-goal-Range o) + (agda2-string-quote txt) args)))) + +;; Note that the following function is a security risk, since it +;; evaluates code without first inspecting it. The code (supposedly) +;; comes from the Agda backend, but there could be bugs in the backend +;; which can be exploited by an attacker which manages to trick +;; someone into type-checking compromised Agda code. + +(defun agda2-respond (response) + "Execute 'agda2_mode_code' within RESPONSE string." + (while (string-match "agda2_mode_code" response) + (setq response (substring response (match-end 0))) + (let ((inhibit-read-only t)) + (eval (read response))))) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;;; User commands and response processing + +(defun agda2-load () + "Load current buffer." + (interactive) + (agda2-go "cmd_load" + (agda2-string-quote (buffer-file-name)) + (agda2-list-quote agda2-include-dirs) + )) + +(defun agda2-compile () + "Compile the current module." + (interactive) + (agda2-go "cmd_compile" + (agda2-string-quote (buffer-file-name)) + (agda2-list-quote agda2-include-dirs) + )) + +(defun agda2-load-action (gs) + "Annotate new goals GS in current buffer." + (agda2-annotate gs)) + +(defun agda2-give() + "Give to the goal at point the expression in it" (interactive) + (agda2-goal-cmd "cmd_give" "expression to give")) + +(defun agda2-give-action (old-g paren) + "Update the goal OLD-G with the expression in it." + (agda2-update old-g paren)) + +(defun agda2-refine () + "Refine the goal at point by the expression in it." (interactive) + (agda2-goal-cmd "cmd_refine" "expression to refine")) + +(defun agda2-make-case () + "Refine the pattern var given in the goal. +Assumes that = {!!} is on one line." + (interactive) + (agda2-goal-cmd "cmd_make_case" "partten var to case")) + +(defun agda2-make-case-action (newcls) + "Replace the line at point with new clauses NEWCLS and reload." + (agda2-forget-all-goals);; we reload later anyway. + (let* ((p0 (point)) + ;; (p1 (goto-char (agda2-decl-beginning))) + (p1 (goto-char (+ (current-indentation) (line-beginning-position)))) + (indent (current-column)) + cl) + (goto-char p0) + (re-search-forward "!}" (line-end-position) 'noerr) + (delete-region p1 (point)) + (while (setq cl (pop newcls)) + (insert cl) + (if newcls (insert "\n" (make-string indent ? )))) + (goto-char p1)) + (agda2-load)) + +(defun agda2-status-action (status) + "Display the string STATUS in the current buffer's mode line. +\(precondition: the current buffer has to use the Agda mode as the +major mode)." + (setq agda2-buffer-external-status status)) + +(defun agda2-info-action (name text) + "Insert TEXT into the Agda info buffer, display it, and display NAME +in the buffer's mode line." + (interactive) + (with-current-buffer (get-buffer-create "*Agda2 information*") + (erase-buffer) + (insert text) + (set-syntax-table agda2-mode-syntax-table) + (set-input-method "Agda") + (goto-char (point-min)) + (put-text-property 0 (length name) 'face '(:weight bold) name) + (setq mode-line-buffer-identification name) + (save-selected-window + (pop-to-buffer (current-buffer) 'not-this-window 'norecord) + (shrink-window + (- (window-height) + (min (truncate + (* (frame-height) agda2-information-window-max-height)) + (max window-min-height + (1+ (count-lines (point-min) (point-max)))))))))) + +(defun agda2-show-goals() + "Show all goals." (interactive) + (agda2-go "cmd_metas")) + +(defun agda2-show-constraints() + "Show constraints." (interactive) + (agda2-go "cmd_constraints")) + +(defun agda2-text-state () + "UNDER CONSTRUCTION" (interactive) + (dolist (o (overlays-in (point-min) (point-max))) + (delete-overlay o)) + (agda2-go "cmd_reset") + (let ((inhibit-read-only t)) + (annotation-preserve-mod-p-and-undo + (set-text-properties (point-min) (point-max) '())) + (force-mode-line-update))) + +(defun agda2-next-goal () "Go to the next goal, if any." (interactive) + (agda2-mv-goal 'next-single-property-change 'agda2-delim2 1 (point-min))) +(defun agda2-previous-goal () "Go to the previous goal, if any." (interactive) + (agda2-mv-goal 'previous-single-property-change 'agda2-delim3 0 (point-max))) +(defun agda2-mv-goal (change delim adjust wrapped) + (agda2-let () + ((go (p) (while (and (setq p (funcall change p 'category)) + (not (eq (get-text-property p 'category) delim)))) + (if p (goto-char (+ adjust p))))) + (or (go (point)) (go wrapped) (message "No goals in the buffer")))) + +(defun agda2-quit () + "Quit and clean up after agda2." (interactive) + (agda2-protect (progn (kill-buffer agda2-buffer) + (kill-buffer (current-buffer))))) + +(defmacro agda2-maybe-normalised (name comment cmd prompt) + "This macro constructs a function NAME which runs CMD. +COMMENT is used to build the function's comment. The function +NAME takes a prefix argument which tells whether it should +normalise types or not when running CMD (through +`agda2-goal-cmd'; PROMPT, if non-nil, is used as the goal command +prompt)." + (let ((eval (make-symbol "eval"))) + `(defun ,name (&optional not-normalise) + ,(concat comment ". + +With a prefix argument the result is not explicitly normalised.") + (interactive "P") + (let ((,eval (if not-normalise "Instantiated" "Normalised"))) + (agda2-goal-cmd (concat ,cmd " Agda.Interaction.BasicOps." ,eval) + ,prompt))))) + +(defmacro agda2-maybe-normalised-toplevel (name comment cmd prompt) + "This macro constructs a function NAME which runs CMD. +COMMENT is used to build the function's comments. The function +NAME takes a prefix argument which tells whether it should +normalise types or not when running CMD (through `agda2-go'; the +string PROMPT is used as the goal command prompt)." + (let ((eval (make-symbol "eval"))) + `(defun ,name (not-normalise expr) + ,(concat comment ". + +With a prefix argument the result is not explicitly normalised.") + (interactive ,(concat "P\nM" prompt ": ")) + (let ((,eval (if not-normalise "Instantiated" "Normalised"))) + (agda2-go (concat ,cmd " Agda.Interaction.BasicOps." ,eval " " + (agda2-string-quote expr))))))) + +(agda2-maybe-normalised + agda2-goal-type + "Show the type of the goal at point" + "cmd_goal_type" + nil) + +(agda2-maybe-normalised + agda2-infer-type + "Infer the type of the goal at point" + "cmd_infer" + "expression to type") + +(agda2-maybe-normalised-toplevel + agda2-infer-type-toplevel + "Infers the type of the given expression. The scope used for +the expression is that of the last point inside the current +top-level module" + "cmd_infer_toplevel" + "Expression") + +(defun agda2-infer-type-maybe-toplevel () + "Infers the type of the given expression. +Either uses the scope of the current goal or, if point is not in a goal, the +top-level scope." + (interactive) + (call-interactively (if (agda2-goal-at (point)) + 'agda2-infer-type + 'agda2-infer-type-toplevel))) + +(agda2-maybe-normalised + agda2-goal-and-context + "Shows the type of the goal at point and the currect context" + "cmd_goal_type_context" + nil) + +(agda2-maybe-normalised + agda2-goal-and-context-and-inferred + "Shows the context, the goal and the given expression's inferred type" + "cmd_goal_type_context_infer" + "expression to type") + +(agda2-maybe-normalised + agda2-show-context + "Show the context of the goal at point" + "cmd_context" + nil) + +(defun agda2-solveAll () + "Solve all goals that are internally already instantiated." (interactive) + (agda2-go "cmd_solveAll" )) + +(defun agda2-solveAll-action (iss) + (save-excursion + (while iss + (let* ((g (pop iss)) (txt (pop iss))) + (agda2-replace-goal g txt) + (agda2-goto-goal g) + (agda2-give))))) + +(defun agda2-compute-normalised (&optional arg) + "Compute the normal form of the expression in the goal at point. +With a prefix argument \"abstract\" is ignored during the computation." + (interactive "P") + (let ((cmd (concat "cmd_compute" + (if arg " True" " False")))) + (agda2-goal-cmd cmd "expression to normalise"))) + +(defun agda2-compute-normalised-toplevel (expr &optional arg) + "Computes the normal form of the given expression. +The scope used for the expression is that of the last point inside the current +top-level module. +With a prefix argument \"abstract\" is ignored during the computation." + (interactive "MExpression: \nP") + (let ((cmd (concat "cmd_compute_toplevel" + (if arg " True" " False") + " "))) + (agda2-go (concat cmd (agda2-string-quote expr))))) + +(defun agda2-compute-normalised-maybe-toplevel () + "Computes the normal form of the given expression, +using the scope of the current goal or, if point is not in a goal, the +top-level scope. +With a prefix argument \"abstract\" is ignored during the computation." + (interactive) + (if (agda2-goal-at (point)) + (call-interactively 'agda2-compute-normalised) + (call-interactively 'agda2-compute-normalised-toplevel))) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;;; + +(defun agda2-annotate (goals) + "Annotates the goals in the current buffer with text properties. +The goal numbers should be given by GOALS (in the order they +appear in the buffer)." + (agda2-forget-all-goals) + (agda2-let (stk top) + ((delims() (re-search-forward "[?]\\|[{][-!]\\|[-!][}]\\|--" nil t)) + (is-lone-questionmark () + (save-excursion + (save-match-data + (backward-char 3) + (looking-at + "\\(.[{(]\\|.\\s \\)[?]\\(\\s \\|[)};]\\|$\\)")))) + (make(p) (agda2-make-goal p (point) (pop goals))) + (err() (error "Unbalanced \{- , -\} , \{\! , \!\}"))) + (save-excursion + (goto-char (point-min)) + (while (and goals (delims)) + (labels ((c (s) (equal s (match-string 0)))) + (cond + ((and (c "--") (not stk)) (end-of-line)) + ((c "{-") (push nil stk)) + ((c "{!") (push (- (point) 2) stk)) + ((c "-}") (unless (and stk (not (pop stk))) (err))) + ((c "!}") (if (and stk (setq top (pop stk))) + (or stk (make top)) + (err))) + ((c "?") (progn + (when (and (not stk) (is-lone-questionmark)) + (delete-char -1) + (insert "{!!}") + (make (- (point) 4))))))))))) + +(defun agda2-make-goal (p q n) + "Make a goal with number N at

{!...!}. Assume the region is clean." + (annotation-preserve-mod-p-and-undo + (flet ((atp (x ps) (add-text-properties x (1+ x) ps))) + (atp p '(category agda2-delim1)) + (atp (1+ p) '(category agda2-delim2)) + (atp (- q 2) '(category agda2-delim3)) + (atp (1- q) '(category agda2-delim4))) + (let ((o (make-overlay p q nil t nil))) + (overlay-put o 'modification-hooks '(agda2-protect-goal-markers)) + (overlay-put o 'agda2-gn n) + (overlay-put o 'face 'highlight) + (overlay-put o 'after-string (propertize (format "%s" n) 'face 'highlight))))) + +(defun agda2-protect-goal-markers (ol action beg end &optional length) + "Ensures that the goal markers cannot be tampered with. +Except if `inhibit-read-only' is non-nil or /all/ of the goal is +modified." + (unless inhibit-read-only + (if action + ;; This is the after-change hook. + nil + ;; This is the before-change hook. + (cond + ((and (<= beg (overlay-start ol)) (>= end (overlay-end ol))) + ;; The user is trying to remove the whole goal: + ;; manually evaporate the overlay and add an undo-log entry so + ;; it gets re-added if needed. + (when (listp buffer-undo-list) + (push (list 'apply 0 (overlay-start ol) (overlay-end ol) + 'move-overlay ol (overlay-start ol) (overlay-end ol)) + buffer-undo-list)) + (delete-overlay ol)) + ((or (< beg (+ (overlay-start ol) 2)) + (> end (- (overlay-end ol) 2))) + (signal 'text-read-only nil)))))) + +(defun agda2-update (old-g new-txt) + "Update the goal OLD-G. +If NEW-TXT is a string, then the goal is replaced by the string, +and otherwise the text inside the goal is retained (parenthesised +if NEW-TXT is `'paren'). + +Removes the goal braces, but does not remove the goal overlay or +text properties." + (multiple-value-bind (p q) (agda2-range-of-goal old-g) + (save-excursion + (cond ((stringp new-txt) + (agda2-replace-goal old-g new-txt)) + ((equal new-txt 'paren) + (goto-char (- q 2)) (insert ")") + (goto-char (+ p 2)) (insert "("))) + (multiple-value-bind (p q) (agda2-range-of-goal old-g) + (delete-region (- q 2) q) + (delete-region p (+ p 2)))))) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;;; Misc + +(defun agda2-process-status () + "Status of `agda2-buffer', or \"no process\"." + (agda2-protect (process-status agda2-process) "no process")) + +(defun agda2-intersperse (sep xs) (interactive) + (let(ys)(while xs (push (pop xs) ys)(push sep ys))(pop ys)(nreverse ys))) + +(defun agda2-goal-Range (o) + "Range of goal overlay O." (interactive) + (format "(Range [Interval %s %s])" + (agda2-mkPos (+ (overlay-start o) 2)) + (agda2-mkPos (- (overlay-end o) 2)))) + +(defun agda2-mkPos (&optional p) + "Position value of P or point." (interactive) + (save-excursion + (if p (goto-char p)) + (format "(Pn \"%s\" %d %d %d)" (buffer-file-name) + (point) (count-lines (point-min) (point)) (1+ (current-column))))) + +(defun agda2-char-quote (c) + "Convert character C to the notation used in Haskell strings. +The non-ASCII characters are actually rendered as +\"\\xNNNN\\&\", i.e. followed by a \"null character\", to avoid +problems if they are followed by digits. ASCII characters (code +points < 128) are converted to singleton strings." + (if (< c 128) + (list c) + ;; FIXME: Why return a list rather than a string? --Stef + (append (format "\\x%x\\&" (encode-char c 'ucs)) nil))) + +(defun agda2-string-quote (s) + "Convert string S into a string representing it in Haskell syntax. +Escape newlines, double quotes, etc.. in the string S, add +surrounding double quotes, and convert non-ASCII characters to the \\xNNNN +notation used in Haskell strings." + (let ((pp-escape-newlines t)) + (mapconcat 'agda2-char-quote (pp-to-string s) ""))) + +(defun agda2-list-quote (strings) + "Convert a list of STRINGS into a string representing it in Haskell syntax." + (concat "[" (mapconcat 'agda2-string-quote strings ", ") "]")) + +(defun agda2-goal-at(pos) + "Return (goal overlay, goal number) at POS, or nil." + (let ((os (and pos (overlays-at pos))) o g) + (while (and os (not(setq g (overlay-get (setq o (pop os)) 'agda2-gn))))) + (if g (list o g)))) + +(defun agda2-goal-overlay (g) + "Returns the overlay of goal number G, if any." + (car + (remove nil + (mapcar (lambda (o) (if (equal (overlay-get o 'agda2-gn) g) o)) + (overlays-in (point-min) (point-max)))))) + +(defun agda2-range-of-goal (g) + "The range of goal G." + (let ((o (agda2-goal-overlay g))) + (if o (list (overlay-start o) (overlay-end o))))) + +(defun agda2-goto-goal (g) + (let ((p (+ 2 (car (agda2-range-of-goal g))))) + (if p (goto-char p)))) + +(defun agda2-replace-goal (g newtxt) + "Replace the content of goal G with NEWTXT." (interactive) + (save-excursion + (multiple-value-bind (p q) (agda2-range-of-goal g) + (setq p (+ p 2) q (- q 2)) + (let ((indent (and (goto-char p) (current-column)))) + (delete-region p q) (insert newtxt) + (while (re-search-backward "^" p t) + (insert-char ? indent) (backward-char (1+ indent))))))) + +(defun agda2-forget-all-goals () + "Remove all goal annotations. +\(Including some text properties which might be used by other +\(minor) modes.)" + (annotation-preserve-mod-p-and-undo + (remove-text-properties (point-min) (point-max) + '(category nil agda2-delim2 nil agda2-delim3 nil + display nil rear-nonsticky nil))) + (let ((p (point-min))) + (while (< (setq p (next-single-char-property-change p 'agda2-gn)) + (point-max)) + (delete-overlay (car (agda2-goal-at p)))))) + +(defun agda2-decl-beginning () + "Find the beginning point of the declaration containing the point. +To do: dealing with semicolon separated decls." + (interactive) + (save-excursion + (let* ((pEnd (point)) + (pDef (progn (goto-char (point-min)) + (re-search-forward "\\s *" pEnd t))) + (cDef (current-column))) + (while (re-search-forward + "where\\(\\s +\\)\\S \\|^\\(\\s *\\)\\S " pEnd t) + (if (match-end 1) + (setq pDef (goto-char (match-end 1)) + cDef (current-column)) + (goto-char (match-end 2)) + (if (>= cDef (current-column)) + (setq pDef (point) + cDef (current-column)))) + (forward-char)) + (goto-char pDef) + (if (equal (current-word) "mutual") + (or (match-end 2) (match-end 1)) + pDef)))) + +(defun agda2-beginning-of-decl () + (interactive) + (goto-char (agda2-decl-beginning))) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;;; Indentation + +(defun agda2-indent () + "This is what happens when TAB is pressed. +Depends on the setting of `agda2-indentation'." + (interactive) + (cond ((eq agda2-indentation 'haskell) (haskell-indent-cycle)) + ((eq agda2-indentation 'eri) (eri-indent)))) + +(defun agda2-indent-reverse () + "This is what happens when S-TAB is pressed. +Depends on the setting of `agda2-indentation'." + (interactive) + (cond ((eq agda2-indentation 'eri) (eri-indent-reverse)))) + +(defun agda2-indent-setup () + "Set up and start the indentation subsystem. +Depends on the setting of `agda2-indentation'." + (interactive) + (cond ((eq agda2-indentation 'haskell) + (labels ((setl (var val) (set (make-local-variable var) val))) + (setl 'indent-line-function 'haskell-indent-cycle) + (setl 'haskell-indent-off-side-keywords-re + "\\<\\(do\\|let\\|of\\|where\\|sig\\|struct\\)\\>[ \t]*")) + (local-set-key "\177" 'backward-delete-char-untabify) + (set (make-local-variable 'haskell-literate) + (if (string-match "\\.lagda$" (buffer-file-name)) + 'latex)) + (setq haskell-indent-mode t) + (run-hooks 'haskell-indent-hook)))) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Comments and paragraphs + +(defun agda2-comments-and-paragraphs-setup nil + "Set up comment and paragraph handling for Agda mode." + + ;; Syntax table setup for comments is done elsewhere. + + ;; Enable highlighting of comments via Font Lock mode (which uses + ;; the syntax table). + (set (make-local-variable 'font-lock-defaults) + '(nil nil nil nil nil)) + + ;; Empty lines (all white space according to Emacs) delimit + ;; paragraphs. + (set (make-local-variable 'paragraph-start) "\\s-*$") + (set (make-local-variable 'paragraph-separate) paragraph-start) + + ;; Support for adding/removing comments. + (set (make-local-variable 'comment-padding) " ") + (set (make-local-variable 'comment-start) "--") + + ;; Support for proper filling of text in comments (requires that + ;; Filladapt is activated). + (when (featurep 'filladapt) + (add-to-list (make-local-variable + 'filladapt-token-table) + '("--" agda2-comment)) + (add-to-list (make-local-variable 'filladapt-token-match-table) + '(agda2-comment agda2-comment) t) + (add-to-list (make-local-variable 'filladapt-token-conversion-table) + '(agda2-comment . exact)))) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Go to definition site + +(defun agda2-goto-definition-keyboard (&optional other-window) + "Go to the definition site of the name under point (if any). +If this function is invoked with a prefix argument then another window is used +to display the given position." + (interactive "P") + (annotation-goto-indirect (point) other-window)) + +(defun agda2-goto-definition-mouse (ev prefix) + "Go to the definition site of the name clicked on, if any. +Otherwise, yank (see `mouse-yank-at-click')." + (interactive "e\nP") + (let ((pos (posn-point (event-end ev)))) + (if (annotation-goto-possible pos) + (annotation-goto-indirect pos) + ;; FIXME: Shouldn't we use something like + ;; (call-interactively (key-binding ev))? --Stef + (mouse-yank-at-click ev prefix)))) + +(defun agda2-go-back nil + "Go back to the previous position in which +`agda2-goto-definition-keyboard' or `agda2-goto-definition-mouse' was +invoked." + (interactive) + (annotation-go-back)) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Implicit arguments + +(defun agda2-display-implicit-arguments (&optional arg) + "Toggle display of implicit arguments. +With prefix argument, turn on display of implicit arguments if +the argument is a positive number, otherwise turn it off." + (interactive "P") + (cond ((eq arg nil) (agda2-go "toggleImplicitArgs")) + ((and (numberp arg) + (> arg 0)) (agda2-go "showImplicitArgs" "True")) + (t (agda2-go "showImplicitArgs" "False")))) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;;; + +(defun agda2-popup-menu-3 (ev) + "If in a goal, popup the goal menu and call chosen command." + (interactive "e") + (let (choice) + (save-excursion + (and (agda2-goal-at (goto-char (posn-point (event-end ev)))) + (setq choice (x-popup-menu ev agda2-goal-map)) + (call-interactively + (lookup-key agda2-goal-map (apply 'vector choice))))))) + +(provide 'agda2-mode) +;;; agda2-mode.el ends here diff --git a/src/data/emacs-mode/agda2.el b/src/data/emacs-mode/agda2.el new file mode 100644 --- /dev/null +++ b/src/data/emacs-mode/agda2.el @@ -0,0 +1,13 @@ +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Agda mode code which should run before the first Agda file is +;; loaded + +(add-to-list 'load-path + (or (file-name-directory load-file-name) (car load-path))) + +(autoload 'agda2-mode "agda2-mode" + "Major mode for editing Agda files (version ≥ 2)." t) +(add-to-list 'auto-mode-alist '("\\.l?agda\\'" . agda2-mode)) +(modify-coding-system-alist 'file "\\.l?agda\\'" 'utf-8) + +(provide 'agda2) diff --git a/src/data/emacs-mode/annotation.el b/src/data/emacs-mode/annotation.el new file mode 100644 --- /dev/null +++ b/src/data/emacs-mode/annotation.el @@ -0,0 +1,182 @@ +;;; annotation.el --- Functions for annotating text with faces and help bubbles + +;;; Commentary: +;; + +;;; Code: +(require 'cl) + +(defconst annotations-offset (- (save-restriction (widen) (point-min)) 1) + "Offset between buffer positions and annotations's positions. +Annotations's positions are based on 1, so this adjusts it to the base +position used by your Emacs.") + +(defvar annotation-bindings nil + "An association list mapping symbols to faces.") +(make-variable-buffer-local 'annotation-bindings) + +(defvar annotation-goto-stack nil + "Positions from which `annotation-goto' was invoked.") + +(defun annotation-goto-possible (pos) + "Return t if there's a hyperlink at the buffer position POS, and nil otherwise." + (if (get-text-property pos 'annotation-goto) t)) + +(defun annotation-goto-indirect (pos &optional other-window) + "Follow the `annotation-goto' hyperlink at position POS, if any. +If OTHER-WINDOW is t, use another window to display the given position." + (let ((previous-file-name buffer-file-name)) + (if (and (annotation-goto (get-text-property pos 'annotation-goto) + other-window) + (not (eq (point) pos))) + (push `(,previous-file-name . ,pos) annotation-goto-stack)))) + +(defun annotation-go-back nil + "Go back to the previous position in which `annotation-goto' was +successfully invoked." + (when annotation-goto-stack + (let ((pos (pop annotation-goto-stack))) + (annotation-goto pos)))) + +(defun annotation-goto (filepos &optional other-window) + "Go to file position FILEPOS if the file is readable. +FILEPOS should have the form (FILE . POS). Return t if successful. + +If OTHER-WINDOW is t, use another window to display the given +position." + (when (consp filepos) + (let ((file (car filepos))) + (if (file-readable-p file) + (progn + (if other-window + (find-file-other-window file) + (find-file file)) + (goto-char (+ (cdr filepos) annotations-offset)) + t) + (error "File does not exist or is unreadable: %s." file))))) + +(defun annotation-annotate (start end anns &optional info goto) + "Annotate text between START and END in the current buffer. +ANNS are the annotations to apply. All the symbols in ANNS are +looked up in `annotation-bindings', and the font-lock-face text +property for the given character range is set to the resulting +list of faces. If the string INFO is non-nil, the mouse-face +property is set to highlight, and INFO is used as the help-echo +string. If GOTO has the form (FILENAME . POSITION), then the +mouse-face property is set to highlight and, when the user clicks +on the annotated text, then point is warped to the given position +in the given file. + +Note that if two faces have the same attribute set, then the first one +takes precedence. + +All characters whose text properties get set also have the +annotation-annotated property set to t, and +annotation-annotations is set to a list with all the properties +that have been set; this ensures that the text properties can +later be removed (if the annotation-* properties are not tampered +with). + +Note finally that nothing happens if either START or END are out of +bounds for the current (possibly narrowed) buffer, or END < START." + (incf start annotations-offset) + (incf end annotations-offset) + (when (and (<= (point-min) start) + (<= start end) + (<= end (point-max))) + (let ((faces (delq nil + (mapcar (lambda (ann) + (cdr (assoc ann annotation-bindings))) + anns))) + (props nil)) + (when faces + (put-text-property start end 'font-lock-face faces) + (add-to-list 'props 'font-lock-face)) + ;; Do this before so `info' can override our default help-echo. + (when (consp goto) + (add-text-properties start end + `(annotation-goto ,goto + mouse-face highlight + help-echo "Click mouse-2 to jump to definition")) + (add-to-list 'props 'annotation-goto) + (add-to-list 'props 'mouse-face) + (add-to-list 'props 'help-echo)) + (when info + (add-text-properties start end + `(mouse-face highlight help-echo ,info)) + (add-to-list 'props 'mouse-face) + (add-to-list 'props 'help-echo)) + (when props + (add-text-properties start end + `(annotation-annotated t + annotation-annotations ,props)))))) + +(defmacro annotation-preserve-mod-p-and-undo (&rest code) + "Run CODE preserving both the undo data and the modification bit." + (let ((modp (make-symbol "modp"))) + `(let ((,modp (buffer-modified-p)) + (buffer-undo-list t)) + (unwind-protect + (progn ,@code) + ;; FIXME: `restore-buffer-modified-p' would be more efficient. + (set-buffer-modified-p ,modp))))) + +(defun annotation-remove-annotations () + "Remove all text properties set by `annotation-annotate' in the current buffer. +This function preserves the file modification stamp of the current buffer +and does not modify the undo list. + +Note: This function may fail if there is read-only text in the buffer." + + ;; remove-text-properties fails for read-only text. + + (annotation-preserve-mod-p-and-undo + (let ((pos (point-min)) + pos2) + (while pos + (setq pos2 (next-single-property-change pos 'annotation-annotated)) + (let ((props (get-text-property pos 'annotation-annotations))) + (when props + (remove-text-properties pos (or pos2 (point-max)) + (mapcan (lambda (prop) (list prop nil)) + (append '(annotation-annotated annotation-annotations) + props))))) + (setq pos pos2))))) + +(defun annotation-load-file (file removep) + "Apply the annotations in FILE. +If (`funcall' REMOVEP anns) is non-nil, then all existing text +properties set by `annotation-annotate' in the current buffer are +first removed. Here anns is a list containing all the +annotations (third argument to `annotation-annotate') to be +applied (in some order, with duplicates removed). + +FILE should contain calls to `annotation-annotate'. The arguments +to `annotation-annotate' should be in normal form, they are not +evaluated. + +This function preserves the file modification stamp of the +current buffer and does not modify the undo list. + +Note: This function may fail if there is read-only text in the buffer." + (annotation-preserve-mod-p-and-undo + (when (file-readable-p file) + (let* ((cmds (with-temp-buffer + (insert "(\n)") (forward-char -2) + (insert-file-contents file) + (goto-char (point-min)) + (read (current-buffer)))) + (anns (delete-dups + (apply 'append (mapcar (lambda (x) (nth 1 (nth 3 x))) + cmds))))) + (if (funcall removep anns) + (annotation-remove-annotations)) + (dolist (cmd cmds) + (destructuring-bind (f start end anns &optional info goto) cmd + (assert (eq f 'annotation-annotate)) + (setq anns (cadr anns)) ;Strip the `quote'. + (setq goto (cadr goto)) ;Strip the `quote'. + (annotation-annotate start end anns info goto))))))) + +(provide 'annotation) +;;; annotation.el ends here diff --git a/src/data/emacs-mode/eri.el b/src/data/emacs-mode/eri.el new file mode 100644 --- /dev/null +++ b/src/data/emacs-mode/eri.el @@ -0,0 +1,186 @@ +;;; eri.el --- Enhanced relative indentation (eri) + +;;; Commentary: + +;;; Code: + +(require 'cl) + +(defun eri-current-line-length nil + "Calculates length of current line." + (- (line-end-position) (line-beginning-position))) + +(defun eri-current-line-empty nil + "Return non-nil if the current line is empty (not counting white space)." + (equal (current-indentation) + (eri-current-line-length))) + +(defun eri-maximum (xs) + "Calculate maximum element in XS. Return nil if the list is empty." + (if xs (apply 'max xs))) + +(defun eri-take (n xs) + "Return the first N elements of XS." + (butlast xs (- (length xs) n))) + +(defun eri-split (x xs) + "Return a pair of lists (XS1 . XS2). +If XS is sorted, then XS = (append XS1 XS2), and all elements in XS1 are <= X, +whereas all elements in XS2 are > X." + (let* ((pos (or (position-if (lambda (y) (> y x)) xs) (length xs))) + (xs1 (eri-take pos xs)) + (xs2 (nthcdr pos xs))) + `(,xs1 . ,xs2))) + +(defun eri-calculate-indentation-points-on-line (max) + "Calculate indentation points on current line. +Only points left of column number MAX are included. +If MAX is nil, then all points are included. Return points in ascending order. + +Example (positions marked with ^ are returned): + + f x y = g 3 (Just y) 5 4 + ^ ^ ^ ^ ^ ^ ^ ^ | + | + MAX" + (let ((result)) + (save-restriction + (beginning-of-line) + ; To make \\` work in the regexp below: + (narrow-to-region (line-beginning-position) (line-end-position)) + (while + (progn + (let ((pos (and (search-forward-regexp + "\\(?:\\s-\\|\\`\\)\\(\\S-\\)" nil t) + (match-beginning 1)))) + (when (not (null pos)) + (let ((pos1 (- pos (line-beginning-position)))) + (when (or (null max) (< pos1 max)) + (add-to-list 'result pos1)))) + (and pos + (< (point) (line-end-position)) + (or (null max) (< (current-column) max)))))) + (nreverse result) ; Destructive operation. + ))) + +(defun eri-new-indentation-point () + "Calculate a new indentation point, two steps in from the +indentation of the first non-empty line above the current line. +If there is no such line 2 is returned." + (save-excursion + (while + (progn + (forward-line -1) + (not (or (bobp) + (not (eri-current-line-empty)))))) + (+ 2 (current-indentation)))) + +(defun eri-calculate-indentation-points (reverse) + "Calculate some indentation points. Gives them in reverse order if +REVERSE is non-nil. See `eri-indent' for a description of how +the indentation points are calculated." + ;; First find a bunch of indentations used above the current line. + (let ((points) + (max)) + (save-excursion + (while + (progn + (forward-line -1) + ; Skip lines with only white space. + (unless (eri-current-line-empty) + (setq points + (append + (eri-calculate-indentation-points-on-line max) + points)) + (setq max (car points))) + ;; Stop after hitting the beginning of the buffer or a + ;; non-empty, non-indented line. + (not (or (bobp) + (and (equal (current-indentation) 0) + (> (eri-current-line-length) 0))))))) + ;; Add a new indentation point. Sort the indentations. + ;; Rearrange the points so that the next point is the one after the + ;; current one. + (let* ((ps (add-to-list 'points (eri-new-indentation-point))) + (ps1 (sort ps '<)) ; Note: sort is destructive. + (ps2 (eri-split (current-indentation) + (remove (current-indentation) ps1)))) + (if reverse + (append (nreverse (car ps2)) (nreverse (cdr ps2))) + (append (cdr ps2) (car ps2)))))) + +(defun eri-indent (&optional reverse) + "Cycle between some possible indentation points. +With prefix argument REVERSE, cycle in reverse order. + +Assume that a file contains the following lines of code, with point on +the line with three dots: + +frob = loooooooooooooooooooooooooong identifier +foo = f a b + where + f (Foo x) y = let bar = x + baz = 3 + 5 + +... + +^ ^ ^ ^ ^ ^ ^ ^ ^ * ^ ^ ^ ^ + +Then the ^'s and the * mark the indentation points that this function +cycles through. The indentation points are selected as follows: + + * All lines before the current one, up to and including the first + non-indented line (or the beginning of the buffer) are considered. + + foo = f a b + where + f (Foo x) y = let bar = x + baz = 3 + 5 + + * On these lines, erase all characters that stand to the right of + some non-white space character on a lower line. + + foo + whe + f (Foo x) y = let b + baz = 3 + 5 + + * Also erase all characters not immediately preceded by white + space. + + f + w + f ( x y = l b + b = 3 + 5 + + * The columns of all remaining characters are indentation points. + + f w f ( x y = l b = 3 + 5 + ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ + + * A new indentation point is also added, two steps in from the + indentation of the first non-empty line above the current line + (or in the second column, if there is no such line). + + f w f ( x y = l b = 3 + 5 + ^ ^ ^ ^ ^ ^ ^ ^ ^ * ^ ^ ^ ^" + (interactive "P") + (let* ((points (eri-calculate-indentation-points reverse)) + (remaining-points (cdr (member (current-indentation) points))) + (indentation (if remaining-points + (car remaining-points) + (car points)))) + (when indentation + (save-excursion (indent-line-to indentation)) + (if (< (current-column) indentation) + (indent-line-to indentation))))) + +(defun eri-indent-reverse nil + "Cycle between some possible indentation points (in reverse order). +See `eri-indent' for a description of how the indentation points are +calculated." + (interactive) + (eri-indent t)) + +(provide 'eri) +;;; eri.el ends here diff --git a/src/full/Agda/Compiler/Agate/Classify.hs b/src/full/Agda/Compiler/Agate/Classify.hs --- a/src/full/Agda/Compiler/Agate/Classify.hs +++ b/src/full/Agda/Compiler/Agate/Classify.hs @@ -72,10 +72,10 @@ Record{} -> return True where -- TODO: implement correctly -- isCompilableType (El s tm) = isCompilableTypeFamily tm - + isCompilableType :: Type -> TCM Bool isCompilableType (El s tm) = isCompilableTypeFamily tm - + isCompilableTypeFamily :: Term -> TCM Bool isCompilableTypeFamily tm = do tm <- reduce tm @@ -126,7 +126,7 @@ go2 [] namesNext grantedNames changed = go namesNext grantedNames changed go2 (name:names) namesNext grantedNames changed = do - b <- f grantedNames name + b <- f grantedNames name case b of True -> go2 names namesNext (name : grantedNames) True -- name is granted to be okay @@ -134,4 +134,4 @@ -- name is unsettled -- - + diff --git a/src/full/Agda/Compiler/Agate/OptimizedPrinter.hs b/src/full/Agda/Compiler/Agate/OptimizedPrinter.hs --- a/src/full/Agda/Compiler/Agate/OptimizedPrinter.hs +++ b/src/full/Agda/Compiler/Agate/OptimizedPrinter.hs @@ -169,7 +169,7 @@ let dvars = map (\i -> text ("v" ++ show i)) [1 .. np + ni] let dvaluedef = sep [ sep (dname : dvars), equals ] <+> text "()" return $ dtypedecl $+$ dvaluedef - Record{} -> + Record{} -> return empty -- no o_xxx since we always use D_xxx Constructor{} -> return empty -- no o_xxx since we always use D_xxx @@ -183,7 +183,7 @@ fTerm = showAsOptimizedTerm fCon name dargs = do dname <- showAsOptimizedConstructor name - return $ parens $ sep (dname : dargs) + return $ parens $ sep (dname : dargs) fBody dpats term = do dterm <- showAsOptimizedTerm term return $ (sep (dfuncname : dpats) <+> equals) <+> nest 2 dterm @@ -192,7 +192,7 @@ -- implementation of the "K" function class ShowAsOptimizedKind a where - showAsOptimizedKind :: a -> TCM Doc + showAsOptimizedKind :: a -> TCM Doc instance ShowAsOptimizedKind Type where showAsOptimizedKind (El s t) = showAsOptimizedKind t @@ -221,7 +221,7 @@ -- implementation of the "T" function class ShowAsOptimizedType a where - showAsOptimizedType :: a -> TCM Doc + showAsOptimizedType :: a -> TCM Doc instance ShowAsOptimizedType QName where showAsOptimizedType s = return $ text $ translateNameAsOptimizedType $ show s @@ -269,7 +269,7 @@ -- implementation of the "O" function class ShowAsOptimizedTerm a where - showAsOptimizedTerm :: a -> TCM Doc + showAsOptimizedTerm :: a -> TCM Doc instance ShowAsOptimizedTerm Name where showAsOptimizedTerm s = return $ text $ translateNameAsOptimizedTerm $ show s diff --git a/src/full/Agda/Compiler/Agate/TranslateName.hs b/src/full/Agda/Compiler/Agate/TranslateName.hs --- a/src/full/Agda/Compiler/Agate/TranslateName.hs +++ b/src/full/Agda/Compiler/Agate/TranslateName.hs @@ -50,4 +50,4 @@ :intToDigit (ord c `mod` 16):escape s ---------------------------------------------------------------- - + diff --git a/src/full/Agda/Compiler/Agate/UntypedPrinter.hs b/src/full/Agda/Compiler/Agate/UntypedPrinter.hs --- a/src/full/Agda/Compiler/Agate/UntypedPrinter.hs +++ b/src/full/Agda/Compiler/Agate/UntypedPrinter.hs @@ -31,7 +31,7 @@ -- implementation of the "X" function class ShowAsUntypedTerm a where - showAsUntypedTerm :: a -> TCM Doc + showAsUntypedTerm :: a -> TCM Doc instance ShowAsUntypedTerm Name where showAsUntypedTerm t = return $ text $ translateNameAsUntypedTerm $ show t diff --git a/src/full/Agda/Compiler/Alonzo/Haskell.hs b/src/full/Agda/Compiler/Alonzo/Haskell.hs --- a/src/full/Agda/Compiler/Alonzo/Haskell.hs +++ b/src/full/Agda/Compiler/Alonzo/Haskell.hs @@ -10,7 +10,7 @@ hsModule name decls = HsModule dummyLoc (Module name) Nothing [] decls hsModuleImporting :: String -> [String] -> [String] -> [HsDecl] -> HsModule -hsModuleImporting name imps qimps decls = +hsModuleImporting name imps qimps decls = HsModule dummyLoc (Module name) Nothing (map hsImport imps ++ impRTS : impRTP : map hsQImport qimps) decls @@ -39,13 +39,13 @@ hsVar :: String -> HsExp hsVar s = HsVar $ UnQual $ HsIdent s -hsCon :: String -> HsExp +hsCon :: String -> HsExp hsCon s = HsCon $ UnQual $ HsIdent s hsLam :: String -> HsExp -> HsExp hsLam n e = HsLambda dummyLoc [HsPVar (HsIdent n)] e -hsAp :: HsExp -> HsExp -> HsExp +hsAp :: HsExp -> HsExp -> HsExp hsAp e1 e2 = HsApp (hsCast e1) $ HsParen (hsCast e2) outputHsModule s hsmod numOfMainS = do diff --git a/src/full/Agda/Compiler/Alonzo/Main.hs b/src/full/Agda/Compiler/Alonzo/Main.hs --- a/src/full/Agda/Compiler/Alonzo/Main.hs +++ b/src/full/Agda/Compiler/Alonzo/Main.hs @@ -64,7 +64,7 @@ withCurrentModule moduleName $ do -- TODO: Hack! builtinMap <- getBuiltinThings -- let sigs = toList sig - -- let definitions = mdefDefs (snd (head sigs)) -- :: Map Name Definition + -- let definitions = mdefDefs (snd (head sigs)) -- :: Map Name Definition let definitions = sigDefinitions sig -- :: Map QName Definition let defs = Map.toList definitions let names = List.map fst defs @@ -121,8 +121,8 @@ -- isMain (Name _ (C.Name _ [C.Id _ "mainS"]) _ _ ) = True isMain n = (show n == "main") - + processDefWithDebug :: (QName,Definition) -> TCM [HsDecl] processDefWithDebug (qname,def) = do def <- instantiateFull def @@ -131,10 +131,10 @@ nameInfo = infoDecl infoName (show name) infoName = "name" ++ (show $ numOfName name) name = qnameName qname - + infoDecl :: String -> String -> HsDecl infoDecl name val = HsFunBind [ HsMatch dummyLoc hsname [] rhs []] where - rhs = HsUnGuardedRhs $ HsLit $ HsString val + rhs = HsUnGuardedRhs $ HsLit $ HsString val hsname = HsIdent name @@ -144,7 +144,7 @@ return [HsFunBind [HsMatch dummyLoc (dfName name) [] rhs hsDecls]] where rhs = HsUnGuardedRhs $ HsVar $ UnQual $ dfNameSub name 1 name = qnameName qname - + processDef (qname,Defn { theDef = Datatype{ dataPars = n, dataClause = Nothing, dataCons = [] } }) = do return [ddecl,vdecl] where name = qnameName qname @@ -189,7 +189,7 @@ hsname = dfName name nDummyArgs 0 = [] nDummyArgs k = (HsPVar $ HsIdent ("v" ++ (show k))) : nDummyArgs (k-1) - + processDef def@(qname,Defn { theDef = Constructor{} }) = return [] @@ -211,7 +211,7 @@ name = qnameName qname processDef (qname, (Defn { theDef = Datatype{dataClause = Just clause} })) = do - -- liftIO $ putStrLn $ gshow $ clauseBod clause + -- liftIO $ putStrLn $ gshow $ clauseBod clause mkSynonym (clauseBod clause) where name = qnameName qname mkSynonym (Lam _ (Abs _ t)) = mkSynonym t @@ -229,7 +229,7 @@ typ = HsTyCon $ Qual hsModuleName $ dataName $ qnameName rhsqname mkSynonym t = __IMPOSSIBLE__ {- do - liftIO $ putStrLn $ gshow t + liftIO $ putStrLn $ gshow t return [] -} @@ -240,12 +240,12 @@ mkSynonym (Lam _ (Abs _ t)) = mkSynonym t mkSynonym (Def newqn args) = return [ddecl, vdecl] where ddecl = HsTypeDecl loc dname [] typ - + loc = dummyLoc dname = dataName name typ = HsTyCon $ UnQual $ dataName $ qnameName newqn mkSynonym t = do - liftIO $ putStrLn $ gshow t + liftIO $ putStrLn $ gshow t return [] -} @@ -301,12 +301,12 @@ (exp, pst) <- runStateT bodyPM pst0 let rhs = HsUnGuardedRhs exp (pats, pst2) <- runStateT (processArgPats args) pst - return $ HsFunBind $ [HsMatch dummyLoc hsid pats rhs decls] + return $ HsFunBind $ [HsMatch dummyLoc hsid pats rhs decls] where decls = [] hsid = dfNameSub name $ fromIntegral number - -- pats = processArgPats args - + -- pats = processArgPats args + contClause :: Name -> Nat -> Clause -> TCM HsDecl contClause name number (Clause{ clausePats = args, clauseBody = body }) = do return $ HsFunBind $ [HsMatch dummyLoc hsid pats rhs decls] where @@ -340,7 +340,7 @@ processPat (VarP _) = do pats <- getPlst case pats of - [] -> do + [] -> do c <- getPclause error $ "Oops! empty pattern list in\n" ++ (gshow c) (p:ps) -> do @@ -363,16 +363,16 @@ return $ HsPParen $ HsPApp cname hspats processPat (LitP (LitInt _ i)) = return $ HsPLit (HsInt i) -processPat (LitP (LitChar _ c)) = +processPat (LitP (LitChar _ c)) = return $ HsPParen $ HsPApp (rtpCon "CharT") [HsPLit (HsChar c)] -processPat (LitP _) = error "Unimplemented literal patttern" +processPat (LitP _) = error "Unimplemented literal patttern" -- processPat (AbsurdP _) = return HsPWildCard - + processBody :: ClauseBody -> PM HsExp -processBody (NoBind cb) = do +processBody (NoBind cb) = do addWildcard - processBody cb + processBody cb processBody (Bind (Abs name cb)) = do -- cnt <- getPcnt addVar @@ -404,8 +404,8 @@ -- Can be a record constructor in which case the def will be for the record. _ -> do ldefs <- getPDefs - if (Map.member qn ldefs) - then do + if (Map.member qn ldefs) + then do definiens <- case theDef <$> Map.lookup qn ldefs of Just df -> return df Nothing -> fail $ "Alonzo: No such definition: " ++ show qn @@ -437,7 +437,7 @@ processLit (LitInt _ i) = HsApp toNat $ intLit i where intLit i = HsParen $ hsPreludeTypedExp "Integer" $ HsLit $ HsInt i toNat = HsVar $ Qual (Module "RTP") $ HsIdent "_primIntegerToNat" -processLit (LitFloat _ f) = hsPreludeTypedExp "Double" $ +processLit (LitFloat _ f) = hsPreludeTypedExp "Double" $ HsLit $ HsFrac $ toRational f -- processLit (LitFloat _ f) = HsApp (HsVar $ rtpCon "FloatT") -- (HsLit $ HsFrac $ toRational f) @@ -455,7 +455,7 @@ unfoldVap p e ((Arg NotHidden t):ts) = do e1 <- evalStateT (processTerm t) p unfoldVap p (hsAp e e1) ts --- unfoldVap p e ((Arg Hidden t):ts) = unfoldVap p e ts +-- unfoldVap p e ((Arg Hidden t):ts) = unfoldVap p e ts unfoldVap p e ((Arg Hidden t):ts) = do e1 <- evalStateT (processTerm t) p unfoldVap p (hsAp e e1) ts @@ -475,7 +475,7 @@ getConArity :: QName -> TCM Nat getConArity qn = do - Defn _ ty _ _ Constructor{conPars = np} <- getConstInfo qn + Defn _ ty _ _ Constructor{conPars = np} <- getConstInfo qn ty' <- normalise ty return $ typeArity ty' - np -- return $ arity ty' diff --git a/src/full/Agda/Compiler/Alonzo/Names.hs b/src/full/Agda/Compiler/Alonzo/Names.hs --- a/src/full/Agda/Compiler/Alonzo/Names.hs +++ b/src/full/Agda/Compiler/Alonzo/Names.hs @@ -41,7 +41,7 @@ id = (dfStr name) ++ "_" ++ (show i) dfQName :: QName -> HsQName -dfQName (QName m n) +dfQName (QName m n) | (moduleStr m) == "RTP" = Qual (Module $ moduleStr m)(HsIdent $ "_"++(show n)) | otherwise = Qual (Module $ moduleStr m) (dfName n) diff --git a/src/full/Agda/Compiler/Alonzo/PatternMonad.hs b/src/full/Agda/Compiler/Alonzo/PatternMonad.hs --- a/src/full/Agda/Compiler/Alonzo/PatternMonad.hs +++ b/src/full/Agda/Compiler/Alonzo/PatternMonad.hs @@ -14,7 +14,7 @@ import Agda.Utils.Size type Defs = Map QName Definition -data PState = PSt +data PState = PSt { cnt :: Int , vars :: [Int] , lst :: [HsPat] @@ -23,11 +23,11 @@ } initPState :: Clause -> Defs -> PState -initPState c@(Clause{ clausePerm = perm }) d = PSt +initPState c@(Clause{ clausePerm = perm }) d = PSt { cnt = 0 , vars = permute perm [0..] , lst = [] - , clause = c + , clause = c , defs = d } @@ -55,7 +55,7 @@ incPcnt = modify $ \s -> s { cnt = 1 + cnt s } addWildcard :: PM() -addWildcard = do +addWildcard = do lst <- getPlst putPlst $ lst++[HsPWildCard] diff --git a/src/full/Agda/Compiler/MAlonzo/Compiler.hs b/src/full/Agda/Compiler/MAlonzo/Compiler.hs --- a/src/full/Agda/Compiler/MAlonzo/Compiler.hs +++ b/src/full/Agda/Compiler/MAlonzo/Compiler.hs @@ -101,7 +101,7 @@ Constructor{} -> return [] Record{ recClause = cl, recFields = flds } -> do ar <- arity <$> normalise ty - return $ tvaldecl q (genericLength flds) ar [cdecl q (genericLength flds)] cl + return $ tvaldecl q (genericLength flds) ar [cdecl q (genericLength flds)] cl Primitive{ primName = s } -> fb <$> primBody s where tag _ [] = [] @@ -204,12 +204,12 @@ LitFloat _ _ -> return $ typed "Double" _ -> return $ l' where l' = HsLit $ hslit l - typed = HsExpTypeSig dummy l' . HsQualType [] . HsTyCon . rtmQual + typed = HsExpTypeSig dummy l' . HsQualType [] . HsTyCon . rtmQual hslit :: Literal -> HsLiteral hslit l = case l of LitInt _ x -> HsInt x LitFloat _ x -> HsFrac (toRational x) - LitString _ x -> HsString x + LitString _ x -> HsString x LitChar _ x -> HsChar x condecl :: QName -> TCM (Nat, HsConDecl) @@ -280,7 +280,7 @@ outFile :: TCM FilePath outFile = snd <$> outFile' - + callGHC :: (Interface, ClockTime) -> TCM () callGHC mainICT = do setInterface mainICT diff --git a/src/full/Agda/Compiler/MAlonzo/Misc.hs b/src/full/Agda/Compiler/MAlonzo/Misc.hs --- a/src/full/Agda/Compiler/MAlonzo/Misc.hs +++ b/src/full/Agda/Compiler/MAlonzo/Misc.hs @@ -124,7 +124,7 @@ -- qualify name s by the module of builtin b bltQual :: String -> String -> TCM HsQName -bltQual b s = do (Def q _) <- getBuiltin b; xqual q (HsIdent s) +bltQual b s = do (Def q _) <- getBuiltin b; xqual q (HsIdent s) -- sub-naming for cascaded definitions for concsecutive clauses dsubname q i | i == 0 = unqhname "d" q @@ -149,7 +149,7 @@ rtmMod = mazMod' "Runtime" rtmQual = UnQual . HsIdent rtmVar = HsVar . rtmQual -rtmError s = rtmVar "error" `HsApp` +rtmError s = rtmVar "error" `HsApp` (HsLit $ HsString $ "MAlonzo Runtime Error: " ++ s) unsafeCoerceMod = Module "Unsafe.Coerce" @@ -176,7 +176,7 @@ dummy :: a dummy = error "MAlonzo : this dummy value should not have been eval'ed." - + -------------------------------------------------- -- For Debugging diff --git a/src/full/Agda/Compiler/MAlonzo/Primitives.hs b/src/full/Agda/Compiler/MAlonzo/Primitives.hs --- a/src/full/Agda/Compiler/MAlonzo/Primitives.hs +++ b/src/full/Agda/Compiler/MAlonzo/Primitives.hs @@ -76,12 +76,12 @@ ," | True = <<1>> (unsafeCoerce (f (x - 1)))" ,"} in f"]) in decls ["ZERO", "SUC"] to totxt from fromtxt - decls cs n1 b1 n2 b2 = + decls cs n1 b1 n2 b2 = ifM (hasCompiledData cs) (return $ L.map (`fakeDS` "id") [n1, n2]) $ do cs' <- mapM pconName cs return $ zipWith (\ n -> fakeDS n . repl cs') [n1, n2] [b1, b2] - + mazNatToInteger = "mazNatToInteger" mazIntegerToNat = "mazIntegerToNat" mazNatToInt = "mazNatToInt" @@ -106,7 +106,7 @@ -- Definition bodies for primitive functions primBody :: String -> TCM HsExp -primBody s = (hsVarUQ . HsIdent <$>) $ maybe unimplemented id $ L.lookup s $ +primBody s = (hsVarUQ . HsIdent <$>) $ maybe unimplemented id $ L.lookup s $ [ -- Integer functions "primIntegerPlus" |-> binAsis "(+)" "Integer" @@ -187,7 +187,7 @@ return $ repl [op, ty, toHB, toTy] $ "(\\ x y -> <<2>> ((<<0>> :: <<1>> -> <<1>> -> Bool) (<<3>> x) (<<3>> y)))" relNat op = do toHI <- bltQual' "NATURAL" mazNatToInteger - rel' toHI op "Integer" + rel' toHI op "Integer" rel op ty = rel' "" op ty pred p = do toHB <- bltQual' "BOOL" mazHBoolToBool return $ repl [p, toHB] $ "(\\ x -> <<1>> (<<0>> x))" @@ -217,7 +217,7 @@ toB (Lam _ (Abs _ t)) = toB t toB _ = return False hasCompiledData _ = return False - + bltQual' b s = prettyPrint <$> bltQual b s diff --git a/src/full/Agda/Interaction/BasicOps.hs b/src/full/Agda/Interaction/BasicOps.hs --- a/src/full/Agda/Interaction/BasicOps.hs +++ b/src/full/Agda/Interaction/BasicOps.hs @@ -3,7 +3,7 @@ #-} module Agda.Interaction.BasicOps where -{- TODO: The operations in this module should return Expr and not String, +{- TODO: The operations in this module should return Expr and not String, for this we need to write a translator from Internal to Abstract syntax. -} @@ -15,11 +15,11 @@ import Data.List import Data.Maybe -import Agda.Interaction.Monad +import Agda.Interaction.Monad import qualified Agda.Syntax.Concrete as C -- ToDo: Remove with instance of ToConcrete import Agda.Syntax.Position -import Agda.Syntax.Abstract +import Agda.Syntax.Abstract import Agda.Syntax.Common import Agda.Syntax.Info(ExprInfo(..),MetaInfo(..)) import Agda.Syntax.Internal (MetaId(..),Type(..),Term(..),Sort(..)) @@ -47,7 +47,7 @@ parseExprIn :: InteractionId -> Range -> String -> TCM Expr parseExprIn ii rng s = do mId <- lookupInteractionId ii - updateMetaVarRange mId rng + updateMetaVarRange mId rng mi <- getMetaInfo <$> lookupMeta mId let pos = case rStart (getRange mi) of Just pos -> pos @@ -58,12 +58,12 @@ giveExpr :: MetaId -> Expr -> TCM Expr -- When translater from internal to abstract is given, this function might return -- the expression returned by the type checker. -giveExpr mi e = - do mv <- lookupMeta mi +giveExpr mi e = + do mv <- lookupMeta mi withMetaInfo (getMetaInfo mv) $ metaTypeCheck' mi e mv - - where metaTypeCheck' mi e mv = - case mvJudgement mv of + + where metaTypeCheck' mi e mv = + case mvJudgement mv of HasType _ t -> do ctx <- getContextArgs let t' = t `piApply` ctx @@ -76,42 +76,42 @@ IsSort _ -> __IMPOSSIBLE__ give :: InteractionId -> Maybe Range -> Expr -> TCM (Expr,[InteractionId]) -give ii mr e = liftTCM $ +give ii mr e = liftTCM $ do setUndo - mi <- lookupInteractionId ii + mi <- lookupInteractionId ii mis <- getInteractionPoints r <- getInteractionRange ii updateMetaVarRange mi $ maybe r id mr giveExpr mi e - removeInteractionPoint ii + removeInteractionPoint ii mis' <- getInteractionPoints - return (e, mis' \\ mis) + return (e, mis' \\ mis) addDecl :: Declaration -> TCM ([InteractionId]) -addDecl d = +addDecl d = do setUndo mis <- getInteractionPoints checkDecl d mis' <- getInteractionPoints - return (mis' \\ mis) + return (mis' \\ mis) refine :: InteractionId -> Maybe Range -> Expr -> TCM (Expr,[InteractionId]) --- If constants has a fixed arity, then it might be better to do +-- If constants has a fixed arity, then it might be better to do -- exact refinement. -refine ii mr e = +refine ii mr e = do mi <- lookupInteractionId ii - mv <- lookupMeta mi + mv <- lookupMeta mi let range = maybe (getRange mv) id mr - let scope = M.getMetaScope mv + let scope = M.getMetaScope mv tryRefine 10 range scope e where tryRefine :: Int -> Range -> ScopeInfo -> Expr -> TCM (Expr,[InteractionId]) tryRefine nrOfMetas r scope e = try nrOfMetas e where try 0 e = throwError (strMsg "Can not refine") try n e = give ii (Just r) e `catchError` (\_ -> try (n-1) (appMeta e)) appMeta :: Expr -> Expr - appMeta e = + appMeta e = let metaVar = QuestionMark $ Agda.Syntax.Info.MetaInfo { Agda.Syntax.Info.metaRange = r @@ -124,24 +124,24 @@ {- refineExact :: InteractionId -> Maybe Range -> Expr -> TCM (Expr,[InteractionId]) -refineExact ii mr e = +refineExact ii mr e = do mi <- lookupInteractionId ii - mv <- lookupMeta mi + mv <- lookupMeta mi let range = maybe (getRange mv) id mr let scope = M.getMetaScope mv - (_,t) <- withMetaInfo (getMetaInfo mv) $ inferExpr e + (_,t) <- withMetaInfo (getMetaInfo mv) $ inferExpr e let arityt = arity t - + tryRefine 10 range scope e where tryRefine :: Int -> Range -> ScopeInfo -> Expr -> TCM (Expr,[InteractionId]) tryRefine nrOfMetas r scope e = try nrOfMetas e where try 0 e = throwError (strMsg "Can not refine") try n e = give ii (Just r) e `catchError` (\_ -> try (n-1) (appMeta e)) appMeta :: Expr -> Expr - appMeta e = + appMeta e = let metaVar = QuestionMark $ Agda.Syntax.Info.MetaInfo {Agda.Syntax.Info.metaRange = r, Agda.Syntax.Info.metaScope = scope} - in App (ExprRange $ r) NotHidden e metaVar + in App (ExprRange $ r) NotHidden e metaVar --ToDo: The position of metaVar is not correct @@ -149,33 +149,33 @@ abstract :: InteractionId -> Maybe Range -> TCM (Expr,[InteractionId]) -abstract ii mr +abstract ii mr refineExact :: InteractionId -> Expr -> TCM (Expr,[InteractionId]) -refineExact ii e = - do +refineExact ii e = + do -} {-| Evaluate the given expression in the current environment -} evalInCurrent :: Expr -> TCM Expr -evalInCurrent e = - do t <- newTypeMeta_ +evalInCurrent e = + do t <- newTypeMeta_ v <- checkExpr e t v' <- normalise v reify v' evalInMeta :: InteractionId -> Expr -> TCM Expr -evalInMeta ii e = +evalInMeta ii e = do m <- lookupInteractionId ii mi <- getMetaInfo <$> lookupMeta m withMetaInfo mi $ evalInCurrent e -data Rewrite = AsIs | Instantiated | HeadNormal | Normalised +data Rewrite = AsIs | Instantiated | HeadNormal | Normalised --rewrite :: Rewrite -> Term -> TCM Term rewrite AsIs t = return t @@ -222,7 +222,7 @@ fmap f (IsEmptyType a) = IsEmptyType a instance Reify Constraint (OutputForm Expr Expr) where - reify (ValueCmp cmp t u v) = CmpInType cmp <$> reify t <*> reify u <*> reify v + reify (ValueCmp cmp t u v) = CmpInType cmp <$> reify t <*> reify u <*> reify v reify (TypeCmp cmp t t') = CmpTypes cmp <$> reify t <*> reify t' reify (SortCmp cmp s s') = CmpSorts cmp <$> reify s <*> reify s' reify (Guarded c cs) = do @@ -259,12 +259,12 @@ show (Assign m e) = show m ++ " := " ++ show e show (IsEmptyType a) = "Is empty: " ++ show a -instance (ToConcrete a c, ToConcrete b d) => +instance (ToConcrete a c, ToConcrete b d) => ToConcrete (OutputForm a b) (OutputForm c d) where toConcrete (OfType e t) = OfType <$> toConcrete e <*> toConcrete t toConcrete (JustType e) = JustType <$> toConcrete e toConcrete (JustSort e) = JustSort <$> toConcrete e - toConcrete (CmpInType cmp t e e') = + toConcrete (CmpInType cmp t e e') = CmpInType cmp <$> toConcrete t <*> toConcrete e <*> toConcrete e' toConcrete (CmpTypes cmp e e') = CmpTypes cmp <$> toConcrete e <*> toConcrete e' toConcrete (CmpSorts cmp e e') = CmpSorts cmp <$> toConcrete e <*> toConcrete e' @@ -295,8 +295,8 @@ --- Printing Operations getConstraint :: Int -> TCM (OutputForm Expr Expr) -getConstraint ci = - do cc <- lookupConstraint ci +getConstraint ci = + do cc <- lookupConstraint ci cc <- reduce cc withConstraint reify cc @@ -334,7 +334,7 @@ PostponedTypeCheckingProblem{} -> unsol typeOfMetaMI :: Rewrite -> MetaId -> TCM (OutputForm Expr MetaId) -typeOfMetaMI norm mi = +typeOfMetaMI norm mi = do mv <- lookupMeta mi withMetaInfo (getMetaInfo mv) $ rewriteJudg mv (mvJudgement mv) @@ -347,7 +347,7 @@ typeOfMeta :: Rewrite -> InteractionId -> TCM (OutputForm Expr InteractionId) -typeOfMeta norm ii = +typeOfMeta norm ii = do mi <- lookupInteractionId ii out <- typeOfMetaMI norm mi return $ fmap (\_ -> ii) out @@ -356,11 +356,11 @@ typeOfMetas :: Rewrite -> TCM ([OutputForm Expr InteractionId],[OutputForm Expr MetaId]) -- First visible metas, then hidden typeOfMetas norm = liftTCM $ - do ips <- getInteractionPoints + do ips <- getInteractionPoints js <- mapM (typeOfMeta norm) ips hidden <- hiddenMetas return $ (js,hidden) - where hiddenMetas = --TODO: Change so that it uses getMetaMI above + where hiddenMetas = --TODO: Change so that it uses getMetaMI above do is <- getInteractionMetas store <- Map.filterWithKey (openAndImplicit is) <$> getMetaStore let mvs = Map.keys store diff --git a/src/full/Agda/Interaction/CommandLine/CommandLine.hs b/src/full/Agda/Interaction/CommandLine/CommandLine.hs --- a/src/full/Agda/Interaction/CommandLine/CommandLine.hs +++ b/src/full/Agda/Interaction/CommandLine/CommandLine.hs @@ -139,7 +139,7 @@ liftIO $ UTF8.putStrLn $ unlines (List.map show cs) showConstraints _ = liftIO $ UTF8.putStrLn ":constraints [cid]" - + showMetas :: [String] -> TCM () showMetas [m] = do i <- InteractionId <$> readM m @@ -154,8 +154,8 @@ s <- showA =<< typeOfMeta Normalised i r <- getInteractionRange i liftIO $ UTF8.putStrLn $ s ++ " " ++ show r -showMetas [] = - do (interactionMetas,hiddenMetas) <- typeOfMetas AsIs +showMetas [] = + do (interactionMetas,hiddenMetas) <- typeOfMetas AsIs mapM_ (liftIO . UTF8.putStrLn) =<< mapM showII interactionMetas mapM_ print' hiddenMetas where @@ -180,7 +180,7 @@ liftIO $ UTF8.print scope metaParseExpr :: InteractionId -> String -> TCM A.Expr -metaParseExpr ii s = +metaParseExpr ii s = do m <- lookupInteractionId ii scope <- getMetaScope <$> lookupMeta m r <- getRange <$> lookupMeta m @@ -192,16 +192,16 @@ concreteToAbstract scope e actOnMeta :: [String] -> (InteractionId -> A.Expr -> TCM a) -> TCM a -actOnMeta (is:es) f = +actOnMeta (is:es) f = do i <- readM is - let ii = InteractionId i + let ii = InteractionId i e <- metaParseExpr ii (unwords es) withInteractionId ii $ f ii e actOnMeta _ _ = __IMPOSSIBLE__ giveMeta :: [String] -> TCM () -giveMeta s | length s >= 2 = +giveMeta s | length s >= 2 = do actOnMeta s (\ii -> \e -> give ii Nothing e) return () giveMeta _ = liftIO $ UTF8.putStrLn $ ": give" ++ " metaid expr" @@ -209,7 +209,7 @@ refineMeta :: [String] -> TCM () -refineMeta s | length s >= 2 = +refineMeta s | length s >= 2 = do actOnMeta s (\ii -> \e -> refine ii Nothing e) return () refineMeta _ = liftIO $ UTF8.putStrLn $ ": refine" ++ " metaid expr" @@ -240,21 +240,21 @@ return Continue where evalInCurrent e = do - t <- newTypeMeta_ + t <- newTypeMeta_ v <- checkExpr e t v' <- normalise v return v' typeOf :: [String] -> TCM () -typeOf s = +typeOf s = do e <- parseExpr (unwords s) e0 <- typeInCurrent Normalised e e1 <- typeInCurrent AsIs e liftIO . UTF8.putStrLn =<< showA e1 typeIn :: [String] -> TCM () -typeIn s@(_:_:_) = +typeIn s@(_:_:_) = actOnMeta s $ \i e -> do e1 <- typeInMeta i Normalised e e2 <- typeInMeta i AsIs e diff --git a/src/full/Agda/Interaction/Highlighting/HTML.hs b/src/full/Agda/Interaction/Highlighting/HTML.hs --- a/src/full/Agda/Interaction/Highlighting/HTML.hs +++ b/src/full/Agda/Interaction/Highlighting/HTML.hs @@ -46,10 +46,10 @@ generateHTML :: A.ModuleName -> TCM () generateHTML mod = do - options <- TCM.commandLineOptions - case optHTMLDir options of - Nothing -> TCM.typeError TCM.HTMLDirUndefined - Just dir -> do + options <- TCM.commandLineOptions + + -- There is a default directory given by 'defaultHTMLDir' + let dir = optHTMLDir options liftIO $ createDirectoryIfMissing True dir -- If the default CSS file should be used, then it is copied to diff --git a/src/full/Agda/Interaction/Highlighting/Precise.hs b/src/full/Agda/Interaction/Highlighting/Precise.hs --- a/src/full/Agda/Interaction/Highlighting/Precise.hs +++ b/src/full/Agda/Interaction/Highlighting/Precise.hs @@ -82,7 +82,7 @@ data MetaInfo = MetaInfo { aspect :: Maybe Aspect - , otherAspects :: [OtherAspect] + , otherAspects :: [OtherAspect] , note :: Maybe String -- ^ This note, if present, can be displayed as a tool-tip or -- something like that. It should contain useful information about @@ -201,7 +201,7 @@ join pms = ( Range { from = head ps, to = last ps + 1 } , head ms ) - where (ps, ms) = unzip pms + where (ps, ms) = unzip pms -- | Decompresses a compressed file. diff --git a/src/full/Agda/Interaction/Imports.hs b/src/full/Agda/Interaction/Imports.hs --- a/src/full/Agda/Interaction/Imports.hs +++ b/src/full/Agda/Interaction/Imports.hs @@ -23,7 +23,7 @@ import Agda.Syntax.Position import qualified Agda.Syntax.Concrete as C import Agda.Syntax.Abstract.Name -import Agda.Syntax.Parser +import Agda.Syntax.Parser import Agda.Syntax.Scope.Base import Agda.Syntax.Scope.Monad import Agda.Syntax.Translation.ConcreteToAbstract diff --git a/src/full/Agda/Interaction/Monad.hs b/src/full/Agda/Interaction/Monad.hs --- a/src/full/Agda/Interaction/Monad.hs +++ b/src/full/Agda/Interaction/Monad.hs @@ -30,8 +30,8 @@ instance MonadUndo [CurrentPoint] IM where - undo = - + undo = + run diff --git a/src/full/Agda/Interaction/Options.hs b/src/full/Agda/Interaction/Options.hs --- a/src/full/Agda/Interaction/Options.hs +++ b/src/full/Agda/Interaction/Options.hs @@ -58,7 +58,7 @@ , optGenerateVimFile :: Bool , optGenerateEmacsFile :: Bool , optGenerateHTML :: Bool - , optHTMLDir :: Maybe FilePath + , optHTMLDir :: FilePath , optCSSFile :: Maybe FilePath , optIgnoreInterfaces :: Bool , optDisablePositivity :: Bool @@ -96,7 +96,7 @@ , optGenerateVimFile = False , optGenerateEmacsFile = False , optGenerateHTML = False - , optHTMLDir = Nothing + , optHTMLDir = defaultHTMLDir , optCSSFile = Nothing , optIgnoreInterfaces = False , optDisablePositivity = False @@ -115,6 +115,10 @@ defaultMAlonzoDir = "." +-- | The default output directory for HTML. + +defaultHTMLDir = "html" + prop_defaultOptions = case checkOpts defaultOptions of Left _ -> False Right _ -> True @@ -148,6 +152,7 @@ , optCompileMAlonzo ] +inputFlag :: FilePath -> CommandLineOptions -> Either String CommandLineOptions inputFlag f o = case optInputFile o of Nothing -> checkOpts $ o { optInputFile = Just f } @@ -180,7 +185,7 @@ ghcFlag f o = checkOpts $ o { optGhcFlags = f : optGhcFlags o } htmlFlag o = checkOpts $ o { optGenerateHTML = True } -htmlDirFlag d o = checkOpts $ o { optHTMLDir = Just d } +htmlDirFlag d o = checkOpts $ o { optHTMLDir = d } cssFlag f o = checkOpts $ o { optCSSFile = Just f } includeFlag d o = checkOpts $ o { optIncludeDirs = d : optIncludeDirs o } @@ -216,7 +221,7 @@ "use the Alonzo compiler (only with --compile)" , Option [] ["malonzo"] (NoArg malonzoFlag) "use the MAlonzo compiler (DEFAULT) (only with --compile)" - , Option [] ["malonzodir"] (ReqArg malonzoDirFlag "DIR") + , Option [] ["malonzo-dir"] (ReqArg malonzoDirFlag "DIR") ("directory for MAlonzo output (default: " ++ defaultMAlonzoDir ++ ")") , Option [] ["ghc-flag"] (ReqArg ghcFlag "GHC-FLAG") @@ -230,7 +235,8 @@ , Option [] ["html"] (NoArg htmlFlag) "generate HTML files with highlighted source code" , Option [] ["html-dir"] (ReqArg htmlDirFlag "DIR") - "directory in which HTML files are placed" + ("directory in which HTML files are placed (default: " ++ + defaultHTMLDir ++ ")") , Option [] ["css"] (ReqArg cssFlag "URL") "the CSS file used by the HTML files (can be relative)" , Option [] ["ignore-interfaces"] (NoArg ignoreInterfacesFlag) @@ -304,7 +310,7 @@ usageInfo (header progName) options ++ "\nPlugins:\n" ++ indent (concatMap pluginMsg pluginInfos) - + where header progName = unlines [ "Agda 2" , "" @@ -313,7 +319,7 @@ indent = unlines . map (" " ++) . lines - pluginMsg (name, help, inherited, opts) + pluginMsg (name, help, inherited, opts) | null opts && null inherited = optHeader | otherwise = usageInfo (optHeader ++ " Plugin-specific options:" ++ diff --git a/src/full/Agda/Main.hs b/src/full/Agda/Main.hs --- a/src/full/Agda/Main.hs +++ b/src/full/Agda/Main.hs @@ -15,6 +15,7 @@ import System.Environment import System.Exit +import System.FilePath import qualified System.IO.UTF8 as UTF8 import Agda.Syntax.Position @@ -70,9 +71,9 @@ case opts of Left err -> liftIO $ optionError err Right opts - | optShowHelp opts -> liftIO printUsage - | optShowVersion opts -> liftIO printVersion - | optRunTests opts -> liftIO $ do + | optShowHelp opts -> liftIO printUsage + | optShowVersion opts -> liftIO printVersion + | optRunTests opts -> liftIO $ do ok <- testSuite unless ok exitFailure | isNothing (optInputFile opts) diff --git a/src/full/Agda/Syntax/Concrete/Definitions.hs b/src/full/Agda/Syntax/Concrete/Definitions.hs --- a/src/full/Agda/Syntax/Concrete/Definitions.hs +++ b/src/full/Agda/Syntax/Concrete/Definitions.hs @@ -251,7 +251,7 @@ where dataOrRec mkDef niceD r x tel t cs = do ds <- niceD fixs cs - return $ + return $ [ NiceDef r [d] [ Axiom (fuseRange x t) f PublicAccess ConcreteDef x (Pi tel t) @@ -435,7 +435,7 @@ mkPrivateClause (Clause x lhs rhs wh with) = Clause x lhs rhs (mkPrivateWhere wh) (map mkPrivateClause with) - + mkPrivateWhere NoWhere = NoWhere mkPrivateWhere (AnyWhere ds) = AnyWhere [Private (getRange ds) ds] mkPrivateWhere (SomeWhere m ds) = SomeWhere m [Private (getRange ds) ds] diff --git a/src/full/Agda/Syntax/Concrete/Operators/Parser.hs b/src/full/Agda/Syntax/Concrete/Operators/Parser.hs --- a/src/full/Agda/Syntax/Concrete/Operators/Parser.hs +++ b/src/full/Agda/Syntax/Concrete/Operators/Parser.hs @@ -101,7 +101,7 @@ return $ f e where restP = return id +++ do - f <- binop op + f <- binop op e <- p return $ flip f e diff --git a/src/full/Agda/Syntax/Concrete/Pretty.hs b/src/full/Agda/Syntax/Concrete/Pretty.hs --- a/src/full/Agda/Syntax/Concrete/Pretty.hs +++ b/src/full/Agda/Syntax/Concrete/Pretty.hs @@ -208,7 +208,7 @@ ] $$ nest 2 (vcat $ map pretty cs) Infix f xs -> pretty f <+> (fsep $ punctuate comma $ map pretty xs) - + Mutual _ ds -> namedBlock "mutual" ds Abstract _ ds -> namedBlock "abstract" ds Private _ ds -> namedBlock "private" ds @@ -225,7 +225,7 @@ , nest 2 $ text "=" <+> pretty e <+> pretty i ] Open _ x i -> hsep [ text "open", pretty x, pretty i ] - Import _ x rn open i -> + Import _ x rn open i -> hsep [ pretty open, text "import", pretty x, as rn, pretty i ] where as Nothing = empty diff --git a/src/full/Agda/Syntax/Info.hs b/src/full/Agda/Syntax/Info.hs --- a/src/full/Agda/Syntax/Info.hs +++ b/src/full/Agda/Syntax/Info.hs @@ -7,7 +7,7 @@ module Agda.Syntax.Info where -import Data.Generics(Data,Typeable) +import Data.Generics(Data,Typeable) import Agda.Syntax.Common import Agda.Syntax.Position import Agda.Syntax.Concrete diff --git a/src/full/Agda/Syntax/Internal.hs b/src/full/Agda/Syntax/Internal.hs --- a/src/full/Agda/Syntax/Internal.hs +++ b/src/full/Agda/Syntax/Internal.hs @@ -45,10 +45,10 @@ deriving (Typeable, Data, Eq, Show) data Sort = Type Nat - | Prop + | Prop | Lub Sort Sort | Suc Sort - | MetaS MetaId + | MetaS MetaId deriving (Typeable, Data, Eq, Show) -- | Something where a meta variable may block reduction. @@ -122,9 +122,9 @@ killRange = fmap killRange -- | Type of argument lists. --- -type Args = [Arg Term] - +-- +type Args = [Arg Term] + -- | Sequence of types. An argument of the first type is bound in later types -- and so on. data Telescope = EmptyTel @@ -151,7 +151,7 @@ instance Foldable Abs where foldr f z (Abs _ t) = f t z -instance Traversable Abs where +instance Traversable Abs where traverse f (Abs x t) = Abs x <$> f t instance Sized a => Sized (Abs a) where @@ -186,7 +186,7 @@ , clauseBody :: ClauseBody } deriving (Typeable, Data, Show) -data ClauseBody = Body Term +data ClauseBody = Body Term | Bind (Abs ClauseBody) | NoBind ClauseBody | NoBody -- for absurd clauses diff --git a/src/full/Agda/Syntax/Parser/Monad.hs b/src/full/Agda/Syntax/Parser/Monad.hs --- a/src/full/Agda/Syntax/Parser/Monad.hs +++ b/src/full/Agda/Syntax/Parser/Monad.hs @@ -144,7 +144,7 @@ -- showInp "" = "at end of file" -- showInp t = "on input " ++ elide 5 t --- +-- -- elide 3 s -- | length (take 4 s) < 4 = s -- | otherwise = "..." diff --git a/src/full/Agda/Syntax/Parser/StringLiterals.hs b/src/full/Agda/Syntax/Parser/StringLiterals.hs --- a/src/full/Agda/Syntax/Parser/StringLiterals.hs +++ b/src/full/Agda/Syntax/Parser/StringLiterals.hs @@ -142,7 +142,7 @@ readNum :: (Char -> Bool) -> Int -> (Char -> Int) -> LookAhead Char readNum isDigit base conv = do c <- eatNextChar - if isDigit c + if isDigit c then readNumAcc isDigit base conv (conv c) else fail "non-digit in numeral" diff --git a/src/full/Agda/Syntax/Scope/Base.hs b/src/full/Agda/Syntax/Scope/Base.hs --- a/src/full/Agda/Syntax/Scope/Base.hs +++ b/src/full/Agda/Syntax/Scope/Base.hs @@ -169,7 +169,7 @@ } -- | Map monadic function over a namespace. -mapNameSpaceM :: Monad m => +mapNameSpaceM :: Monad m => (NamesInScope -> m NamesInScope ) -> (ModulesInScope -> m ModulesInScope) -> NameSpace -> m NameSpace diff --git a/src/full/Agda/Syntax/Translation/AbstractToConcrete.hs b/src/full/Agda/Syntax/Translation/AbstractToConcrete.hs --- a/src/full/Agda/Syntax/Translation/AbstractToConcrete.hs +++ b/src/full/Agda/Syntax/Translation/AbstractToConcrete.hs @@ -200,7 +200,7 @@ withAbstractPrivate i m = case (defAccess i, defAbstract i) of (PublicAccess, ConcreteDef) -> m - (p,a) -> + (p,a) -> do ds <- m return $ abst a $ priv p $ ds where @@ -344,7 +344,7 @@ toConcrete (A.Fun i a b) = bracket piBrackets - $ do a' <- toConcreteCtx FunctionSpaceDomainCtx a + $ do a' <- toConcreteCtx FunctionSpaceDomainCtx a b' <- toConcreteCtx TopCtx b return $ C.Fun (getRange i) (mkArg a') b' where diff --git a/src/full/Agda/Syntax/Translation/ConcreteToAbstract.hs b/src/full/Agda/Syntax/Translation/ConcreteToAbstract.hs --- a/src/full/Agda/Syntax/Translation/ConcreteToAbstract.hs +++ b/src/full/Agda/Syntax/Translation/ConcreteToAbstract.hs @@ -238,7 +238,7 @@ flatten (x,(y,z)) = (x,y,z) instance ToAbstract c a => ToAbstract [c] [a] where - toAbstract = mapM toAbstract + toAbstract = mapM toAbstract instance ToAbstract c a => ToAbstract (Maybe c) (Maybe a) where toAbstract Nothing = return Nothing @@ -605,7 +605,7 @@ do let cs = map conName cons dups = nub $ cs \\ nub cs bad = filter (`elem` dups) cs - unless (distinct cs) $ + unless (distinct cs) $ setCurrentRange (getRange bad) $ typeError $ DuplicateConstructors dups diff --git a/src/full/Agda/Syntax/Translation/InternalToAbstract.hs b/src/full/Agda/Syntax/Translation/InternalToAbstract.hs --- a/src/full/Agda/Syntax/Translation/InternalToAbstract.hs +++ b/src/full/Agda/Syntax/Translation/InternalToAbstract.hs @@ -411,7 +411,7 @@ instance (Reify i1 a1, Reify i2 a2) => Reify (i1,i2) (a1,a2) where reify (x,y) = (,) <$> reify x <*> reify y -instance (Reify t t', Reify a a') +instance (Reify t t', Reify a a') => Reify (Judgement t a) (Judgement t' a') where reify (HasType i t) = HasType <$> reify i <*> reify t reify (IsSort i) = IsSort <$> reify i diff --git a/src/full/Agda/Termination/CallGraph.hs b/src/full/Agda/Termination/CallGraph.hs --- a/src/full/Agda/Termination/CallGraph.hs +++ b/src/full/Agda/Termination/CallGraph.hs @@ -54,7 +54,7 @@ -- @'Unknown' '<=' 'Le' '<=' 'Lt'@. -- -- See 'Call' for more information. --- +-- -- TODO: document orders which are call-matrices themselves. data Order = Lt | Le | Unknown | Mat (Matrix Integer Order) @@ -64,7 +64,7 @@ show Lt = "<" show Le = "=" show Unknown = "?" - show (Mat m) = "Mat " ++ show m + show (Mat m) = "Mat " ++ show m --instance Ord Order where -- max = maxO @@ -76,7 +76,7 @@ coarbitrary Lt = variant 0 coarbitrary Le = variant 1 coarbitrary Unknown = variant 2 - coarbitrary (Mat m) = variant 3 + coarbitrary (Mat m) = variant 3 -- | Multiplication of 'Order's. (Corresponds to sequential -- composition.) @@ -87,7 +87,7 @@ Lt .*. _ = Lt Le .*. o = o Unknown .*. _ = Unknown -(Mat m1) .*. (Mat m2) = if (okM m1 m2) then +(Mat m1) .*. (Mat m2) = if (okM m1 m2) then Mat $ mul orderSemiring m1 m2 else (collapse m1) .*. (collapse m2) @@ -107,7 +107,7 @@ supremum = foldr maxO Unknown maxO :: Order -> Order -> Order -maxO o1 o2 = case (o1,o2) of +maxO o1 o2 = case (o1,o2) of (_,Lt) -> Lt (Lt,_) -> Lt (Unknown,_) -> o2 @@ -123,7 +123,7 @@ -- infimum = foldr min Lt -- DELETE ? -- | @('Order', 'max', '.*.')@ forms a semiring, with 'Unknown' as zero --- and 'Le' as one. +-- and 'Le' as one. orderSemiring :: Semiring Order orderSemiring = diff --git a/src/full/Agda/Termination/Matrix.hs b/src/full/Agda/Termination/Matrix.hs --- a/src/full/Agda/Termination/Matrix.hs +++ b/src/full/Agda/Termination/Matrix.hs @@ -310,10 +310,10 @@ ------------------------------------------------------------------------ -- Zipping (assumes non-empty matrices) -zipWith :: (a -> b -> c) -> +zipWith :: (a -> b -> c) -> Matrix Integer a -> Matrix Integer b -> Matrix Integer c -zipWith f m1 m2 - = fromLists (Size { rows = toInteger $ length ll, +zipWith f m1 m2 + = fromLists (Size { rows = toInteger $ length ll, cols = toInteger $ length (head ll) }) ll where ll = List.zipWith (List.zipWith f) (toLists m1) (toLists m2) diff --git a/src/full/Agda/Termination/TermCheck.hs b/src/full/Agda/Termination/TermCheck.hs --- a/src/full/Agda/Termination/TermCheck.hs +++ b/src/full/Agda/Termination/TermCheck.hs @@ -1,7 +1,7 @@ {-# LANGUAGE CPP #-} {- Checking for Structural recursion - Authors: Andreas Abel, Nils Anders Danielsson, Ulf Norell, + Authors: Andreas Abel, Nils Anders Danielsson, Ulf Norell, Karl Mehltretter and others Created: 2007-05-28 Source : TypeCheck.Rules.Decl @@ -115,7 +115,7 @@ case r of Right _ -> return r Left _ -> do - -- now try to termination check regarding the dot patterns + -- now try to termination check regarding the dot patterns calls2 <- collect conf{ useDotPatterns = True } reportS "term.lex" 30 $ unlines [ "Calls (dot patterns): " ++ show calls2 @@ -236,7 +236,7 @@ instance PrettyTCM DeBruijnPat where prettyTCM (VarDBP i) = text $ show i prettyTCM (ConDBP c ps) = parens (prettyTCM c <+> hsep (map prettyTCM ps)) - prettyTCM (LitDBP l) = prettyTCM l + prettyTCM (LitDBP l) = prettyTCM l unusedVar :: DeBruijnPat unusedVar = LitDBP (LitString noRange "term.unused.pat.var") @@ -314,7 +314,7 @@ return $ Just (i - 1, t, absBody b) stripBind conf i (DotP _) (Body b) = __IMPOSSIBLE__ stripBind conf i (LitP l) b = return $ Just (i, LitDBP l, b) -stripBind conf i (ConP c args) b = do +stripBind conf i (ConP c args) b = do r <- stripBinds conf i (map unArg args) b case r of Just (i', dbps, b') -> return $ Just (i', ConDBP c dbps, b') @@ -371,7 +371,7 @@ , nest 2 $ text "rhs:" <+> prettyTCM t0 ]) loop pats0 Le t0 - where + where Just fInd = toInteger <$> List.elemIndex f names loop :: [DeBruijnPat] -> Order -> Term -> TCM Calls loop pats guarded t = do @@ -394,17 +394,17 @@ calls <- collectCalls (loop pats Unknown) args - reportSDoc "term.found.call" 10 + reportSDoc "term.found.call" 10 (sep [ text "found call from" <+> prettyTCM f , nest 2 $ text "to" <+> prettyTCM g ]) -- insert this call into the call list case List.elemIndex g names of - + -- call leads outside the mutual block and can be ignored Nothing -> return calls - + -- call is to one of the mutally recursive functions Just gInd' -> do @@ -413,14 +413,14 @@ nrows = genericLength args + 1 matrix' = addGuardedness guarded (ncols - 1) matrix - reportSDoc "term.kept.call" 10 + reportSDoc "term.kept.call" 10 (sep [ text "kept call from" <+> prettyTCM f <+> hsep (map prettyTCM pats) - , nest 2 $ text "to" <+> prettyTCM g <+> + , nest 2 $ text "to" <+> prettyTCM g <+> hsep (map (parens . prettyTCM) args) , nest 2 $ text ("call matrix: " ++ show matrix) ]) - + return (Term.insert (Term.Call { Term.source = fInd @@ -470,12 +470,12 @@ {- | compareArgs suc pats ts - compare a list of de Bruijn patterns (=parameters) @pats@ - with a list of arguments @ts@ and create a call maxtrix + compare a list of de Bruijn patterns (=parameters) @pats@ + with a list of arguments @ts@ and create a call maxtrix with |ts| rows and |pats| columns. If sized types are enabled, @suc@ is the name of the size successor. - -} + -} compareArgs :: Maybe QName -> [DeBruijnPat] -> [Term] -> TCM [[Term.Order]] compareArgs suc pats ts = mapM (\t -> mapM (compareTerm suc t) pats) ts @@ -532,7 +532,7 @@ case (length ts, length ps) of (0,0) -> return Term.Le -- c <= c (0,1) -> return Term.Unknown -- c not<= c x - (1,0) -> __IMPOSSIBLE__ + (1,0) -> __IMPOSSIBLE__ (1,1) -> compareTerm' suc (unArg (head ts)) (head ps) (_,_) -> do -- build "call matrix" m <- mapM (\t -> mapM (compareTerm' suc (unArg t)) ps) ts @@ -551,5 +551,5 @@ compareVar i (LitDBP _) = return $ Term.Unknown compareVar i (ConDBP c ps) = do os <- mapM (compareVar i) ps - let o = Term.supremum os + let o = Term.supremum os return $ (Term..*.) Term.Lt o diff --git a/src/full/Agda/Termination/Termination.hs b/src/full/Agda/Termination/Termination.hs --- a/src/full/Agda/Termination/Termination.hs +++ b/src/full/Agda/Termination/Termination.hs @@ -47,11 +47,11 @@ -- positive. -- -- The termination criterion is taken from Jones et al. --- In the completed call graph, each idempotent call-matrix +-- In the completed call graph, each idempotent call-matrix -- from a function to itself must have a decreasing argument. -- Idempotency is wrt. matrix multiplication. -- --- This criterion is strictly more liberal than searching for a +-- This criterion is strictly more liberal than searching for a -- lexicographic order (and easier to implement, but harder to justify). terminates :: (Ord meta, Monoid meta) => CallGraph meta -> Either meta () @@ -63,12 +63,12 @@ checkIdems [] = Right () checkIdems ((c,m):xs) = if (checkIdem c) then checkIdems xs else Left m -{- Convention (see TermCheck): +{- Convention (see TermCheck): Guardedness flag is in position (0,0) of the matrix, it is always present even if the functions are all recursive. The examples below do not include the guardedness flag, though. -} - + checkIdem :: Call -> Bool checkIdem c = let b = target c == source c @@ -105,14 +105,14 @@ flat = 1 aux = 2 c1 = Call { source = flat, target = aux - , cm = CallMatrix $ fromLists (Size 2 1) [[Lt], [Lt]] + , cm = CallMatrix $ fromLists (Size 2 1) [[Lt], [Lt]] } c2 = Call { source = aux, target = aux , cm = CallMatrix $ fromLists (Size 2 2) [ [Lt, Unknown] - , [Unknown, Le]] + , [Unknown, Le]] } c3 = Call { source = aux, target = flat - , cm = CallMatrix $ fromLists (Size 1 2) [[Unknown, Le]] + , cm = CallMatrix $ fromLists (Size 1 2) [[Unknown, Le]] } prop_terminates_example1 = isRight $ terminates example1 @@ -130,10 +130,10 @@ plus = 1 c = Call { source = plus, target = plus , cm = CallMatrix $ fromLists (Size 2 2) [ [Unknown, Le] - , [Lt, Unknown] ] + , [Lt, Unknown] ] } -prop_terminates_example2 = isRight $ terminates example2 +prop_terminates_example2 = isRight $ terminates example2 -- | A related example which is anyway handled: argument swapping addition -- using two alternating functions. @@ -153,10 +153,10 @@ plus' = 2 c f g = Call { source = f, target = g , cm = CallMatrix $ fromLists (Size 2 2) [ [Unknown, Le] - , [Lt, Unknown] ] + , [Lt, Unknown] ] } -prop_terminates_example3 = isRight $ terminates example3 +prop_terminates_example3 = isRight $ terminates example3 -- | A contrived example. -- @@ -176,22 +176,22 @@ g = 2 c1 = Call { source = f, target = f , cm = CallMatrix $ fromLists (Size 2 2) [ [Le, Unknown] - , [Unknown, Le] ] + , [Unknown, Le] ] } c2 = Call { source = f, target = g , cm = CallMatrix $ fromLists (Size 2 2) [ [Lt, Unknown] - , [Unknown, Le] ] + , [Unknown, Le] ] } c3 = Call { source = g, target = f , cm = CallMatrix $ fromLists (Size 2 2) [ [Le, Unknown] - , [Unknown, Le] ] + , [Unknown, Le] ] } prop_terminates_example4 = isLeft $ terminates example4 -- | This should terminate. -- --- @f (S x) (S y) = g x (S y) + f (S (S x)) y@ +-- @f (S x) (S y) = g x (S y) + f (S (S x)) y@ -- -- @g (S x) (S y) = f (S x) (S y) + g x (S y)@ @@ -202,22 +202,22 @@ g = 2 c1 = Call { source = f, target = g , cm = CallMatrix $ fromLists (Size 2 2) [ [Lt, Unknown] - , [Unknown, Le] ] + , [Unknown, Le] ] } c2 = Call { source = f, target = f , cm = CallMatrix $ fromLists (Size 2 2) [ [Unknown, Unknown] - , [Unknown, Lt] ] + , [Unknown, Lt] ] } c3 = Call { source = g, target = f , cm = CallMatrix $ fromLists (Size 2 2) [ [Le, Unknown] - , [Unknown, Le] ] + , [Unknown, Le] ] } c4 = Call { source = g, target = g , cm = CallMatrix $ fromLists (Size 2 2) [ [Lt, Unknown] - , [Unknown, Le] ] + , [Unknown, Le] ] } -prop_terminates_example5 = isRight $ terminates example5 +prop_terminates_example5 = isRight $ terminates example5 -- | Another example which should fail. -- @@ -233,16 +233,16 @@ where f = 1 c1 = Call { source = f, target = f - , cm = CallMatrix $ fromLists (Size 1 1) [ [Lt] ] + , cm = CallMatrix $ fromLists (Size 1 1) [ [Lt] ] } c2 = Call { source = f, target = f - , cm = CallMatrix $ fromLists (Size 1 1) [ [Le] ] + , cm = CallMatrix $ fromLists (Size 1 1) [ [Le] ] } c3 = Call { source = f, target = f - , cm = CallMatrix $ fromLists (Size 1 1) [ [Le] ] + , cm = CallMatrix $ fromLists (Size 1 1) [ [Le] ] } -prop_terminates_example6 = isLeft $ terminates example6 +prop_terminates_example6 = isLeft $ terminates example6 ------------------------------------------------------------------------ -- All tests diff --git a/src/full/Agda/TypeChecking/Conversion.hs b/src/full/Agda/TypeChecking/Conversion.hs --- a/src/full/Agda/TypeChecking/Conversion.hs +++ b/src/full/Agda/TypeChecking/Conversion.hs @@ -249,7 +249,7 @@ a <- reduce a case funView (unEl a) of FunV (Arg _ b) _ -> do - reportSDoc "tc.conv.args" 10 $ + reportSDoc "tc.conv.args" 10 $ sep [ text "compareArgs" <+> parens (text $ show pol) , nest 2 $ sep [ prettyTCM arg1 , text "~~" <+> prettyTCM arg2 diff --git a/src/full/Agda/TypeChecking/Coverage.hs b/src/full/Agda/TypeChecking/Coverage.hs --- a/src/full/Agda/TypeChecking/Coverage.hs +++ b/src/full/Agda/TypeChecking/Coverage.hs @@ -80,7 +80,7 @@ whenM (optCompletenessCheck <$> commandLineOptions) $ case pss of [] -> return () - _ -> + _ -> setCurrentRange (getRange cs) $ typeError $ CoverageFailure f pss whenM (optUnreachableCheck <$> commandLineOptions) $ @@ -207,7 +207,7 @@ let theta = delta1 `abstract` gamma `abstract` delta2' debugTel "theta" theta - -- Apply the unifying substitution to Θ + -- Apply the unifying substitution to Θ -- We get ρ' : Θ' -> Θ -- π : Θ' -> Θ (theta', iperm, rho', _) <- instantiateTel sub' theta diff --git a/src/full/Agda/TypeChecking/Errors.hs b/src/full/Agda/TypeChecking/Errors.hs --- a/src/full/Agda/TypeChecking/Errors.hs +++ b/src/full/Agda/TypeChecking/Errors.hs @@ -105,7 +105,6 @@ FieldOutsideRecord -> "FieldOutsideRecord" FileNotFound _ _ -> "FileNotFound" GenericError _ -> "GenericError" - HTMLDirUndefined -> "HTMLDirUndefined" IlltypedPattern _ _ -> "IlltypedPattern" IncompletePatternMatching _ _ -> "IncompletePatternMatching" InternalError _ -> "InternalError" @@ -374,12 +373,12 @@ two = zipWith (\a b -> [a,b]) s (tail s) NoSuchModule x -> fsep $ pwords "No such module" ++ [pretty x] - AmbiguousName x ys -> vcat + AmbiguousName x ys -> vcat [ fsep $ pwords "Ambiguous name" ++ [pretty x <> text "."] ++ pwords "It could refer to any one of" , nest 2 $ vcat $ map nameWithBinding ys ] - AmbiguousModule x ys -> vcat + AmbiguousModule x ys -> vcat [ fsep $ pwords "Ambiguous module name" ++ [pretty x <> text "."] ++ pwords "It could refer to any one of" , nest 2 $ vcat $ map prettyTCM ys @@ -485,8 +484,7 @@ com [] = empty com (_:_) = comma - HTMLDirUndefined -> - fwords "You have to specify where to place the HTML files." + where mpar n args | n > 0 && not (null args) = parens diff --git a/src/full/Agda/TypeChecking/Free.hs b/src/full/Agda/TypeChecking/Free.hs --- a/src/full/Agda/TypeChecking/Free.hs +++ b/src/full/Agda/TypeChecking/Free.hs @@ -1,7 +1,7 @@ {-# LANGUAGE CPP #-} -- | Computing the free variables of a term. -module Agda.TypeChecking.Free +module Agda.TypeChecking.Free ( FreeVars(..) , Free(..) , allVars diff --git a/src/full/Agda/TypeChecking/MetaVars.hs b/src/full/Agda/TypeChecking/MetaVars.hs --- a/src/full/Agda/TypeChecking/MetaVars.hs +++ b/src/full/Agda/TypeChecking/MetaVars.hs @@ -343,7 +343,7 @@ pr _ = text ".." in text "args:" <+> sep (map (pr . unArg) args) - + ids <- checkArgs x args reportSDoc "tc.meta.assign" 15 $ @@ -439,7 +439,7 @@ updateMeta :: (MonadTCM tcm, Data a, Occurs a, Abstract a) => MetaId -> a -> tcm () -updateMeta mI t = +updateMeta mI t = do mv <- lookupMeta mI withMetaInfo (getMetaInfo mv) $ do args <- getContextArgs diff --git a/src/full/Agda/TypeChecking/Monad/Base.hs b/src/full/Agda/TypeChecking/Monad/Base.hs --- a/src/full/Agda/TypeChecking/Monad/Base.hs +++ b/src/full/Agda/TypeChecking/Monad/Base.hs @@ -234,7 +234,7 @@ -- ** Meta variables --------------------------------------------------------------------------- -data MetaVariable = +data MetaVariable = MetaVar { mvInfo :: MetaInfo , mvPriority :: MetaPriority -- ^ some metavariables are more eager to be instantiated , mvJudgement :: Judgement Type MetaId @@ -291,7 +291,7 @@ getMetaEnv m = clEnv $ getMetaInfo m getMetaSig :: MetaVariable -> Signature -getMetaSig m = clSignature $ getMetaInfo m +getMetaSig m = clSignature $ getMetaInfo m --------------------------------------------------------------------------- -- ** Interaction meta variables @@ -803,9 +803,8 @@ | AmbiguousParseForApplication [C.Expr] [C.Expr] | NoParseForLHS C.Pattern | AmbiguousParseForLHS C.Pattern [C.Pattern] - -- Usage errors. - | HTMLDirUndefined - deriving (Typeable) + -- Usage errors + deriving (Typeable) data TCErr = TypeError TCState (Closure TypeError) | Exception Range String diff --git a/src/full/Agda/TypeChecking/Monad/Builtin.hs b/src/full/Agda/TypeChecking/Monad/Builtin.hs --- a/src/full/Agda/TypeChecking/Monad/Builtin.hs +++ b/src/full/Agda/TypeChecking/Monad/Builtin.hs @@ -20,7 +20,7 @@ Just (Builtin y) -> typeError $ DuplicateBuiltinBinding b y x Just (Prim _) -> typeError $ NoSuchBuiltinName b Nothing -> modify $ \st -> - st { stLocalBuiltins = + st { stLocalBuiltins = Map.insert b (Builtin x) $ stLocalBuiltins st } diff --git a/src/full/Agda/TypeChecking/Monad/Closure.hs b/src/full/Agda/TypeChecking/Monad/Closure.hs --- a/src/full/Agda/TypeChecking/Monad/Closure.hs +++ b/src/full/Agda/TypeChecking/Monad/Closure.hs @@ -13,5 +13,5 @@ $ withEnv env $ withTrace trace $ k x - + diff --git a/src/full/Agda/TypeChecking/Monad/Env.hs b/src/full/Agda/TypeChecking/Monad/Env.hs --- a/src/full/Agda/TypeChecking/Monad/Env.hs +++ b/src/full/Agda/TypeChecking/Monad/Env.hs @@ -30,7 +30,7 @@ local $ \e -> e { envAnonymousModules = (m, n) : envAnonymousModules e } --- | Set the current environment to the given +-- | Set the current environment to the given withEnv :: MonadTCM tcm => TCEnv -> tcm a -> tcm a withEnv env m = local (const env) m diff --git a/src/full/Agda/TypeChecking/Monad/MetaVars.hs b/src/full/Agda/TypeChecking/Monad/MetaVars.hs --- a/src/full/Agda/TypeChecking/Monad/MetaVars.hs +++ b/src/full/Agda/TypeChecking/Monad/MetaVars.hs @@ -46,7 +46,7 @@ getMetaPriority i = mvPriority <$> lookupMeta i createMetaInfo :: MonadTCM tcm => tcm MetaInfo -createMetaInfo = +createMetaInfo = do r <- getCurrentRange buildClosure r @@ -79,14 +79,14 @@ isInteractionMeta m = fmap (m `elem`) getInteractionMetas lookupInteractionId :: MonadTCM tcm => InteractionId -> tcm MetaId -lookupInteractionId ii = +lookupInteractionId ii = do mmi <- Map.lookup ii <$> gets stInteractionPoints case mmi of Just mi -> return mi _ -> fail $ "no such interaction point: " ++ show ii judgementInteractionId :: MonadTCM tcm => InteractionId -> tcm (Judgement Type MetaId) -judgementInteractionId ii = +judgementInteractionId ii = do mi <- lookupInteractionId ii mvJudgement <$> lookupMeta mi @@ -112,7 +112,7 @@ getInteractionScope :: MonadTCM tcm => InteractionId -> tcm ScopeInfo -getInteractionScope ii = +getInteractionScope ii = do mi <- lookupInteractionId ii mv <- lookupMeta mi return $ getMetaScope mv diff --git a/src/full/Agda/TypeChecking/Monad/Signature.hs b/src/full/Agda/TypeChecking/Monad/Signature.hs --- a/src/full/Agda/TypeChecking/Monad/Signature.hs +++ b/src/full/Agda/TypeChecking/Monad/Signature.hs @@ -73,7 +73,7 @@ where d' = d { defName = q } new +++ old = new { defDisplay = defDisplay new ++ defDisplay old } - + hideTel EmptyTel = EmptyTel hideTel (ExtendTel (Arg _ t) tel) = ExtendTel (Arg Hidden t) $ hideTel <$> tel @@ -413,7 +413,7 @@ current = envCurrentModule env m = qnameModule q --- | get type of a constant +-- | get type of a constant typeOfConst :: MonadTCM tcm => QName -> tcm Type typeOfConst q = defType <$> (instantiateDef =<< getConstInfo q) diff --git a/src/full/Agda/TypeChecking/Polarity.hs b/src/full/Agda/TypeChecking/Polarity.hs --- a/src/full/Agda/TypeChecking/Polarity.hs +++ b/src/full/Agda/TypeChecking/Polarity.hs @@ -90,7 +90,7 @@ isLin <- checkSizeIndex np sizeArg target return $ isPos && isLin - + ifM (and <$> mapM check cons) (return [Covariant]) (return [Invariant]) diff --git a/src/full/Agda/TypeChecking/Positivity.hs b/src/full/Agda/TypeChecking/Positivity.hs --- a/src/full/Agda/TypeChecking/Positivity.hs +++ b/src/full/Agda/TypeChecking/Positivity.hs @@ -393,7 +393,7 @@ occs <- computeOccurrences q let onItem (item, occs) = do es <- mapM (computeEdge qs) occs - return $ Graph.unions $ + return $ Graph.unions $ map (\(b, w) -> Graph.singleton (itemToNode item) b w) es Graph.unions <$> mapM onItem (Map.assocs occs) where diff --git a/src/full/Agda/TypeChecking/Primitive.hs b/src/full/Agda/TypeChecking/Primitive.hs --- a/src/full/Agda/TypeChecking/Primitive.hs +++ b/src/full/Agda/TypeChecking/Primitive.hs @@ -196,7 +196,7 @@ _ -> return $ NoReduction t -- | Conceptually: @redBind m f k = either (return . Left . f) k =<< m@ -redBind :: MonadTCM tcm => tcm (Reduced a a') -> (a -> b) -> +redBind :: MonadTCM tcm => tcm (Reduced a a') -> (a -> b) -> (a' -> tcm (Reduced b b')) -> tcm (Reduced b b') redBind ma f k = do r <- ma diff --git a/src/full/Agda/TypeChecking/Reduce.hs b/src/full/Agda/TypeChecking/Reduce.hs --- a/src/full/Agda/TypeChecking/Reduce.hs +++ b/src/full/Agda/TypeChecking/Reduce.hs @@ -225,7 +225,7 @@ (_, []) -> defaultResult -- no definition for head (_, cls@(Clause{ clausePats = ps } : _)) | length ps <= length args -> - do let (args1,args2) = splitAt (length ps) args + do let (args1,args2) = splitAt (length ps) args ev <- appDef v0 cls args1 case ev of NoReduction v -> return $ v `apply` args2 @@ -249,7 +249,7 @@ DontKnow (Just m) -> return $ NoReduction $ blocked m $ v `apply` args Yes args' | hasBody body -> return $ YesReduction ( - -- TODO: let matchPatterns also return the reduced forms + -- TODO: let matchPatterns also return the reduced forms -- of the original arguments! app args' body) | otherwise -> return $ NoReduction $ notBlocked $ v `apply` args diff --git a/src/full/Agda/TypeChecking/Rules/Data.hs b/src/full/Agda/TypeChecking/Rules/Data.hs --- a/src/full/Agda/TypeChecking/Rules/Data.hs +++ b/src/full/Agda/TypeChecking/Rules/Data.hs @@ -47,7 +47,7 @@ -- Look up the type of the datatype. t <- instantiateFull =<< typeOfConst name - -- The parameters are in scope when checking the constructors. + -- The parameters are in scope when checking the constructors. dataDef <- bindParameters ps t $ \tel t0 -> do -- Parameters are always hidden in constructors diff --git a/src/full/Agda/TypeChecking/Rules/Def.hs b/src/full/Agda/TypeChecking/Rules/Def.hs --- a/src/full/Agda/TypeChecking/Rules/Def.hs +++ b/src/full/Agda/TypeChecking/Rules/Def.hs @@ -133,7 +133,7 @@ traceCall (CheckClause t c) $ checkLeftHandSide c aps t $ \gamma delta sub xs ps t' perm -> do let mkBody v = foldr (\x t -> Bind $ Abs x t) (Body $ substs sub v) xs - (body, with) <- checkWhere (size delta) wh $ + (body, with) <- checkWhere (size delta) wh $ case rhs of A.RHS e | any (containsAbsurdPattern . namedThing . unArg) aps -> diff --git a/src/full/Agda/TypeChecking/Rules/LHS.hs b/src/full/Agda/TypeChecking/Rules/LHS.hs --- a/src/full/Agda/TypeChecking/Rules/LHS.hs +++ b/src/full/Agda/TypeChecking/Rules/LHS.hs @@ -85,7 +85,7 @@ -- be longer than the pattern dpi [] _ _ = [] dpi (_ : ps) (Nothing : s) as = dpi ps s as - dpi (p : ps) (Just u : s) (a : as) = + dpi (p : ps) (Just u : s) (a : as) = case p of A.DotP _ e -> DPI e u a : dpi ps s as A.ImplicitP _ -> dpi ps s as @@ -274,7 +274,7 @@ let TelV tel0' b0 = telView a ps <- insertImplicitPatterns ps tel0' unless (size tel0' >= size ps) $ typeError $ TooManyArgumentsInLHS (size ps) a - let tel0 = useNamesFromPattern ps tel0' + let tel0 = useNamesFromPattern ps tel0' (as, bs) = splitAt (size ps) $ telToList tel0 gamma = telFromList as b = telePi (telFromList bs) b0 diff --git a/src/full/Agda/TypeChecking/Rules/LHS/Instantiate.hs b/src/full/Agda/TypeChecking/Rules/LHS/Instantiate.hs --- a/src/full/Agda/TypeChecking/Rules/LHS/Instantiate.hs +++ b/src/full/Agda/TypeChecking/Rules/LHS/Instantiate.hs @@ -48,7 +48,7 @@ -- s' : Substitution Γσ let s' = rename psR s - reportSDoc "tc.lhs.inst" 15 $ nest 2 $ + reportSDoc "tc.lhs.inst" 15 $ nest 2 $ text "s' =" <+> fsep (punctuate comma $ map (maybe (text "_") prettyTCM) s') -- rho : [Tm Γσ]Γ @@ -58,20 +58,20 @@ let tel1 = flattenTel tel names1 = teleNames tel - reportSDoc "tc.lhs.inst" 15 $ nest 2 $ + reportSDoc "tc.lhs.inst" 15 $ nest 2 $ text "tel1 =" <+> brackets (fsep $ punctuate comma $ map prettyTCM tel1) -- tel2 : [Type Γσ]Γ let tel2 = substs rho tel1 - reportSDoc "tc.lhs.inst" 15 $ nest 2 $ + reportSDoc "tc.lhs.inst" 15 $ nest 2 $ text "tel2 =" <+> brackets (fsep $ punctuate comma $ map prettyTCM tel2) -- tel3 : [Type Γσ]Γσ tel3 <- instantiateFull $ permute ps tel2 let names3 = permute ps names1 - reportSDoc "tc.lhs.inst" 15 $ nest 2 $ + reportSDoc "tc.lhs.inst" 15 $ nest 2 $ text "tel3 =" <+> brackets (fsep $ punctuate comma $ map prettyTCM tel3) -- p : Permutation (Γσ -> Γσ~) @@ -86,13 +86,13 @@ let tel4 = substs rho' (permute p tel3) names4 = permute p names3 - reportSDoc "tc.lhs.inst" 15 $ nest 2 $ + reportSDoc "tc.lhs.inst" 15 $ nest 2 $ text "tel4 =" <+> brackets (fsep $ punctuate comma $ map prettyTCM tel4) -- tel5 = Γσ~ let tel5 = unflattenTel names4 tel4 - reportSDoc "tc.lhs.inst" 15 $ nest 2 $ + reportSDoc "tc.lhs.inst" 15 $ nest 2 $ text "tel5 =" <+> prettyTCM tel5 -- remember the types of the instantiations diff --git a/src/full/Agda/TypeChecking/Rules/Record.hs b/src/full/Agda/TypeChecking/Rules/Record.hs --- a/src/full/Agda/TypeChecking/Rules/Record.hs +++ b/src/full/Agda/TypeChecking/Rules/Record.hs @@ -46,7 +46,7 @@ let m = mnameFromList $ qnameToList name hide (Arg _ x) = Arg Hidden x htel = map hide $ telToList tel - rect = El s $ Def name $ reverse + rect = El s $ Def name $ reverse [ Arg h (Var i []) | (i, Arg h _) <- zip [0..] $ reverse $ telToList gamma ] @@ -120,7 +120,7 @@ setScope scope >> checkProjs ftel1 ftel2 (fs' ++ fs) checkProjs ftel1 (ExtendTel (Arg _ _) ftel2) (A.Field info x t : fs) = do -- check the type (in the context of the telescope) - -- the previous fields will be free in + -- the previous fields will be free in reportSDoc "tc.rec.proj" 5 $ sep [ text "checking projection" , nest 2 $ vcat diff --git a/src/full/Agda/TypeChecking/Serialise.hs b/src/full/Agda/TypeChecking/Serialise.hs --- a/src/full/Agda/TypeChecking/Serialise.hs +++ b/src/full/Agda/TypeChecking/Serialise.hs @@ -272,7 +272,7 @@ value n = A.MName `fmap` value n instance EmbPrj A.Name where - icode (A.Name a b c d) = icode4' a b c d + icode (A.Name a b c d) = icode4' a b c d value = vcase valu where valu [a, b, c, d] = valu4 A.Name a b c d valu _ = __IMPOSSIBLE__ @@ -346,8 +346,8 @@ icode (Fun a b) = icode2 6 a b icode (Sort a ) = icode1 7 a icode (MetaV a b) = icode2 8 a b - value = vcase valu where valu [0, a, b] = valu2 Var a b - valu [1, a, b] = valu2 Lam a b + value = vcase valu where valu [0, a, b] = valu2 Var a b + valu [1, a, b] = valu2 Lam a b valu [2, a] = valu1 Lit a valu [3, a, b] = valu2 Def a b valu [4, a, b] = valu2 Con a b @@ -623,7 +623,7 @@ case maybeU of Just (U u) -> maybe (__IMPOSSIBLE__) return (cast u) Nothing -> do - v <- valu . (! ix) =<< asks nodeE + v <- valu . (! ix) =<< asks nodeE lift $ H.insert memo (ix, aTyp) (U v) return v @@ -682,7 +682,7 @@ where f m c = fromIntegral c * magic + hashInt32 m magic = 0xdeadbeef golden :: Int32 - golden = 1013904242 + golden = 1013904242 hashInt32 x = mulHi x golden + x mulHi :: Int32 -> Int32 -> Int32 mulHi a b = fromIntegral (r `shiftR` 32) diff --git a/src/full/Agda/TypeChecking/SizedTypes.hs b/src/full/Agda/TypeChecking/SizedTypes.hs --- a/src/full/Agda/TypeChecking/SizedTypes.hs +++ b/src/full/Agda/TypeChecking/SizedTypes.hs @@ -35,7 +35,7 @@ ] u <- reduce u v <- reduce v - reportSDoc "tc.conv.size" 15 $ + reportSDoc "tc.conv.size" 15 $ nest 2 $ sep [ text (show u) <+> prettyTCM cmp , text (show v) ] @@ -57,7 +57,7 @@ trivial u v = liftTCM $ do a <- sizeExpr u b <- sizeExpr v - reportSDoc "tc.conv.size" 15 $ + reportSDoc "tc.conv.size" 15 $ nest 2 $ sep [ text (show a) <+> text "<=" , text (show b) ] @@ -122,7 +122,7 @@ -- | Throws a 'patternViolation' if the term isn't a proper size expression. sizeExpr :: MonadTCM tcm => Term -> tcm (SizeExpr, Int) sizeExpr u = do - u <- reduce u -- Andreas, 2009-02-09. + u <- reduce u -- Andreas, 2009-02-09. -- This is necessary to surface the solutions of metavariables. s <- sizeView u case s of @@ -234,7 +234,7 @@ -- type Solution = Map Int SizeExpr -- data SizeExpr = SizeVar Int Int -- e.g. x + 5 -- | SizeConst Weight -- a number or infinity --- data Weight = Finite Int | Infinite +-- data Weight = Finite Int | Infinite -- data Node = Rigid Rigid -- | Flex FlexId -- data Rigid = RConst Weight diff --git a/src/full/Agda/TypeChecking/Substitute.hs b/src/full/Agda/TypeChecking/Substitute.hs --- a/src/full/Agda/TypeChecking/Substitute.hs +++ b/src/full/Agda/TypeChecking/Substitute.hs @@ -34,7 +34,7 @@ Def c args' -> Def c (args' ++ args) Con c args' -> Con c (args' ++ args) Lam _ u -> absApp u v `apply` args0 - MetaV x args' -> MetaV x (args' ++ args) + MetaV x args' -> MetaV x (args' ++ args) Lit l -> __IMPOSSIBLE__ Pi _ _ -> __IMPOSSIBLE__ Fun _ _ -> __IMPOSSIBLE__ @@ -383,7 +383,7 @@ telePi EmptyTel t = t telePi (ExtendTel u tel) t = el $ fn u b where - el = El (sLub s1 s2) + el = El (sLub s1 s2) b = fmap (flip telePi t) tel s1 = getSort $ unArg u s2 = getSort $ absBody b @@ -397,7 +397,7 @@ telePi_ EmptyTel t = t telePi_ (ExtendTel u tel) t = el $ Pi u b where - el = El (sLub s1 s2) + el = El (sLub s1 s2) b = fmap (flip telePi_ t) tel s1 = getSort $ unArg u s2 = getSort $ absBody b diff --git a/src/full/Agda/TypeChecking/Telescope.hs b/src/full/Agda/TypeChecking/Telescope.hs --- a/src/full/Agda/TypeChecking/Telescope.hs +++ b/src/full/Agda/TypeChecking/Telescope.hs @@ -75,7 +75,7 @@ teleArgNames = map (fmap fst) . telToList teleArgs :: Telescope -> Args -teleArgs tel = +teleArgs tel = reverse [ Arg h (Var i []) | (i, Arg h _) <- zip [0..] $ reverse (telToList tel) ] -- | A telescope split in two. diff --git a/src/full/Agda/TypeChecking/Test/Generators.hs b/src/full/Agda/TypeChecking/Test/Generators.hs --- a/src/full/Agda/TypeChecking/Test/Generators.hs +++ b/src/full/Agda/TypeChecking/Test/Generators.hs @@ -139,7 +139,7 @@ , tcIsType = False } where - (defs, cons) = flip evalState 0 $ + (defs, cons) = flip evalState 0 $ (,) <$> mapM mkName ds <*> mapM mkName cs tick = do x <- get; put (x + 1); return x @@ -293,7 +293,7 @@ genName :: Gen Args -> Gen Term genName args = frequency - [ (varF, genVar args) + [ (varF, genVar args) , (defF, genDef args) , (conF, genCon args) ] @@ -352,14 +352,14 @@ xs1 = take n1 xs n2 = n - n1 xs2 = drop n1 xs - + [] `ilv` ys = ys xs `ilv` [] = xs (x:xs) `ilv` (y:ys) = x : y : (xs `ilv` ys) - + shrinkOne [] = [] shrinkOne (x:xs) = [ x' : noShrink xs | x' <- shrinkC conf x ] - ++ [ noShrink x : xs' | xs' <- shrinkOne xs ] + ++ [ noShrink x : xs' | xs' <- shrinkOne xs ] instance (ShrinkC a a', ShrinkC b b') => ShrinkC (a, b) (a', b') where noShrink (x, y) = (noShrink x, noShrink y) diff --git a/src/full/Agda/TypeChecking/With.hs b/src/full/Agda/TypeChecking/With.hs --- a/src/full/Agda/TypeChecking/With.hs +++ b/src/full/Agda/TypeChecking/With.hs @@ -97,7 +97,7 @@ strip EmptyTel [] [] | 0 == 0 = return [] strip (ExtendTel a tel) (p : ps) (q : qs) = do reportSDoc "tc.with.strip" 15 $ vcat - [ text "strip" + [ text "strip" , nest 2 $ text "ps =" <+> fsep (punctuate comma $ map prettyA (p : ps)) , nest 2 $ text "qs =" <+> fsep (punctuate comma $ map (showPat . unArg) (q : qs)) , nest 2 $ text "tel=" <+> prettyTCM (ExtendTel a tel) @@ -123,7 +123,7 @@ ConP c qs' -> case namedThing $ unArg p of A.ConP _ (A.AmbQ cs') ps' -> do - + Con c' [] <- constructorForm =<< reduce (Con c []) c <- return $ c' `withRangeOf` c let getCon (Con c []) = c diff --git a/src/full/Agda/Utils/List.hs b/src/full/Agda/Utils/List.hs --- a/src/full/Agda/Utils/List.hs +++ b/src/full/Agda/Utils/List.hs @@ -12,7 +12,7 @@ import Data.Function type Prefix a = [a] -type Suffix a = [a] +type Suffix a = [a] -- | Check if a list has a given prefix. If so, return the list -- minus the prefix. diff --git a/src/full/Agda/Utils/ReadP.hs b/src/full/Agda/Utils/ReadP.hs --- a/src/full/Agda/Utils/ReadP.hs +++ b/src/full/Agda/Utils/ReadP.hs @@ -12,13 +12,13 @@ -- Module : "Text.ParserCombinators.ReadP" -- Copyright : (c) The University of Glasgow 2002 -- License : BSD-style (see the file libraries/base/LICENSE) --- +-- -- Maintainer : libraries@haskell.org -- Stability : provisional -- Portability : non-portable (local universal quantification) -- -- This is a library of parser combinators, originally written by Koen Claessen. --- It parses all alternatives in parallel, so it never keeps hold of +-- It parses all alternatives in parallel, so it never keeps hold of -- the beginning of the input string, a common source of space leaks with -- other parsers. The '(+++)' choice combinator is genuinely commutative; -- it makes no difference which branch is \"shorter\". @@ -26,10 +26,10 @@ ----------------------------------------------------------------------------- module Agda.Utils.ReadP - ( + ( -- * The 'ReadP' type ReadP, -- :: * -> *; instance Functor, Monad, MonadPlus - + -- * Primitive operations get, -- :: ReadP Char look, -- :: ReadP String @@ -107,7 +107,7 @@ -- most common case: two gets are combined Get f1 `mplus` Get f2 = Get (\c -> f1 c `mplus` f2 c) - + -- results are delivered as soon as possible Result x p `mplus` q = Result x (p `mplus` q) p `mplus` Result x q = Result x (p `mplus` q) @@ -212,9 +212,9 @@ -- ^ Transforms a parser into one that does the same, but -- in addition returns the exact characters read. -- IMPORTANT NOTE: 'gather' gives a runtime error if its first argument --- is built using any occurrences of readS_to_P. +-- is built using any occurrences of readS_to_P. gather (R m) = - R (\k -> gath id (m (\a -> return (\s -> k (s,a))))) + R (\k -> gath id (m (\a -> return (\s -> k (s,a))))) where gath l (Get f) = Get (\c -> gath (l.(c:)) (f c)) gath l Fail = Fail @@ -454,7 +454,7 @@ > xs +<+ _ = xs > > prop_Gather s = -> forAll readPWithoutReadS $ \p -> +> forAll readPWithoutReadS $ \p -> > readP_to_S (gather p) s =~ > [ ((pre,x::Int),s') > | (x,s') <- readP_to_S p s diff --git a/src/full/Agda/Utils/Serialise.hs b/src/full/Agda/Utils/Serialise.hs --- a/src/full/Agda/Utils/Serialise.hs +++ b/src/full/Agda/Utils/Serialise.hs @@ -45,7 +45,7 @@ mapS (IFun f g) sa = bindS g sa $ returnS . f (>->) :: BiMonad m => m a -> m b -> m (a,b) -sa >-> sb = bindS fst sa $ \a -> +sa >-> sb = bindS fst sa $ \a -> bindS snd sb $ \b -> returnS (a,b) diff --git a/src/full/Agda/Utils/Trie.hs b/src/full/Agda/Utils/Trie.hs --- a/src/full/Agda/Utils/Trie.hs +++ b/src/full/Agda/Utils/Trie.hs @@ -3,7 +3,7 @@ -- Module : Unstable.Org.Lochan.Trie -- Copyright : (c) Keith Wansbrough 2005 -- License : BSD-style --- +-- -- Maintainer : keith.hlib at lochan.org -- : modified and extended by Ulf Norell -- Stability : experimental @@ -29,8 +29,8 @@ -- * Derived operations takeWhile, takeWhile_V, fringe, ) where - + import Prelude hiding (takeWhile, lookup) import Data.Map (Map) import qualified Data.Map as Map @@ -78,7 +78,7 @@ where lift _ Nothing y = y lift _ x Nothing = x lift _ (Just x) (Just y) = Just (f x y) - + -- |Insertion. insert :: Ord k => [k] -> v -> Trie k v -> Trie k v diff --git a/src/full/Agda/Utils/Warshall.hs b/src/full/Agda/Utils/Warshall.hs --- a/src/full/Agda/Utils/Warshall.hs +++ b/src/full/Agda/Utils/Warshall.hs @@ -31,10 +31,10 @@ -- assuming a square matrix warshall :: SemiRing a => Matrix a -> Matrix a -warshall a0 = loop r a0 where +warshall a0 = loop r a0 where b@((r,c),(r',c')) = bounds a0 -- assuming r == c and r' == c' - loop k a | k <= r' = - loop (k+1) (array b [ ((i,j), + loop k a | k <= r' = + loop (k+1) (array b [ ((i,j), (a!(i,j)) `oplus` ((a!(i,k)) `otimes` (a!(k,j)))) | i <- [r..r'], j <- [c..c'] ]) | otherwise = a @@ -54,7 +54,7 @@ es <- Map.lookup i g foldr oplus Nothing [ Just v | (j', v) <- es, j == j' ] - m = array b [ ((n, m), edge i j) | (i, n) <- nodes, (j, m) <- nodes ] + m = array b [ ((n, m), edge i j) | (i, n) <- nodes, (j, m) <- nodes ] fromMatrix matrix = Map.fromList $ do (i, n) <- nodes @@ -64,9 +64,9 @@ ] return (i, es) --- edge weight in the graph, forming a semi ring +-- edge weight in the graph, forming a semi ring -data Weight = Finite Int | Infinite +data Weight = Finite Int | Infinite deriving (Eq) inc :: Weight -> Int -> Weight @@ -91,9 +91,9 @@ -- constraints --------------------------------------------------- --- nodes of the graph are either --- * flexible variables (with identifiers drawn from Int), --- * rigid variables (also identified by Ints), or +-- nodes of the graph are either +-- * flexible variables (with identifiers drawn from Int), +-- * rigid variables (also identified by Ints), or -- * constants (like 0, infinity, or anything between) data Node = Rigid Rigid @@ -107,7 +107,7 @@ type NodeId = Int type RigidId = Int type FlexId = Int -type Scope = RigidId -> Bool +type Scope = RigidId -> Bool -- which rigid variables a flex may be instatiated to instance Show Node where @@ -119,7 +119,7 @@ infinite (RConst Infinite) = True infinite _ = False --- isBelow r w r' +-- isBelow r w r' -- checks, if r and r' are connected by w (meaning w not infinite) -- wether r + w <= r' -- precondition: not the same rigid variable @@ -133,7 +133,7 @@ -- a constraint is an edge in the graph data Constraint = NewFlex FlexId Scope | Arc Node Int Node --- Arc v1 k v2 at least one of v1,v2 is a VMeta (Flex), +-- Arc v1 k v2 at least one of v1,v2 is a VMeta (Flex), -- the other a VMeta or a VGen (Rigid) -- if k <= 0 this means $^(-k) v1 <= v2 -- otherwise v1 <= $^k v3 @@ -150,7 +150,7 @@ -- graph (matrix) ------------------------------------------------ -data Graph = Graph +data Graph = Graph { flexScope :: Map FlexId Scope -- scope for each flexible var , nodeMap :: Map Node NodeId -- node labels to node numbers , intMap :: Map NodeId Node -- node numbers to node labels @@ -185,7 +185,7 @@ } return i --- addEdge n1 k n2 +-- addEdge n1 k n2 -- improves the weight of egde n1->n2 to be at most k -- also adds nodes if not yet present addEdge :: Node -> Int -> Node -> GM () @@ -205,13 +205,13 @@ buildGraph cs = execState (mapM_ addConstraint cs) initGraph mkMatrix :: Int -> (Int -> Int -> Weight) -> Matrix Weight -mkMatrix n g = array ((0,0),(n-1,n-1)) +mkMatrix n g = array ((0,0),(n-1,n-1)) [ ((i,j), g i j) | i <- [0..n-1], j <- [0..n-1]] -- displaying matrices with row and column labels -------------------- -- a matrix with row descriptions in b and column descriptions in c -data LegendMatrix a b c = LegendMatrix +data LegendMatrix a b c = LegendMatrix { matrix :: Matrix a , rowdescr :: Int -> b , coldescr :: Int -> c @@ -221,13 +221,13 @@ show (LegendMatrix m rd cd) = -- first show column description let ((r,c),(r',c')) = bounds m - in foldr (\ j s -> "\t" ++ show (cd j) ++ s) "" [c .. c'] ++ + in foldr (\ j s -> "\t" ++ show (cd j) ++ s) "" [c .. c'] ++ -- then output rows foldr (\ i s -> "\n" ++ show (rd i) ++ - foldr (\ j t -> "\t" ++ show (m!(i,j)) ++ t) - (s) + foldr (\ j t -> "\t" ++ show (m!(i,j)) ++ t) + (s) [c .. c']) - "" [r .. r'] + "" [r .. r'] -- solving the constraints ------------------------------------------- @@ -249,15 +249,15 @@ -- sizeRigid r n returns the size expression corresponding to r + n sizeRigid :: Rigid -> Int -> SizeExpr sizeRigid (RConst k) n = SizeConst (inc k n) -sizeRigid (RVar i) n = SizeVar i n +sizeRigid (RVar i) n = SizeVar i n {- apply :: SizeExpr -> Solution -> SizeExpr apply e@(SizeExpr (Rigid _) _) phi = e apply e@(SizeExpr (Flex x) i) phi = case Map.lookup x phi of Nothing -> e - Just (SizeExpr v j) -> SizeExpr v (i + j) - + Just (SizeExpr v j) -> SizeExpr v (i + j) + after :: Solution -> Solution -> Solution after psi phi = Map.map (\ e -> e `apply` phi) psi -} @@ -304,12 +304,12 @@ -} solve :: Constraints -> Maybe Solution -solve cs = -- trace (show cs) $ - -- trace (show lm0) $ +solve cs = -- trace (show cs) $ + -- trace (show lm0) $ -- trace (show lm) $ -- trace (show d) $ let solution = if solvable then loop1 flexs rigids emptySolution else Nothing - in -- trace (show solution) $ + in -- trace (show solution) $ solution where -- compute the graph and its transitive closure m gr = buildGraph cs @@ -323,7 +323,7 @@ lm = LegendMatrix m legend legend -- trace only -- compute the sets of flexible and rigid node numbers - ns = Map.keys (nodeMap gr) + ns = Map.keys (nodeMap gr) -- a set of flexible variables flexs = foldl (\ l k -> case k of (Flex i) -> i : l (Rigid _) -> l) [] ns @@ -337,21 +337,21 @@ -- check whether there is a solution -- d = [ m!(i,i) | i <- [0 .. (n-1)] ] -- diagonal --- a rigid variable might not be less than it self, so no -.. on the +-- a rigid variable might not be less than it self, so no -.. on the -- rigid part of the diagonal solvable = all (\ x -> x >= Finite 0) [ m!(i,i) | i <- rInds ] && -- a rigid variable might not be bounded below by infinity or -- bounded above by a constant -- it might not be related to another rigid variable - all (\ (r, r') -> r == r' || + all (\ (r, r') -> r == r' || let Just row = (Map.lookup (Rigid r) (nodeMap gr)) Just col = (Map.lookup (Rigid r') (nodeMap gr)) edge = m!(row,col) - in isBelow r edge r' ) + in isBelow r edge r' ) [ (r,r') | r <- rigids, r' <- rigids ] && -- a flexible variable might not be strictly below a rigid variable - all (\ (x, v) -> + all (\ (x, v) -> let Just row = (Map.lookup (Flex x) (nodeMap gr)) Just col = (Map.lookup (Rigid (RVar v)) (nodeMap gr)) edge = m!(row,col) @@ -375,41 +375,41 @@ loop1 :: [FlexId] -> [Rigid] -> Solution -> Maybe Solution loop1 [] rgds subst = Just subst loop1 flxs [] subst = loop2 flxs subst - loop1 flxs (r:rgds) subst = + loop1 flxs (r:rgds) subst = let row = fromJust $ Map.lookup (Rigid r) (nodeMap gr) (flxs',subst') = - foldl (\ (flx,sub) f -> + foldl (\ (flx,sub) f -> let col = fromJust $ Map.lookup (Flex f) (nodeMap gr) in case (inScope f r, m!(row,col)) of --- Finite z | z <= 0 -> - (True, Finite z) -> +-- Finite z | z <= 0 -> + (True, Finite z) -> let trunc z | z >= 0 = 0 | otherwise = -z in (flx, extendSolution sub f (sizeRigid r (trunc z))) _ -> (f : flx, sub) - ) ([], subst) flxs + ) ([], subst) flxs in loop1 flxs' rgds subst' {- loop2 while flexible variables j left search the row j for entry i - if j --n--> i with n >= 0 (meaning j <= i + n) then j = i + if j --n--> i with n >= 0 (meaning j <= i + n) then j = i -} loop2 :: [FlexId] -> Solution -> Maybe Solution - loop2 [] subst = Just subst + loop2 [] subst = Just subst loop2 (f:flxs) subst = loop3 0 subst where row = fromJust $ Map.lookup (Flex f) (nodeMap gr) - loop3 col subst | col >= n = + loop3 col subst | col >= n = -- default to infinity - loop2 flxs (extendSolution subst f (SizeConst Infinite)) + loop2 flxs (extendSolution subst f (SizeConst Infinite)) loop3 col subst = case Map.lookup col (intMap gr) of - Just (Rigid r) | not (infinite r) -> + Just (Rigid r) | not (infinite r) -> case (inScope f r, m!(row,col)) of - (True, Finite z) | z >= 0 -> - loop2 flxs (extendSolution subst f (sizeRigid r z)) + (True, Finite z) | z >= 0 -> + loop2 flxs (extendSolution subst f (sizeRigid r z)) (_, Infinite) -> loop3 (col+1) subst _ -> -- trace ("unusable rigid: " ++ show r ++ " for flex " ++ show f) Nothing -- NOT: loop3 (col+1) subst