;;; GNU Guix --- Functional package management for GNU
;;; Copyright © 2015 Paul van der Walt <paul@denknerd.org>
;;; Copyright © 2016, 2017 David Craven <david@craven.ch>
;;; Copyright © 2018 Alex ter Weele <alex.ter.weele@gmail.com>
;;; Copyright © 2019, 2021, 2022 Eric Bavier <bavier@posteo.net>
;;; Copyright © 2022 Attila Lendvai <attila@lendvai.name>
;;;
;;; This file is part of GNU Guix.
;;;
;;; GNU Guix is free software; you can redistribute it and/or modify it
;;; under the terms of the GNU General Public License as published by
;;; the Free Software Foundation; either version 3 of the License, or (at
;;; your option) any later version.
;;;
;;; GNU Guix is distributed in the hope that it will be useful, but
;;; WITHOUT ANY WARRANTY; without even the implied warranty of
;;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
;;; GNU General Public License for more details.
;;;
;;; You should have received a copy of the GNU General Public License
;;; along with GNU Guix.  If not, see <http://www.gnu.org/licenses/>.

(define-module (gnu packages idris)
  #:use-module (gnu packages)
  #:use-module (gnu packages haskell-check)
  #:use-module (gnu packages haskell-web)
  #:use-module (gnu packages haskell-xyz)
  #:use-module (gnu packages libffi)
  #:use-module (gnu packages multiprecision)
  #:use-module (gnu packages ncurses)
  #:use-module (gnu packages perl)
  #:use-module (guix build-system gnu)
  #:use-module (guix build-system haskell)
  #:use-module (guix download)
  #:use-module (guix git-download)
  #:use-module (guix utils)
  #:use-module ((guix licenses) #:prefix license:)
  #:use-module (guix packages))

(define-public idris
  (package
    (name "idris")
    (version "1.3.4")
    (source (origin
              (method git-fetch)
              (uri (git-reference
                    (url "https://github.com/idris-lang/Idris-dev.git")
                    (commit (string-append "v" version))))
              (file-name (git-file-name name version))
              (sha256
               (base32
                "0cd2a92323hb9a6wy8sc0cqwnisf4pv8y9y2rxvxcbyv8cs1q8g2"))
              (patches (search-patches "idris-test-ffi008.patch"))))
    (build-system haskell-build-system)
    (native-inputs                      ;For tests
     (list perl ghc-cheapskate ghc-tasty ghc-tasty-golden
           ghc-tasty-rerun))
    (inputs
     (list gmp
           ncurses
           ghc-aeson
           ghc-annotated-wl-pprint
           ghc-ansi-terminal
           ghc-ansi-wl-pprint
           ghc-async
           ghc-base64-bytestring
           ghc-blaze-html
           ghc-blaze-markup
           ghc-cheapskate
           ghc-code-page
           ghc-fingertree
           ghc-fsnotify
           ghc-ieee754
           ghc-libffi
           ghc-megaparsec
           ghc-network
           ghc-optparse-applicative
           ghc-regex-tdfa
           ghc-safe
           ghc-split
           ghc-terminal-size
           ghc-uniplate
           ghc-unordered-containers
           ghc-utf8-string
           ghc-vector
           ghc-vector-binary-instances
           ghc-zip-archive))
    (arguments
     `(#:configure-flags
       (list (string-append "--datasubdir="
                            (assoc-ref %outputs "out") "/lib/idris")
             "-fFFI" "-fGMP")
       #:phases
       (modify-phases %standard-phases
         ;; This allows us to call the 'idris' binary before installing.
         (add-after 'unpack 'set-ld-library-path
           (lambda _
             (setenv "LD_LIBRARY_PATH" (string-append (getcwd) "/dist/build"))))
         (add-before 'configure 'update-constraints
           (lambda _
             (substitute* "idris.cabal"
               (("(aeson|ansi-terminal|bytestring|haskeline|libffi|megaparsec|network|optparse-applicative)\\s+[<>=0-9. &|]+" all dep)
                dep))))
         (add-before 'configure 'set-cc-command
           (lambda _
             (setenv "CC" ,(cc-for-target))))
         (a<tr><td><span title='2016-03-08 11:38:46 +0100'>2016-03-08</span></td><td><a href='/guix/commit/tests/guix-build.sh?id=95cd4971d07fe312a4e0d21b72e7bf1bba493753'>packages: Support the deprecated "NAME-VERSION" syntax.</a><span class='msg-avail'>...<span class='msg-tooltip'>Fixes a typo introduced in 1b846da8c372bee78851439fd9e72b2499115e5a that
would lead to a backtrace when using the deprecated syntax.

* gnu/packages.scm (%find-package): Turn the first argument to
'call-with-values' into a thunk.  Use #:select instead of '@' to select
the right 'package-name-&gt;name+version' procedure.
</span></span></td><td>Ludovic Courtès</td></tr>
<tr><td><span title='2016-03-03 00:18:30 +0100'>2016-03-03</span></td><td><a href='/guix/commit/tests/guix-build.sh?id=94d609aba8e14963459c21863ab56da2b5f01517'>guix build: -S returns the replacement's source.</a><span class='msg-avail'>...<span class='msg-tooltip'>Reported by Mark H Weaver.

* guix/scripts/build.scm (options-&gt;derivations): When SRC and GRAFT? are
true, use the source of P's replacement.
* tests/guix-build.sh: Add test.
</span></span></td><td>Ludovic Courtès</td></tr>
<tr><td><span title='2016-03-02 21:41:41 +0100'>2016-03-02</span></td><td><a href='/guix/commit/tests/guix-build.sh?id=1b846da8c372bee78851439fd9e72b2499115e5a'>utils: Use '@' for separating package names and version numbers.</a><span class='msg-avail'>...<span class='msg-tooltip'>This provides the ability to use numbers in package names.

Fixes &lt;http://bugs.gnu.org/19219&gt;.

* guix/utils.scm (package-name-&gt;name+version): New procedure.
* gnu/packages.scm (%find-package): Add a FALLBACK? keyword argument.
Use the previous method when no package is found.
(specification-&gt;package+output, specification-&gt;package): Adapt
documentation to new syntax.
* doc/guix.texi (Invoking guix package, Invoking guix import): Likewise.
* guix/ui.scm (package-specification-&gt;name+version+output): Likewise.
* guix/scripts/import/hackage.scm (show-help): Likewise.
* tests/guix-build.sh: Adapt to new syntax.
* tests/guix-lint.sh: Likewise.
* tests/guix-package.sh: Likewise.
* tests/ui.scm ("package-specification-&gt;name+version+output"): Likewise.
* tests/utils.scm ("package-name-&gt;name+version"): Likewise.
* NEWS: Mention new syntax.
</span></span></td><td>Mathieu Lirzin</td></tr>
<tr><td><span title='2016-03-02 14:47:07 +0100'>2016-03-02</span></td><td><a href='/guix/commit/tests/guix-build.sh?id=442a6ff5eae094f1fd4e09241a2f35c33ab908da'>tests: Disable grafts by default.</a><span class='msg-avail'>...<span class='msg-tooltip'>Fixes &lt;http://bugs.gnu.org/22872&gt;.
Reported by myglc2 &lt;myglc2@gmail.com&gt;.

* test-env.in: Define and export 'GUIX_BUILD_OPTIONS'.
* tests/guix-build.sh: When setting 'GUIX_BUILD_OPTIONS', make sure it
contains '--no-grafts'.
* tests/guix-package.sh: Likewise.
* tests/guix-daemon.sh: Add (%graft? #f) in Scheme snippets.
</span></span></td><td>Ludovic Courtès</td></tr>
<tr><td><span title='2016-02-01 08:59:13 +0100'>2016-02-01</span></td><td><a href='/guix/commit/tests/guix-build.sh?id=47c0f92c37dc7d50d9d4598ce5b91c4cdfec6ed1'>guix build: Add '--with-input'.</a><span class='msg-avail'>...<span class='msg-tooltip'>* guix/scripts/build.scm (transform-package-inputs): New procedure.
(%transformations): Add it.
(%transformation-options, show-transformation-options-help): Add
--with-input.
* tests/scripts-build.scm ("options-&gt;transformation, with-input"):
("options-&gt;transformation, with-input, no matches"): New tests.
* tests/guix-build.sh: Add tests.
* doc/guix.texi (Package Transformation Options): Document it.
</span></span></td><td>Ludovic Courtès</td></tr>
"--build" ipkg
                                     ;; only trigger a build, as --ibcsubdir
                                     ;; already installs .ibc files.

                                     (apply append (map (lambda (path)
                                                          (list "--idrispath"
                                                                path))
                                                        idris-path-subdirs)))))
            ;; FIXME: Seems to be a bug in idris that causes a dubious failure.
            (apply system* install-cmd)))))))

(define-public idris-lightyear
  (let ((commit "6d65ad111b4bed2bc131396f8385528fc6b3678a"))
    (package
      (name "idris-lightyear")
      (version (git-version "0.1" "1" commit))
      (source (origin
                (method git-fetch)
                (uri (git-reference
                      (url "https://github.com/ziman/lightyear")
                      (commit commit)))
                (file-name (git-file-name name version))
                (sha256
                 (base32
                  "1pkxnn3ryr0v0cin4nasw7kgkc9dnnpja1nfbj466mf3qv5s98af"))))
      (build-system gnu-build-system)
      (native-inputs
       (list idris))
      (arguments (idris-default-arguments name))
      (home-page "https://github.com/ziman/lightyear")
      (synopsis "Lightweight parser combinator library for Idris")
      (description "Lightweight parser combinator library for Idris, inspired
by Parsec.  This package is used (almost) the same way as Parsec, except for one
difference: backtracking.")
      (license license:bsd-2))))

(define-public idris-wl-pprint
  (let ((commit "1d365fcf4ba075859844dbc5eb96a90f57b9f338"))
    (package
      (name "idris-wl-pprint")
      (version (git-version "0.1" "1" commit))
      (source (origin
                (method git-fetch)
                (uri (git-reference
                      (url "https://github.com/shayan-najd/wl-pprint")
                      (commit commit)))
                (file-name (git-file-name name version))
                (sha256
                 (base32
                  "0g7c3y9smifdz4sivi3qmvymhdr7v9kfq45fmfmmvkqcrix0spzn"))))
      (build-system gnu-build-system)
      (native-inputs
       (list idris))
      (arguments (idris-default-arguments name))
      (home-page "https://github.com/shayan-najd/wl-pprint")
      (synopsis "Pretty printing library")
      (description "A pretty printing library for Idris based on Phil Wadler's
paper A Prettier Printer and on Daan Leijen's extensions in the Haskell
wl-pprint library.")
      (license license:bsd-2))))

(define-public idris-bifunctors
  (let ((commit "53d06a6ccfe70c49c9ae8c8a4135981dd2173202"))
    (package
      (name "idris-bifunctors")
      (version (git-version "0.1" "1" commit))
      (source (origin
                (method git-fetch)
                (uri (git-reference
                      (url "https://github.com/HuwCampbell/Idris-Bifunctors")
                      (commit commit)))
                (file-name (string-append name "-" version "-checkout"))
                (sha256
                 (base32
                  "02vbsd3rmgnj0l1qq787709qcxjbr9890cbad4ykn27f77jk81h4"))))
      (build-system gnu-build-system)
      (native-inputs
       (list idris))
      (arguments (idris-default-arguments name))
      (home-page "https://github.com/HuwCampbell/Idris-Bifunctors")
      (synopsis "Bifunctor library")
      (description "This is a bifunctor library for Idris based off the
excellent Haskell Bifunctors package from Edward Kmett.")
      (license license:bsd-3))))

(define-public idris-lens
  (let ((commit "26f012005f6849806cea630afe317e42cae97f29"))
    (package
      (name "idris-lens")
      (version (git-version "0.1" "1" commit))
      (source (origin
                (method git-fetch)
                (uri (git-reference
                      (url "https://github.com/HuwCampbell/idris-lens")
                      (commit commit)))
                (file-name (git-file-name name version))
                (sha256
                 (base32
                  "06jzfj6rad08rk92w8jk5byi79svmyg0mrcqhibgx8rkjjy6vmai"))))
      (build-system gnu-build-system)
      (native-inputs
       (list idris))
      (propagated-inputs
       (list idris-bifunctors))
      (arguments (idris-default-arguments name))
      (home-page "https://github.com/HuwCampbell/idris-lens")
      (synopsis "Van Laarhoven lenses for Idris")
      (description "Lenses are composable functional references.  They allow
accessing and modifying data within a structure.")
      (license license:bsd-3))))