;; Copyright (c) 2014 Microsoft Corporation. All rights reserved.
;; Released under Apache 2.0 license as described in the file LICENSE.
;;
;; Author: Soonho Kong
;;

(require 'cl-lib)
(require 'lean-util)

;; Constructor
;; ===========
(defun lean-cmd-load (file-name)
  "Load the Lean file named [file-name].

Lean will create a \"snapshot\" (aka backtracking point) after
each command. Lean uses the “snapshots” to process incremental
updates efficiently."
  `(LOAD ,file-name))

(defun lean-cmd-visit (file-name)
  "sets [file-name] as the \"current\" file.

Lean can keep information about multiple files. This command The
remaining commands are all with respect to the current file. If
[file-name] has not been loaded yet, then this command will load
it. Some of the remaining commands apply  'changes'  to the current
file. The LOAD command can be used to discard all these changes,
and enforce the content of the file stored in file system."
  `(VISIT ,file-name))

(defun lean-cmd-replace (line-number new-line)
  "Replace the line [line-number] (in the current file) with [new-line].

 Lean uses the snapshots to process the request efficiently. If
 [line-number] is greater than the total number of lines in the
 lean buffer, then empty lines are introduced. The lines are
 indexed from 1."
  `(REPLACE ,line-number ,new-line))

(defun lean-cmd-insert (line-number new-line)
  "Insert [new-line] (in the current file) before line [line-number].

If [line-number] is greater than the total number of lines in the
lean buffer, then empty lines are introduced. The lines are
indexed from 1."
  `(INSERT ,line-number ,new-line))

(defun lean-cmd-remove (line-number)
  "Remove line [line-number] (in the current file).

The lines are indexed from 1. If [line-number] is greater than
the total number of lines in the lean buffer, then the command is
ignored."
  `(REMOVE ,line-number))

(defun lean-cmd-info (line-number)
  "Extracts typing information associated with line [line-number].

Lean produces a possible empty sequence of entries terminated with '--ENDINFO'"
  `(INFO ,line-number))

(defun lean-cmd-check (line-number line)
  "Check whether the text editor and Lean have the 'same view' of the current file + modifications"
  `(CHECK ,line-number ,line))

(defun lean-cmd-set (option-name option-value)
  "Set a Lean option [option-name] with [option-value].

[option-name] must be a valid Lean option. Any option that can be
set using the command set_option in a ‘.lean’ file is supported."
  `(SET ,option-name ,option-value))

(defun lean-cmd-eval (lean-cmd)
  "Evaluates a Lean command [lean-cmd].

It has the effect of evaluating a command in the end of the current file"
  `(EVAL ,lean-cmd))

;; Type
;; ====
(defun lean-cmd-type (cmd)
  (cl-first cmd))

;; Get functions
;; =============
(defun lean-cmd-load-get-file-name (load-cmd)
  (cl-second load-cmd))
(defun lean-cmd-visit-get-file-name (visit-cmd)
  (cl-second visit-cmd))
(defun lean-cmd-replace-get-line-number (replace-cmd)
  (cl-second replace-cmd))
(defun lean-cmd-replace-get-line (replace-cmd)
  (cl-third replace-cmd))
(defun lean-cmd-insert-get-line-number (insert-cmd)
  (cl-second insert-cmd))
(defun lean-cmd-insert-get-line (insert-cmd)
  (cl-third insert-cmd))
(defun lean-cmd-remove-get-line-number (remove-cmd)
  (cl-second remove-cmd))
(defun lean-cmd-info-get-line-number (info-cmd)
  (cl-second info-cmd))
(defun lean-cmd-check-get-line-number (check-cmd)
  (cl-second check-cmd))
(defun lean-cmd-check-get-line (check-cmd)
  (cl-third check-cmd))
(defun lean-cmd-set-get-option-name (set-cmd)
  (cl-second set-cmd))
(defun lean-cmd-set-get-option-value (set-cmd)
  (cl-third set-cmd))
(defun lean-cmd-eval-get-lean-cmd (eval-cmd)
  (cl-second eval-cmd))

;; -- Test
(cl-assert (string= (lean-cmd-load-get-file-name (lean-cmd-load "nat.lean"))
                    "nat.lean"))
(cl-assert (string= (lean-cmd-visit-get-file-name (lean-cmd-visit "nat.lean"))
                    "nat.lean"))
(cl-assert (string=
            (lean-cmd-load-get-file-name (lean-cmd-load "library/standard/bool.lean"))
            "library/standard/bool.lean"))
(cl-assert (string=
            (lean-cmd-load-get-file-name (lean-cmd-load "~/work/lean/basic.lean"))
            "~/work/lean/basic.lean"))
(cl-assert (string=
            (lean-cmd-visit-get-file-name (lean-cmd-visit "library/standard/bool.lean"))
            "library/standard/bool.lean"))
(cl-assert (string=
            (lean-cmd-visit-get-file-name (lean-cmd-visit "~/work/lean/basic.lean"))
            "~/work/lean/basic.lean"))
(cl-assert (= (lean-cmd-replace-get-line-number
               (lean-cmd-replace 34 "∀ (n : nat), ne (succ n) zero"))
              34))
(cl-assert (string= (lean-cmd-replace-get-line
                     (lean-cmd-replace 34 "∀ (n : nat), ne (succ n) zero"))
                    "∀ (n : nat), ne (succ n) zero"))
(cl-assert (= (lean-cmd-insert-get-line-number
               (lean-cmd-insert 34 "∀ (n : nat), ne (succ n) zero"))
              34))
(cl-assert (string= (lean-cmd-insert-get-line
                     (lean-cmd-insert 34 "∀ (n : nat), ne (succ n) zero"))
                    "∀ (n : nat), ne (succ n) zero"))
(cl-assert (= (lean-cmd-insert-get-line-number (lean-cmd-remove 34))
              34))
(cl-assert (= (lean-cmd-info-get-line-number (lean-cmd-info 34))
              34))
(cl-assert (= (lean-cmd-check-get-line-number
               (lean-cmd-check 34 "∀ (n : nat), ne (succ n) zero"))
              34))
(cl-assert (string= (lean-cmd-check-get-line
                     (lean-cmd-replace 34 "∀ (n : nat), ne (succ n) zero"))
                    "∀ (n : nat), ne (succ n) zero"))
(cl-assert (string= (lean-cmd-set-get-option-name
                     (lean-cmd-set "pp.implicit" "true"))
                    "pp.implicit"))
(cl-assert (string= (lean-cmd-set-get-option-value
                     (lean-cmd-set "pp.implicit" "true"))
                    "true"))
(cl-assert (string= (lean-cmd-eval-get-lean-cmd
                     (lean-cmd-eval "print 3"))
                    "print 3"))

;; to-string functions
;; ===================
(defun lean-cmd-load-to-string (cmd)
  "Convert LOAD command to string"
  (format "LOAD %s" (expand-file-name (lean-cmd-load-get-file-name cmd))))
(defun lean-cmd-visit-to-string (cmd)
  "Convert VISIT command to string"
  (format "VISIT %s" (expand-file-name (lean-cmd-load-get-file-name cmd))))
(defun lean-cmd-replace-to-string (cmd)
  "Convert Replace command to string"
  (format "REPLACE %d\n%s" (lean-cmd-replace-get-line-number cmd)
          (lean-cmd-replace-get-line cmd)))
(defun lean-cmd-insert-to-string (cmd)
  "Convert Insert command to string"
  (format "INSERT %d\n%s" (lean-cmd-insert-get-line-number cmd)
          (lean-cmd-insert-get-line cmd)))
(defun lean-cmd-remove-to-string (cmd)
  "Convert Remove command to string"
  (format "REMOVE %d" (lean-cmd-remove-get-line-number cmd)))
(defun lean-cmd-info-to-string (cmd)
  "Convert Info command to string"
  (format "INFO %d" (lean-cmd-info-get-line-number cmd)))
(defun lean-cmd-check-to-string (cmd)
  "Convert Check command to string"
  (format "CHECK %d\n%s" (lean-cmd-check-get-line-number cmd)
          (lean-cmd-check-get-line cmd)))

(defun lean-cmd-to-string (cmd)
  "Convert command to string"
  (cl-case (lean-cmd-type cmd)
    ('LOAD    (lean-cmd-load-to-string    cmd))
    ('VISIT   (lean-cmd-visit-to-string   cmd))
    ('REPLACE (lean-cmd-replace-to-string cmd))
    ('INSERT  (lean-cmd-insert-to-string  cmd))
    ('REMOVE  (lean-cmd-remove-to-string  cmd))
    ('INFO    (lean-cmd-info-to-string    cmd))
    ('CHECK   (lean-cmd-check-to-string   cmd))))

;; -- Test
(cl-assert (string= (lean-cmd-to-string (lean-cmd-load "~/work/lean/basic.lean"))
                    (concat "LOAD " (expand-file-name "~/work/lean/basic.lean"))))
(cl-assert (string= (lean-cmd-to-string (lean-cmd-visit "~/work/lean/basic.lean"))
                    (concat "VISIT " (expand-file-name "~/work/lean/basic.lean"))))
(cl-assert (string= (lean-cmd-to-string (lean-cmd-replace 42 "∀ (n : nat), ne (succ n) zero"))
                    (concat "REPLACE 42" "\n" "∀ (n : nat), ne (succ n) zero")))
(cl-assert (string= (lean-cmd-to-string (lean-cmd-insert 42 "∀ (n : nat), ne (succ n) zero"))
                    (concat "INSERT 42" "\n" "∀ (n : nat), ne (succ n) zero")))
(cl-assert (string= (lean-cmd-to-string (lean-cmd-remove 42))
                    (concat "REMOVE 42")))
(cl-assert (string= (lean-cmd-to-string (lean-cmd-info 42))
                    (concat "INFO 42")))
(cl-assert (string= (lean-cmd-to-string (lean-cmd-check 42 "∀ (n : nat), ne (succ n) zero"))
                    (concat "CHECK 42" "\n" "∀ (n : nat), ne (succ n) zero")))
;; ----------------
(provide 'lean-cmd)