[pure] [lsp] Try to recover unit testing of pure interface

PR #289 silently removed important unit tests in the Pure module.

We fix this, in particular:

- we add parsing offsets to LP's position type (this is very
  convenient for certain operations.

- we add a new parsing API in pure to allow parsing resumption

- we add new tests, including parsing resumption.

- we fix `Command.equal` as to have equality functions ignore
positions.

Co-authored-by: Alidra <40537601+Alidra@users.noreply.github.com>

Author: ejgallego

lambdapi.opam

@@ -38,6 +38,8 @@ depends: [
   "odoc" {with-doc}
   "lwt_ppx" {>= "1"}
   "uri" {>= "1.1"}
+  # tests
+  "ppx_inline_test" { with-test }
 ]
 build: [
   ["dune" "subst"] {dev}

src/common/pos.ml

@@ -5,11 +5,14 @@ open Lplib open Base
 (** Type of a position, corresponding to a continuous range of characters in a
     (utf8-encoded) source. *)
 type pos =
-  { fname      : string option (** File name for the position.       *)
-  ; start_line : int (** Line number of the starting point.          *)
-  ; start_col  : int (** Column number (utf8) of the starting point. *)
-  ; end_line   : int (** Line number of the ending point.            *)
-  ; end_col    : int (** Column number (utf8) of the ending point.   *) }
+  { fname        : string option (** File name for the position.       *)
+  ; start_line   : int (** Line number of the starting point.          *)
+  ; start_col    : int (** Column number (utf8) of the starting point. *)
+  ; start_offset : int (** Number of chars since the beginning of the document for the starting point *)
+  ; end_line     : int (** Line number of the ending point.            *)
+  ; end_col      : int (** Column number (utf8) of the ending point.   *)
+  ; end_offset   : int (** Number of chars since the beginning of the document for the ending point *)
+  }
 
 (** Total comparison function on pos. *)
 let cmp : pos cmp = fun p1 p2 ->
@@ -62,8 +65,11 @@ let cat : pos -> pos -> pos = fun p1 p2 ->
       if p1.fname <> p2.fname then invalid_arg __LOC__ else p1.fname*)
   ; start_line = p1.start_line
   ; start_col = p1.start_col
+  ; start_offset = p1.start_offset
   ; end_line = p2.end_line
-  ; end_col = p2.end_col }
+  ; end_col = p2.end_col
+  ; end_offset = p2.end_offset
+  }
 
 let cat : popt -> popt -> popt = fun p1 p2 ->
   match p1, p2 with
@@ -131,9 +137,11 @@ let locate : ?fname:string -> Lexing.position * Lexing.position -> pos =
   let fname = if p1.pos_fname = "" then fname else Some(p1.pos_fname) in
   let start_line = p1.pos_lnum in
   let start_col = p1.pos_cnum - p1.pos_bol in
+  let start_offset = p1.pos_cnum in
   let end_line = p2.pos_lnum in
   let end_col = p2.pos_cnum - p2.pos_bol in
- {fname; start_line; start_col; end_line; end_col}
+  let end_offset = p2.pos_cnum in
+  {fname; start_line; start_col; start_offset; end_line; end_col; end_offset }
 
 (** [make_pos lps elt] creates a located element from the lexing positions
    [lps] and the element [elt]. *)

src/export/coq.ml

@@ -132,7 +132,7 @@ let set_encoding : string -> unit = fun f ->
     (fun i b ->
       if not b then
         let pos =
-          Some {fname=Some f;start_line=0;start_col=0;end_line=0;end_col=0}
+          Some {fname=Some f;start_line=0;start_col=0;start_offset=0;end_line=0;end_col=0;end_offset=0}
         in fatal pos "Builtin %s undefined." (name_of_index i))
     found
 

src/lsp/lp_doc.ml

@@ -138,8 +138,10 @@ let new_doc ~uri ~version ~text =
           fname = Some(uri);
           start_line = 0;
           start_col  = 0;
+          start_offset  = 0;
           end_line = 0;
-          end_col = 0
+          end_col = 0;
+          end_offset  = 0
         } in
       (None, [(1, msg), Some(loc)])
   in
@@ -161,8 +163,10 @@ let dummy_loc =
     Pos.{ fname = None
         ; start_line = 1
         ; start_col = 1
+        ; start_offset = -1
         ; end_line = 2
         ; end_col = 2
+        ; end_offset = -1
         }
 
 let check_text ~doc =

src/lsp/lp_lsp.ml

@@ -64,8 +64,10 @@ let do_check_text ofmt ~doc =
           fname = Some(doc.uri);
           start_line = 0;
           start_col  = 0;
+          start_offset  = 0;
           end_line = 0;
-          end_col = 0
+          end_col = 0;
+          end_offset  = 0;
         } in
       (doc, Lp_doc.mk_error ~doc loc msg)
   in

src/parsing/parser.ml

@@ -15,6 +15,8 @@ let parser_fatal : Pos.pos -> ('a,'b) koutfmt -> 'a = fun pos fmt ->
 
 (** Module type of a parser. *)
 module type PARSER = sig
+  type lexbuf
+
   val parse : in_channel -> Syntax.ast
   (** [parse inchan] returns a stream of commands parsed from
       channel [inchan]. Commands are parsed lazily and the channel is
@@ -27,11 +29,16 @@ module type PARSER = sig
   val parse_string : string -> string -> Syntax.ast
   (** [parse_string f s] returns a stream of parsed commands from string [s]
       which comes from file [f] ([f] can be anything). *)
+
+  val parse_from_lexbuf : lexbuf -> Syntax.ast
+  (** [parse_from_lexbuf lexbuf] is the same than [parse_string] but with an
+      already created lexbuf *)
+
 end
 
 module Lp :
 sig
-  include PARSER
+  include PARSER with type lexbuf := Sedlexing.lexbuf
 
   val parse_term : in_channel -> Syntax.p_term Stream.t
   (** [parse inchan] returns a stream of terms parsed from
@@ -57,6 +64,10 @@ sig
       string [s] which comes from file [f] ([f] can be anything). *)
 
   val parse_qid : string -> Core.Term.qident
+
+  val parse_from_lexbuf : Sedlexing.lexbuf -> Syntax.ast
+  (** [parse_from_lexbuf lexbuf] Same than [parse_string] but with an already created lexbuf *)
+
   end
 = struct
 
@@ -97,6 +108,9 @@ sig
   let parse_string ~grammar_entry fname s =
     stream_of_lexbuf ~grammar_entry ~fname (Sedlexing.Utf8.from_string s)
 
+  let parse_from_lexbuf ~grammar_entry lexbuf =
+    stream_of_lexbuf ~grammar_entry ?fname:None lexbuf
+
   let parse_term = parse ~grammar_entry:LpParser.term_alone
   let parse_term_string = parse_string ~grammar_entry:LpParser.term_alone
   let parse_rwpatt_string =
@@ -113,10 +127,12 @@ sig
   let parse_string = parse_string ~grammar_entry:LpParser.command
   let parse_file = parse_file ~grammar_entry:LpParser.command
 
+  let parse_from_lexbuf = parse_from_lexbuf ~grammar_entry:LpParser.command
+
 end
 
 (** Parsing dk syntax. *)
-module Dk : PARSER = struct
+module Dk : PARSER with type lexbuf := Lexing.lexbuf = struct
 
   let token : Lexing.lexbuf -> DkTokens.token =
     let r = ref DkTokens.EOF in fun lb ->
@@ -156,6 +172,8 @@ module Dk : PARSER = struct
     stream_of_lexbuf ~inchan ~fname (Lexing.from_channel inchan)
 
   let parse_string fname s = stream_of_lexbuf ~fname (Lexing.from_string s)
+
+  let parse_from_lexbuf lexbuf = stream_of_lexbuf ?fname:None lexbuf
 end
 
 (* Include parser of new syntax so that functions are directly available.*)

src/parsing/syntax.ml

@@ -296,6 +296,10 @@ type p_modifier_aux =
 
 type p_modifier = p_modifier_aux loc
 
+(* ppx ? *)
+let eq_p_modifier { elt = m1; _} {elt = m2; _} =
+  m1 = m2
+
 let is_prop {elt; _} = match elt with P_prop _ -> true | _ -> false
 let is_opaq {elt; _} = match elt with P_opaq -> true | _ -> false
 let is_expo {elt; _} = match elt with P_expo _ -> true | _ -> false
@@ -462,7 +466,7 @@ let eq_p_symbol : p_symbol eq = fun
   { p_sym_mod=p_sym_mod2; p_sym_nam=p_sym_nam2; p_sym_arg=p_sym_arg2;
     p_sym_typ=p_sym_typ2; p_sym_trm=p_sym_trm2; p_sym_prf=p_sym_prf2;
     p_sym_def=p_sym_def2} ->
-  p_sym_mod1 = p_sym_mod2
+  List.eq eq_p_modifier p_sym_mod1 p_sym_mod2
   && eq_p_ident p_sym_nam1 p_sym_nam2
   && List.eq eq_p_params p_sym_arg1 p_sym_arg2
   && Option.eq eq_p_term p_sym_typ1 p_sym_typ2

src/pure/dune

@@ -2,5 +2,7 @@
  (name pure)
  (public_name lambdapi.pure)
  (modules :standard)
+ (inline_tests (deps tests/foo.lp tests/lambdapi.pkg))
+ (preprocess (pps ppx_inline_test))
  (libraries camlp-streams lambdapi.handle lambdapi.core)
  (flags -w +3))