package vsrocq-language-server

  1. Overview
  2. Docs
VSRocq language server

Install 

dune-project
 Dependency

github.com Readme Edit opam file Versions (7)

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.4.3.tar.gz
md5=fbc594cef4ba2469882803c12fb5cd51
sha512=2f93d42591e9030f2786f1d9a9783ed92c2cd299ccfd99d0a65f3b5984762f61c1bec3b3f854a557f72ca6c309e9c1eaec27065f0ee1a9cb9dfa4a7ee05dac15

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
(**************************************************************************)
(*                                                                        *)
(*                                 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

let context_of_vernac_state (st : Vernacstate.t) =
  let st = st.Vernacstate.interp in
  Vernacstate.Interp.unfreeze_interp_state st;
  begin match st.lemmas with
  | None ->
    let env = Global.env () in
    let sigma = Evd.from_env env in
    sigma, env
  | Some lemmas ->
    let open Declare in
    let open Vernacstate in
    lemmas |> LemmaStack.with_top ~f:Proof.get_current_context
  end

(** 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


let get_proof_context (checked : sentence_checking_result option) =
  match checked with
  | None -> log (fun () -> "Cannot find state for get_proof_context"); None
  | Some (Failure _) -> log (fun () -> "Context requested in error state"); None
  | Some (Success None) -> log (fun () -> "Context requested in a remotely checked state"); None
  | Some (Success (Some st)) -> Some (context_of_vernac_state st)