package vsrocq-language-server

  1. Overview
  2. Docs
VSRocq language server

Install 

dune-project
 Dependency

github.com Readme Edit opam file Versions (8)

Authors

  1. E
    Enrico Tassi
  2. M
    Maxime Dénès
  3. R
    Romain Tetley

Maintainers

  1. E
    Enrico Tassi <enrico.tassi@inria.fr>

Sources

vsrocq-language-server-2.5.0.tar.gz
md5=15c22fee2131c4b3dae4258e8a4484f6
sha512=b5ab3eea5bb6af643d635781e741a7a7b217fcc33e84c2c9e3448962118a63e174569ef6069c50af2ab57508d5cef476a8cfade14957a9654b1fea16c29a08b9

doc/src/vsrocq-language-server.dm/utilities.ml.html

Source file utilities.ml

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
(**************************************************************************)
(*                                                                        *)
(*                                 VSRocq                                  *)
(*                                                                        *)
(*                   Copyright INRIA and contributors                     *)
(*       (see version control and README file for authors & dates)        *)
(*                                                                        *)
(**************************************************************************)
(*                                                                        *)
(*   This file is distributed under the terms of the MIT License.         *)
(*   See LICENSE file.                                                    *)
(*                                                                        *)
(**************************************************************************)

open Types

let Log log = Log.mk_log "utilities"

let shift_loc ~start ~offset loc =
  let (loc_start, loc_stop) = Loc.unloc loc in
  if loc_start >= start then Loc.shift_loc offset offset loc
  else if loc_stop > start then Loc.shift_loc 0 offset loc
  else loc

let shift_feedback ~start ~offset (level, oloc, qf, msg as feedback) =
  match oloc with
  | None -> feedback
  | Some loc ->
    let loc' = shift_loc ~start ~offset loc in
    if loc' == loc then feedback else (level, Some loc', qf, msg)

let shift_1qf ~start ~offset q =
  let loc = Quickfix.loc q in
  let loc' = shift_loc ~start ~offset loc in
  if loc' == loc then q else Quickfix.make ~loc:loc' (Quickfix.pp q)

let shift_quickfix ~start ~offset qf =
  Option.Smart.map (CList.Smart.map (shift_1qf ~start ~offset)) qf

let shift_checking_result ~start ~offset = function
  | Success _ | Failure ((None,_),_,_) as x -> x
  | (Failure ((Some loc,e),qf,st)) as x ->
      let loc' = shift_loc ~start ~offset loc in
      let qf' = shift_quickfix ~start ~offset qf in
      if loc' == loc && qf' == qf then x else Failure ((Some loc',e),qf',st)

let doc_id = ref (-1)
let fresh_doc_id () = incr doc_id; !doc_id

let feedback_pipe_cleanup { rocq_feeder; sel_feedback_queue; sel_cancellation_handle } =
  Feedback.del_feeder rocq_feeder;
  Queue.clear sel_feedback_queue;
  Sel.Event.cancel sel_cancellation_handle

(** Returns the vernac state after the sentence *)
let get_vernac_state (checked : sentence_checking_result option) =
  match checked with
  | None -> log (fun () -> "Cannot find state for get_vernac_state"); None
  | Some (Failure (_,_,None)) -> log (fun () -> "State requested after error with no state"); None
  | Some (Success None) -> log (fun () -> "State requested in a remotely checked state"); None
  | Some (Success (Some st))
  | Some (Failure (_,_, Some st)) -> Some st

[%%if rocq ="8.18" || rocq ="8.19"]
let vernacstate_synterp_parsing x = x.Vernacstate.synterp.Vernacstate.Synterp.parsing
[%%else]
let vernacstate_synterp_parsing x = Vernacstate.(Synterp.parsing x.synterp)
[%%endif]

let option_to_list = function
  | None -> []
  | Some x -> [x]

[%%if rocq = "8.18" || rocq = "8.19"]
let constrs_of_local_binder = function
  | Constrexpr.CLocalAssum (_, _, ty) -> [ty]
  | Constrexpr.CLocalDef (_, e, e_opt) -> e :: option_to_list e_opt
  | Constrexpr.CLocalPattern _ -> []
[%%else]
let constrs_of_local_binder = function
  | Constrexpr.CLocalAssum (_, _, _, ty) -> [ty]
  | Constrexpr.CLocalDef (_, _, e, e_opt) -> e :: option_to_list e_opt
  | Constrexpr.CLocalPattern _ -> []
[%%endif]