;;; 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 Eric Bavier <bavier@posteo.net>
;;;
;;; 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/>.

;;; TODO
;;;
;;;  - Idris has multiple backends, but we only register Chez as an
;;;  input. Decide how to make backends optional, and/or which ones to package
;;;  by default.
;;;
;;;  - Set RUNPATH instead of using LD_LIBRARY_PATH. See
;;;  http://blog.tremily.us/posts/rpath/ This needs patching Idris so that it
;;;  stops using a wrapper script and finds its libidris_support.so
;;;  e.g. relative to the executable.

(define-module (gnu packages idris)
  #:use-module (gnu packages)
  #:use-module (gnu packages base)
  #:use-module (gnu packages bash)
  #:use-module (gnu packages chez)
  #: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 llvm)
  #:use-module (gnu packages multiprecision)
  #:use-module (gnu packages ncurses)
  #:use-module (gnu packages node)
  #:use-module (gnu packages perl)
  #:use-module (gnu packages racket)
  #:use-module (gnu packages version-control)
  #:use-module (guix build-system gnu)
  #:use-module (guix build-system haskell)
  #:use-module (guix download)
  #:use-module (guix git)
  #:use-module (guix git-download)
  #:use-module ((guix licenses) #:prefix license:)
  #:use-module (guix packages)
  #:use-module (guix utils)
  #:use-module (ice-9 match)
  #:use-module (ice-9 regex)
  #:export (make-idris-package))

(define-public idris-1.3.3
  (package
    (name "idris")
    (version "1.3.3")
    (source (origin
              (method url-fetch)
              (uri (string-append
                    "https://hackage.haskell.org/package/"
                    "idris-" version "/idris-" version ".tar.gz"))
              (sha256
               (base32
                "1pachwc6msw3n1mz2z1r1w6h518w9gbhdvbaa5vi1qp3cn3wm6q4"))
              (patches (search-patches "idris-disable-test.patch"))))
    (build-system haskell-build-system)
    (native-inputs                      ;For tests
     `(("perl" ,perl)
       ("clang" ,clang)                 ; the tests want to generate exeutables
       ("ghc-cheapskate" ,ghc-cheapskate)
       ("ghc-tasty" ,ghc-tasty)
       ("ghc-tasty-golden" ,ghc-tasty-golden)
       ("ghc-tasty-rerun" ,ghc-tasty-rerun)))
    (inputs
     `(("bash" ,bash-minimal)
       ("clang" ,clang) ; FIXME clang compiles faster than gcc, but (cc-for-target) ignores it
       ("gmp" ,gmp)
       ("ncurses" ,ncurses)
       ("ghc-aeson" ,ghc-aeson)
       ("ghc-annotated-wl-pprint" ,ghc-annotated-wl-pprint)
       ("ghc-ansi-terminal" ,ghc-ansi-terminal)
       ("ghc-ansi-wl-pprint" ,ghc-ansi-wl-pprint)
       ("ghc-async" ,ghc-async)
       ("ghc-base64-bytestring" ,ghc-base64-bytestring)
       ("ghc-blaze-html" ,ghc-blaze-html)
       ("ghc-blaze-markup" ,ghc-blaze-markup)
       ("ghc-cheapskate" ,ghc-cheapskate)
       ("ghc-code-page" ,ghc-code-page)
       ("ghc-fingertree" ,ghc-fingertree)
       ("ghc-fsnotify" ,ghc-fsnotify)
       ("ghc-ieee754" ,ghc-ieee754)
       ("ghc-libffi" ,ghc-libffi)
       ("ghc-megaparsec" ,ghc-megaparsec)
       ("ghc-network" ,ghc-network)
       ("ghc-optparse-applicative" ,ghc-optparse-applicative)
       ("ghc-regex-tdfa" ,ghc-regex-tdfa)
       ("ghc-safe" ,ghc-safe)
       ("ghc-split" ,ghc-split)
       ("ghc-terminal-size" ,ghc-terminal-size)
       ("ghc-uniplate" ,ghc-uniplate)
       ("ghc-unordered-containers" ,ghc-unordered-containers)
       ("ghc-utf8-string" ,ghc-utf8-string)
       ("ghc-vector" ,ghc-vector)
       ("ghc-vector-binary-instances" ,ghc-vector-binary-instances)
       ("ghc-zip-archive" ,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"))
             #t))
         (add-after 'unpack 'update-constraints
           (lambda _
             (substitute* "idris.cabal"
               ;; This is only needed for v1.3.3, later it got relaxed upstream
               (("ansi-terminal < 0\\.9") "ansi-terminal < 0.10"))
             #t))
         (add-before 'configure 'set-cc-command
           (lambda _
             (setenv "CC" ,(cc-for-target))
             #t))
         (add-after 'install 'fix-libs-install-location
           (lambda* (#:key outputs #:allow-other-keys)
             (let* ((out (assoc-ref outputs "out"))
                    (lib (string-append out "/lib/idris"))
                    (modules (string-append lib "/libs")))
               (for-each
                (lambda (module)
                  (symlink (string-append modules "/" module)
                           (string-append lib "/" module)))
                '("prelude" "base" "contrib" "effects" "pruviloj")))
             #t))
         (delete 'check)                ;Run check later
         (add-after 'install 'check
           (lambda* (#:key outputs #:allow-other-keys #:rest args)
             (let ((out (assoc-ref outputs "out")))
               (chmod "test/scripts/timeout" #o755) ;must be executable
               (setenv "TASTY_NUM_THREADS" (number->string (parallel-job-count)))
               (setenv "PATH" (string-append out "/bin:" (getenv "PATH")))
               (apply (assoc-ref %standard-phases 'check) args))))
         (add-before 'check 'restore-libidris_rts
           (lambda* (#:key outputs #:allow-other-keys)
             ;; The Haskell build system moves this library to the
             ;; "static" output.  Idris only knows how to find it in the
             ;; "out" output, so we restore it here.
             (let ((out (assoc-ref outputs "out"))
                   (static (assoc-ref outputs "static"))
                   (filename "/lib/idris/rts/libidris_rts.a"))
               (rename-file (string-append static filename)
                            (string-append out filename)))
              #t))
         (add-before 'check 'wrap-program
           (lambda* (#:key outputs inputs #:allow-other-keys)
             (let* ((out (assoc-ref outputs "out"))
                    (exe (string-append out "/bin/idris")))
               (wrap-program exe
                 `("IDRIS_CC" = (,',(cc-for-target))))
               (with-directory-excursion (string-append out "/bin/")
                 (symlink ,name (string-append ,name "-" ,version))))
             #t)))))
    (native-search-paths
     (list (search-path-specification
            (variable "IDRIS_LIBRARY_PATH")
            (files '("lib/idris")))))
    (home-page "https://www.idris-lang.org")
    (synopsis "General purpose language with full dependent types")
    (description "Idris is a general purpose language with full dependent
types.  It is compiled, with eager evaluation.  Dependent types allow types to
be predicated on values, meaning that some aspects of a program's behaviour
can be specified precisely in the type.  The language is closely related to
Epigram and Agda.")
    (license license:bsd-3)))

(define-public idris idris-1.3.3)

(define-public idris-1.3.3-1
  ;; This is the current latest from the v1.x branch.
  (let ((commit "55459867fc3f1ac34527a5dd998c37e72b15d488")
        (revision "1"))
    (package
      (inherit idris-1.3.3)
      (version (git-version "1.3.3" revision commit))
      (source (origin
                (method git-fetch)
                (uri (git-reference
                      (url "https://github.com/attila-lendvai/Idris2")
                      (commit commit)))
                (sha256
                 (base32
                  "0qsn1953jy74pgppwkax8yrlswb3v46x541ahbl95rshf666nsj6"))
                (file-name (git-file-name "idris" version))))
      (inputs
       (append (package-inputs idris-1.3.3)
               `(("ghc-haskeline-0.8" ,ghc-haskeline-0.8)))))))

(define* (make-idris-package source version
                             #:key bootstrap-idris
                             (ignore-test-failures? #false)
                             (unwrap? #true)
                             (tests? #true)
                             (files-to-patch-for-shell
                              '("src/Compiler/Scheme/Chez.idr"
                                "src/Compiler/Scheme/Racket.idr"
                                "src/Compiler/Scheme/Gambit.idr"
                                "src/Compiler/ES/Node.idr"
                                "bootstrap/idris2_app/idris2.rkt"
                                "bootstrap/idris2_app/idris2.ss"))
                             (with-bootstrap-shortcut? #true))
  (package
    (name "idris2")
    (version version)
    (source (match source
              ((commit hash . url)
               (origin
                 (method git-fetch)
                 (uri (git-reference
                       (url (if (null? url)
                                "https://github.com/idris-lang/Idris2.git"
                                (car url)))
                       (commit commit)))
                 (sha256 (base32 hash))
                 (file-name (git-file-name name version))))
              ((? git-checkout?)
               source)))
    (build-system gnu-build-system)
    (native-inputs
     `(,@(if with-bootstrap-shortcut?
             `(("chez-scheme" ,chez-scheme))
             `(("bootstrap-idris" ,bootstrap-idris)))
       ("cc" ,clang-toolchain-12) ; clang or older clang-toolchain's don't have a bin/cc
       ("coreutils" ,coreutils)
       ("git" ,git)
       ("node" ,node)                 ; only for the tests
       ("racket" ,racket)             ; only for the tests
       ("sed" ,sed)))
    (inputs
     `(("bash" ,bash-minimal)
       ("chez-scheme" ,chez-scheme)
       ("gmp" ,gmp)))
    (arguments
     `(#:tests? ,tests?
       #:make-flags
       (list (string-append "CC=" ,(cc-for-target))
             ,@(if with-bootstrap-shortcut?
                   '((string-append "SCHEME="
                                    (assoc-ref %build-inputs "chez-scheme")
                                    "/bin/scheme"))
                   `((string-append "BOOTSTRAP_IDRIS="
                                    (assoc-ref %build-inputs "bootstrap-idris")
                                    "/bin/" ,(package-name bootstrap-idris))))
             (string-append "PREFIX=" (assoc-ref %outputs "out"))
             "-j1")
       #:phases
       (modify-phases %standard-phases
         (delete 'bootstrap)
         (delete 'configure)
         (delete 'check)  ; check must happen after install and wrap-program
         (add-after 'unpack 'patch-paths
           (lambda* (#:key inputs #:allow-other-keys)
             (substitute* ',files-to-patch-for-shell
               ((,(regexp-quote "#!/bin/sh"))
                (string-append "#!" (assoc-ref inputs "bash") "/bin/sh"))
               (("/usr/bin/env")
                (string-append (assoc-ref inputs "coreutils") "/bin/env")))
             #true))
         ,@(if unwrap?
               `((add-after 'install 'unwrap
                   (lambda* (#:key outputs #:allow-other-keys)
                     ;; The bin/idris2 calls bin/idris2_app/idris2.so which is
                     ;; the real executable, but it sets LD_LIBRARY_PATH
                     ;; incorrectly.  Remove bin/idris2 and replace it with
                     ;; bin/idris2_app/idris2.so instead.
                     (let ((out (assoc-ref outputs "out")))
                       (delete-file (string-append out "/bin/idris2"))
                       (rename-file (string-append out "/bin/idris2_app/idris2.so")
                                    (string-append out "/bin/idris2"))
                       (delete-file-recursively (string-append out "/bin/idris2_app"))
                       (delete-file-recursively (string-append out "/lib")))
                     #true)))
               '())
         ,@(if with-bootstrap-shortcut?
               `((replace 'build
                   (lambda* (#:key make-flags #:allow-other-keys)
                     ;; i.e. do not build it using the previous version of
                     ;; Idris, but rather compile the comitted compiler
                     ;; output.
                     (apply invoke "make" "bootstrap" make-flags))))
               '())
         (add-after 'unwrap 'wrap-program
           (lambda* (#:key outputs inputs #:allow-other-keys)
             (let* ((chez (string-append (assoc-ref inputs "chez-scheme")
                                         "/bin/scheme"))
                    (out (assoc-ref outputs "out"))
                    (exe (string-append out "/bin/" ,name))
                    (version ,version))
               (wrap-program exe
                 `("IDRIS2_PREFIX" = (,out))
                 `("LD_LIBRARY_PATH" prefix (,(string-append out "/idris2-" version "/lib")))
                 `("CC" = (,',(cc-for-target)))
                 `("CHEZ" = (,chez)))
               (with-directory-excursion (string-append out "/bin/")
                 (symlink ,name (string-append ,name "-" ,version))))
             #true))
         (add-after 'wrap-program 'check
           (lambda* (#:key outputs make-flags #:allow-other-keys)
             (,(if ignore-test-failures?
                   'false-if-exception
                   'begin)
              (apply invoke "make"
                     "INTERACTIVE="
                     (string-append "IDRIS2="
                                    (assoc-ref outputs "out")
                                    "/bin/" ,name)
                     "test" make-flags))
             #true)))))
    (home-page "https://www.idris-lang.org")
    (synopsis "General purpose language with full dependent types")
    (description "Idris is a general purpose language with full dependent
types.  It is compiled, with eager evaluation.  Dependent types allow types to
be predicated on values, meaning that some aspects of a program's behaviour
can be specified precisely in the type.  The language is closely related to
Epigram and Agda.")
    (license license:bsd-3)))

(define-public idris2-0.5.1
  (make-idris-package '("v0.5.1"
                        "09k5fxnplp6fv3877ynz1lwq9zapxcxbvfvkn6g68yb0ivrff978")
                      "0.5.1"))

;; Idris modules use the gnu-build-system so that the IDRIS_LIBRARY_PATH is set.
(define (idris-default-arguments name)
  `(#:modules ((guix build gnu-build-system)
               (guix build utils)
               (ice-9 ftw)
               (ice-9 match))
    #:phases
    (modify-phases %standard-phases
      (delete 'configure)
      (delete 'build)
      (delete 'check)
      (replace 'install
        (lambda* (#:key inputs outputs #:allow-other-keys)
          (let* ((out (assoc-ref outputs "out"))
                 (idris (assoc-ref inputs "idris"))
                 (idris-bin (string-append idris "/bin/idris"))
                 (idris-libs (string-append idris "/lib/idris/libs"))
                 (module-name (and (string-prefix? "idris-" ,name)
                                   (substring ,name 6)))
                 (ibcsubdir (string-append out "/lib/idris/" module-name))
                 (ipkg (string-append module-name ".ipkg"))
                 (idris-library-path (getenv "IDRIS_LIBRARY_PATH"))
                 (idris-path (string-split idris-library-path #\:))
                 (idris-path-files (apply append
                                          (map (lambda (path)
                                                 (map (lambda (dir)
                                                        (string-append path "/" dir))
                                                      (scandir path))) idris-path)))
                 (idris-path-subdirs (filter (lambda (path)
                                               (and path (match (stat:type (stat path))
                                                           ('directory #t)
                                                           (_ #f))))
                                                    idris-path-files))
                 (install-cmd (cons* idris-bin
                                     "--ibcsubdir" ibcsubdir
                                     "--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)
            #t))))))

(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
       `(("idris" ,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
       `(("idris" ,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
       `(("idris" ,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
       `(("idris" ,idris)))
      (propagated-inputs
       `(("idris-bifunctors" ,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))))