Simon Génier pushed to branch source-spans-2 at Stefan / Typer

Commits: 8cfa2243 by Simon Génier at 2021-09-30T11:39:27-04:00 Locations now track their end points.

- - - - -

9 changed files:

- src/debug.ml - src/elab.ml - src/eval.ml - src/lexer.ml - src/opslexp.ml - src/prelexer.ml - src/sexp.ml - src/source.ml - tests/lexer_test.ml

Changes:

===================================== src/debug.ml ===================================== @@ -45,20 +45,22 @@ let print_info (message : string) (location : Source.Location.t) : unit =

(* Print aPretokens *) let debug_pretokens_print pretoken = - print_string " "; + print_string " ";

- match pretoken with - | Preblock(loc, pts,_) - -> print_info "Preblock: " loc; - print_string "{"; pretokens_print pts; print_string " }" + match pretoken with + | Preblock (loc, pts) + -> print_info "Preblock: " loc; + print_string "{"; + pretokens_print pts; + print_string " }"

- | Pretoken(loc, str) - -> print_info "Pretoken: " loc; - print_string ("'" ^ str ^ "'"); + | Pretoken (loc, str) + -> print_info "Pretoken: " loc; + print_string ("'" ^ str ^ "'");

- | Prestring(loc, str) - -> print_info "Prestring: " loc; - print_string (""" ^ str ^ """) + | Prestring (loc, str) + -> print_info "Prestring: " loc; + print_string (""" ^ str ^ """)

(* Print a List of Pretokens *) let debug_pretokens_print_all pretokens = @@ -70,7 +72,7 @@ let debug_sexp_print sexp = | Symbol(_, "") -> print_string "Epsilon " (* "ε" *)

- | Block(loc, pts, _) + | Block(loc, pts) -> print_info "Block: " loc; print_string "{"; pretokens_print pts; print_string " }"

===================================== src/elab.ml ===================================== @@ -1516,11 +1516,11 @@ let sform_immediate ctx loc sargs ot = | [(String _) as se] -> mkImm (se), Inferred DB.type_string | [(Integer _) as se] -> mkImm (se), Inferred DB.type_int | [(Float _) as se] -> mkImm (se), Inferred DB.type_float - | [Block (_sl, pts, _el)] + | [Block (_location, pts)] -> let grm = ectx_get_grammar ctx in - let tokens = lex default_stt pts in - let (se, _) = sexp_parse_all grm tokens None in - elaborate ctx se ot + let tokens = lex default_stt pts in + let (se, _) = sexp_parse_all grm tokens None in + elaborate ctx se ot | [_se] -> (sexp_error loc ("Non-immediate passed to ##typer-immediate"); sform_dummy_ret ctx loc)

===================================== src/eval.ml ===================================== @@ -355,13 +355,14 @@ let make_block loc _depth args_val = match args_val with (* From what would we like to make a block? *) | [Vstring str] -> let source = new Source.source_string str in - Vsexp (Block (loc, (Prelexer.prelex source), loc)) + Vsexp (Block (loc, (Prelexer.prelex source))) | _ -> error loc "Sexp.block expects one string as argument"

-let reader_parse loc _depth args_val = match args_val with - | [Velabctx ectx; Vsexp (Block (_,toks,_))] -> - let grm = ectx_get_grammar ectx in - o2v_list (sexp_parse_all_to_list grm (Lexer.lex default_stt toks) (Some ";")) +let reader_parse loc _depth = function + | [Velabctx ectx; Vsexp (Block (_, toks))] + -> let grm = ectx_get_grammar ectx in + let tokens = Lexer.lex default_stt toks in + o2v_list (sexp_parse_all_to_list grm tokens (Some ";")) | [Velabctx _; s] -> (warning loc "Reader.parse do nothing without a Block"; s) | _ -> error loc "Reader.parse expects an ElabContext and a Block as argument"

@@ -627,17 +628,17 @@ and sexp_dispatch loc depth args = | _ -> value_fatal loc sxp "sexp_dispatch expects a Sexp as 1st arg" in

match sxp with - | Node (op, s) -> eval_call nd [Vsexp op; o2v_list s] - | Symbol (_ , s) -> eval_call sym [Vstring s] - | String (_ , s) -> eval_call str [Vstring s] - | Integer (_ , i) -> eval_call it [Vinteger i] - | Float (_ , f) -> eval_call flt [Vfloat f] - | Block (_ , _, _) as b -> - (* I think this code breaks what Blocks are. *) - (* We delay parsing but parse with default_stt and default_grammar... *) - (*let toks = Lexer.lex default_stt s in - let s = sexp_parse_all_to_list default_grammar toks (Some ";") in*) - eval_call blk [Vsexp b] + | Node (op, s) -> eval_call nd [Vsexp op; o2v_list s] + | Symbol (_ , s) -> eval_call sym [Vstring s] + | String (_ , s) -> eval_call str [Vstring s] + | Integer (_ , i) -> eval_call it [Vinteger i] + | Float (_ , f) -> eval_call flt [Vfloat f] + | Block (_ , _) as b -> + (* I think this code breaks what Blocks are. We delay parsing but parse + with default_stt and default_grammar... *) + (* let toks = Lexer.lex default_stt s in + let s = sexp_parse_all_to_list default_grammar toks (Some ";") in*) + eval_call blk [Vsexp b]

(* -------------------------------------------------------------------------- *) and print_eval_result i lxp =

===================================== src/lexer.ml ===================================== @@ -127,7 +127,7 @@ let lex_symbol

| CKinner prec' -> let left = mksym start_point escaped in - let op_location = source#location in + let op_point = source#point in

(* To be considered `inner`, an operator char needs to have something on its LHS or its RHS, otherwise, treat it as a @@ -142,7 +142,8 @@ let lex_symbol in if lhs_p || rhs_p || lf dummy_epsilon <> dummy_epsilon then - let op = hSymbol (op_location, Printf.sprintf "__%c__" c) in + let op_text, op_location = source#slice op_point in + let op = hSymbol (op_location, Printf.sprintf "__%s__" op_text) in let lf' = if prec' > prec then fun s -> lf (Node (op, [left; s])) @@ -210,14 +211,14 @@ let lex (token_env : token_env) (pretokens : pretoken list) : sexp list = match pretokens with | [] -> List.rev acc

- | Preblock (start_location, block_pretokens, end_location) :: pretokens' - -> loop pretokens' (Block (start_location, block_pretokens, end_location) :: acc) + | Preblock (location, block_pretokens) :: pretokens' + -> loop pretokens' (Block (location, block_pretokens) :: acc)

| Prestring (location, text) :: pretokens' -> loop pretokens' (String (location, text) :: acc)

- | Pretoken ({file; line; column}, name) :: pretokens' - -> let source = new Source.source_string ~file ~line ~column name in + | Pretoken ({file; start_line = l; start_column = c; _}, name) :: pretokens' + -> let source = new Source.source_string ~file ~line:l ~column:c name in let tokens = split_presymbol token_env source in loop pretokens' (List.rev_append tokens acc) in

===================================== src/opslexp.ml ===================================== @@ -601,7 +601,7 @@ and check'' erased ctx e = | Imm (Float (_, _)) -> DB.type_float | Imm (Integer (_, _)) -> DB.type_int | Imm (String (_, _)) -> DB.type_string - | Imm (Block (_, _, _) | Symbol _ | Node (_, _)) + | Imm (Block (_, _) | Symbol _ | Node (_, _)) -> (error_tc ~loc:(lexp_location e) "Unsupported immediate value!"; DB.type_int) | SortLevel SLz -> DB.type_level @@ -1005,7 +1005,7 @@ and get_type ctx e = | Imm (Float (_, _)) -> DB.type_float | Imm (Integer (_, _)) -> DB.type_int | Imm (String (_, _)) -> DB.type_string - | Imm (Block (_, _, _) | Symbol _ | Node (_, _)) -> DB.type_int + | Imm (Block (_, _) | Symbol _ | Node (_, _)) -> DB.type_int | Builtin (_, t) -> t | SortLevel _ -> DB.type_level | Sort (l, Stype e) -> mkSort (l, Stype (mkSortLevel (mkSLsucc e)))

===================================== src/prelexer.ml ===================================== @@ -27,7 +27,7 @@ let prelexer_error loc = Log.log_error ~section:"PRELEXER" ~loc type pretoken = | Pretoken of location * string | Prestring of location * string - | Preblock of location * pretoken list * location + | Preblock of location * pretoken list

module Pretoken = struct type t = pretoken @@ -39,7 +39,7 @@ module Pretoken = struct -> String.equal l_name r_name | Prestring (_, l_text), Prestring (_, r_text) -> String.equal l_text r_text - | Preblock (_, l_inner, _), Preblock (_, r_inner, _) + | Preblock (_, l_inner), Preblock (_, r_inner) -> Listx.equal equal l_inner r_inner | _ -> false end @@ -69,7 +69,7 @@ let rec consume_until_newline (source : #Source.t) : unit = consumed. *) let prelex (source : #Source.t) : pretoken list = let rec loop - (ctx : (Source.Location.t * pretoken list) list) + (ctx : (Source.Point.t * pretoken list) list) (acc : pretoken list) : pretoken list =

@@ -77,8 +77,9 @@ let prelex (source : #Source.t) : pretoken list = | None -> (match ctx with | [] -> List.rev acc - | ((location, _) :: _ctx) - -> prelexer_error location "Unmatched opening brace"; + | ((brace_point, _) :: _) + -> let location = source#make_location brace_point in + prelexer_error location "Unmatched opening brace"; List.rev acc)

| Some (c) when c <= ' ' @@ -92,50 +93,60 @@ let prelex (source : #Source.t) : pretoken list =

(* A string. *) | Some ('"') - -> source#advance; + -> let quote_point = source#point in + source#advance; let rec prestring chars = - match source#next with + match source#peek with | None | Some ('\n') - -> let location = source#location in + -> source#advance; + let location = source#make_location quote_point in prelexer_error location "Unterminated string"; loop ctx (Prestring (location, "") :: acc)

| Some ('"') - -> let location = source#location in + -> source#advance; + let location = source#make_location quote_point in let pretoken = Prestring (location, string_implode (List.rev chars)) in loop ctx (pretoken :: acc)

| Some ('\') - -> (match source#next with + -> let escape_point = source#point in + source#advance; + (match source#next with | None | Some ('\n') - -> let location = source#location in + -> let location = source#make_location escape_point in prelexer_error location "Unterminated escape sequence"; loop ctx (Prestring (location, "") :: acc) | Some ('t') -> prestring ('\t' :: chars) | Some ('n') -> prestring ('\n' :: chars) | Some ('r') -> prestring ('\r' :: chars) | Some ('u') - -> let location = source#location in + -> let location = source#make_location escape_point in prelexer_error location "Unimplemented unicode escape"; prestring chars | Some (c) -> prestring (c :: chars))

- | Some (char) -> prestring (char :: chars) + | Some (char) + -> source#advance; + prestring (char :: chars) in prestring []

| Some ('{') - -> source#advance; - loop ((source#location, acc) :: ctx) [] + -> let point = source#point in + source#advance; + loop ((point, acc) :: ctx) []

| Some ('}') - -> source#advance; - let location = source#location in + -> let closing_brace_point = source#point in + source#advance; (match ctx with - | ((slocation, sacc) :: ctx) - -> let preblock = Preblock (slocation, List.rev acc, location) in + | ((opening_brace_point, sacc) :: ctx) + -> let location = source#make_location opening_brace_point in + let preblock = Preblock (location, List.rev acc) in loop ctx (preblock :: sacc) | _ - -> prelexer_error location "Unmatched closing brace"; + -> let location = source#make_location closing_brace_point in + prelexer_error location "Unmatched closing brace"; loop ctx acc)

(* A pretoken. *) @@ -154,11 +165,12 @@ let prelex (source : #Source.t) : pretoken list = loop ctx (Pretoken (location, text) :: acc)

| Some ('\') - -> source#advance; + -> let escape_point = source#point in + source#advance; (match source#next with | Some _ -> pretok () | None - -> let error_location = source#location in + -> let error_location = source#make_location escape_point in source#advance; let text, location = source#slice start_point in prelexer_error @@ -173,32 +185,44 @@ let prelex (source : #Source.t) : pretoken list = in loop [] []

-let pretoken_name pretok = - match pretok with - | Pretoken _ -> "Pretoken" - | Prestring _ -> "Prestring" - | Preblock _ -> "Preblock" - -let rec pretoken_string pretok = - match pretok with - | Preblock(_,pts,_) -> "{" ^ ( - List.fold_left (fun str pts -> str ^ " " ^ (pretoken_string pts)) - "" pts) ^ " }" - | Pretoken(_, str) -> str - | Prestring(_, str) -> """ ^ str ^ """ - -let pretokens_string pretokens = - List.fold_left (fun str pt -> str ^ (pretoken_string pt)) "" pretokens - - -let pretokens_print p = print_string (pretokens_string p) - +let pretoken_name : pretoken -> string = function + | Pretoken _ -> "Pretoken" + | Prestring _ -> "Prestring" + | Preblock _ -> "Preblock" + +let rec pretoken_string' (output : string -> unit) : pretoken -> unit = function + | Preblock (_, []) -> + output "{}" + | Preblock (_, head :: tail) -> + output "{"; + pretoken_string' output head; + List.iter (fun pt -> output " "; pretoken_string' output pt) tail; + output "}" + | Pretoken (_, text) -> + output text + | Prestring (_, text) -> + output {|"|}; + output text; + output {|"|} + +let pretoken_string (pretoken : pretoken) : string = + let buffer = Buffer.create 32 in + pretoken_string' (Buffer.add_string buffer) pretoken; + Buffer.contents buffer + +let pretokens_string (pretokens : pretoken list) : string = + let buffer = Buffer.create 32 in + List.iter (pretoken_string' (Buffer.add_string buffer)) pretokens; + Buffer.contents buffer + +let pretokens_print : pretoken list -> unit = + List.iter (pretoken_string' print_string)

(* Prelexer comparison, ignoring source-line-number info, used for tests. *) let rec pretokens_equal p1 p2 = match p1, p2 with | Pretoken (_, s1), Pretoken (_, s2) -> s1 = s2 | Prestring (_, s1), Prestring (_, s2) -> s1 = s2 - | Preblock (_, ps1, _), Preblock (_, ps2, _) -> + | Preblock (_, ps1), Preblock (_, ps2) -> pretokens_eq_list ps1 ps2 | _ -> false and pretokens_eq_list ps1 ps2 = match ps1, ps2 with

===================================== src/sexp.ml ===================================== @@ -31,7 +31,7 @@ type integer = Z.t type symbol = location * string

type sexp = (* Syntactic expression, kind of like Lisp. *) - | Block of location * pretoken list * location + | Block of location * pretoken list | Symbol of symbol | String of location * string | Integer of location * integer @@ -69,7 +69,7 @@ let emptyString = hString ""

let rec sexp_location (s : sexp) : location = match s with - | Block (l, _, _) -> l + | Block (l, _) -> l | Symbol (l, _) -> l | String (l, _) -> l | Integer (l, _) -> l @@ -82,11 +82,14 @@ let rec sexp_string ?(print_locations = false) sexp = (if print_locations then let open Source.Location in - let {file; line; column; _} = sexp_location sexp in - Printf.sprintf "#;("%s" %d %d) " file line column + let {file; start_line; start_column; end_line; end_column} = + sexp_location sexp + in + Printf.sprintf + "#;("%s" %d %d %d %d) " file start_line start_column end_line end_column else "") ^ match sexp with - | Block(_,pts,_) -> "{" ^ (pretokens_string pts) ^ " }" + | Block(_, pts) -> "{" ^ (pretokens_string pts) ^ " }" | Symbol(_, "") -> "()" (* Epsilon *) | Symbol(_, name) -> name | String(_, str) -> """ ^ str ^ """ @@ -263,7 +266,7 @@ let sexp_parse_all_to_list grm tokens limit : sexp list =

(* Sexp comparison, ignoring source-line-number info, used for tests. *) let rec sexp_equal s1 s2 = match s1, s2 with - | Block (_, ps1, _), Block (_, ps2, _) -> pretokens_eq_list ps1 ps2 + | Block (_, ps1), Block (_, ps2) -> pretokens_eq_list ps1 ps2 | Symbol (_, s1), Symbol (_, s2) -> s1 = s2 | String (_, s1), String (_, s2) -> s1 = s2 | Integer (_, n1), Integer (_, n2) -> n1 = n2

===================================== src/source.ml ===================================== @@ -29,23 +29,69 @@ module Point = struct end

module Location = struct - type t = {file : string; line : int; column : int} - - let dummy = {file = ""; line = 0; column = 0} - + type t = + { + file : string; + start_line : int; + start_column : int; + end_line : int; + end_column : int; + } + + let dummy = + { + file = ""; + start_line = 0; + start_column = 0; + end_line = 0; + end_column = 0; + } + + (* Creates a zero-width location around the given point. *) let of_point (file : string) (_, line, column : Point.t) : t = - - {file; line; column} - - let to_string ({file; line; column; _} : t) : string = - Printf.sprintf "%s:%d:%d" file line column + { + file; + start_line = line; + start_column = column; + end_line = line; + end_column = column; + } + + let to_string + ({file; start_line; start_column; end_line; end_column} : t) + : string = + + if Int.equal start_line end_line && Int.equal start_column end_column + then Printf.sprintf "%s:%d:%d" file start_line start_column + else + Printf.sprintf + "%s:%d:%d-%d:%d" file start_line start_column end_line end_column

let equal (l : t) (r : t) = - let {file = l_file; line = l_line; column = l_column} = l in - let {file = r_file; line = r_line; column = r_column} = r in + let + { + file = l_file; + start_line = l_start_line; + start_column = l_start_column; + end_line = l_end_line; + end_column = l_end_column; + } = l + in + let + { + file = r_file; + start_line = r_start_line; + start_column = r_start_column; + end_line = r_end_line; + end_column = r_end_column; + } = r + in + String.equal l_file r_file - && Int.equal l_line r_line - && Int.equal l_column r_column + && Int.equal l_start_line r_start_line + && Int.equal l_start_column r_start_column + && Int.equal l_end_line r_end_line + && Int.equal l_end_column r_end_column end

(* Traditionally, line numbers start at 1… *) @@ -68,24 +114,26 @@ object (self) the text. *) method virtual peek : char option

- (* The current location of the cursor. *) - method location : Location.t = - {file; line; column} - + (* The current point of the cursor. *) method point : Point.t = (self#offset, line, column)

(* The current offset of the cursor in the file, in bytes. *) method virtual private offset : int

+ (* Makes a location starting at the given point and ending at the current + cursor position. *) + method make_location (_, start_line, start_column : Point.t) : Location.t = + {file; start_line; start_column; end_line = line; end_column = column} + (* Slices the text, from (and including) a starting point and to (and excluding) the curent cursor offset.

Note that the source is required only to buffer the last line read and may raise an Invalid_argument if the slice extends before the start of the line. *) - method slice (offset, line, column : Point.t) : string * Location.t = - (self#slice_impl offset, {file; line; column}) + method slice (offset, _, _ as point : Point.t) : string * Location.t = + (self#slice_impl offset, self#make_location point)

method virtual private slice_impl : int -> string

===================================== tests/lexer_test.ml ===================================== @@ -30,11 +30,10 @@ let test_lex name pretokens expected = locations. *) let rec sexp_equal actual expected = match actual, expected with - | Sexp.Block (actual_start, actual_pretokens, actual_end), - Sexp.Block (expected_start, expected_pretokens, expected_end) - -> Location.equal actual_start expected_start + | Sexp.Block (actual_location, actual_pretokens), + Sexp.Block (expected_location, expected_pretokens) + -> Location.equal actual_location expected_location && Listx.equal Pretoken.equal actual_pretokens expected_pretokens - && Location.equal actual_end expected_end | Sexp.Symbol (actual_location, actual_name), Sexp.Symbol (expected_location, expected_name) -> Location.equal actual_location expected_location @@ -67,36 +66,42 @@ let test_lex name pretokens expected = add_test "LEXER" name lex

let l : Source.Location.t = - {file = "test.typer"; line = 1; column = 1} + { + file = "test.typer"; + start_line = 1; + start_column = 1; + end_line = 1; + end_column = 1; + }

let () = test_lex "Inner operator inside a presymbol" [Pretoken (l, "a.b")] - [Node (Symbol ({l with column = 2}, "__.__"), - [Symbol ({l with column = 1}, "a"); - Symbol ({l with column = 3}, "b")])] + [Node (Symbol ({l with start_column = 2; end_column = 3}, "__.__"), + [Symbol ({l with start_column = 1; end_column = 2}, "a"); + Symbol ({l with start_column = 3; end_column = 4}, "b")])]

let () = test_lex "Inner operators at the beginning of a presymbol" [Pretoken (l, ".b")] - [Node (Symbol ({l with column = 1}, "__.__"), - [epsilon {l with column = 1}; - Symbol ({l with column = 2}, "b")])] + [Node (Symbol ({l with start_column = 1; end_column = 2}, "__.__"), + [epsilon {l with start_column = 1; end_column = 1}; + Symbol ({l with start_column = 2; end_column = 3}, "b")])]

let () = test_lex "Inner operators at the end of a presymbol" [Pretoken (l, "a.")] - [Node (Symbol ({l with column = 2}, "__.__"), - [Symbol ({l with column = 1}, "a"); - epsilon {l with column = 3}])] + [Node (Symbol ({l with start_column = 2; end_column = 3}, "__.__"), + [Symbol ({l with start_column = 1; end_column = 2}, "a"); + epsilon {l with start_column = 3; end_column = 3}])]

let () = test_lex "An inner operator by itself is a simple symbol" [Pretoken (l, ".")] - [Symbol ({l with column = 1}, ".")] + [Symbol ({l with start_column = 1; end_column = 2}, ".")]

let () = run_all ()

View it on GitLab: https://gitlab.com/monnier/typer/-/commit/8cfa22437d3c12681e5435f03c5b68b6e4...