diff --git a/src/parser/loc.ml b/src/parser/loc.ml index f748500c..babf5634 100644 --- a/src/parser/loc.ml +++ b/src/parser/loc.ml @@ -1,3 +1,15 @@ +module Input : sig + type t + + val string : string -> t + val file : string -> t + val to_pploc_input : t -> Pp_loc.Input.t +end = struct + include Pp_loc.Input + + let to_pploc_input x = x +end + type position = Position.t type t = { start: position; end_: position } @@ -11,3 +23,13 @@ let merge a b : t = let of_lexloc ((p1, p2) : Lexing.position * Lexing.position) : t = { start = Position.of_lexpos p1; end_ = Position.of_lexpos p2 } + +(** Pretty print using pp_loc *) +let pp_loc ?max_lines ~(input : Input.t) out (l : t list) : unit = + let input = Input.to_pploc_input input in + let to_pploc (self : t) : Pp_loc.loc = + Position.to_pploc_pos self.start, Position.to_pploc_pos self.end_ + in + let l = List.map to_pploc l in + + Pp_loc.pp ?max_lines ~input out l diff --git a/src/parser/position.ml b/src/parser/position.ml index 6b6d527e..921ef225 100644 --- a/src/parser/position.ml +++ b/src/parser/position.ml @@ -24,3 +24,6 @@ let pp out self = Format.fprintf out "at line %d, column %d" self.line self.col (** Build position from a lexing position *) let of_lexpos (p : Lexing.position) : t = { file = p.pos_fname; line = p.pos_lnum; col = p.pos_cnum - p.pos_bol } + +let to_pploc_pos (self : t) : Pp_loc.Position.t = + Pp_loc.Position.of_line_col self.line (self.col + 1) diff --git a/unittest/parser/p1.expected b/unittest/parser/p1.expected index 259ab264..47ac08e9 100644 --- a/unittest/parser/p1.expected +++ b/unittest/parser/p1.expected @@ -1,14 +1,24 @@ t1: f (g x) y -loc(t1): at line 1, column 0 - at line 1, column 9 +loc(t1): 1 | f (g x) y + ^^^^^^^^^ + t2: let x := 1 in f (f x 2) -loc(t2): at line 1, column 0 - at line 1, column 22 +loc(t2): 1 | let x:= 1 in f (f x 2) + ^^^^^^^^^^^^^^^^^^^^^^ + t3: let l := map f (list 1 2 3) in let l2 := rev l in = (rev l2) l -loc(t3): at line 1, column 0 - at line 1, column 60 +loc(t3): 1 | let l := map f (list 1 2 3) in + 1 | let l2 := rev l in rev l2 = l + t4: let assm := ==> (is_foo p) (= (filter p l) nil) in true -loc(t4): at line 1, column 0 - at line 1, column 51 +loc(t4): 1 | let assm := is_foo p ==> (filter p l = nil) in true + ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + t5: let f := lam (x y : int) (z : bool). (= (+ x y) z) and g := lam x. (f (f x)) in is_g g -loc(t5): at line 1, column 0 - at line 1, column 84 +loc(t5): 1 | let f := fn (x y : int) (z:bool). ( x+ y) = z + 1 | and g := fn x. f (f x) in is_g g + d1: def f (x y : list int) : list int := if (= x 0) y whatever; #ty f; diff --git a/unittest/parser/p1.ml b/unittest/parser/p1.ml index c10ce7fb..0b762214 100644 --- a/unittest/parser/p1.ml +++ b/unittest/parser/p1.ml @@ -12,10 +12,12 @@ let () = let test_term_str what s = let t = P.term_of_string s in + let input = Loc.Input.string s in match t with | Ok t -> Fmt.printf "%s: %a@." what A.pp_term t; - Fmt.printf "loc(%s): %a@." what Loc.pp (A.loc t) + (*Fmt.printf "loc(%s): %a@." what Loc.pp @@ A.loc t*) + Fmt.printf "loc(%s): %a@." what (Loc.pp_loc ~max_lines:5 ~input) [ A.loc t ] | Error err -> Fmt.printf "FAIL:@ error while parsing %S:@ %a@." what P.Error.pp err