;;; test-ob-ada-spark.el --- tests for ob-ada-spark.el  -*- lexical-binding: t; -*-

;; Copyright (c) 2024 Free Software Foundation, Inc.
;; Authors: Francesc Rocher
;; Maintainer: Francesc Rocher <francesc.rocher@gmail.com>

;; This file is part of GNU Emacs.

;; This program 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.

;; This program 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 this program.  If not, see <https://www.gnu.org/licenses/>.

;;; Code:
(require 'ob-core)
(require 'ob-ada-spark)

(org-test-for-executable "gnatmake")
(org-test-for-executable "gnatprove")

(unless (featurep 'ob-ada-spark)
  (signal 'missing-test-dependency "Support for Ada and SPARK code blocks"))

;; Simple programs

(ert-deftest ob-ada-spark/simple/hello-world ()
  "Simple program: Hello world"
  (org-test-at-id
   "778e63c2-2644-4a6f-8e7d-f956fa3d9241"
   (org-babel-next-src-block)
   (should (equal "Hello world" (org-babel-execute-src-block)))))

(ert-deftest ob-ada-spark/simple/recursive-fibonacci ()
  "Simple program: Recursive Fibonacci"
  (org-test-at-id
   "6281cb40-26cc-423e-88c8-e8f26901ee4a"
   (org-babel-next-src-block)
   (should (= 610 (org-babel-execute-src-block)))))

(ert-deftest ob-ada-spark/simple/sequential-fibonacci ()
  "Simple program: Sequential Fibonacci"
  (org-test-at-id
   "41b4514b-0d46-4011-b5fa-7997aecf75a9"
   (org-babel-next-src-block)
   (should (= 610 (org-babel-execute-src-block)))))

(ert-deftest ob-ada-spark/simple/utf8-identifiers ()
  "Simple program: UTF-8 indentifiers"
  (org-test-at-id
   "06e4dc5b-5566-486b-81af-cb7c547d46f1"
   (org-babel-next-src-block)
   (should (equal "Average: 32" (org-babel-execute-src-block)))))

(ert-deftest ob-ada-spark/simple/utf8-identifiers-error ()
  "Simple program: UTF-8 indentifiers"
  (org-test-at-id
   "06e4dc5b-5566-486b-81af-cb7c547d46f1"
   (org-babel-next-src-block 2)
   (when (should (buffer-live-p (get-buffer org-babel-error-buffer-name)))
     (kill-buffer org-babel-error-buffer-name))
   :type 'error))

;; Using templates

(ert-deftest ob-ada-spark/using-templates/main-template ()
  "Using templates: Main template"
  (org-test-at-id
   "a2a64153-a7b6-4c32-84c5-a589f0caac93"
   (org-babel-next-src-block)
   (should (equal "Hello world" (org-babel-execute-src-block)))))

(ert-deftest ob-ada-spark/using-templates/fibonacci ()
  "Using templates: Fibonacci"
  (org-test-at-id
   "cbef4ee3-63e3-4295-8b26-e2470e30b1ff"
   (org-babel-next-src-block)
   (should (= 610 (org-babel-execute-src-block)))))

(ert-deftest ob-ada-spark/using-templates/invlaid-template-name ()
  "Using templates: Invalid template name"
  (org-test-at-id
   "3fb0ac1c-dfed-4d2f-9803-d1dea18eec45"
   (org-babel-next-src-block)
   (when (should (buffer-live-p (get-buffer org-babel-error-buffer-name)))
     (kill-buffer org-babel-error-buffer-name))
   :type 'error))

;; Literate programming

(ert-deftest ob-ada-spark/literate-programming/hello-noweb ()
  "Literate programming: Hello noweb"
  (org-test-at-id
   "5386221e-da6f-411f-8dd5-3045e14b2e15"
   (org-babel-next-src-block 2)
   (should (equal "Hello noweb" (org-babel-execute-src-block)))))

(ert-deftest ob-ada-spark/literate-programming/constant-literals ()
  "Literate programming: Constant literals"
  (org-test-at-id
   "1bc1f537-e31f-4b8e-adb3-bdd474673e17"
   (org-babel-next-src-block 2)
   (should (equal "1 Hello 2 Hello 3 Hello"
                  (org-babel-execute-src-block)))))

(ert-deftest ob-ada-spark/literate-programming/constant-literals-invalid-literal-name ()
  "Literate programming: Constant literals - Invalid literal name"
  (org-test-at-id
   "1bc1f537-e31f-4b8e-adb3-bdd474673e17"
   (org-babel-next-src-block 3)
   (when (should (buffer-live-p (get-buffer org-babel-error-buffer-name)))
     (kill-buffer org-babel-error-buffer-name))
   :type 'error))

(ert-deftest ob-ada-spark/using-templates/evaluated-literals ()
  "Using templates: Evaluated literals"
  (org-test-at-id
   "7cc220c1-a917-4af4-a497-7e247f1c15ae"
   (org-babel-next-src-block)
   (should (equal "SUM is 353" (org-babel-execute-src-block)))))

;; User-defined templates

(setq ob-ada-spark-template:test
      '((:params . ((:unit . "main") (:results silent)))
        (:body . "
with Ada.Text_IO; use Ada.Text_IO;
%s
procedure Main is
   procedure Write_Answer (N : Natural) is
   begin
      Put_Line (\"Answer:\" & N'Image);
   end Write_Answer;
begin
   %s
end Main;
")))

(ert-deftest ob-ada-spark/user-defined-template/test ()
  "Users-defined templates: Test"
  (org-test-at-id
   "70feb9e8-19f1-402b-b1d0-4c8ccdf2cfe4"
   (org-babel-next-src-block)
   (should (equal "Answer: 42" (org-babel-execute-src-block)))))

(ert-deftest ob-ada-spark/user-defined-template/using-evaluated-literals ()
  "Users-defined templates: Using evaluated literals"
  (org-test-at-id
   "2a05b182-07bf-4ba5-9cca-128919cb837e"
   (org-babel-next-src-block)
   (should (equal "Answer: 42" (org-babel-execute-src-block)))))

(ert-deftest ob-ada-spark/user-defined-template/using-noweb-and-evaluated-literals ()
  "Users-defined templates: Using noweb and evaluated literals"
  (org-test-at-id
   "69e852b1-a278-4051-8719-917cfb59c582"
   (org-babel-next-src-block 2)
   (should (equal "Answer: 42" (org-babel-execute-src-block)))))

;; Proving SPARK Code

(ert-deftest ob-ada-spark/proving-spark-code/stone ()
  "Proving SPARK code: Stone"
  (org-test-at-id
      "fd628dbb-aacc-4931-aab5-5816f7c85b46"
   (org-babel-next-src-block)
   (org-babel-execute-src-block)
   (should (search-forward "#+begin_example" nil t))
   (forward-line 1)
   (let ((report-begin (point-at-bol))
         (report-end 0))
     (should (search-forward "#+end_example" nil t))
     (forward-line -1)
     (setq report-end (point-at-eol))
     (should
      (string-match
       "Phase 1 of 2: generation of Global contracts ...
\\(.\\|\n\\)+
Phase 2 of 2: full checking of SPARK legality rules ..."
       (buffer-substring-no-properties report-begin report-end))))))

(ert-deftest ob-ada-spark/proving-spark-code/bronze ()
  "Proving SPARK code: Bronze"
  (org-test-at-id
      "79b4ca15-8127-467d-b239-dd190cb45f2d"
    (org-babel-next-src-block)
    (org-babel-execute-src-block)
    (should (search-forward "#+begin_example" nil t))
    (forward-line 1)
    (let ((report-begin (point-at-bol))
          (report-end 0))
      (should (search-forward "#+end_example" nil t))
      (forward-line -1)
      (setq report-end (point-at-eol))
      (should
       (string-match
        "Phase 1 of 2: generation of Global contracts ...
\\(.\\|\n\\)+
Phase 2 of 2: analysis of data and information flow ...
\\(.\\|\n\\)+
main.adb:8:07: info: data dependencies proved
main.adb:9:07: info: flow dependencies proved"
        (buffer-substring-no-properties report-begin report-end))))))

(ert-deftest ob-ada-spark/proving-spark-code/silver ()
  "Proving SPARK code: Silver"
  (org-test-at-id
      "4529e47f-835a-4410-883a-b3fab0026553"
    (org-babel-next-src-block)
    (org-babel-execute-src-block)
    (should (search-forward "#+begin_example" nil t))
    (forward-line 1)
    (let ((report-begin (point-at-bol))
          (report-end 0))
      (should (search-forward "#+end_example" nil t))
      (forward-line -1)
      (setq report-end (point-at-eol))
      (should
       (string-match
        "Phase 1 of 2: generation of Global contracts ...
\\(.\\|\n\\)+
Phase 2 of 2: flow analysis and proof ...
\\(.\\|\n\\)+
main.adb:8:07: info: data dependencies proved
main.adb:9:07: info: flow dependencies proved
main.adb:11:18: info: postcondition proved
main.adb:14:14: info: range check proved
main.adb:18:04: info: precondition proved
main.adb:19:30: info: range check proved"
        (buffer-substring-no-properties report-begin report-end))))))

(provide 'test-ob-ada-spark)
;;; test-ob-ada-spark.el ends here