Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

jump to defn based on Locate Library loop and .glob files #265

Draft
wants to merge 2 commits into
base: master
Choose a base branch
from
Draft

jump to defn based on Locate Library loop and .glob files #265

Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
34221b1
jump to defn based on Locate Library loop and .glob files
aa755 Nov 30, 2022
05fb367
bugfixes in globfile-based jumping and Locate Library based targetfil…
aa755 Feb 3, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
108 changes: 72 additions & 36 deletions company-coq.el
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -70,6 +70,7 @@
;; an answer from the prover (company-coq-talking-to-prover).

(require 'cl-lib) ;; Compatibility
(require 'f) ;; File io convenience to open .glob files
(require 'company) ;; Autocompletion
(require 'company-math) ;; Math symbols
(require 'dash) ;; -when-let, -if-let, -zip, -keep, etc.
Expand Down Expand Up @@ -412,6 +413,15 @@ The result matches any symbol in HEADERS, followed by BODY."
(concat "^[[:blank:]]*\\_<\\(" (regexp-opt headers) "\\)\\_>"
(when body (concat "\\s-*\\(" body "\\)"))))

(defconst company-coq-definitions-kwds-globfile `("def" "ind" "constr" "prf");; add regexp-opt here
"Keywords that introduce a definition in a .glob file.")

(defun company-coq-make-headers-regexp-glob (body)
"Construct a regexp from HEADERS and BODY.
The result matches any symbol in HEADERS, followed by BODY."
(concat "^[[:blank:]]*\\_<\\(" (regexp-opt company-coq-definitions-kwds-globfile) "\\)\\_> \\([0-9]*\\):\\([0-9]*\\)"
(when body (concat "\\s-*\\(" body "[^a-zA-Zα-ωΑ-Ω0-9_']" "\\)"))))

(defconst company-coq-definitions-kwds `("Class" "CoFixpoint" "CoInductive" "Coercion" "Corollary"
"Declare Module" "Definition" "Example" "Fact" "Fixpoint"
"Function" "Functional Scheme" "Global Instance" "Inductive"
Expand All @@ -420,6 +430,7 @@ The result matches any symbol in HEADERS, followed by BODY."
"Variant" "with")
"Keywords that introduce a definition.")


(defconst company-coq-definitions-regexp (company-coq-make-headers-regexp company-coq-definitions-kwds
company-coq-id-regexp)
"Regexp used to locate symbol definitions in the current buffer.")
Expand Down Expand Up @@ -2104,6 +2115,7 @@ for FALLBACK (followed by \\s-*:[^=]) instead. If the target can
be found, call CALLBACK with the point where TARGET or FALLBACK
was found, and the value to be returned."
(let ((point-pos (company-coq-search-then-scroll-up-1 target fallback)))
(message "point-pos is %s" point-pos)
(if point-pos
(when (functionp callback)
(apply callback point-pos))
Expand Down Expand Up @@ -2166,27 +2178,6 @@ Returns the corresponding (logical name . real name) pair."
(setq longest (cons logical real)))
finally return longest))

(defun company-coq-library-path (lib-path mod-name fallback-spec)
"Find a .v file likely to hold the definition of (LIB-PATH MOD-NAME).
May also return a buffer visiting that file. FALLBACK-SPEC is a
module path specification to be used if [Locate Library] points
to a non-existent file (for an example of such a case, try
\[Locate Library Peano] in 8.4pl3)."
(if (and (equal lib-path "")
proof-script-buffer
(or (equal mod-name "Top")
(and (buffer-file-name proof-script-buffer)
(equal (concat mod-name ".v")
(file-name-nondirectory (buffer-file-name proof-script-buffer))))))
proof-script-buffer
(let* ((lib-name (concat lib-path mod-name))
(output (company-coq-ask-prover-swallow-errors (format company-coq-locate-lib-cmd lib-name))))
(or (and output (save-match-data
(when (and (string-match company-coq-locate-lib-output-format output)
(string-match-p company-coq-compiled-regexp (match-string-no-properties 3 output)))
(concat (match-string-no-properties 2 output) ".v"))))
(and fallback-spec (expand-file-name (concat mod-name ".v") (cdr fallback-spec)))))))

(defun company-coq--locate-name (name functions)
"Find location of NAME using FUNCTIONS.
FUNCTIONS are called successively with NAME until one of them
Expand All @@ -2201,11 +2192,19 @@ in that file."
(concat "\\`" (regexp-opt headers) "\\_>[\n[:space:]]+" "\\(" company-coq-symbol-regexp "\\)"))

(defun company-coq--loc-fully-qualified-name (fqn)
"Find source file for fully qualified name FQN."
(let* ((spec (company-coq-longest-matching-path-spec fqn))
(logical (if spec (concat (car spec) ".") ""))
(mod-name (replace-regexp-in-string "\\..*\\'" "" fqn nil nil nil (length logical))))
(company-coq-library-path logical mod-name spec)))
(cl-labels
((recs (fqn)
(message "fqn-loc %s" fqn)
(let* ((output (company-coq-ask-prover-swallow-errors (format company-coq-locate-lib-cmd fqn))))
(or (and output
(save-match-data
(when (and (string-match company-coq-locate-lib-output-format output)
(string-match-p company-coq-compiled-regexp (match-string-no-properties 3 output)))
(cons (match-string-no-properties 2 output) fqn))))
(let* ((prefixfqn (file-name-sans-extension fqn)))
(if (< (length prefixfqn) (length fqn)) (recs prefixfqn)))))))
(recs fqn)));; do if file exists as it was done before
;; (replace-regexp-in-string "_build/default" "" (recs fqn) nil 'literal)

(defun company-coq--fqn-with-regexp-1 (name cmd-format response-format)
"Find qualified name of NAME using CMD-FORMAT and RESPONSE-FORMAT."
Expand All @@ -2218,14 +2217,46 @@ in that file."
"Find qualified name of NAME using CMD-FORMAT and RESPONSE-HEADERS."
(company-coq--fqn-with-regexp-1 name cmd-format (company-coq--loc-output-regexp response-headers)))

(defun company-coq--loc-from-globfile (globfile glob_relative_fqn)
"Find qualified char offset of GLOB_RELATIVE_FQN in GLOBFILE. GLOB_RELATIVE_FQN the fully qualified name (fqn) relative to the fqn of the file, except that it is in the globfile format: the last . is replaced by a space"
(message "looking for %s in globfile %s" glob_relative_fqn globfile)
(-when-let* ((globfile-content (f-read-text globfile))
(startindex (save-match-data
(and (string-match (company-coq-make-headers-regexp-glob glob_relative_fqn) globfile-content)
(match-string-no-properties 2 globfile-content)))))
(string-to-number startindex)))

(defun glob_relative_fqn (vfile_fqn short-name fqn)
"compute the name of this definition as expected to be in the .glob file in the line corresponding to the declartion side. fqn is the fully qualified name (fqn) of this definition. vfile_fqn is the fqn of the .v file corresponding to the .glob file. shortname is the leaf of fqn"
(if (string= (concat vfile_fqn "." short-name) fqn)
(concat "<> " short-name)
(let ((relative_fqn_except_leaf (substring fqn (1+(length vfile_fqn)) (-(1+(length short-name))))));; the middle part of fqn excluding the fully qualified name for the file and excluding the leaf
(concat relative_fqn_except_leaf " " short-name))))

(defun company-coq--loc-fqn-with-regexp (fqn regexp)
"Find location of NAME using CMD-FORMAT and RESPONSE-HEADERS.
Returns a cons as specified by `company-coq--locate-name'."
(or (-when-let* ((loc (company-coq--loc-fully-qualified-name fqn));; will fail iff the definition is in current file
(vfile (concat (replace-regexp-in-string "_build/default" "" (car loc) nil 'literal) ".v"))
Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

to be on the safer side, check that the parent directory of _build has a dune-project file

(globfile (concat (car loc) ".glob"))
(vfile_fqn (cdr loc))
(short-name (replace-regexp-in-string "\\`.*\\." "" fqn))
(glob_name (glob_relative_fqn vfile_fqn short-name fqn)))
(cons vfile (or (company-coq--loc-from-globfile globfile glob_name)
regexp)
))
(cons proof-script-buffer regexp)
))

(defun company-coq--loc-with-regexp (name cmd-format response-headers)
"Find location of NAME using CMD-FORMAT and RESPONSE-HEADERS.
Returns a cons as specified by `company-coq--locate-name'."
(-when-let* ((fqn (company-coq--fqn-with-regexp name cmd-format response-headers))
(loc (company-coq--loc-fully-qualified-name fqn))
(short-name (replace-regexp-in-string "\\`.*\\." "" fqn)))
(cons loc (concat (company-coq-make-headers-regexp response-headers)
"\\s-*\\(" (regexp-quote short-name) "\\)\\_>"))))
(short-name (replace-regexp-in-string "\\`.*\\." "" fqn)))
(company-coq--loc-fqn-with-regexp
fqn
(concat (company-coq-make-headers-regexp response-headers)
"\\s-*\\(" (regexp-quote short-name) "\\)\\_>"))))

(defun company-coq--loc-symbol (symbol)
"Find the location of SYMBOL."
Expand All @@ -2238,11 +2269,14 @@ Returns a cons as specified by `company-coq--locate-name'."
(defun company-coq--loc-constructor (constructor)
"Find the location of CONSTRUCTOR."
;; First check if CONSTRUCTOR is indeed a constructor
(when (company-coq--fqn-with-regexp constructor "Locate %s." '("Constructor"))
;; Then obtain its parent type using Print
(-when-let* ((parent (company-coq--fqn-with-regexp
constructor "Print %s." '("Inductive" "CoInductive" "Variant"))))
(company-coq--loc-with-regexp parent "Locate %s." '("Inductive")))))
(-when-let* ((fqn (company-coq--fqn-with-regexp constructor "Locate %s." '("Constructor")))
(itype (company-coq--fqn-with-regexp
constructor "Print %s." '("Inductive" "CoInductive" "Variant"))))
(company-coq--loc-fqn-with-regexp
fqn
(concat (company-coq-make-headers-regexp '("Inductive" "CoInductive" "Variant"))
"\\s-*\\(" (regexp-quote itype) "\\)\\_>"));; it is hard to find the declaration of a constructor because there is no leading marker unlike declaration of Inductives. so we locate the inductive. of course, if the .glob file is available, this is ignored anyway
))

(defun company-coq--loc-field (field)
"Find the location of FIELD (from a record)."
Expand All @@ -2261,7 +2295,7 @@ Returns a cons as specified by `company-coq--locate-name'."
(let ((candidates (company-coq-candidates-modules module)))
(cl-loop for candidate in candidates
when (string= module candidate)
thereis (cons (company-coq-get-prop 'location candidate) nil))))
thereis (cons (replace-regexp-in-string "_build/default" "" (company-coq-get-prop 'location candidate) nil 'literal) nil))))

(defun company-coq--maybe-complain-docs-not-found (interactive-p doc-type name)
"If INTERACTIVE-P, complain that do DOC-TYPE was found for NAME."
Expand Down Expand Up @@ -2331,6 +2365,7 @@ FQN-FUNCTIONS: see `company-coq-locate-internal'."

(defun company-coq-jump-to-definition-1 (target location fallback)
"Jump to TARGET in LOCATION. If not found, jump to FALLBACK."
(message "jump target is %s" target)
(cond
((bufferp location)
(company-coq--save-location)
Expand All @@ -2341,6 +2376,7 @@ FQN-FUNCTIONS: see `company-coq-locate-internal'."
(t (user-error "Not found: %S" location)))
(company-coq-search-then-scroll-up target fallback #'company-coq--pulse-and-recenter))

;; top level entry point for jump-to-definition.
(defun company-coq-jump-to-definition (name &optional fqn-functions)
"Jump to the definition of NAME, using FQN-FUNCTIONS to find it.
Interactively, use the identifier at point."
Expand Down