new parser for lp files

dune-project

@@ -31,7 +31,6 @@ systems: Dedukti, Coq, HRS, CPF.")
   (dream-pure (>= 1.0.0~alpha2))
   (dream-httpaf (>= 1.0.0~alpha3))
   (dream (>= 1.0.0~alpha6))
-  (menhir (>= 20200624))
   (sedlex (>= 3.2))
   (alcotest :with-test)
   (alt-ergo :with-test)

lambdapi.opam

@@ -25,7 +25,6 @@ depends: [
   "dream-pure" {>= "1.0.0~alpha2"}
   "dream-httpaf" {>= "1.0.0~alpha3"}
   "dream" {>= "1.0.0~alpha6"}
-  "menhir" {>= "20200624"}
   "sedlex" {>= "3.2"}
   "alcotest" {with-test}
   "alt-ergo" {with-test}

src/common/logger.ml

@@ -32,9 +32,11 @@ let update_log_enabled () =
 
 (** [make key name desc] registers a new logger and returns its pp. *)
 let make logger_key logger_name logger_desc =
+
   (* Sanity checks. *)
   if String.length logger_name <> 4 then
     invalid_arg "Logger.make: name must be 4 characters long";
+
   let check data =
     if logger_key  = data.logger_key then
       invalid_arg "Logger.make: key is already used";
@@ -44,6 +46,7 @@ let make logger_key logger_name logger_desc =
   List.iter check Stdlib.(!loggers);
 
   let logger_enabled = ref false in
+
   (* Actual printing function. *)
   let pp fmt =
     Color.update_with_color Stdlib.(!Error.err_fmt);

src/common/pos.ml

@@ -23,7 +23,60 @@ let cmp : pos cmp = fun p1 p2 ->
     (p1.start_line, p1.start_col, (p1.fname, p1.end_line, p1.end_col))
     (p2.start_line, p2.start_col, (p2.fname, p2.end_line, p2.end_col))
 
-(** Convenient short name for an optional position. *)
+(** [cat p1 p2] returns a position starting from [p1] start and ending with
+   [p2] end. The result position uses [p2] fname. *)
+let cat : pos -> pos -> pos = fun p1 p2 ->
+  { fname = p2.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_offset = p2.end_offset }
+
+(** [locate ?fname (p1,p2)] converts the pair of Lexing positions [p1,p2] and
+    filename [fname] into a {!type:pos}. *)
+let locate : ?fname:string -> Lexing.position * Lexing.position -> pos =
+  fun ?fname (p1, p2) ->
+  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
+  let end_offset = p2.pos_cnum in
+  {fname; start_line; start_col; start_offset; end_line; end_col; end_offset }
+
+(** [lexing p] converts a [pos] into a [Lexing.position]. *)
+let lexing (p:pos): Lexing.position =
+  { pos_fname = (match p.fname with None -> "" | Some s -> s)
+  ; pos_lnum = p.start_line
+  ; pos_bol = p.start_offset - p.start_col
+  ; pos_cnum = p.start_offset }
+
+(** [to_string ?print_fname pos] transforms [pos] into a readable string. If
+    [print_fname] is [true] (the default), the filename contained in [pos] is
+    printed. *)
+let to_string : ?print_dirname:bool -> ?print_fname:bool -> pos -> string =
+  fun ?(print_dirname=true) ?(print_fname=true)
+    {fname; start_line; start_col; end_line; end_col} ->
+  let fname =
+    if print_fname then
+      match fname with
+      | None -> ""
+      | Some n -> (if print_dirname then n else Filename.basename n) ^ ":"
+    else ""
+  in
+  if start_line <> end_line then
+    Printf.sprintf "%s%d:%d-%d:%d" fname start_line start_col end_line end_col
+  else if start_col = end_col then
+    Printf.sprintf "%s%d:%d" fname start_line start_col
+  else
+    Printf.sprintf "%s%d:%d-%d" fname start_line start_col end_col
+
+
+
+(** Type of optional positions. *)
 type popt = pos option
 
 (** [equal p1 p2] tells whether [p1] and [p2] denote the same position. *)
@@ -33,46 +86,13 @@ let equal : popt -> popt -> bool = fun p1 p2 ->
   | (None    , None    ) -> true
   | (_       , _       ) -> false
 
-(** Type constructor extending a type (e.g. a piece of abstract syntax) with a
-    a source code position. *)
-type 'a loc =
-  { elt : 'a   (** The element that is being localised.        *)
-  ; pos : popt (** Position of the element in the source code. *) }
-
-(** Localised string type (widely used). *)
-type strloc = string loc
-
-(** [make pos elt] associates the position [pos] to [elt]. *)
-let make : popt -> 'a -> 'a loc = fun pos elt -> { elt ; pos }
-
-(** [none elt] wraps [elt] in a ['a loc] structure without any specific source
-    code position. *)
-let none : 'a -> 'a loc = fun elt -> make None elt
-
-(** [in_pos pos elt] associates the position [pos] to [elt]. *)
-let in_pos : pos -> 'a -> 'a loc = fun p elt -> make (Some p) elt
-
 (** [pos_end po] creates a position from the end of position [po]. *)
 let pos_end : popt -> popt = fun po ->
   match po with
   | None -> None
   | Some p -> Some {p with start_line = p.end_line; start_col = p.end_col}
 
-(** [cat p1 p2] returns a position starting from [p1] start and ending with
-   [p2] end. [p1] and [p2] must have the same filename. *)
-let cat : pos -> pos -> pos = fun p1 p2 ->
-  { fname = p2.fname
-    (*FIXME: temporary fix for
-      https://github.com/Deducteam/lambdapi/issues/1001
-      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_offset = p2.end_offset
-  }
-
+(** [cat] extends and hide the above [cat] function from [pos] to [popt]. *)
 let cat : popt -> popt -> popt = fun p1 p2 ->
   match p1, p2 with
   | Some p1, Some p2 -> Some (cat p1 p2)
@@ -89,27 +109,42 @@ let shift : int -> popt -> popt = fun k p ->
 let after = shift 1
 let before = shift (-1)
 
-(** [to_string ?print_fname pos] transforms [pos] into a readable string. If
-    [print_fname] is [true] (the default), the filename contained in [pos] is
-    printed. *)
-let to_string : ?print_dirname:bool -> ?print_fname:bool -> pos -> string =
-  fun ?(print_dirname=true) ?(print_fname=true)
-    {fname; start_line; start_col; end_line; end_col} ->
-  let fname =
-    if not print_fname then "" else
-    match fname with
-    | None    -> ""
-    | Some(n) ->
-        if print_dirname then n ^ ":"
-        else
-          Filename.basename n ^ ":"
-  in
-  if start_line <> end_line then
-    Printf.sprintf "%s%d:%d-%d:%d" fname start_line start_col end_line end_col
-  else if start_col = end_col then
-    Printf.sprintf "%s%d:%d" fname start_line start_col
-  else
-    Printf.sprintf "%s%d:%d-%d" fname start_line start_col end_col
+(** [lexing_opt p] converts a [popt] into a [Lexing.position]. *)
+let lexing_opt (p:popt): Lexing.position =
+  match p with
+  | None -> {pos_fname=""; pos_lnum=1; pos_bol=0; pos_cnum=0}
+  | Some p -> lexing p
+
+
+
+(** Type constructor extending a type (e.g. a piece of abstract syntax) with a
+    an optional source code position. *)
+type 'a loc =
+  { elt : 'a   (** The element that is being localised.        *)
+  ; pos : popt (** Position of the element in the source code. *) }
+
+(** Localised string type (widely used). *)
+type strloc = string loc
+
+(** [make pos elt] associates the position [pos] to [elt]. *)
+let make : popt -> 'a -> 'a loc = fun pos elt -> { elt ; pos }
+
+(** [none elt] wraps [elt] in a ['a loc] structure without any specific source
+    code position. *)
+let none : 'a -> 'a loc = fun elt -> make None elt
+
+(** [map f loc] applies function [f] on the value of [loc] and keeps the
+    position unchanged. *)
+let map : ('a -> 'b) -> 'a loc -> 'b loc = fun f loc ->
+  {loc with elt = f loc.elt}
+
+(** [in_pos pos elt] associates the position [pos] to [elt]. *)
+let in_pos : pos -> 'a -> 'a loc = fun p elt -> make (Some p) elt
+
+(** [make_pos lps elt] creates a located element from the lexing positions
+   [lps] and the element [elt]. *)
+let make_pos : Lexing.position * Lexing.position -> 'a -> 'a loc =
+  fun lps elt -> in_pos (locate lps) elt
 
 let popt_to_string :
   ?print_dirname:bool -> ?print_fname:bool -> popt -> string =
@@ -119,45 +154,27 @@ let popt_to_string :
     | Some (p) -> to_string ~print_dirname ~print_fname p
 
 (** [pp ppf pos] prints the optional position [pos] on [ppf]. *)
-let pp : popt Lplib.Base.pp = fun ppf p ->
+let pp : popt pp = fun ppf p ->
   string ppf (popt_to_string p)
 
 (** [short ppf pos] prints the optional position [pos] on [ppf]. *)
-let short : popt Lplib.Base.pp = fun ppf p ->
+let short : popt pp = fun ppf p ->
   let print_fname=false in
   string ppf (popt_to_string ~print_fname p)
 
-(** [map f loc] applies function [f] on the value of [loc] and keeps the
-    position unchanged. *)
-let map : ('a -> 'b) -> 'a loc -> 'b loc = fun f loc ->
-  {loc with elt = f loc.elt}
+(** [pp_lexing ppf lps] prints the Lexing.position pair [lps] on [ppf]. *)
+let pp_lexing : (Lexing.position * Lexing.position) pp =
+  fun ppf lps -> short ppf (Some (locate lps))
 
-(** [locate ?fname loc] converts the pair of position [loc] and filename
-    [fname] of the Lexing library into a {!type:pos}. *)
-let locate : ?fname:string -> Lexing.position * Lexing.position -> pos =
-  fun ?fname (p1, p2) ->
-  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
-  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]. *)
-let make_pos : Lexing.position * Lexing.position -> 'a -> 'a loc =
-  fun lps elt -> in_pos (locate lps) elt
 
 (** [print_file_contents escape sep delimiters pos] prints the contents of the
     file at position [pos]. [sep] is the separator replacing each newline
     (e.g. "<br>\n"). [delimiters] is a pair of delimiters used to wrap the
     "unknown location" message returned when the position does not refer to a
     file. [escape] is used to escape the file contents.*)
 let print_file_contents :
-  escape:(string -> string) ->
-    delimiters:(string*string) -> popt Lplib.Base.pp =
+  escape:(string -> string) -> delimiters:(string*string) -> popt pp =
   fun ~escape ~delimiters:(db,de) ppf pos ->
   match pos with
   | Some { fname=Some fname; start_line; start_col; end_line; end_col } ->

src/handle/command.ml

@@ -626,8 +626,8 @@ let get_proof_data : compiler -> sig_state -> p_command -> cmd_output =
   with
   | Timeout                as e -> raise e
   | Fatal(Some(Some(_)),_) as e -> raise e
-  | Fatal(None         ,m)      -> fatal pos "Error on command.@.%s" m
-  | Fatal(Some(None)   ,m)      -> fatal pos "Error on command.@.%s" m
+  | Fatal(None         ,m)      -> fatal pos "%s" m
+  | Fatal(Some(None)   ,m)      -> fatal pos "%s" m
   | e                           ->
       fatal pos "Uncaught exception: %s." (Printexc.to_string e)
 

src/handle/query.ml

@@ -184,9 +184,9 @@ let handle : Sig_state.t -> proof_state option -> p_query -> result =
   let ctxt = Env.to_ctxt env in
   let p = new_problem() in
   match elt with
-  | P_query_search s ->
+  | P_query_search q ->
       let dbpath = Path.default_dbpath in
-      return string (Tool.Indexing.search_cmd_txt ss s ~dbpath)
+      return string (Tool.Indexing.search_cmd_txt_query ss q ~dbpath)
   | P_query_debug(_,_)
   | P_query_verbose(_)
   | P_query_flag(_,_)

src/handle/rewrite.ml

@@ -372,7 +372,7 @@ let swap : eq_config -> term -> term -> term -> term -> term =
    equational lemma that is appied. It handles the full set of SSReflect
    patterns. *)
 let rewrite : Sig_state.t -> problem -> popt -> goal_typ -> bool ->
-              (term, binder) Parsing.Syntax.rw_patt option -> term -> term =
+              (term, binder) Parsing.Syntax.rwpatt option -> term -> term =
   fun ss p pos {goal_hyps=g_env; goal_type=g_type; _} l2r pat t ->
 
   (* Obtain the required symbols from the current signature. *)

src/handle/tactic.ml

@@ -307,29 +307,32 @@ let p_query_of_term (c:config) (pos:popt) (t:term) :p_query =
     | Symb s, ts -> p_query c pos s ts
     | _ -> fatal pos "Unhandled query expression: %a." term t*)
 
+(** [p_term_of_string pos t] turns into a p_term a string literal term [t]
+    that is part of a bigger term obtained by scoping and normalizing of a
+    p_term at position [pos]. *)
 let p_term_of_string (pos:popt) (t:term): p_term =
   match t with
   | Symb s when String.is_string_literal s.sym_name ->
       begin
         let string = remove_quotes s.sym_name in
-        let fname = match pos with Some{fname=Some fn;_} -> fn | _ -> "" in
-        let stream = Parsing.Parser.Lp.parse_term_string fname string in
-        try Stream.next stream with Stream.Failure -> assert false
+        let p = lexing_opt (after s.sym_pos) in
+        Parsing.Parser.Lp.parse_term_string p string
       end
-  | _ -> fatal pos "refine tactic not applied to a term string literal"
+  | _ -> fatal pos "not a string literal"
 
-let p_rw_patt_of_string (pos:popt) (t:term): p_rw_patt option =
+(** [p_rwpatt_of_string pos t] turns into a p_rwpatt option a string literal
+    term [t] that is part of a bigger term obtained by scoping and normalizing
+    of a p_term at position [pos]. *)
+let p_rwpatt_of_string (pos:popt) (t:term): p_rwpatt option =
+  if Logger.log_enabled() then
+    log "p_rwpatt_of_string %a %a" Pos.short pos term t;
   match t with
   | Symb s when String.is_string_literal s.sym_name ->
       let string = remove_quotes s.sym_name in
       if string = "" then None
-      else
-        begin
-          let fname = match pos with Some{fname=Some fn;_} -> fn | _ -> "" in
-          let stream = Parsing.Parser.Lp.parse_rwpatt_string fname string in
-          try Some (Stream.next stream) with Stream.Failure -> assert false
-        end
-  | _ -> fatal pos "rewrite tactic not applied to a pattern string literal"
+      else let p = lexing_opt (after s.sym_pos) in
+           Some (Parsing.Parser.Lp.parse_rwpatt_string p string)
+  | _ -> fatal pos "not a string literal"
 
 let is_right (pos:popt) (t:term): bool =
   match t with
@@ -343,8 +346,9 @@ let is_right (pos:popt) (t:term): bool =
       end
   | _ -> fatal pos "rewrite tactic not applied to a side string literal"
 
-(** [p_tactic t] interprets the term [t] as a tactic. *)
-let p_tactic (ss:Sig_state.t) (pos:popt) :int StrMap.t -> term -> p_tactic =
+(** [p_tactic ss pos idmap t] interprets as a tactic the term [t] obtained by
+    scoping and normalization of a p_term at position [pos]. *)
+let p_tactic (ss:Sig_state.t) (pos:popt): int StrMap.t -> term -> p_tactic =
   let c = get_config ss pos in
   let rec tac idmap t = Pos.make pos (tac_aux idmap t)
   and tac_aux idmap t =
@@ -383,7 +387,7 @@ let p_tactic (ss:Sig_state.t) (pos:popt) :int StrMap.t -> term -> p_tactic =
             | T_repeat, _ -> assert false
             | T_rewrite, [side;pat;_;t] ->
                 P_tac_rewrite(is_right pos side,
-                              p_rw_patt_of_string pos pat, p_term pos idmap t)
+                              p_rwpatt_of_string pos pat, p_term pos idmap t)
             | T_rewrite, _ -> assert false
             | T_set, [t1;_;t2] ->
                 P_tac_set(p_ident_of_sym pos t1, p_term pos idmap t2)
@@ -632,7 +636,7 @@ let rec handle :
       let g = List.fold_left remove g ids in
       {ps with proof_goals = g::gs}
   | P_tac_rewrite(l2r,pat,eq) ->
-      let pat = Option.map (Scope.scope_rw_patt ss env) pat in
+      let pat = Option.map (Scope.scope_rwpatt ss env) pat in
       let p = new_problem() in
       tac_refine pos ps gt gs p
         (Rewrite.rewrite ss p pos gt l2r pat (scope eq))
@@ -683,7 +687,7 @@ let rec handle :
   | P_tac_eval pt ->
       let t = Eval.snf (Env.to_ctxt env) (scope pt) in
       let idmap = get_names g in
-      handle ss sym_pos prv ps (p_tactic ss pos idmap t)
+      handle ss sym_pos prv ps (p_tactic ss pt.pos idmap t)
 
 (** Representation of a tactic output. *)
 type tac_output = proof_state * Query.result
@@ -700,7 +704,7 @@ let handle :
     ps, Query.handle ss (Some ps) q
   | _ ->
   match ps.proof_goals with
-  | [] -> fatal pos "No remaining goals."
+  | [] -> fatal pos "No remaining goal."
   | g::_ ->
     if Logger.log_enabled() then log ("goal %a") Goal.pp_no_hyp g;
     handle ss sym_pos prv ps tac, None

src/parsing/dune

@@ -3,11 +3,9 @@
  (public_name lambdapi.parsing)
  (modules :standard)
  (preprocess (pps sedlex.ppx))
- (libraries camlp-streams lambdapi.core menhirLib pratter sedlex sedlex.ppx lambdapi.common)
+ (libraries camlp-streams lambdapi.core pratter sedlex sedlex.ppx lambdapi.common)
  (flags -w +3))
 
-(menhir (flags --explain --external-tokens LpLexer) (modules lpParser))
-
 (ocamllex dkLexer)
 
 (menhir (flags --explain --external-tokens DkTokens) (modules dkParser))