refactor(emacs): move tests in *.el files to 'test' directory
This commit is contained in:
Soonho Kong
parent
45b7327d63
commit
2ba43f1432
5 changed files with 493 additions and 369 deletions
|
|
@ -7,8 +7,9 @@
|
|||
(require 'cl-lib)
|
||||
(require 'lean-util)
|
||||
|
||||
;; Constructor
|
||||
;; ===========
|
||||
|
||||
;; Load
|
||||
;; ----
|
||||
(defun lean-cmd-load (file-name)
|
||||
"Load the Lean file named [file-name].
|
||||
|
||||
|
|
@ -17,6 +18,15 @@ each command. Lean uses the “snapshots” to process incremental
|
|||
updates efficiently."
|
||||
`(LOAD ,file-name))
|
||||
|
||||
(defun lean-cmd-load-get-file-name (load-cmd)
|
||||
(cl-second load-cmd))
|
||||
|
||||
(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))))
|
||||
|
||||
;; Visit
|
||||
;; -----
|
||||
(defun lean-cmd-visit (&optional file-name)
|
||||
"sets [file-name] as the \"current\" file.
|
||||
|
||||
|
|
@ -28,6 +38,16 @@ file. The LOAD command can be used to discard all these changes,
|
|||
and enforce the content of the file stored in file system."
|
||||
`(VISIT ,(or file-name (buffer-file-name))))
|
||||
|
||||
(defun lean-cmd-visit-get-file-name (visit-cmd)
|
||||
(cl-second visit-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))))
|
||||
|
||||
|
||||
;; Replace
|
||||
;; -------
|
||||
(defun lean-cmd-replace (line-number new-line)
|
||||
"Replace the line [line-number] (in the current file) with [new-line].
|
||||
|
||||
|
|
@ -37,6 +57,19 @@ and enforce the content of the file stored in file system."
|
|||
indexed from 1."
|
||||
`(REPLACE ,line-number ,new-line))
|
||||
|
||||
(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-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)))
|
||||
|
||||
;; Insert
|
||||
;; ------
|
||||
(defun lean-cmd-insert (line-number new-line)
|
||||
"Insert [new-line] (in the current file) before line [line-number].
|
||||
|
||||
|
|
@ -45,6 +78,19 @@ lean buffer, then empty lines are introduced. The lines are
|
|||
indexed from 1."
|
||||
`(INSERT ,line-number ,new-line))
|
||||
|
||||
(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-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)))
|
||||
|
||||
;; Remove
|
||||
;; ------
|
||||
(defun lean-cmd-remove (line-number)
|
||||
"Remove line [line-number] (in the current file).
|
||||
|
||||
|
|
@ -53,16 +99,53 @@ the total number of lines in the lean buffer, then the command is
|
|||
ignored."
|
||||
`(REMOVE ,line-number))
|
||||
|
||||
(defun lean-cmd-remove-get-line-number (remove-cmd)
|
||||
(cl-second remove-cmd))
|
||||
|
||||
(defun lean-cmd-remove-to-string (cmd)
|
||||
"Convert Remove command to string"
|
||||
(format "REMOVE %d" (lean-cmd-remove-get-line-number cmd)))
|
||||
|
||||
;; Info
|
||||
;; ----
|
||||
(defun lean-cmd-info (line-number &optional column-number)
|
||||
"Extracts typing information associated with line [line-number].
|
||||
|
||||
Lean produces a possible empty sequence of entries terminated with '--ENDINFO'"
|
||||
`(INFO ,line-number ,column-number))
|
||||
|
||||
(defun lean-cmd-info-get-line-number (info-cmd)
|
||||
(cl-second info-cmd))
|
||||
|
||||
(defun lean-cmd-info-get-column-number (info-cmd)
|
||||
(cl-third info-cmd))
|
||||
|
||||
(defun lean-cmd-info-to-string (cmd)
|
||||
"Convert Info command to string"
|
||||
(let ((col (lean-cmd-info-get-column-number cmd)))
|
||||
(if col
|
||||
(format "INFO %d %d" (lean-cmd-info-get-line-number cmd) col)
|
||||
(format "INFO %d" (lean-cmd-info-get-line-number cmd)))))
|
||||
|
||||
;; Check
|
||||
;; -----
|
||||
(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-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-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)))
|
||||
|
||||
;; Set
|
||||
;; ---
|
||||
(defun lean-cmd-set (option-name option-value)
|
||||
"Set a Lean option [option-name] with [option-value].
|
||||
|
||||
|
|
@ -70,218 +153,128 @@ Lean produces a possible empty sequence of entries terminated with '--ENDINFO'"
|
|||
set using the command set_option in a ‘.lean’ file is supported."
|
||||
`(SET ,option-name ,option-value))
|
||||
|
||||
(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-set-to-string (cmd)
|
||||
"Convert Set command to string"
|
||||
(format "SET\n%s %s" (lean-cmd-set-get-option-name cmd)
|
||||
(lean-cmd-set-get-option-value cmd)))
|
||||
|
||||
;; Eval
|
||||
;; ----
|
||||
(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))
|
||||
|
||||
(defun lean-cmd-eval-get-lean-cmd (eval-cmd)
|
||||
(cl-second eval-cmd))
|
||||
|
||||
(defun lean-cmd-eval-to-string (cmd)
|
||||
"Convert Eval command to string"
|
||||
(format "EVAL\n%s" (lean-cmd-eval-get-lean-cmd cmd)))
|
||||
|
||||
;; Options
|
||||
;; -------
|
||||
(defun lean-cmd-options ()
|
||||
"Display all configuration options available in Lean."
|
||||
`(OPTIONS))
|
||||
|
||||
(defun lean-cmd-options-to-string (cmd)
|
||||
"Convert Options command to string"
|
||||
(format "OPTIONS"))
|
||||
|
||||
;; Clear Cache
|
||||
;; -----------
|
||||
(defun lean-cmd-clear-cache ()
|
||||
"Clear Cache"
|
||||
`(CLEAR-CACHE))
|
||||
|
||||
(defun lean-cmd-clear-cache-to-string (cmd)
|
||||
"Convert clear-cache command to string"
|
||||
(format "CLEAR_CACHE"))
|
||||
|
||||
;; Show
|
||||
;; ----
|
||||
(defun lean-cmd-show ()
|
||||
"Display the \"lines\" associated with the current buffer, or at least"
|
||||
`(SHOW))
|
||||
|
||||
(defun lean-cmd-show-to-string (cmd)
|
||||
"Convert show command to string"
|
||||
(format "SHOW"))
|
||||
|
||||
;; Valid
|
||||
;; -----
|
||||
(defun lean-cmd-valid ()
|
||||
"Display valid/invalid lines. Invalid lines are the one we need to refresh type information"
|
||||
`(VALID))
|
||||
|
||||
(defun lean-cmd-valid-to-string (cmd)
|
||||
"Convert valid command to string"
|
||||
(format "VALID"))
|
||||
|
||||
;; Findp
|
||||
;; -----
|
||||
(defun lean-cmd-findp (line-number prefix)
|
||||
"Find All auto-complete candidates matched with prefix at line-number"
|
||||
`(FINDP ,line-number ,prefix))
|
||||
|
||||
(defun lean-cmd-findg (line-number column-number patterns)
|
||||
"FINDG generates a sequence of declarations that may be used to “fill” a particular placeholder"
|
||||
`(FINDG ,line-number ,column-number ,patterns))
|
||||
|
||||
(defun lean-cmd-wait ()
|
||||
"Block server until all pending information has been computed."
|
||||
`(WAIT))
|
||||
|
||||
;; 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-info-get-column-number (info-cmd)
|
||||
(cl-third 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))
|
||||
(defun lean-cmd-findp-get-line-number (findp-cmd)
|
||||
(cl-second findp-cmd))
|
||||
|
||||
(defun lean-cmd-findp-get-prefix (findp-cmd)
|
||||
(cl-third findp-cmd))
|
||||
(defun lean-cmd-findg-get-line-number (findg-cmd)
|
||||
(cl-second findg-cmd))
|
||||
(defun lean-cmd-findg-get-column-number (findg-cmd)
|
||||
(cl-third findg-cmd))
|
||||
(defun lean-cmd-findg-get-patterns (findg-cmd)
|
||||
(cl-fourth findg-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-info-get-column-number (lean-cmd-info 34 11))
|
||||
11))
|
||||
(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"))
|
||||
(cl-assert (= (lean-cmd-findp-get-line-number
|
||||
(lean-cmd-findp 10 "iff_"))
|
||||
10))
|
||||
(cl-assert (string= (lean-cmd-findp-get-prefix
|
||||
(lean-cmd-findp 10 "iff_"))
|
||||
"iff_"))
|
||||
|
||||
(cl-assert (= (lean-cmd-findg-get-line-number
|
||||
(lean-cmd-findg 48 10 "+intro -and -elim"))
|
||||
48))
|
||||
(cl-assert (= (lean-cmd-findg-get-column-number
|
||||
(lean-cmd-findg 48 10 "+intro -and -elim"))
|
||||
10))
|
||||
(cl-assert (string= (lean-cmd-findg-get-patterns
|
||||
(lean-cmd-findg 48 10 "+intro -and -elim"))
|
||||
"+intro -and -elim"))
|
||||
|
||||
|
||||
;; 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"
|
||||
(let ((col (lean-cmd-info-get-column-number cmd)))
|
||||
(if col
|
||||
(format "INFO %d %d" (lean-cmd-info-get-line-number cmd) col)
|
||||
(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-set-to-string (cmd)
|
||||
"Convert Set command to string"
|
||||
(format "SET\n%s %s" (lean-cmd-set-get-option-name cmd)
|
||||
(lean-cmd-set-get-option-value cmd)))
|
||||
(defun lean-cmd-eval-to-string (cmd)
|
||||
"Convert Eval command to string"
|
||||
(format "EVAL\n%s" (lean-cmd-eval-get-lean-cmd cmd)))
|
||||
(defun lean-cmd-options-to-string (cmd)
|
||||
"Convert Options command to string"
|
||||
(format "OPTIONS"))
|
||||
(defun lean-cmd-clear-cache-to-string (cmd)
|
||||
"Convert clear-cache command to string"
|
||||
(format "CLEAR_CACHE"))
|
||||
(defun lean-cmd-show-to-string (cmd)
|
||||
"Convert show command to string"
|
||||
(format "SHOW"))
|
||||
(defun lean-cmd-valid-to-string (cmd)
|
||||
"Convert valid command to string"
|
||||
(format "VALID"))
|
||||
(defun lean-cmd-findp-to-string (cmd)
|
||||
"Convert findp command to string"
|
||||
(format "FINDP %d\n%s"
|
||||
(lean-cmd-findp-get-line-number cmd)
|
||||
(lean-cmd-findp-get-prefix cmd)))
|
||||
|
||||
;; Findg
|
||||
;; -----
|
||||
(defun lean-cmd-findg (line-number column-number patterns)
|
||||
"FINDG generates a sequence of declarations that may be used to “fill” a particular placeholder"
|
||||
`(FINDG ,line-number ,column-number ,patterns))
|
||||
|
||||
(defun lean-cmd-findg-get-line-number (findg-cmd)
|
||||
(cl-second findg-cmd))
|
||||
|
||||
(defun lean-cmd-findg-get-column-number (findg-cmd)
|
||||
(cl-third findg-cmd))
|
||||
|
||||
(defun lean-cmd-findg-get-patterns (findg-cmd)
|
||||
(cl-fourth findg-cmd))
|
||||
|
||||
(defun lean-cmd-findg-to-string (cmd)
|
||||
"Convert findg command to string"
|
||||
(format "FINDG %d %d\n%s"
|
||||
(lean-cmd-findg-get-line-number cmd)
|
||||
(lean-cmd-findg-get-column-number cmd)
|
||||
(lean-cmd-findg-get-patterns cmd)))
|
||||
|
||||
;; Wait
|
||||
;; ----
|
||||
(defun lean-cmd-wait ()
|
||||
"Block server until all pending information has been computed."
|
||||
`(WAIT))
|
||||
|
||||
(defun lean-cmd-wait-to-string (cmd)
|
||||
"Convert wait command to string"
|
||||
(format "WAIT"))
|
||||
|
||||
|
||||
;; Type
|
||||
;; ====
|
||||
(defun lean-cmd-type (cmd)
|
||||
(cl-first cmd))
|
||||
|
||||
(defun lean-cmd-to-string (cmd)
|
||||
"Convert command to string"
|
||||
(cl-case (lean-cmd-type cmd)
|
||||
|
|
@ -302,29 +295,5 @@ It has the effect of evaluating a command in the end of the current file"
|
|||
('FINDG (lean-cmd-findg-to-string cmd))
|
||||
('WAIT (lean-cmd-wait-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-info 42 11))
|
||||
(concat "INFO 42 11")))
|
||||
(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")))
|
||||
(cl-assert (string= (lean-cmd-to-string (lean-cmd-findp 42 "iff_"))
|
||||
(concat "FINDP 42" "\n" "iff_")))
|
||||
(cl-assert (string= (lean-cmd-to-string (lean-cmd-findg 48 10 "+intro -and -elim"))
|
||||
(concat "FINDG 48 10" "\n" "+intro -and -elim")))
|
||||
(cl-assert (string= (lean-cmd-to-string (lean-cmd-wait))
|
||||
(concat "WAIT")))
|
||||
|
||||
;; ----------------
|
||||
(provide 'lean-cmd)
|
||||
|
|
|
|||
|
|
@ -36,25 +36,8 @@
|
|||
(defun lean-info-type-body-str (typeinfo)
|
||||
(string-join (lean-info-type-body typeinfo) "\n"))
|
||||
|
||||
;; -- Test
|
||||
(cl-assert (lean-info-type-p 'TYPE))
|
||||
(cl-assert (lean-info-type-p "-- TYPE|121|2"))
|
||||
(cl-assert (lean-info-type-p '("-- TYPE|121|2" "not (eq zero (succ m'))" "→ decidable (eq zero (succ m'))")))
|
||||
(cl-assert (equal (lean-info-type-parse-header "-- TYPE|121|2")
|
||||
'(121 2)))
|
||||
(cl-assert (equal (lean-info-type-parse '("-- TYPE|121|2" "not (eq zero (succ m'))" "→ decidable (eq zero (succ m'))"))
|
||||
'(TYPE
|
||||
(121 2)
|
||||
("not (eq zero (succ m'))"
|
||||
"→ decidable (eq zero (succ m'))"))))
|
||||
(cl-assert (equal
|
||||
(lean-info-type-pos
|
||||
(lean-info-type-parse '("-- TYPE|121|2" "not (eq zero (succ m'))" "→ decidable (eq zero (succ m'))")))
|
||||
'(121 2)))
|
||||
|
||||
;; Overload Information
|
||||
;; --------------------
|
||||
|
||||
(defun lean-info-overload-type (overload)
|
||||
(cl-first overload))
|
||||
(defun lean-info-overload-p (overload)
|
||||
|
|
@ -77,55 +60,6 @@
|
|||
(body (-split-on "--" (cdr seq))))
|
||||
`(OVERLOAD ,header ,body))))
|
||||
|
||||
;; -- Test
|
||||
(cl-assert (lean-info-overload-p 'OVERLOAD))
|
||||
(cl-assert (lean-info-overload-p "-- OVERLOAD|121|2"))
|
||||
(cl-assert (lean-info-overload-p '("-- OVERLOAD|121|2" "not (eq zero (succ m'))" "→ decidable (eq zero (succ m'))")))
|
||||
(cl-assert (equal (lean-info-overload-parse-header "-- OVERLOAD|121|2")
|
||||
'(121 2)))
|
||||
(cl-assert
|
||||
(equal
|
||||
(lean-info-overload-parse
|
||||
'("-- OVERLOAD|121|2"
|
||||
"not (eq zero (succ m'))"
|
||||
"→ decidable (eq zero (succ m'))"
|
||||
"--"
|
||||
"not (eq one (succ m'))"
|
||||
"→ decidable (eq zero (succ m'))"
|
||||
"--"
|
||||
"not (eq two (succ m'))"
|
||||
"→ decidable (eq zero (succ m'))"))
|
||||
'(OVERLOAD (121 2)
|
||||
(("not (eq zero (succ m'))" "→ decidable (eq zero (succ m'))")
|
||||
("not (eq one (succ m'))" "→ decidable (eq zero (succ m'))")
|
||||
("not (eq two (succ m'))" "→ decidable (eq zero (succ m'))")))))
|
||||
(cl-assert (equal
|
||||
(lean-info-overload-pos
|
||||
(lean-info-overload-parse
|
||||
'("-- OVERLOAD|121|2"
|
||||
"not (eq zero (succ m'))"
|
||||
"→ decidable (eq zero (succ m'))"
|
||||
"--"
|
||||
"not (eq one (succ m'))"
|
||||
"→ decidable (eq zero (succ m'))"
|
||||
"--"
|
||||
"not (eq two (succ m'))"
|
||||
"→ decidable (eq zero (succ m'))")))
|
||||
'(121 2)))
|
||||
(cl-assert (equal (lean-info-overload-names (lean-info-overload-parse
|
||||
'("-- OVERLOAD|121|2"
|
||||
"not (eq zero (succ m'))"
|
||||
"→ decidable (eq zero (succ m'))"
|
||||
"--"
|
||||
"not (eq one (succ m'))"
|
||||
"→ decidable (eq zero (succ m'))"
|
||||
"--"
|
||||
"not (eq two (succ m'))"
|
||||
"→ decidable (eq zero (succ m'))")))
|
||||
'("not (eq zero (succ m'))\n→ decidable (eq zero (succ m'))"
|
||||
"not (eq one (succ m'))\n→ decidable (eq zero (succ m'))"
|
||||
"not (eq two (succ m'))\n→ decidable (eq zero (succ m'))")))
|
||||
|
||||
;; Synth Information
|
||||
;; ----------------
|
||||
(defun lean-info-synth-type (synth)
|
||||
|
|
@ -151,22 +85,6 @@
|
|||
(defun lean-info-synth-body-str (synth)
|
||||
(string-join (lean-info-synth-body synth) "\n"))
|
||||
|
||||
;; -- Test
|
||||
(cl-assert (lean-info-synth-p 'SYNTH))
|
||||
(cl-assert (lean-info-synth-p "-- SYNTH|121|2"))
|
||||
(cl-assert (lean-info-synth-p '("-- SYNTH|121|2" "not (eq zero (succ m'))" "→ decidable (eq zero (succ m'))")))
|
||||
(cl-assert (equal (lean-info-synth-parse-header "-- SYNTH|121|2")
|
||||
'(121 2)))
|
||||
(cl-assert (equal (lean-info-synth-parse '("-- SYNTH|121|2" "not (eq zero (succ m'))" "→ decidable (eq zero (succ m'))"))
|
||||
'(SYNTH
|
||||
(121 2)
|
||||
("not (eq zero (succ m'))"
|
||||
"→ decidable (eq zero (succ m'))"))))
|
||||
(cl-assert (equal
|
||||
(lean-info-synth-pos
|
||||
(lean-info-synth-parse '("-- SYNTH|121|2" "not (eq zero (succ m'))" "→ decidable (eq zero (succ m'))")))
|
||||
'(121 2)))
|
||||
|
||||
;; Coercion Information
|
||||
;; ----------------
|
||||
(defun lean-info-coercion-type (coercion)
|
||||
|
|
@ -198,29 +116,6 @@
|
|||
(defun lean-info-coercion-type-str (coercion)
|
||||
(string-join (lean-info-coercion-type coercion) "\n"))
|
||||
|
||||
;; -- Test
|
||||
(cl-assert (lean-info-coercion-p 'COERCION))
|
||||
(cl-assert (lean-info-coercion-p "-- COERCION|121|2"))
|
||||
(cl-assert (lean-info-coercion-p '("-- COERCION|417|15"
|
||||
"of_nat m"
|
||||
"--"
|
||||
"int")))
|
||||
(cl-assert (equal (lean-info-coercion-parse-header "-- COERCION|121|2")
|
||||
'(121 2)))
|
||||
(cl-assert (equal (lean-info-coercion-parse '("-- COERCION|417|15"
|
||||
"of_nat"
|
||||
"--"
|
||||
"int"))
|
||||
'(COERCION
|
||||
(417 15)
|
||||
("of_nat")
|
||||
("int"))))
|
||||
(cl-assert (equal
|
||||
(lean-info-coercion-pos
|
||||
(lean-info-coercion-parse '("-- COERCION|417|15"
|
||||
"of_nat")))
|
||||
'(417 15)))
|
||||
|
||||
;; Extra Information
|
||||
;; ----------------
|
||||
(defun lean-info-extra-type (extra)
|
||||
|
|
@ -252,29 +147,6 @@
|
|||
(defun lean-info-extra-type-str (extra)
|
||||
(string-join (lean-info-extra-type extra) "\n"))
|
||||
|
||||
;; -- Test
|
||||
(cl-assert (lean-info-extra-p 'EXTRA))
|
||||
(cl-assert (lean-info-extra-p "-- EXTRA_TYPE|121|2"))
|
||||
(cl-assert (lean-info-extra-p '("-- EXTRA_TYPE|417|15"
|
||||
"rec_on b ff tt"
|
||||
"--"
|
||||
"bool")))
|
||||
(cl-assert (equal (lean-info-extra-parse-header "-- EXTRA_TYPE|121|2")
|
||||
'(121 2)))
|
||||
(cl-assert (equal (lean-info-extra-parse '("-- EXTRA_TYPE|417|15"
|
||||
"rec_on b ff tt"
|
||||
"--"
|
||||
"bool"))
|
||||
'(EXTRA
|
||||
(417 15)
|
||||
("rec_on b ff tt")
|
||||
("bool"))))
|
||||
(cl-assert (equal
|
||||
(lean-info-extra-pos
|
||||
(lean-info-extra-parse '("-- EXTRA_TYPE|417|15"
|
||||
"of_nat")))
|
||||
'(417 15)))
|
||||
|
||||
;; Identifier Information
|
||||
;; ----------------------
|
||||
(defun lean-info-identifier-type (identifier)
|
||||
|
|
@ -300,20 +172,6 @@
|
|||
(defun lean-info-identifier-body-str (identifier)
|
||||
(string-join (lean-info-identifier-body identifier) "\n"))
|
||||
|
||||
;; -- Test
|
||||
(cl-assert (lean-info-identifier-p 'IDENTIFIER))
|
||||
(cl-assert (lean-info-identifier-p "-- IDENTIFIER|121|2"))
|
||||
(cl-assert (lean-info-identifier-p '("-- IDENTIFIER|121|2" "foo.f")))
|
||||
(cl-assert (equal (lean-info-identifier-parse-header "-- IDENTIFIER|121|2")
|
||||
'(121 2)))
|
||||
(cl-assert (equal (lean-info-identifier-parse '("-- IDENTIFIER|121|2" "foo.f"))
|
||||
'(IDENTIFIER
|
||||
(121 2)
|
||||
("foo.f"))))
|
||||
(cl-assert (equal
|
||||
(lean-info-identifier-pos
|
||||
(lean-info-identifier-parse '("-- IDENTIFIER|121|2" "foo.f")))
|
||||
'(121 2)))
|
||||
|
||||
;; Symbol Information
|
||||
;; ----------------
|
||||
|
|
@ -340,22 +198,6 @@
|
|||
(defun lean-info-symbol-body-str (symbol)
|
||||
(string-join (lean-info-symbol-body symbol) "\n"))
|
||||
|
||||
;; -- Test
|
||||
(cl-assert (lean-info-symbol-p 'SYMBOL))
|
||||
(cl-assert (lean-info-symbol-p "-- SYMBOL|121|2"))
|
||||
(cl-assert (lean-info-symbol-p (lean-info-symbol-parse '("-- SYMBOL|121|2" "→"))))
|
||||
(cl-assert (equal (lean-info-symbol-parse-header "-- SYMBOL|121|2")
|
||||
'(121 2)))
|
||||
(cl-assert (lean-info-symbol-p '("-- SYMBOL|121|2" "→")))
|
||||
(cl-assert (equal (lean-info-symbol-parse '("-- SYMBOL|121|2" "→"))
|
||||
'(SYMBOL
|
||||
(121 2)
|
||||
("→"))))
|
||||
(cl-assert (equal
|
||||
(lean-info-symbol-pos
|
||||
(lean-info-symbol-parse '("-- SYMBOL|121|2" "→")))
|
||||
'(121 2)))
|
||||
|
||||
(defun lean-info-id-symbol-body-str (info)
|
||||
(case (lean-info-kind info)
|
||||
('IDENTIFIER (string-join (lean-info-symbol-body info) "\n"))
|
||||
|
|
@ -385,25 +227,6 @@
|
|||
(defun lean-info-column (info)
|
||||
(cl-second (lean-info-pos info)))
|
||||
|
||||
;; -- test
|
||||
(cl-assert (equal
|
||||
(lean-info-pos
|
||||
(lean-info-type-parse '("-- TYPE|121|2" "not (eq zero (succ m'))" "→ decidable (eq zero (succ m'))")))
|
||||
'(121 2)))
|
||||
(cl-assert (equal
|
||||
(lean-info-pos
|
||||
(lean-info-overload-parse
|
||||
'("-- OVERLOAD|121|2"
|
||||
"not (eq zero (succ m'))"
|
||||
"→ decidable (eq zero (succ m'))"
|
||||
"--"
|
||||
"not (eq one (succ m'))"
|
||||
"→ decidable (eq zero (succ m'))"
|
||||
"--"
|
||||
"not (eq two (succ m'))"
|
||||
"→ decidable (eq zero (succ m'))")))
|
||||
'(121 2)))
|
||||
|
||||
;; Info Parsing
|
||||
;; ================
|
||||
(defun lean-info-list-split (str)
|
||||
|
|
|
|||
113
src/emacs/test/lean-cmd-test.el
Normal file
113
src/emacs/test/lean-cmd-test.el
Normal file
|
|
@ -0,0 +1,113 @@
|
|||
;; Copyright (c) 2014 Microsoft Corporation. All rights reserved.
|
||||
;; Released under Apache 2.0 license as described in the file LICENSE.
|
||||
;;
|
||||
;; Author: Soonho Kong
|
||||
;;
|
||||
|
||||
(require 'ert)
|
||||
(require 'lean-cmd)
|
||||
|
||||
(ert-deftest lean-test-cmd-get ()
|
||||
"Test lean-cmd-*-get-*"
|
||||
(should (string= (lean-cmd-load-get-file-name (lean-cmd-load "nat.lean"))
|
||||
"nat.lean"))
|
||||
(should (string= (lean-cmd-visit-get-file-name (lean-cmd-visit "nat.lean"))
|
||||
"nat.lean"))
|
||||
(should (string=
|
||||
(lean-cmd-load-get-file-name (lean-cmd-load "library/standard/bool.lean"))
|
||||
"library/standard/bool.lean"))
|
||||
(should (string=
|
||||
(lean-cmd-load-get-file-name (lean-cmd-load "~/work/lean/basic.lean"))
|
||||
"~/work/lean/basic.lean"))
|
||||
(should (string=
|
||||
(lean-cmd-visit-get-file-name (lean-cmd-visit "library/standard/bool.lean"))
|
||||
"library/standard/bool.lean"))
|
||||
(should (string=
|
||||
(lean-cmd-visit-get-file-name (lean-cmd-visit "~/work/lean/basic.lean"))
|
||||
"~/work/lean/basic.lean"))
|
||||
(should (= (lean-cmd-replace-get-line-number
|
||||
(lean-cmd-replace 34 "∀ (n : nat), ne (succ n) zero"))
|
||||
34))
|
||||
(should (string= (lean-cmd-replace-get-line
|
||||
(lean-cmd-replace 34 "∀ (n : nat), ne (succ n) zero"))
|
||||
"∀ (n : nat), ne (succ n) zero"))
|
||||
(should (= (lean-cmd-insert-get-line-number
|
||||
(lean-cmd-insert 34 "∀ (n : nat), ne (succ n) zero"))
|
||||
34))
|
||||
(should (string= (lean-cmd-insert-get-line
|
||||
(lean-cmd-insert 34 "∀ (n : nat), ne (succ n) zero"))
|
||||
"∀ (n : nat), ne (succ n) zero"))
|
||||
(should (= (lean-cmd-insert-get-line-number (lean-cmd-remove 34))
|
||||
34))
|
||||
(should (= (lean-cmd-info-get-line-number (lean-cmd-info 34))
|
||||
34))
|
||||
(should (= (lean-cmd-info-get-column-number (lean-cmd-info 34 11))
|
||||
11))
|
||||
(should (= (lean-cmd-check-get-line-number
|
||||
(lean-cmd-check 34 "∀ (n : nat), ne (succ n) zero"))
|
||||
34))
|
||||
(should (string= (lean-cmd-check-get-line
|
||||
(lean-cmd-replace 34 "∀ (n : nat), ne (succ n) zero"))
|
||||
"∀ (n : nat), ne (succ n) zero"))
|
||||
(should (string= (lean-cmd-set-get-option-name
|
||||
(lean-cmd-set "pp.implicit" "true"))
|
||||
"pp.implicit"))
|
||||
(should (string= (lean-cmd-set-get-option-value
|
||||
(lean-cmd-set "pp.implicit" "true"))
|
||||
"true"))
|
||||
(should (string= (lean-cmd-eval-get-lean-cmd
|
||||
(lean-cmd-eval "print 3"))
|
||||
"print 3"))
|
||||
(should (= (lean-cmd-findp-get-line-number
|
||||
(lean-cmd-findp 10 "iff_"))
|
||||
10))
|
||||
(should (string= (lean-cmd-findp-get-prefix
|
||||
(lean-cmd-findp 10 "iff_"))
|
||||
"iff_"))
|
||||
|
||||
(should (= (lean-cmd-findg-get-line-number
|
||||
(lean-cmd-findg 48 10 "+intro -and -elim"))
|
||||
48))
|
||||
(should (= (lean-cmd-findg-get-column-number
|
||||
(lean-cmd-findg 48 10 "+intro -and -elim"))
|
||||
10))
|
||||
(should (string= (lean-cmd-findg-get-patterns
|
||||
(lean-cmd-findg 48 10 "+intro -and -elim"))
|
||||
"+intro -and -elim")))
|
||||
|
||||
(ert-deftest lean-test-cmd-to-string ()
|
||||
"Test lean-cmd-to-string"
|
||||
(should (string= (lean-cmd-to-string (lean-cmd-load "~/work/lean/basic.lean"))
|
||||
(concat "LOAD " (expand-file-name "~/work/lean/basic.lean"))))
|
||||
(should (string= (lean-cmd-to-string (lean-cmd-visit "~/work/lean/basic.lean"))
|
||||
(concat "VISIT " (expand-file-name "~/work/lean/basic.lean"))))
|
||||
(should (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")))
|
||||
(should (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")))
|
||||
(should (string= (lean-cmd-to-string (lean-cmd-remove 42))
|
||||
(concat "REMOVE 42")))
|
||||
(should (string= (lean-cmd-to-string (lean-cmd-info 42))
|
||||
(concat "INFO 42")))
|
||||
(should (string= (lean-cmd-to-string (lean-cmd-info 42 11))
|
||||
(concat "INFO 42 11")))
|
||||
(should (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")))
|
||||
(should (string= (lean-cmd-to-string (lean-cmd-set "pp.implicit" "true"))
|
||||
(concat "SET" "\n" "pp.implicit true" )))
|
||||
(should (string= (lean-cmd-to-string (lean-cmd-eval "check 3"))
|
||||
(concat "EVAL" "\n" "check 3" )))
|
||||
(should (string= (lean-cmd-to-string (lean-cmd-options))
|
||||
(concat "OPTIONS")))
|
||||
(should (string= (lean-cmd-to-string (lean-cmd-clear-cache))
|
||||
(concat "CLEAR_CACHE")))
|
||||
(should (string= (lean-cmd-to-string (lean-cmd-show))
|
||||
(concat "SHOW")))
|
||||
(should (string= (lean-cmd-to-string (lean-cmd-valid))
|
||||
(concat "VALID")))
|
||||
(should (string= (lean-cmd-to-string (lean-cmd-findp 42 "iff_"))
|
||||
(concat "FINDP 42" "\n" "iff_")))
|
||||
(should (string= (lean-cmd-to-string (lean-cmd-findg 48 10 "+intro -and -elim"))
|
||||
(concat "FINDG 48 10" "\n" "+intro -and -elim")))
|
||||
(should (string= (lean-cmd-to-string (lean-cmd-wait))
|
||||
(concat "WAIT"))))
|
||||
201
src/emacs/test/lean-info-test.el
Normal file
201
src/emacs/test/lean-info-test.el
Normal file
|
|
@ -0,0 +1,201 @@
|
|||
;; Copyright (c) 2014 Microsoft Corporation. All rights reserved.
|
||||
;; Released under Apache 2.0 license as described in the file LICENSE.
|
||||
;;
|
||||
;; Author: Soonho Kong
|
||||
;;
|
||||
|
||||
(require 'ert)
|
||||
(require 'lean-info)
|
||||
|
||||
(ert-deftest lean-test-info-type ()
|
||||
"Test lean-info-type"
|
||||
(should (lean-info-type-p 'TYPE))
|
||||
(should (lean-info-type-p "-- TYPE|121|2"))
|
||||
(should (lean-info-type-p '("-- TYPE|121|2" "not (eq zero (succ m'))" "→ decidable (eq zero (succ m'))")))
|
||||
(should (equal (lean-info-type-parse-header "-- TYPE|121|2")
|
||||
'(121 2)))
|
||||
(should (equal (lean-info-type-parse '("-- TYPE|121|2" "not (eq zero (succ m'))" "→ decidable (eq zero (succ m'))"))
|
||||
'(TYPE
|
||||
(121 2)
|
||||
("not (eq zero (succ m'))"
|
||||
"→ decidable (eq zero (succ m'))"))))
|
||||
(should (equal
|
||||
(lean-info-type-pos
|
||||
(lean-info-type-parse '("-- TYPE|121|2" "not (eq zero (succ m'))" "→ decidable (eq zero (succ m'))")))
|
||||
'(121 2))))
|
||||
|
||||
(ert-deftest lean-test-info-overload ()
|
||||
"Test lean-info-overload"
|
||||
(should (lean-info-overload-p 'OVERLOAD))
|
||||
(should (lean-info-overload-p "-- OVERLOAD|121|2"))
|
||||
(should (lean-info-overload-p '("-- OVERLOAD|121|2" "not (eq zero (succ m'))" "→ decidable (eq zero (succ m'))")))
|
||||
(should (equal (lean-info-overload-parse-header "-- OVERLOAD|121|2")
|
||||
'(121 2)))
|
||||
(should
|
||||
(equal
|
||||
(lean-info-overload-parse
|
||||
'("-- OVERLOAD|121|2"
|
||||
"not (eq zero (succ m'))"
|
||||
"→ decidable (eq zero (succ m'))"
|
||||
"--"
|
||||
"not (eq one (succ m'))"
|
||||
"→ decidable (eq zero (succ m'))"
|
||||
"--"
|
||||
"not (eq two (succ m'))"
|
||||
"→ decidable (eq zero (succ m'))"))
|
||||
'(OVERLOAD (121 2)
|
||||
(("not (eq zero (succ m'))" "→ decidable (eq zero (succ m'))")
|
||||
("not (eq one (succ m'))" "→ decidable (eq zero (succ m'))")
|
||||
("not (eq two (succ m'))" "→ decidable (eq zero (succ m'))")))))
|
||||
(should (equal
|
||||
(lean-info-overload-pos
|
||||
(lean-info-overload-parse
|
||||
'("-- OVERLOAD|121|2"
|
||||
"not (eq zero (succ m'))"
|
||||
"→ decidable (eq zero (succ m'))"
|
||||
"--"
|
||||
"not (eq one (succ m'))"
|
||||
"→ decidable (eq zero (succ m'))"
|
||||
"--"
|
||||
"not (eq two (succ m'))"
|
||||
"→ decidable (eq zero (succ m'))")))
|
||||
'(121 2)))
|
||||
(should (equal (lean-info-overload-names (lean-info-overload-parse
|
||||
'("-- OVERLOAD|121|2"
|
||||
"not (eq zero (succ m'))"
|
||||
"→ decidable (eq zero (succ m'))"
|
||||
"--"
|
||||
"not (eq one (succ m'))"
|
||||
"→ decidable (eq zero (succ m'))"
|
||||
"--"
|
||||
"not (eq two (succ m'))"
|
||||
"→ decidable (eq zero (succ m'))")))
|
||||
'("not (eq zero (succ m'))\n→ decidable (eq zero (succ m'))"
|
||||
"not (eq one (succ m'))\n→ decidable (eq zero (succ m'))"
|
||||
"not (eq two (succ m'))\n→ decidable (eq zero (succ m'))"))))
|
||||
|
||||
|
||||
(ert-deftest lean-test-info-synth ()
|
||||
"Test lean-info-synth"
|
||||
;; -- Test
|
||||
(should (lean-info-synth-p 'SYNTH))
|
||||
(should (lean-info-synth-p "-- SYNTH|121|2"))
|
||||
(should (lean-info-synth-p '("-- SYNTH|121|2" "not (eq zero (succ m'))" "→ decidable (eq zero (succ m'))")))
|
||||
(should (equal (lean-info-synth-parse-header "-- SYNTH|121|2")
|
||||
'(121 2)))
|
||||
(should (equal (lean-info-synth-parse '("-- SYNTH|121|2" "not (eq zero (succ m'))" "→ decidable (eq zero (succ m'))"))
|
||||
'(SYNTH
|
||||
(121 2)
|
||||
("not (eq zero (succ m'))"
|
||||
"→ decidable (eq zero (succ m'))"))))
|
||||
(should (equal
|
||||
(lean-info-synth-pos
|
||||
(lean-info-synth-parse '("-- SYNTH|121|2" "not (eq zero (succ m'))" "→ decidable (eq zero (succ m'))")))
|
||||
'(121 2))))
|
||||
|
||||
(ert-deftest lean-test-info-coercion ()
|
||||
"Test lean-info-coercion"
|
||||
;; -- Test
|
||||
(should (lean-info-coercion-p 'COERCION))
|
||||
(should (lean-info-coercion-p "-- COERCION|121|2"))
|
||||
(should (lean-info-coercion-p '("-- COERCION|417|15"
|
||||
"of_nat m"
|
||||
"--"
|
||||
"int")))
|
||||
(should (equal (lean-info-coercion-parse-header "-- COERCION|121|2")
|
||||
'(121 2)))
|
||||
(should (equal (lean-info-coercion-parse '("-- COERCION|417|15"
|
||||
"of_nat"
|
||||
"--"
|
||||
"int"))
|
||||
'(COERCION
|
||||
(417 15)
|
||||
("of_nat")
|
||||
("int"))))
|
||||
(should (equal
|
||||
(lean-info-coercion-pos
|
||||
(lean-info-coercion-parse '("-- COERCION|417|15"
|
||||
"of_nat")))
|
||||
'(417 15))))
|
||||
|
||||
(ert-deftest lean-test-info-extra ()
|
||||
"Test lean-info-extra"
|
||||
;; -- Test
|
||||
(should (lean-info-extra-p 'EXTRA))
|
||||
(should (lean-info-extra-p "-- EXTRA_TYPE|121|2"))
|
||||
(should (lean-info-extra-p '("-- EXTRA_TYPE|417|15"
|
||||
"rec_on b ff tt"
|
||||
"--"
|
||||
"bool")))
|
||||
(should (equal (lean-info-extra-parse-header "-- EXTRA_TYPE|121|2")
|
||||
'(121 2)))
|
||||
(should (equal (lean-info-extra-parse '("-- EXTRA_TYPE|417|15"
|
||||
"rec_on b ff tt"
|
||||
"--"
|
||||
"bool"))
|
||||
'(EXTRA
|
||||
(417 15)
|
||||
("rec_on b ff tt")
|
||||
("bool"))))
|
||||
(should (equal
|
||||
(lean-info-extra-pos
|
||||
(lean-info-extra-parse '("-- EXTRA_TYPE|417|15"
|
||||
"of_nat")))
|
||||
'(417 15))))
|
||||
|
||||
(ert-deftest lean-test-info-identifier ()
|
||||
"Test lean-info-identifier"
|
||||
;; -- Test
|
||||
(should (lean-info-identifier-p 'IDENTIFIER))
|
||||
(should (lean-info-identifier-p "-- IDENTIFIER|121|2"))
|
||||
(should (lean-info-identifier-p '("-- IDENTIFIER|121|2" "foo.f")))
|
||||
(should (equal (lean-info-identifier-parse-header "-- IDENTIFIER|121|2")
|
||||
'(121 2)))
|
||||
(should (equal (lean-info-identifier-parse '("-- IDENTIFIER|121|2" "foo.f"))
|
||||
'(IDENTIFIER
|
||||
(121 2)
|
||||
("foo.f"))))
|
||||
(should (equal
|
||||
(lean-info-identifier-pos
|
||||
(lean-info-identifier-parse '("-- IDENTIFIER|121|2" "foo.f")))
|
||||
'(121 2))))
|
||||
|
||||
(ert-deftest lean-test-info-symbol ()
|
||||
"Test lean-info-symbol"
|
||||
;; -- Test
|
||||
(should (lean-info-symbol-p 'SYMBOL))
|
||||
(should (lean-info-symbol-p "-- SYMBOL|121|2"))
|
||||
(should (lean-info-symbol-p (lean-info-symbol-parse '("-- SYMBOL|121|2" "→"))))
|
||||
(should (equal (lean-info-symbol-parse-header "-- SYMBOL|121|2")
|
||||
'(121 2)))
|
||||
(should (lean-info-symbol-p '("-- SYMBOL|121|2" "→")))
|
||||
(should (equal (lean-info-symbol-parse '("-- SYMBOL|121|2" "→"))
|
||||
'(SYMBOL
|
||||
(121 2)
|
||||
("→"))))
|
||||
(should (equal
|
||||
(lean-info-symbol-pos
|
||||
(lean-info-symbol-parse '("-- SYMBOL|121|2" "→")))
|
||||
'(121 2))))
|
||||
|
||||
(ert-deftest lean-test-info-pos ()
|
||||
"Test lean-info-pos"
|
||||
(should (equal
|
||||
(lean-info-pos
|
||||
(lean-info-type-parse '("-- TYPE|121|2" "not (eq zero (succ m'))" "→ decidable (eq zero (succ m'))")))
|
||||
'(121 2)))
|
||||
(should (equal
|
||||
(lean-info-pos
|
||||
(lean-info-overload-parse
|
||||
'("-- OVERLOAD|121|2"
|
||||
"not (eq zero (succ m'))"
|
||||
"→ decidable (eq zero (succ m'))"
|
||||
"--"
|
||||
"not (eq one (succ m'))"
|
||||
"→ decidable (eq zero (succ m'))"
|
||||
"--"
|
||||
"not (eq two (succ m'))"
|
||||
"→ decidable (eq zero (succ m'))")))
|
||||
'(121 2)))
|
||||
|
||||
)
|
||||
18
src/emacs/test/test-helper.el
Normal file
18
src/emacs/test/test-helper.el
Normal file
|
|
@ -0,0 +1,18 @@
|
|||
;; Copyright (c) 2014 Microsoft Corporation. All rights reserved.
|
||||
;; Released under Apache 2.0 license as described in the file LICENSE.
|
||||
;;
|
||||
;; Author: Soonho Kong
|
||||
;;
|
||||
|
||||
(defconst lean-test/test-path
|
||||
(f-parent (f-this-file)))
|
||||
|
||||
(defconst lean-test/root-path
|
||||
(f-parent lean-test/test-path))
|
||||
|
||||
(add-to-list 'load-path lean-test/root-path)
|
||||
|
||||
;; Avoid Emacs 23 interupting the tests with:
|
||||
;; File bar-autoloads.el changed on disk. Reread from disk? (yes or no)
|
||||
(fset 'y-or-n-p (lambda (_) t))
|
||||
(fset 'yes-or-no-p (lambda (_) t))
|
||||
Loading…
Reference in a new issue