Skip to content

Commit

Permalink
Merge pull request #126 from GaloisInc/sc/position-range-shadow
Browse files Browse the repository at this point in the history
CN server: enhance abstractions for `Position`s and `Range`s
  • Loading branch information
samcowger authored Nov 4, 2024
2 parents ccd67a0 + 28f6e42 commit 7c4bc32
Show file tree
Hide file tree
Showing 5 changed files with 79 additions and 17 deletions.
27 changes: 10 additions & 17 deletions cn-lsp/server/lib/lspCn.ml
Original file line number Diff line number Diff line change
Expand Up @@ -6,10 +6,8 @@ module CF = Cerb_frontend
module CG = Cerb_global

(* LSP *)
module LspDocumentUri = Lsp.Types.DocumentUri
module LspPosition = Lsp.Types.Position
module LspRange = Lsp.Types.Range
module LspDiagnostic = Lsp.Types.Diagnostic
module LspDocumentUri = Lsp.Types.DocumentUri

module CerbM = struct
type error = CF.Errors.error
Expand All @@ -28,21 +26,16 @@ end
module Cerb = struct
open CerbM

let loc_to_source_range (loc : Cerb_location.t) : (string * LspRange.t) option =
let posn_to_lsp (p : Lexing.position) : LspPosition.t =
LspPosition.create ~line:(p.pos_lnum - 1) ~character:(p.pos_cnum - p.pos_bol)
let loc_to_source_range (loc : Cerb_location.t) : (string * Range.t) option =
let path_opt =
match Cn.Locations.start_pos loc, Cn.Locations.end_pos loc with
| Some pos, _ | _, Some pos -> Some pos.pos_fname
| _ -> None
in
match Cn.Locations.start_pos loc, Cn.Locations.end_pos loc with
| Some start, Some end_ ->
(* TODO: handle when start and end have different filenames? *)
let path = start.pos_fname in
let range = LspRange.create ~start:(posn_to_lsp start) ~end_:(posn_to_lsp end_) in
Some (path, range)
| Some pos, None | None, Some pos ->
let path = pos.pos_fname in
let range = LspRange.create ~start:(posn_to_lsp pos) ~end_:(posn_to_lsp pos) in
Some (path, range)
| None, None -> None
let range_opt = Range.of_cerb_loc loc in
match path_opt, range_opt with
| Some path, Some range -> Some (path, range)
| _ -> None
;;

let error_to_string ((loc, cause) : error) : string = CF.Pp_errors.to_string (loc, cause)
Expand Down
20 changes: 20 additions & 0 deletions cn-lsp/server/lib/position.ml
Original file line number Diff line number Diff line change
@@ -0,0 +1,20 @@
open! Base

type t = Lsp.Types.Position.t

let create ~(line : int) ~(character : int) = Lsp.Types.Position.create ~line ~character
let eq (p1 : t) (p2 : t) : bool = p1.line = p2.line && p1.character = p2.character

let lt (p1 : t) (p2 : t) : bool =
p1.line < p2.line || (p1.line = p2.line && p1.character < p2.character)
;;

let le (p1 : t) (p2 : t) : bool = lt p1 p2 || eq p1 p2

let gt (p1 : t) (p2 : t) : bool =
p1.line > p2.line || (p1.line = p2.line && p1.character > p2.character)
;;

let ge (p1 : t) (p2 : t) : bool = gt p1 p2 || eq p1 p2
let compare (p1 : t) (p2 : t) : int = if lt p1 p2 then -1 else if gt p1 p2 then 1 else 0
let to_string (p : t) : string = Printf.sprintf "%i:%i" p.line p.character
12 changes: 12 additions & 0 deletions cn-lsp/server/lib/position.mli
Original file line number Diff line number Diff line change
@@ -0,0 +1,12 @@
open! Base

type t = Lsp.Types.Position.t

val create : line:int -> character:int -> t
val compare : t -> t -> int
val lt : t -> t -> bool
val le : t -> t -> bool
val eq : t -> t -> bool
val ge : t -> t -> bool
val gt : t -> t -> bool
val to_string : t -> string
26 changes: 26 additions & 0 deletions cn-lsp/server/lib/range.ml
Original file line number Diff line number Diff line change
@@ -0,0 +1,26 @@
open! Base

type t = Lsp.Types.Range.t

let create ~(start : Position.t) ~(end_ : Position.t) : t =
Lsp.Types.Range.create ~start ~end_
;;

let to_string (range : t) : string =
Printf.sprintf "%s-%s" (Position.to_string range.start) (Position.to_string range.end_)
;;

let ( |--| ) ((l1, c1) : int * int) ((l2, c2) : int * int) : t =
create
~start:(Position.create ~line:l1 ~character:c1)
~end_:(Position.create ~line:l2 ~character:c2)
;;

let of_cerb_loc (loc : Cerb_location.t) : t option =
match Cerb_location.to_cartesian loc with
| None -> None
| Some ((l1, c1), (l2, c2)) ->
let start = Position.create ~line:l1 ~character:c1 in
let end_ = Position.create ~line:l2 ~character:c2 in
Some (create ~start ~end_)
;;
11 changes: 11 additions & 0 deletions cn-lsp/server/lib/range.mli
Original file line number Diff line number Diff line change
@@ -0,0 +1,11 @@
open! Base

type t = Lsp.Types.Range.t

val create : start:Position.t -> end_:Position.t -> t
val to_string : t -> string

(** Convenience notation: [(begin_line, begin_char) |--| (end_line, end_char)] *)
val ( |--| ) : int * int -> int * int -> t

val of_cerb_loc : Cerb_location.t -> t option

0 comments on commit 7c4bc32

Please sign in to comment.