package coq-lsp

  1. Overview
  2. Docs
package coq-lsp
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Source file utils.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
86
87
88
89
90
91
(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

(************************************************************************)
(* Coq Language Server Protocol                                         *)
(* Copyright 2022-2023 Inria      -- Dual License LGPL 2.1 / GPL3+      *)
(* Written by: Emilio J. Gallego Arias                                  *)
(************************************************************************)

(* We convert in case of failure to some default values *)

let utf16_offset_of_utf8_offset ~lines ~line ~byte =
  if line < Array.length lines then
    let line = Array.get lines line in
    Lang.Utf.utf16_offset_of_utf8_offset ~line ~offset:byte
  else 0

let to_range ~lines (p : Loc.t) : Lang.Range.t =
  let Loc.{ line_nb; line_nb_last; bol_pos; bol_pos_last; bp; ep; _ } = p in

  let start_line = line_nb - 1 in
  let end_line = line_nb_last - 1 in

  (* cols *)
  let start_col = bp - bol_pos in
  let end_col = ep - bol_pos_last in

  let start_col =
    utf16_offset_of_utf8_offset ~lines ~line:start_line ~byte:start_col
  in
  let end_col =
    utf16_offset_of_utf8_offset ~lines ~line:end_line ~byte:end_col
  in
  Lang.Range.
    { start = { line = start_line; character = start_col; offset = bp }
    ; end_ = { line = end_line; character = end_col; offset = ep }
    }

let to_orange ~lines = Option.map (to_range ~lines)

(* Separation of parsing and execution made upstream API hard to use for us
   :/ *)
let pmeasure (measure, print) fn =
  match measure fn () with
  | Ok _ as r -> Feedback.msg_notice @@ print r
  | Error (exn, _) as r ->
    Feedback.msg_notice @@ print r;
    Exninfo.iraise exn

let with_fail fn =
  try
    fn ();
    CErrors.user_err (Pp.str "The command has not failed!")
  with exn when CErrors.noncritical exn ->
    let exn = Exninfo.capture exn in
    let msg = CErrors.iprint exn in
    Feedback.msg_notice ?loc:None
      Pp.(str "The command has indeed failed with message:" ++ fnl () ++ msg)

let with_ctrl ctrl ~st ~fn =
  let st = State.to_coq st in
  match ctrl with
  | Vernacexpr.ControlTime ->
    pmeasure System.(measure_duration, fmt_transaction_result) fn
  | Vernacexpr.ControlInstructions ->
    pmeasure System.(count_instructions, fmt_instructions_result) fn
  | Vernacexpr.ControlTimeout n -> (
    match Control.timeout (float_of_int n) fn () with
    | None -> Exninfo.iraise (Exninfo.capture CErrors.Timeout)
    | Some x -> x)
  (* fail and succeed *)
  | Vernacexpr.ControlFail ->
    with_fail fn;
    Vernacstate.Interp.invalidate_cache ();
    Vernacstate.unfreeze_full_state st
  | Vernacexpr.ControlSucceed ->
    fn ();
    Vernacstate.Interp.invalidate_cache ();
    Vernacstate.unfreeze_full_state st
  (* Unsupported by coq-lsp, maybe deprecate upstream *)
  | Vernacexpr.ControlRedirect _ -> fn ()

let with_control ~fn ~control ~st =
  List.fold_right (fun ctrl fn () -> with_ctrl ctrl ~st ~fn) control fn ()
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct