Agda 2.2.0 → 2.2.2
raw patch · 75 files changed
+3382/−527 lines, 75 filesdep ~binarynew-component:exe:agda-mode
Dependency ranges changed: binary
Files
- Agda.cabal +36/−12
- README +216/−200
- src/agda-mode/Main.hs +190/−0
- src/data/emacs-mode/agda-input.el +817/−0
- src/data/emacs-mode/agda2-abbrevs.el +105/−0
- src/data/emacs-mode/agda2-highlight.el +314/−0
- src/data/emacs-mode/agda2-mode.el +1004/−0
- src/data/emacs-mode/agda2.el +13/−0
- src/data/emacs-mode/annotation.el +182/−0
- src/data/emacs-mode/eri.el +186/−0
- src/full/Agda/Compiler/Agate/Classify.hs +4/−4
- src/full/Agda/Compiler/Agate/OptimizedPrinter.hs +5/−5
- src/full/Agda/Compiler/Agate/TranslateName.hs +1/−1
- src/full/Agda/Compiler/Agate/UntypedPrinter.hs +1/−1
- src/full/Agda/Compiler/Alonzo/Haskell.hs +3/−3
- src/full/Agda/Compiler/Alonzo/Main.hs +24/−24
- src/full/Agda/Compiler/Alonzo/Names.hs +1/−1
- src/full/Agda/Compiler/Alonzo/PatternMonad.hs +4/−4
- src/full/Agda/Compiler/MAlonzo/Compiler.hs +4/−4
- src/full/Agda/Compiler/MAlonzo/Misc.hs +3/−3
- src/full/Agda/Compiler/MAlonzo/Primitives.hs +5/−5
- src/full/Agda/Interaction/BasicOps.hs +42/−42
- src/full/Agda/Interaction/CommandLine/CommandLine.hs +11/−11
- src/full/Agda/Interaction/Highlighting/HTML.hs +4/−4
- src/full/Agda/Interaction/Highlighting/Precise.hs +2/−2
- src/full/Agda/Interaction/Imports.hs +1/−1
- src/full/Agda/Interaction/Monad.hs +2/−2
- src/full/Agda/Interaction/Options.hs +13/−7
- src/full/Agda/Main.hs +4/−3
- src/full/Agda/Syntax/Concrete/Definitions.hs +2/−2
- src/full/Agda/Syntax/Concrete/Operators/Parser.hs +1/−1
- src/full/Agda/Syntax/Concrete/Pretty.hs +2/−2
- src/full/Agda/Syntax/Info.hs +1/−1
- src/full/Agda/Syntax/Internal.hs +7/−7
- src/full/Agda/Syntax/Parser/Monad.hs +1/−1
- src/full/Agda/Syntax/Parser/StringLiterals.hs +1/−1
- src/full/Agda/Syntax/Scope/Base.hs +1/−1
- src/full/Agda/Syntax/Translation/AbstractToConcrete.hs +2/−2
- src/full/Agda/Syntax/Translation/ConcreteToAbstract.hs +2/−2
- src/full/Agda/Syntax/Translation/InternalToAbstract.hs +1/−1
- src/full/Agda/Termination/CallGraph.hs +6/−6
- src/full/Agda/Termination/Matrix.hs +3/−3
- src/full/Agda/Termination/TermCheck.hs +16/−16
- src/full/Agda/Termination/Termination.hs +24/−24
- src/full/Agda/TypeChecking/Conversion.hs +1/−1
- src/full/Agda/TypeChecking/Coverage.hs +2/−2
- src/full/Agda/TypeChecking/Errors.hs +3/−5
- src/full/Agda/TypeChecking/Free.hs +1/−1
- src/full/Agda/TypeChecking/MetaVars.hs +2/−2
- src/full/Agda/TypeChecking/Monad/Base.hs +4/−5
- src/full/Agda/TypeChecking/Monad/Builtin.hs +1/−1
- src/full/Agda/TypeChecking/Monad/Closure.hs +1/−1
- src/full/Agda/TypeChecking/Monad/Env.hs +1/−1
- src/full/Agda/TypeChecking/Monad/MetaVars.hs +4/−4
- src/full/Agda/TypeChecking/Monad/Signature.hs +2/−2
- src/full/Agda/TypeChecking/Polarity.hs +1/−1
- src/full/Agda/TypeChecking/Positivity.hs +1/−1
- src/full/Agda/TypeChecking/Primitive.hs +1/−1
- src/full/Agda/TypeChecking/Reduce.hs +2/−2
- src/full/Agda/TypeChecking/Rules/Data.hs +1/−1
- src/full/Agda/TypeChecking/Rules/Def.hs +1/−1
- src/full/Agda/TypeChecking/Rules/LHS.hs +2/−2
- src/full/Agda/TypeChecking/Rules/LHS/Instantiate.hs +6/−6
- src/full/Agda/TypeChecking/Rules/Record.hs +2/−2
- src/full/Agda/TypeChecking/Serialise.hs +5/−5
- src/full/Agda/TypeChecking/SizedTypes.hs +4/−4
- src/full/Agda/TypeChecking/Substitute.hs +3/−3
- src/full/Agda/TypeChecking/Telescope.hs +1/−1
- src/full/Agda/TypeChecking/Test/Generators.hs +5/−5
- src/full/Agda/TypeChecking/With.hs +2/−2
- src/full/Agda/Utils/List.hs +1/−1
- src/full/Agda/Utils/ReadP.hs +8/−8
- src/full/Agda/Utils/Serialise.hs +1/−1
- src/full/Agda/Utils/Trie.hs +3/−3
- src/full/Agda/Utils/Warshall.hs +43/−43
Agda.cabal view
@@ -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
README view
@@ -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=<installation location>+ 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=<installation location> - cabal install --prefix=<the install path>+ (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- <agda-mode-dir>. 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 <agda-mode-dir>- cp src/emacs-mode/*.el <agda-mode-dir>+ 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 "<agda-mode-dir>")- (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
+ src/agda-mode/Main.hs view
@@ -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
+ src/data/emacs-mode/agda-input.el view
@@ -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" . ("⋦")) (">~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
+ src/data/emacs-mode/agda2-abbrevs.el view
@@ -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
+ src/data/emacs-mode/agda2-highlight.el view
@@ -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
+ src/data/emacs-mode/agda2-mode.el view
@@ -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<sexp>' 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 <clause> = {!<var>!} 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 <P>{!...!}<Q>. 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
+ src/data/emacs-mode/agda2.el view
@@ -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)
+ src/data/emacs-mode/annotation.el view
@@ -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
+ src/data/emacs-mode/eri.el view
@@ -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
src/full/Agda/Compiler/Agate/Classify.hs view
@@ -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 --- +
src/full/Agda/Compiler/Agate/OptimizedPrinter.hs view
@@ -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
src/full/Agda/Compiler/Agate/TranslateName.hs view
@@ -50,4 +50,4 @@ :intToDigit (ord c `mod` 16):escape s ----------------------------------------------------------------- +
src/full/Agda/Compiler/Agate/UntypedPrinter.hs view
@@ -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
src/full/Agda/Compiler/Alonzo/Haskell.hs view
@@ -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
src/full/Agda/Compiler/Alonzo/Main.hs view
@@ -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'
src/full/Agda/Compiler/Alonzo/Names.hs view
@@ -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)
src/full/Agda/Compiler/Alonzo/PatternMonad.hs view
@@ -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]
src/full/Agda/Compiler/MAlonzo/Compiler.hs view
@@ -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
src/full/Agda/Compiler/MAlonzo/Misc.hs view
@@ -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
src/full/Agda/Compiler/MAlonzo/Primitives.hs view
@@ -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
src/full/Agda/Interaction/BasicOps.hs view
@@ -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
src/full/Agda/Interaction/CommandLine/CommandLine.hs view
@@ -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
src/full/Agda/Interaction/Highlighting/HTML.hs view
@@ -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
src/full/Agda/Interaction/Highlighting/Precise.hs view
@@ -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.
src/full/Agda/Interaction/Imports.hs view
@@ -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
src/full/Agda/Interaction/Monad.hs view
@@ -30,8 +30,8 @@ instance MonadUndo [CurrentPoint] IM where- undo = - + undo =+ run
src/full/Agda/Interaction/Options.hs view
@@ -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:" ++
src/full/Agda/Main.hs view
@@ -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)
src/full/Agda/Syntax/Concrete/Definitions.hs view
@@ -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]
src/full/Agda/Syntax/Concrete/Operators/Parser.hs view
@@ -101,7 +101,7 @@ return $ f e where restP = return id +++ do- f <- binop op + f <- binop op e <- p return $ flip f e
src/full/Agda/Syntax/Concrete/Pretty.hs view
@@ -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
src/full/Agda/Syntax/Info.hs view
@@ -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
src/full/Agda/Syntax/Internal.hs view
@@ -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
src/full/Agda/Syntax/Parser/Monad.hs view
@@ -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 = "..."
src/full/Agda/Syntax/Parser/StringLiterals.hs view
@@ -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"
src/full/Agda/Syntax/Scope/Base.hs view
@@ -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
src/full/Agda/Syntax/Translation/AbstractToConcrete.hs view
@@ -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
src/full/Agda/Syntax/Translation/ConcreteToAbstract.hs view
@@ -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
src/full/Agda/Syntax/Translation/InternalToAbstract.hs view
@@ -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
src/full/Agda/Termination/CallGraph.hs view
@@ -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 =
src/full/Agda/Termination/Matrix.hs view
@@ -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)
src/full/Agda/Termination/TermCheck.hs view
@@ -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
src/full/Agda/Termination/Termination.hs view
@@ -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
src/full/Agda/TypeChecking/Conversion.hs view
@@ -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
src/full/Agda/TypeChecking/Coverage.hs view
@@ -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
src/full/Agda/TypeChecking/Errors.hs view
@@ -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
src/full/Agda/TypeChecking/Free.hs view
@@ -1,7 +1,7 @@ {-# LANGUAGE CPP #-} -- | Computing the free variables of a term.-module Agda.TypeChecking.Free +module Agda.TypeChecking.Free ( FreeVars(..) , Free(..) , allVars
src/full/Agda/TypeChecking/MetaVars.hs view
@@ -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
src/full/Agda/TypeChecking/Monad/Base.hs view
@@ -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
src/full/Agda/TypeChecking/Monad/Builtin.hs view
@@ -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 }
src/full/Agda/TypeChecking/Monad/Closure.hs view
@@ -13,5 +13,5 @@ $ withEnv env $ withTrace trace $ k x- +
src/full/Agda/TypeChecking/Monad/Env.hs view
@@ -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
src/full/Agda/TypeChecking/Monad/MetaVars.hs view
@@ -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
src/full/Agda/TypeChecking/Monad/Signature.hs view
@@ -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)
src/full/Agda/TypeChecking/Polarity.hs view
@@ -90,7 +90,7 @@ isLin <- checkSizeIndex np sizeArg target return $ isPos && isLin- + ifM (and <$> mapM check cons) (return [Covariant]) (return [Invariant])
src/full/Agda/TypeChecking/Positivity.hs view
@@ -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
src/full/Agda/TypeChecking/Primitive.hs view
@@ -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
src/full/Agda/TypeChecking/Reduce.hs view
@@ -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
src/full/Agda/TypeChecking/Rules/Data.hs view
@@ -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
src/full/Agda/TypeChecking/Rules/Def.hs view
@@ -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 ->
src/full/Agda/TypeChecking/Rules/LHS.hs view
@@ -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
src/full/Agda/TypeChecking/Rules/LHS/Instantiate.hs view
@@ -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
src/full/Agda/TypeChecking/Rules/Record.hs view
@@ -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
src/full/Agda/TypeChecking/Serialise.hs view
@@ -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)
src/full/Agda/TypeChecking/SizedTypes.hs view
@@ -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
src/full/Agda/TypeChecking/Substitute.hs view
@@ -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
src/full/Agda/TypeChecking/Telescope.hs view
@@ -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.
src/full/Agda/TypeChecking/Test/Generators.hs view
@@ -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)
src/full/Agda/TypeChecking/With.hs view
@@ -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
src/full/Agda/Utils/List.hs view
@@ -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.
src/full/Agda/Utils/ReadP.hs view
@@ -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
src/full/Agda/Utils/Serialise.hs view
@@ -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)
src/full/Agda/Utils/Trie.hs view
@@ -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
src/full/Agda/Utils/Warshall.hs view
@@ -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