;;; ob-ada-spark.el --- org-babel functions for Ada & SPARK -*- lexical-binding: t; -*-

;; Copyright (C) 2021-2024 Free Software Foundation, Inc.

;; Author: Francesc Rocher
;; Maintainer: Francesc Rocher
;; Keywords: literate programming, reproducible research, Ada/SPARK
;; URL: https://orgmode.org

;; This file is part of GNU Emacs.

;; GNU Emacs 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 Emacs 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 ob-ada-spark. If not, see <https://www.gnu.org/licenses/>.

;;; Commentary:

;; Org-Babel support for evaluating Ada & SPARK code and proving SPARK code.

;;; Requirements:

;; * An Ada compiler (gnatmake)
;; * A SPARK formal verification tool (gnatprove)
;; * Emacs ada-mode, optional but strongly recommended, see
;;   <https://www.nongnu.org/ada-mode/>

;;; Code:

(require 'ob)
(require 'time-stamp)

(org-assert-version)

(defvar org-babel-tangle-lang-exts)
(add-to-list 'org-babel-tangle-lang-exts '("ada" . "adb"))

(defvar org-babel-temporary-directory)

(defvar org-babel-default-header-args:ada '((:args . nil)
                                            (:cflags . nil)
                                            (:pflags . nil)
                                            (:prove . nil)
                                            (:template . nil)
                                            (:unit . nil)
                                            (:with . nil))
  "Ada/SPARK default header arguments.")

(defconst org-babel-header-args:ada '((args . any)
                                      (cflags . any)
                                      (pflags . any)
                                      (prove . ((nil t)))
                                      (template . :any)
                                      (unit . :any)
                                      (with . nil))
  "Ada/SPARK specific header arguments.")

(defconst ob-ada-spark-template-var-name-format "ob-ada-spark-template:%s"
  "Format of the name of the template variables.
All templates must be defined in a variable with a name
compatible with this format. The template name is only the '%s'
part. From the source block, templates can be used in the
':template' header with the template name.

For example, the template defined in the variable
`ob-ada-spark-template:ada-main' is used in the header of the
source block with ':template ada-main'.")

(defcustom org-babel-ada-spark-compile-command "gnatmake"
  "Command used to compile Ada/SPARK code into an executable.
May be either a command in the path, like gnatmake, or an
absolute path name.

If using Alire 2.x, install the default native toolchain, with
`alr install gnat_native', and write here the path to gnatmake or
append $HOME/.alire/bin to PATH."
  :group 'org-babel
  :type 'string
  :package-version '(Org . "9.7")
  :safe #'stringp)

(defcustom org-babel-ada-spark-prove-command "gnatprove"
  "Command used to prove SPARK code.
May be either a command in the path, like gnatprove, or an
absolute path name, like /opt/ada/bin/gnatprove.

If using Alire 2.x, install gnatprove, `alr install gnatprove',
and write here the path to gnatprove or append $HOME/.alire/bin
to PATH."
  :group 'org-babel
  :type 'string
  :package-version '(Org . "9.7")
  :safe #'stringp)

(defcustom org-babel-ada-spark-default-compile-flags
  "-f -we -gnata -gnateF -gnateV -gnatf -gnatVa -gnatwa -gnatX -gnat2022 -gnatW8"
  "Default compiler flags for Ada and SPARK.
These flags are used to compile Ada and SPARK code. Any
additional flags specified in the ':clfags' header is passed
after the default ones.

Default flags for gnatmake are:

  -f        Force recompilations of non predefined units
  -we       Treat all warnings as errors
  -gnata    Assertions enabled. Pragma Assert/Debug to be activated
  -gnateF   Check overflow on predefined Float types
  -gnateV   Validity checks on subprogram parameters
  -gnatf    Full errors. Verbose details, all undefined references
  -gnatwa   Enable selected warning modes (turn on all info/warnings)
  -gnatX    Language extensions permitted
  -gnat2022 Ada 2022 mode
  -gnatW8   Wide character encoding method (?=h/u/s/e/8/b)
"
  :group 'org-babel
  :type 'string
  :package-version '(Org . "9.7")
  :safe #'stringp)

(defcustom org-babel-ada-spark-default-prove-flags
  "-f --assumptions --level=4 --report=all --verbose"
  "Default flags for gnatprove.
These flags are used to prove SPARK code. Any additional flag
specified in the ':pflags' header is passed after the default
ones.

The compiler flags are also passed to gnatprove using the
'-cargs' flag, both the the default flags in
`org-babel-ada-spark-default-compile-flags' and the flags
specified in the ':cflags' header, in that order.

Default flags for gnatprove are:

  -f                Force recompilation/analysis of all units
  --assumptions     Output assumptions information
  --level=4         Set the level of proof (0 = faster to 4 = more powerful)
  --report=all      Set the report mode of GNATprove (r=fail*, all,
                    provers, statistics)
  --verbose         Output extra verbose information
"
  :group 'org-babel
  :type 'string
  :package-version '(Org . "9.7")
  :safe #'stringp)

(defcustom org-babel-ada-spark-default-file-header
  (lambda ()
    (format
     "-----------------------------------------------------------------------------
--
--  Source code generated automatically by 'org-babel-tangle' from
--  file %s
--  %s
--
--  DO NOT EDIT!!
--
-----------------------------------------------------------------------------

"
     (buffer-file-name (current-buffer))
     (time-stamp-string "%Y-%02m-%02d %02H:%02M:%02S")))
  "Header written in files generated with `org-babel-tangle'."
  :group 'org-babel
  :type 'function
  :package-version '(Org . "9.7"))

(defvar ob-ada-spark-template:ada-main
  '((:params . ((:unit . "main") (:cflags . "-gnatW8")))
    (:body . "with Ada.Text_IO; use Ada.Text_IO;
%s
procedure Main is
%s
end Main;
"))
  "Template for a basic Main procedure written in Ada 2022.
Makes use of the Ada.Text_IO (with and use clauses). Admits
additional with'ed packages and a procedure body.

Use this template as a starting point for new Ada templates. All
templates must include two placeholders, for the with section and
for the body.

Example of use:

#+begin_src ada :template ada-main :with System.OS_Lib
   Time : constant String := Current_Time_String;
begin
   Put_Line (Time);
#+end_src

The resulting body is:

with Ada.Text_IO; use Ada.Text_IO;
with System.OS_Lib; use System.OS_Lib;

procedure Main is
   Time : constant String := Current_Time_String;
begin
   Put_Line (Time);
end Main;
")

(defvar ob-ada-spark-template:spark-main
  '((:params . ((:cflags . "-gnatW8") (:prove . t) (:unit . "main")))
    (:body . "with Ada.Text_IO; use Ada.Text_IO;
%s
procedure Main with Spark_Mode => On is
%s
end Main;
"))
  "Template for a basic Main procedure written in SPARK.
Makes use of the Ada.Text_IO (with and use clauses). Admits
additional with'ed packages and a procedure body.

Use this template as a starting point for new SPARK templates. All
templates must include two placeholders, for the with section and
for the body.

Example of use:

#+begin_src ada :template ada-main :with System.OS_Lib
   Put_Line (Current_Time_String);
#+end_src

The resulting body is:

with Ada.Text_IO; use Ada.Text_IO;
with System.OS_Lib; use System.OS_Lib;

procedure Main is
begin
   Put_Line (Current_Time_String);
end Main;
")

(defun ob-ada-spark-replace-params-from-template (params)
  "Replace headers in PARAMS with headers defined in the template.
If a template defines a set of params, replace the values in
PARAMS with the values defined in the template, overwriting
parameters already defined in the source code block.
Return the new list of PARAMS, or the original list if the
template does not define any header or no template is used."
  (let* ((template-name (cdr (assq :template params)))
         (template (eval
                    (intern-soft
                     (format ob-ada-spark-template-var-name-format
                             template-name)))))
    (if template
        (progn
          (message "-- replacing params from template %s" template-name)
          (mapc (lambda (p)
                  (assq-delete-all (car p) params))
                (cdr (assq :params template)))
          (append params (cdr (assq :params template))))
      params)))

(defun org-babel-expand-body:ada (body params)
  "Expand BODY according to PARAMS and return the expanded body.
Body expansion comprises replacement of template and literal
variables.
First, template is filled with the value of ':with' and ':body'
headers in PARAMS. Second, all literal variables are replaced by
the values found in the ':var' header of PARAMS."
  (let* ((template-name (cdr (assq :template params)))
         (template (eval
                    (intern-soft
                     (format ob-ada-spark-template-var-name-format
                             template-name))))
         (vars (org-babel--get-vars params))
         (with (cdr (assq :with params))))

    (if (and template-name (null template))
        (error
         "Invalid template name '%s', variable ob-ada-spark-template:%s undefined"
         template-name template-name))

    ;; Use the body defined in the template, if any. It needs two
    ;; parameters: the 'with' section (defined in params) and the
    ;; 'body' section (the contents of source code block)
    (setq body
          (if template
              (progn
                (message "-- expanding body from template %s" template-name)
                (format
                 ;; body's template as format control string
                 (cdr (assq :body template))
                 (if (null with) ""
                   ;; replace :with parameter
                   (mapconcat
                    (lambda (w) (format "with %s; use %s;\n" w w))
                    (split-string with " " t)
                    ""))
                 ;; use body in the source code block
                 body))
            body))

    ;; expand literal variables in the body, if any
    (when vars
      (mapc
       (lambda (var)
         (let ((key (car var))
               (val (cdr var)))
           (setq body (string-replace (format "%s" key) (format "%s" val) body))))
       vars))
    body))

(defun org-babel-execute:ada (body params)
  "Execute or prove a block of Ada/SPARK code with org-babel.
BODY contains the Ada/SPARK source code to evaluate. PARAMS is
the list of source code block parameters.

This function is called by `org-babel-execute-src-block'"
  (let* ((processed-params (org-babel-process-params params))
         (all-params
          (ob-ada-spark-replace-params-from-template processed-params))
         (full-body (org-babel-expand-body:ada body all-params))
         (prove (cdr (assq :prove all-params))))
    (if prove
        (ob-ada-spark-prove full-body all-params)
      (ob-ada-spark-execute full-body all-params))))

(defun ob-ada-spark-execute (body params)
  "Execute or prove a block of Ada/SPARK code with org-babel.
BODY contains the Ada/SPARK source code to evaluate, already
expanded when using templates. PARAMS is the list of source code
block parameters, also expanded with the template parameters.

This function is called by `org-babel-execute:ada'"
  (let* ((args (cdr (assq :args params)))
         (cflags (cdr (assq :cflags params)))
         (unit (cdr (assq :unit params)))
         (default-directory (org-babel-temp-directory))
         (tmp-src-file (if unit
                           (file-name-concat (org-babel-temp-directory)
                                             (concat unit ".adb"))
                         (org-babel-temp-file "ada-src-" ".adb")))
         (tmp-bin-file (if unit
                           (file-name-concat (org-babel-temp-directory) unit)
                         (org-babel-temp-file "ada-bin-" org-babel-exeext))))

    ;; write compilation unit
    (with-temp-file tmp-src-file (insert body))

    ;; clean previous evaluation of the same unit
    (if (stringp unit)
        (cl-mapcar
         (lambda (ext)
           (let ((file (file-name-concat default-directory
                                         (concat unit ext))))
             (if (file-exists-p file) (delete-file file))))
         '("" ".ali" ".o")))

    ;; compile
    (setq compile-command
          (format "%s %s -o %s %s %s"
                  org-babel-ada-spark-compile-command
                  (or org-babel-ada-spark-default-compile-flags "")
                  tmp-bin-file
                  (or cflags "")
                  tmp-src-file))
    (message "-- Ada compile-command: %s" compile-command)
    (org-babel-eval compile-command "")

    ;; execute
    (let* ((exec-command (concat tmp-bin-file (if args (concat " " args) "")))
           (results
            (org-trim
             (org-remove-indentation
              (org-babel-eval exec-command "")))))
      (org-babel-reassemble-table
       (org-babel-result-cond (cdr (assq :result-params params))
         (org-babel-read results)
         (let ((tmp-file (org-babel-temp-file "ada-")))
           (with-temp-file tmp-file (insert results))
           (org-babel-import-elisp-from-file tmp-file)))
       (org-babel-pick-name
        (cdr (assq :colname-names params)) (cdr (assq :colnames params)))
       (org-babel-pick-name
        (cdr (assq :rowname-names params)) (cdr (assq :rownames params)))))))

(defun ob-ada-spark-prove (body params)
  "Prove a block of SPARK code with org-babel.
BODY contains the SPARK source code to prove, already expanded
when using templates. PARAMS is the list of source code block
parameters, also expanded with the template parameters.

This function is called by `org-babel-execute:ada'"
  (let* ((cflags (cdr (assq :cflags params)))
         (pflags (cdr (assq :pflags params)))
         (unit (cdr (assq :unit params)))
         (default-directory (org-babel-temp-directory))
         (tmp-src-file (if unit (concat unit ".adb") "spark_src.adb"))
         (tmp-gpr-file (if unit (concat unit ".gpr") "spark_prj.gpr"))
         (tmp-project (file-name-sans-extension tmp-gpr-file))
         (prove-command-args
          (format "-P %s %s %s -u %s -cargs %s %s"
                  tmp-gpr-file
                  (or org-babel-ada-spark-default-prove-flags "")
                  (or pflags "")
                  tmp-src-file
                  (or org-babel-ada-spark-default-compile-flags "")
                  (or cflags ""))))

    ;; write compilation unit
    (with-temp-file tmp-src-file (insert body))

    ;; create temporary project
    (with-temp-file tmp-gpr-file
      (insert (format "project %s is
  for Source_Dirs use (\"%s\");
  for Source_Files use (\"%s\");
  for Main use (\"%s\");
end %s;
"
                      tmp-project
                      default-directory
                      tmp-src-file
                      tmp-src-file
                      tmp-project)))

    ;; remove gnatprove directory and clean previous evaluation of the
    ;; same unit
    (delete-directory
     (file-name-concat org-babel-temporary-directory "gnatprove") t)
    (org-babel-eval
     (format "%s --clean %s"
             org-babel-ada-spark-prove-command prove-command-args)
     "")

    ;; invoke gnatprove
    (let* ((prove-command
            (format "%s %s"
                    org-babel-ada-spark-prove-command prove-command-args))
           (results
            (org-trim
             (org-remove-indentation
              (org-babel-eval prove-command "")))))
      (message "-- SPARK prove-command: %s" prove-command)
      (org-babel-reassemble-table
       (org-babel-result-cond (cdr (assq :result-params params))
         (org-babel-read results)
         (let ((tmp-file (org-babel-temp-file "ada-")))
           (with-temp-file tmp-file (insert results))
           (org-babel-import-elisp-from-file tmp-file)))
       (org-babel-pick-name
        (cdr (assq :colname-names params)) (cdr (assq :colnames params)))
       (org-babel-pick-name
        (cdr (assq :rowname-names params)) (cdr (assq :rownames params)))))))

(defun org-babel-prep-session:ada-spark ()
  "This function does nothing.
Ada and SPARK are compiled languages with no support for
sessions."
  (error "Ada & SPARK are compiled languages -- no support for sessions"))

(defvar ada-skel-initial-string--backup "")

(defun ob-ada-spark-pre-tangle-hook ()
  "This function is called just before `org-babel-tangle'.
When using tangle to export Ada/SPARK code to a file, this
function is used to set the header of the file according to the
value of the variable `org-babel-ada-spark-default-file-header'."
  ;; ada-skel-initial-string is defined in ada-mode and is inserted
  ;; automatically when Emacs sets ada-mode in an empty buffer; switching
  ;; temporarily its value so the org-babel-ada-spark-default-file-header is
  ;; inserted
  (if (boundp 'ada-skel-initial-string)
      (progn (setq ada-skel-initial-string--backup ada-skel-initial-string)
             (setq ada-skel-initial-string (funcall org-babel-ada-spark-default-file-header)))))

(defun ob-ada-spark-post-tangle-hook ()
  "This function is called just after `org-babel-tangle'.
Once the file has been generated, this function restores the
value of the header inserted into Ada/SPARK files."
  ;; if ada-skel-initial-string has not been inserted by ada-mode, then
  ;; insert the default header
  (if (boundp 'ada-skel-initial-string)
      (setq ada-skel-initial-string ada-skel-initial-string--backup)
    (save-excursion
      (goto-char (point-min))
      (insert (funcall org-babel-ada-spark-default-file-header)))))

(add-hook 'org-babel-pre-tangle-hook #'ob-ada-spark-pre-tangle-hook)
(add-hook 'org-babel-post-tangle-hook #'ob-ada-spark-post-tangle-hook)

(provide 'ob-ada-spark)

;;; ob-ada-spark.el ends here