Septembre 2021 - Typer - mailman.iro.umontreal.ca

[Git][monnier/typer][source-spans-2] Locations now track their end points.
by Simon Génier (＠ilovemonoids) 30 Sep '21

30 Sep '21

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/8cfa22437d3c12681e5435f03c5b68b6e… -- View it on GitLab: https://gitlab.com/monnier/typer/-/commit/8cfa22437d3c12681e5435f03c5b68b6e… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer] Pushed new branch source-spans-2
by Simon Génier (＠ilovemonoids) 30 Sep '21

30 Sep '21

Simon Génier pushed new branch source-spans-2 at Stefan / Typer -- View it on GitLab: https://gitlab.com/monnier/typer/-/tree/source-spans-2 You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer] Pushed new branch purge-docstr
by Simon Génier (＠ilovemonoids) 29 Sep '21

29 Sep '21

Simon Génier pushed new branch purge-docstr at Stefan / Typer -- View it on GitLab: https://gitlab.com/monnier/typer/-/tree/purge-docstr You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer] Pushed new branch ocaml-4.11
by Simon Génier (＠ilovemonoids) 28 Sep '21

28 Sep '21

Simon Génier pushed new branch ocaml-4.11 at Stefan / Typer -- View it on GitLab: https://gitlab.com/monnier/typer/-/tree/ocaml-4.11 You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][location-inside-source] Compute location inside the source from the given point.
by Simon Génier (＠ilovemonoids) 28 Sep '21

28 Sep '21

Simon Génier pushed to branch location-inside-source at Stefan / Typer Commits: 87882dea by Simon Génier at 2021-09-28T17:45:35-04:00 Compute location inside the source from the given point. - - - - - 3 changed files: - src/lexer.ml - src/prelexer.ml - src/source.ml Changes: ===================================== src/lexer.ml ===================================== @@ -37,8 +37,8 @@ let unescape str = let lex_number (source : #Source.t) - (start_location : Source.Location.t) (start_point : Source.Point.t) + (doc : string) : sexp = let rec lex_exponent () = @@ -48,8 +48,8 @@ let lex_number lex_exponent () | _ - -> let source = source#slice start_point in - Float (start_location, float_of_string source) + -> let source, location = source#slice start_point doc in + Float (location, float_of_string source) in let lex_exponent_sign () = @@ -60,8 +60,8 @@ let lex_number (* TODO: error if there are no signs or digits after the 'e'? *) | _ - -> let source = source#slice start_point in - Float (start_location, float_of_string source) + -> let source, location = source#slice start_point doc in + Float (location, float_of_string source) in let rec lex_fractional () = @@ -75,8 +75,8 @@ let lex_number lex_exponent_sign () | _ - -> let source = source#slice start_point in - Float (start_location, float_of_string source) + -> let source, location = source#slice start_point doc in + Float (location, float_of_string source) in let rec lex_integer () = @@ -94,8 +94,8 @@ let lex_number lex_exponent_sign () | _ - -> let source = source#slice start_point in - Integer (start_location, Z.of_string source) + -> let source, location = source#slice start_point doc in + Integer (location, Z.of_string source) in lex_integer () @@ -105,31 +105,30 @@ let lex_symbol (token_env : token_env) (source : #Source.t) (doc : string) - (start_location : Source.Location.t) (start_point : Source.Point.t) : sexp = - let mksym start_location start_point escaped = + let mksym start_point escaped = if Source.Point.equal start_point source#point - then epsilon start_location + then epsilon (Source.Location.of_point source#file start_point doc) else - let raw_name = source#slice start_point in + let raw_name, location = source#slice start_point doc in let name = if escaped then unescape raw_name else raw_name in - hSymbol (start_location, name) + hSymbol (location, name) in - let rec loop start_location start_point prec lf (escaped : bool) = + let rec loop start_point prec lf (escaped : bool) = match source#peek with | None - -> lf (mksym start_location start_point escaped) + -> lf (mksym start_point escaped) | Some c -> (match token_env.(Char.code c) with | CKseparate - -> lf (mksym start_location start_point escaped) + -> lf (mksym start_point escaped) | CKinner prec' - -> let left = mksym start_location start_point escaped in + -> let left = mksym start_point escaped in let op_location = source#location doc in (* To be considered `inner`, an operator char needs to have @@ -151,9 +150,9 @@ let lex_symbol then fun s -> lf (Node (op, [left; s])) else fun s -> Node (op, [lf left; s]) in - loop (source#location doc) source#point prec' lf' false + loop source#point prec' lf' false else - loop start_location start_point prec lf escaped + loop start_point prec lf escaped | CKnormal -> (source#advance; @@ -165,11 +164,11 @@ let lex_symbol leading byte, so it has to count as 1 as well ;-) *) | '\\' when not is_last -> source#advance; - loop start_location start_point prec lf true + loop start_point prec lf true - | _ -> loop start_location start_point prec lf escaped)) + | _ -> loop start_point prec lf escaped)) in - loop start_location start_point 0 (fun s -> s) false + loop start_point 0 (fun s -> s) false let split_presymbol (token_env : token_env) @@ -182,7 +181,6 @@ let split_presymbol | None -> List.rev acc | Some (c) -> let start_point = source#point in - let start_location = source#location doc in let token = match c with (* A negative number literal, or a symbol starting with '-'. *) @@ -190,21 +188,21 @@ let split_presymbol -> (source#advance; match source#peek with | Some ('0' .. '9') - -> lex_number source start_location start_point + -> lex_number source start_point doc | _ - -> lex_symbol token_env source doc start_location start_point) + -> lex_symbol token_env source doc start_point) | '0' .. '9' -> (source#advance; - lex_number source start_location start_point) + lex_number source start_point doc) | _ when token_env.(Char.code c) = CKseparate -> source#advance; - let name = source#slice start_point in - hSymbol (start_location, name) + let name, location = source#slice start_point doc in + hSymbol (location, name) | _ - -> lex_symbol token_env source doc start_location start_point + -> lex_symbol token_env source doc start_point in loop (token :: acc) in ===================================== src/prelexer.ml ===================================== @@ -61,7 +61,7 @@ end (* FIXME: Handle multiline strings. *) let rec consume_until_newline (source : #Source.t) : unit = - match source#next_char with + match source#next with | None | Some ('\n') -> () | Some _ -> consume_until_newline source @@ -96,14 +96,14 @@ let prelex (source : #Source.t) : pretoken list = -> source#advance; let start_point = source#point in consume_until_newline source; - let new_doc = String.trim (source#slice start_point) in - loop ctx acc (doc ^ "\n" ^ new_doc) + let new_doc, _ = source#slice start_point "" in + loop ctx acc (doc ^ "\n" ^ String.trim new_doc) (* A string. *) | Some ('"') -> source#advance; let rec prestring chars = - match source#next_char with + match source#next with | None | Some ('\n') -> let location = source#location doc in prelexer_error location "Unterminated string"; @@ -115,7 +115,7 @@ let prelex (source : #Source.t) : pretoken list = loop ctx (pretoken :: acc) "" | Some ('\\') - -> (match source#next_char with + -> (match source#next with | None | Some ('\n') -> let location = source#location doc in prelexer_error location "Unterminated escape sequence"; @@ -155,25 +155,25 @@ let prelex (source : #Source.t) : pretoken list = let rec pretok () = match source#peek with | None | Some ('%' | '"' | '{' | '}') - -> let location = source#location doc in - let text = source#slice start_point in + -> let text, location = source#slice start_point doc in loop ctx (Pretoken (location, text) :: acc) "" | Some (c) when c <= ' ' - -> let location = source#location doc in - let text = source#slice start_point in + -> let text, location = source#slice start_point doc in source#advance; loop ctx (Pretoken (location, text) :: acc) "" | Some ('\\') -> source#advance; - (match source#next_char with + (match source#next with | Some _ -> pretok () | None - -> let location = source#location doc in + -> let error_location = source#location doc in source#advance; - let text = source#slice start_point in - prelexer_error location ("Unterminated escape sequence in: " ^ text); + let text, location = source#slice start_point doc in + prelexer_error + error_location + ("Unterminated escape sequence in: " ^ text); loop ctx (Pretoken (location, text) :: acc) "") | Some _ ===================================== src/source.ml ===================================== @@ -33,6 +33,14 @@ module Location = struct let dummy = {file = ""; line = 0; column = 0; docstr = ""} + let of_point + (file : string) + (_, line, column : Point.t) + (docstr : string) + : t = + + {file; line; column; docstr} + let to_string ({file; line; column; _} : t) : string = Printf.sprintf "%s:%d:%d" file line column @@ -81,7 +89,10 @@ object (self) 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 virtual slice : Point.t -> string + method slice (offset, line, column : Point.t) (docstr : string) : string * Location.t = + (self#slice_impl offset, {file; line; column; docstr}) + + method virtual private slice_impl : int -> string (* Moves the cursor forward one byte *) method advance : unit = @@ -99,7 +110,7 @@ object (self) method private virtual advance_impl : unit (* Returns the char at the cursor, then advances it forward. *) - method next_char : char option = + method next : char option = let c = self#peek in self#advance; c @@ -133,12 +144,12 @@ class source_file file_name = object (self) with | End_of_file -> None - method advance_impl = + method private advance_impl = offset <- offset + 1 method private offset = line_offset + offset - method slice (start_offset, _, _) = + method private slice_impl start_offset = let relative_start_offset = start_offset - line_offset in String.sub source_line relative_start_offset (offset - relative_start_offset) end @@ -159,11 +170,11 @@ object then Some (source.[offset]) else None - method advance_impl = + method private advance_impl = offset <- offset + 1 method private offset = offset - method slice (start_offset, _, _) = + method private slice_impl start_offset = String.sub source start_offset (offset - start_offset) end View it on GitLab: https://gitlab.com/monnier/typer/-/commit/87882dea3ad0446c118b20b7c61aa3bcb… -- View it on GitLab: https://gitlab.com/monnier/typer/-/commit/87882dea3ad0446c118b20b7c61aa3bcb… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][location-inside-source] 4 commits: Shorten the names of a few methods on source objects.
by Simon Génier (＠ilovemonoids) 28 Sep '21

28 Sep '21

Simon Génier pushed to branch location-inside-source at Stefan / Typer Commits: 4fb0ccd3 by Simon Génier at 2021-06-09T12:40:18-04:00 Shorten the names of a few methods on source objects. These names were redundants. For instance in `current_offset`, the `current` part is already hinted at by the fact that source objects are a kind of cursor. Overall I think the new names a clearer since they are more concise. - - - - - aff91a51 by Simon Génier at 2021-09-28T17:16:11-04:00 Merge branch 'shorten-source-methods' - - - - - e8a59f86 by Simon Génier at 2021-09-28T17:25:19-04:00 Replace raw offsets with points which also track line and column. - - - - - 0b3b0b5b by Simon Génier at 2021-09-28T17:28:19-04:00 Compute location inside the source from the given point. - - - - - 3 changed files: - src/lexer.ml - src/prelexer.ml - src/source.ml Changes: ===================================== src/lexer.ml ===================================== @@ -37,35 +37,35 @@ let unescape str = let lex_number (source : #Source.t) - (start_location : Source.Location.t) - (start_offset : int) + (start_point : Source.Point.t) + (doc : string) : sexp = let rec lex_exponent () = - match source#peek_char with + match source#peek with | Some ('0' .. '9') -> source#advance; lex_exponent () | _ - -> let source = source#slice_from_offset start_offset in - Float (start_location, float_of_string source) + -> let source, location = source#slice start_point doc in + Float (location, float_of_string source) in let lex_exponent_sign () = - match source#peek_char with + match source#peek with | Some ('0' .. '9' | '+' | '-') -> source#advance; lex_exponent () (* TODO: error if there are no signs or digits after the 'e'? *) | _ - -> let source = source#slice_from_offset start_offset in - Float (start_location, float_of_string source) + -> let source, location = source#slice start_point doc in + Float (location, float_of_string source) in let rec lex_fractional () = - match source#peek_char with + match source#peek with | Some ('0' .. '9') -> source#advance; lex_fractional () @@ -75,12 +75,12 @@ let lex_number lex_exponent_sign () | _ - -> let source = source#slice_from_offset start_offset in - Float (start_location, float_of_string source) + -> let source, location = source#slice start_point doc in + Float (location, float_of_string source) in let rec lex_integer () = - match source#peek_char with + match source#peek with | Some ('0' .. '9') -> source#advance; lex_integer () @@ -94,8 +94,8 @@ let lex_number lex_exponent_sign () | _ - -> let source = source#slice_from_offset start_offset in - Integer (start_location, Z.of_string source) + -> let source, location = source#slice start_point doc in + Integer (location, Z.of_string source) in lex_integer () @@ -105,41 +105,40 @@ let lex_symbol (token_env : token_env) (source : #Source.t) (doc : string) - (start_location : Source.Location.t) - (start_offset : int) + (start_point : Source.Point.t) : sexp = - let mksym start_location start_offset escaped = - if Int.equal start_offset source#current_offset - then epsilon start_location + let mksym start_point escaped = + if Source.Point.equal start_point source#point + then epsilon (Source.Location.of_point source#file_name start_point doc) else - let raw_name = source#slice_from_offset start_offset in + let raw_name, location = source#slice start_point doc in let name = if escaped then unescape raw_name else raw_name in - hSymbol (start_location, name) + hSymbol (location, name) in - let rec loop start_location start_offset prec lf (escaped : bool) = - match source#peek_char with + let rec loop start_point prec lf (escaped : bool) = + match source#peek with | None - -> lf (mksym start_location start_offset escaped) + -> lf (mksym start_point escaped) | Some c -> (match token_env.(Char.code c) with | CKseparate - -> lf (mksym start_location start_offset escaped) + -> lf (mksym start_point escaped) | CKinner prec' - -> let left = mksym start_location start_offset escaped in - let op_location = source#current_location doc in + -> let left = mksym start_point escaped in + let op_location = source#location doc in (* To be considered `inner`, an operator char needs to have something on its LHS or its RHS, otherwise, treat it as a normal char. `.` can be the normal function composition operator as well. *) - let lhs_p = start_offset != source#current_offset in + let lhs_p = not (Source.Point.equal start_point source#point) in source#advance; let rhs_p = - (match source#peek_char with + (match source#peek with | None -> false | Some c' -> CKseparate != token_env.(Char.code c')) in @@ -151,13 +150,13 @@ let lex_symbol then fun s -> lf (Node (op, [left; s])) else fun s -> Node (op, [lf left; s]) in - loop (source#current_location doc) source#current_offset prec' lf' false + loop source#point prec' lf' false else - loop start_location start_offset prec lf escaped + loop start_point prec lf escaped | CKnormal -> (source#advance; - let is_last = Option.is_none source#peek_char in + let is_last = Option.is_none source#peek in match c with (* Skip next char, in case it's a special token. For utf-8, simply advancing is risky but actually works: '\' counts as 1 @@ -165,11 +164,11 @@ let lex_symbol leading byte, so it has to count as 1 as well ;-) *) | '\\' when not is_last -> source#advance; - loop start_location start_offset prec lf true + loop start_point prec lf true - | _ -> loop start_location start_offset prec lf escaped)) + | _ -> loop start_point prec lf escaped)) in - loop start_location start_offset 0 (fun s -> s) false + loop start_point 0 (fun s -> s) false let split_presymbol (token_env : token_env) @@ -178,33 +177,32 @@ let split_presymbol : sexp list = let rec loop (acc : sexp list) : sexp list = - match source#peek_char with + match source#peek with | None -> List.rev acc | Some (c) - -> let start_offset = source#current_offset in - let start_location = source#current_location doc in + -> let start_point = source#point in let token = match c with (* A negative number literal, or a symbol starting with '-'. *) | '-' -> (source#advance; - match source#peek_char with + match source#peek with | Some ('0' .. '9') - -> lex_number source start_location start_offset + -> lex_number source start_point doc | _ - -> lex_symbol token_env source doc start_location start_offset) + -> lex_symbol token_env source doc start_point) | '0' .. '9' -> (source#advance; - lex_number source start_location start_offset) + lex_number source start_point doc) | _ when token_env.(Char.code c) = CKseparate -> source#advance; - let name = source#slice_from_offset start_offset in - hSymbol (start_location, name) + let name, location = source#slice start_point doc in + hSymbol (location, name) | _ - -> lex_symbol token_env source doc start_location start_offset + -> lex_symbol token_env source doc start_point in loop (token :: acc) in ===================================== src/prelexer.ml ===================================== @@ -74,7 +74,7 @@ let prelex (source : #Source.t) : pretoken list = (doc : string) : pretoken list = - match source#peek_char with + match source#peek with | None -> (match ctx with | [] -> List.rev acc @@ -94,10 +94,10 @@ let prelex (source : #Source.t) : pretoken list = (* line's bounds seems ok: String.sub line 1 0 == "" *) | Some ('@') -> source#advance; - let start_offset = source#current_offset in + let start_point = source#point in consume_until_newline source; - let new_doc = String.trim (source#slice_from_offset start_offset) in - loop ctx acc (doc ^ "\n" ^ new_doc) + let new_doc, _ = source#slice start_point "" in + loop ctx acc (doc ^ "\n" ^ String.trim new_doc) (* A string. *) | Some ('"') @@ -105,26 +105,26 @@ let prelex (source : #Source.t) : pretoken list = let rec prestring chars = match source#next_char with | None | Some ('\n') - -> let location = source#current_location doc in + -> let location = source#location doc in prelexer_error location "Unterminated string"; loop ctx (Prestring (location, "") :: acc) "" | Some ('"') - -> let location = source#current_location doc in + -> let location = source#location doc in let pretoken = Prestring (location, string_implode (List.rev chars)) in loop ctx (pretoken :: acc) "" | Some ('\\') -> (match source#next_char with | None | Some ('\n') - -> let location = source#current_location doc in + -> let location = source#location doc 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#current_location doc in + -> let location = source#location doc in prelexer_error location "Unimplemented unicode escape"; prestring chars | Some (c) -> prestring (c :: chars)) @@ -134,12 +134,12 @@ let prelex (source : #Source.t) : pretoken list = | Some ('{') -> source#advance; - let ctx' = (source#current_location doc, acc) :: ctx in + let ctx' = (source#location doc, acc) :: ctx in loop ctx' [] doc | Some ('}') -> source#advance; - let location = source#current_location doc in + let location = source#location doc in (match ctx with | ((slocation, sacc) :: ctx) -> let preblock = Preblock (slocation, List.rev acc, location) in @@ -150,18 +150,16 @@ let prelex (source : #Source.t) : pretoken list = (* A pretoken. *) | Some _ - -> let start_offset = source#current_offset in + -> let start_point = source#point in source#advance; let rec pretok () = - match source#peek_char with + match source#peek with | None | Some ('%' | '"' | '{' | '}') - -> let location = source#current_location doc in - let text = source#slice_from_offset start_offset in + -> let text, location = source#slice start_point doc in loop ctx (Pretoken (location, text) :: acc) "" | Some (c) when c <= ' ' - -> let location = source#current_location doc in - let text = source#slice_from_offset start_offset in + -> let text, location = source#slice start_point doc in source#advance; loop ctx (Pretoken (location, text) :: acc) "" @@ -170,10 +168,12 @@ let prelex (source : #Source.t) : pretoken list = (match source#next_char with | Some _ -> pretok () | None - -> let location = source#current_location doc in + -> let error_location = source#location doc in source#advance; - let text = source#slice_from_offset start_offset in - prelexer_error location ("Unterminated escape sequence in: " ^ text); + let text, location = source#slice start_point doc in + prelexer_error + error_location + ("Unterminated escape sequence in: " ^ text); loop ctx (Pretoken (location, text) :: acc) "") | Some _ ===================================== src/source.ml ===================================== @@ -18,11 +18,29 @@ * You should have received a copy of the GNU General Public License along * with this program. If not, see <http://www.gnu.org/licenses/>. *) +module Point = struct + (* offset * line * column *) + type t = int * int * int + + let equal (l, _, _ : t) (r, _, _ : t) : bool = + (* The line and column are metadata, only the offset is necessary for + determining equality. *) + Int.equal l r +end + module Location = struct type t = {file : string; line : int; column : int; docstr : string} let dummy = {file = ""; line = 0; column = 0; docstr = ""} + let of_point + (file : string) + (_, line, column : Point.t) + (docstr : string) + : t = + + {file; line; column; docstr} + let to_string ({file; line; column; _} : t) : string = Printf.sprintf "%s:%d:%d" file line column @@ -43,37 +61,43 @@ let first_column_of_line = 1 (* A source object is text paired with a cursor. The text can be lazily loaded as it is accessed byte by byte, but it must be retained for future reference by error messages. *) -class virtual t (base_line : int) (base_column : int) (file_name : string) = +class virtual t (base_line : int) (base_column : int) (file : string) = object (self) val mutable line = base_line val mutable column = base_column (* A path if the text comes from a file, otherwise a meaningful identifier. *) - method file_name : string = file_name + method file : string = file (* Return the byte at the cursor, or None if the cursor is at the end of the text. *) - method virtual peek_char : char option + method virtual peek : char option (* The current location of the cursor. *) - method current_location (docstr : string) : Location.t = - {file = file_name; line; column; docstr} + method location (docstr : string) : Location.t = + {file; line; column; docstr} + + method point : Point.t = + (self#offset, line, column) (* The current offset of the cursor in the file, in bytes. *) - method virtual current_offset : int + method virtual private offset : int - (* Slices the text, from (and including) a starting offset and to (and + (* 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 virtual slice_from_offset : int -> string + method slice (offset, line, column : Point.t) (docstr : string) : string * Location.t = + (self#slice_impl offset, {file = file_name; line; column; docstr}) + + method virtual private slice_impl : int -> string (* Moves the cursor forward one byte *) method advance : unit = let is_utf8_head c = Char.code c < 128 || Char.code c >= 192 in - let c = self#peek_char in + let c = self#peek in self#advance_impl; match c with | Some '\n' @@ -87,7 +111,7 @@ object (self) (* Returns the char at the cursor, then advances it forward. *) method next_char : char option = - let c = self#peek_char in + let c = self#peek in self#advance; c end @@ -103,29 +127,29 @@ class source_file file_name = object (self) val mutable line_offset = 0 val mutable offset = 0 - method private peek_char_unchecked = + method private peek_unchecked = if offset < String.length source_line then source_line.[offset] else '\n' - method peek_char = + method peek = if offset <= String.length source_line - then Some self#peek_char_unchecked + then Some self#peek_unchecked else try line_offset <- line_offset + 1 + String.length source_line; source_line <- input_line in_channel; offset <- 0; - Some self#peek_char_unchecked + Some self#peek_unchecked with | End_of_file -> None - method advance_impl = + method private advance_impl = offset <- offset + 1 - method current_offset = line_offset + offset + method private offset = line_offset + offset - method slice_from_offset start_offset = + method private slice_impl start_offset = let relative_start_offset = start_offset - line_offset in String.sub source_line relative_start_offset (offset - relative_start_offset) end @@ -141,16 +165,16 @@ object val mutable offset = 0 - method peek_char = + method peek = if offset < String.length source then Some (source.[offset]) else None - method advance_impl = + method private advance_impl = offset <- offset + 1 - method current_offset = offset + method private offset = offset - method slice_from_offset start_offset = + method private slice_impl start_offset = String.sub source start_offset (offset - start_offset) end View it on GitLab: https://gitlab.com/monnier/typer/-/compare/81e7e20ee757b578f0a3017e5f4a8c48… -- View it on GitLab: https://gitlab.com/monnier/typer/-/compare/81e7e20ee757b578f0a3017e5f4a8c48… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][offsets-to-points] 3 commits: Shorten the names of a few methods on source objects.
by Simon Génier (＠ilovemonoids) 28 Sep '21

28 Sep '21

Simon Génier pushed to branch offsets-to-points at Stefan / Typer Commits: 4fb0ccd3 by Simon Génier at 2021-06-09T12:40:18-04:00 Shorten the names of a few methods on source objects. These names were redundants. For instance in `current_offset`, the `current` part is already hinted at by the fact that source objects are a kind of cursor. Overall I think the new names a clearer since they are more concise. - - - - - aff91a51 by Simon Génier at 2021-09-28T17:16:11-04:00 Merge branch 'shorten-source-methods' - - - - - e8a59f86 by Simon Génier at 2021-09-28T17:25:19-04:00 Replace raw offsets with points which also track line and column. - - - - - 3 changed files: - src/lexer.ml - src/prelexer.ml - src/source.ml Changes: ===================================== src/lexer.ml ===================================== @@ -38,34 +38,34 @@ let unescape str = let lex_number (source : #Source.t) (start_location : Source.Location.t) - (start_offset : int) + (start_point : Source.Point.t) : sexp = let rec lex_exponent () = - match source#peek_char with + match source#peek with | Some ('0' .. '9') -> source#advance; lex_exponent () | _ - -> let source = source#slice_from_offset start_offset in + -> let source = source#slice start_point in Float (start_location, float_of_string source) in let lex_exponent_sign () = - match source#peek_char with + match source#peek with | Some ('0' .. '9' | '+' | '-') -> source#advance; lex_exponent () (* TODO: error if there are no signs or digits after the 'e'? *) | _ - -> let source = source#slice_from_offset start_offset in + -> let source = source#slice start_point in Float (start_location, float_of_string source) in let rec lex_fractional () = - match source#peek_char with + match source#peek with | Some ('0' .. '9') -> source#advance; lex_fractional () @@ -75,12 +75,12 @@ let lex_number lex_exponent_sign () | _ - -> let source = source#slice_from_offset start_offset in + -> let source = source#slice start_point in Float (start_location, float_of_string source) in let rec lex_integer () = - match source#peek_char with + match source#peek with | Some ('0' .. '9') -> source#advance; lex_integer () @@ -94,7 +94,7 @@ let lex_number lex_exponent_sign () | _ - -> let source = source#slice_from_offset start_offset in + -> let source = source#slice start_point in Integer (start_location, Z.of_string source) in @@ -106,40 +106,40 @@ let lex_symbol (source : #Source.t) (doc : string) (start_location : Source.Location.t) - (start_offset : int) + (start_point : Source.Point.t) : sexp = - let mksym start_location start_offset escaped = - if Int.equal start_offset source#current_offset + let mksym start_location start_point escaped = + if Source.Point.equal start_point source#point then epsilon start_location else - let raw_name = source#slice_from_offset start_offset in + let raw_name = source#slice start_point in let name = if escaped then unescape raw_name else raw_name in hSymbol (start_location, name) in - let rec loop start_location start_offset prec lf (escaped : bool) = - match source#peek_char with + let rec loop start_location start_point prec lf (escaped : bool) = + match source#peek with | None - -> lf (mksym start_location start_offset escaped) + -> lf (mksym start_location start_point escaped) | Some c -> (match token_env.(Char.code c) with | CKseparate - -> lf (mksym start_location start_offset escaped) + -> lf (mksym start_location start_point escaped) | CKinner prec' - -> let left = mksym start_location start_offset escaped in - let op_location = source#current_location doc in + -> let left = mksym start_location start_point escaped in + let op_location = source#location doc in (* To be considered `inner`, an operator char needs to have something on its LHS or its RHS, otherwise, treat it as a normal char. `.` can be the normal function composition operator as well. *) - let lhs_p = start_offset != source#current_offset in + let lhs_p = not (Source.Point.equal start_point source#point) in source#advance; let rhs_p = - (match source#peek_char with + (match source#peek with | None -> false | Some c' -> CKseparate != token_env.(Char.code c')) in @@ -151,13 +151,13 @@ let lex_symbol then fun s -> lf (Node (op, [left; s])) else fun s -> Node (op, [lf left; s]) in - loop (source#current_location doc) source#current_offset prec' lf' false + loop (source#location doc) source#point prec' lf' false else - loop start_location start_offset prec lf escaped + loop start_location start_point prec lf escaped | CKnormal -> (source#advance; - let is_last = Option.is_none source#peek_char in + let is_last = Option.is_none source#peek in match c with (* Skip next char, in case it's a special token. For utf-8, simply advancing is risky but actually works: '\' counts as 1 @@ -165,11 +165,11 @@ let lex_symbol leading byte, so it has to count as 1 as well ;-) *) | '\\' when not is_last -> source#advance; - loop start_location start_offset prec lf true + loop start_location start_point prec lf true - | _ -> loop start_location start_offset prec lf escaped)) + | _ -> loop start_location start_point prec lf escaped)) in - loop start_location start_offset 0 (fun s -> s) false + loop start_location start_point 0 (fun s -> s) false let split_presymbol (token_env : token_env) @@ -178,33 +178,33 @@ let split_presymbol : sexp list = let rec loop (acc : sexp list) : sexp list = - match source#peek_char with + match source#peek with | None -> List.rev acc | Some (c) - -> let start_offset = source#current_offset in - let start_location = source#current_location doc in + -> let start_point = source#point in + let start_location = source#location doc in let token = match c with (* A negative number literal, or a symbol starting with '-'. *) | '-' -> (source#advance; - match source#peek_char with + match source#peek with | Some ('0' .. '9') - -> lex_number source start_location start_offset + -> lex_number source start_location start_point | _ - -> lex_symbol token_env source doc start_location start_offset) + -> lex_symbol token_env source doc start_location start_point) | '0' .. '9' -> (source#advance; - lex_number source start_location start_offset) + lex_number source start_location start_point) | _ when token_env.(Char.code c) = CKseparate -> source#advance; - let name = source#slice_from_offset start_offset in + let name = source#slice start_point in hSymbol (start_location, name) | _ - -> lex_symbol token_env source doc start_location start_offset + -> lex_symbol token_env source doc start_location start_point in loop (token :: acc) in ===================================== src/prelexer.ml ===================================== @@ -74,7 +74,7 @@ let prelex (source : #Source.t) : pretoken list = (doc : string) : pretoken list = - match source#peek_char with + match source#peek with | None -> (match ctx with | [] -> List.rev acc @@ -94,9 +94,9 @@ let prelex (source : #Source.t) : pretoken list = (* line's bounds seems ok: String.sub line 1 0 == "" *) | Some ('@') -> source#advance; - let start_offset = source#current_offset in + let start_point = source#point in consume_until_newline source; - let new_doc = String.trim (source#slice_from_offset start_offset) in + let new_doc = String.trim (source#slice start_point) in loop ctx acc (doc ^ "\n" ^ new_doc) (* A string. *) @@ -105,26 +105,26 @@ let prelex (source : #Source.t) : pretoken list = let rec prestring chars = match source#next_char with | None | Some ('\n') - -> let location = source#current_location doc in + -> let location = source#location doc in prelexer_error location "Unterminated string"; loop ctx (Prestring (location, "") :: acc) "" | Some ('"') - -> let location = source#current_location doc in + -> let location = source#location doc in let pretoken = Prestring (location, string_implode (List.rev chars)) in loop ctx (pretoken :: acc) "" | Some ('\\') -> (match source#next_char with | None | Some ('\n') - -> let location = source#current_location doc in + -> let location = source#location doc 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#current_location doc in + -> let location = source#location doc in prelexer_error location "Unimplemented unicode escape"; prestring chars | Some (c) -> prestring (c :: chars)) @@ -134,12 +134,12 @@ let prelex (source : #Source.t) : pretoken list = | Some ('{') -> source#advance; - let ctx' = (source#current_location doc, acc) :: ctx in + let ctx' = (source#location doc, acc) :: ctx in loop ctx' [] doc | Some ('}') -> source#advance; - let location = source#current_location doc in + let location = source#location doc in (match ctx with | ((slocation, sacc) :: ctx) -> let preblock = Preblock (slocation, List.rev acc, location) in @@ -150,18 +150,18 @@ let prelex (source : #Source.t) : pretoken list = (* A pretoken. *) | Some _ - -> let start_offset = source#current_offset in + -> let start_point = source#point in source#advance; let rec pretok () = - match source#peek_char with + match source#peek with | None | Some ('%' | '"' | '{' | '}') - -> let location = source#current_location doc in - let text = source#slice_from_offset start_offset in + -> let location = source#location doc in + let text = source#slice start_point in loop ctx (Pretoken (location, text) :: acc) "" | Some (c) when c <= ' ' - -> let location = source#current_location doc in - let text = source#slice_from_offset start_offset in + -> let location = source#location doc in + let text = source#slice start_point in source#advance; loop ctx (Pretoken (location, text) :: acc) "" @@ -170,9 +170,9 @@ let prelex (source : #Source.t) : pretoken list = (match source#next_char with | Some _ -> pretok () | None - -> let location = source#current_location doc in + -> let location = source#location doc in source#advance; - let text = source#slice_from_offset start_offset in + let text = source#slice start_point in prelexer_error location ("Unterminated escape sequence in: " ^ text); loop ctx (Pretoken (location, text) :: acc) "") ===================================== src/source.ml ===================================== @@ -18,6 +18,16 @@ * You should have received a copy of the GNU General Public License along * with this program. If not, see <http://www.gnu.org/licenses/>. *) +module Point = struct + (* offset * line * column *) + type t = int * int * int + + let equal (l, _, _ : t) (r, _, _ : t) : bool = + (* The line and column are metadata, only the offset is necessary for + determining equality. *) + Int.equal l r +end + module Location = struct type t = {file : string; line : int; column : int; docstr : string} @@ -43,37 +53,40 @@ let first_column_of_line = 1 (* A source object is text paired with a cursor. The text can be lazily loaded as it is accessed byte by byte, but it must be retained for future reference by error messages. *) -class virtual t (base_line : int) (base_column : int) (file_name : string) = +class virtual t (base_line : int) (base_column : int) (file : string) = object (self) val mutable line = base_line val mutable column = base_column (* A path if the text comes from a file, otherwise a meaningful identifier. *) - method file_name : string = file_name + method file : string = file (* Return the byte at the cursor, or None if the cursor is at the end of the text. *) - method virtual peek_char : char option + method virtual peek : char option (* The current location of the cursor. *) - method current_location (docstr : string) : Location.t = - {file = file_name; line; column; docstr} + method location (docstr : string) : Location.t = + {file; line; column; docstr} + + method point : Point.t = + (self#offset, line, column) (* The current offset of the cursor in the file, in bytes. *) - method virtual current_offset : int + method virtual private offset : int - (* Slices the text, from (and including) a starting offset and to (and + (* 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 virtual slice_from_offset : int -> string + method virtual slice : Point.t -> string (* Moves the cursor forward one byte *) method advance : unit = let is_utf8_head c = Char.code c < 128 || Char.code c >= 192 in - let c = self#peek_char in + let c = self#peek in self#advance_impl; match c with | Some '\n' @@ -87,7 +100,7 @@ object (self) (* Returns the char at the cursor, then advances it forward. *) method next_char : char option = - let c = self#peek_char in + let c = self#peek in self#advance; c end @@ -103,29 +116,29 @@ class source_file file_name = object (self) val mutable line_offset = 0 val mutable offset = 0 - method private peek_char_unchecked = + method private peek_unchecked = if offset < String.length source_line then source_line.[offset] else '\n' - method peek_char = + method peek = if offset <= String.length source_line - then Some self#peek_char_unchecked + then Some self#peek_unchecked else try line_offset <- line_offset + 1 + String.length source_line; source_line <- input_line in_channel; offset <- 0; - Some self#peek_char_unchecked + Some self#peek_unchecked with | End_of_file -> None method advance_impl = offset <- offset + 1 - method current_offset = line_offset + offset + method private offset = line_offset + offset - method slice_from_offset start_offset = + method slice (start_offset, _, _) = let relative_start_offset = start_offset - line_offset in String.sub source_line relative_start_offset (offset - relative_start_offset) end @@ -141,7 +154,7 @@ object val mutable offset = 0 - method peek_char = + method peek = if offset < String.length source then Some (source.[offset]) else None @@ -149,8 +162,8 @@ object method advance_impl = offset <- offset + 1 - method current_offset = offset + method private offset = offset - method slice_from_offset start_offset = + method slice (start_offset, _, _) = String.sub source start_offset (offset - start_offset) end View it on GitLab: https://gitlab.com/monnier/typer/-/compare/b6f70b8a97488267c3dc6ebc32f6e6a5… -- View it on GitLab: https://gitlab.com/monnier/typer/-/compare/b6f70b8a97488267c3dc6ebc32f6e6a5… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer] Deleted branch shorten-source-methods
by Simon Génier (＠ilovemonoids) 28 Sep '21

28 Sep '21

Simon Génier deleted branch shorten-source-methods at Stefan / Typer -- You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][master] 2 commits: Shorten the names of a few methods on source objects.
by Simon Génier (＠ilovemonoids) 28 Sep '21

28 Sep '21

Simon Génier pushed to branch master at Stefan / Typer Commits: 4fb0ccd3 by Simon Génier at 2021-06-09T12:40:18-04:00 Shorten the names of a few methods on source objects. These names were redundants. For instance in `current_offset`, the `current` part is already hinted at by the fact that source objects are a kind of cursor. Overall I think the new names a clearer since they are more concise. - - - - - aff91a51 by Simon Génier at 2021-09-28T17:16:11-04:00 Merge branch 'shorten-source-methods' - - - - - 3 changed files: - src/lexer.ml - src/prelexer.ml - src/source.ml Changes: ===================================== src/lexer.ml ===================================== @@ -42,30 +42,30 @@ let lex_number : sexp = let rec lex_exponent () = - match source#peek_char with + match source#peek with | Some ('0' .. '9') -> source#advance; lex_exponent () | _ - -> let source = source#slice_from_offset start_offset in + -> let source = source#slice start_offset in Float (start_location, float_of_string source) in let lex_exponent_sign () = - match source#peek_char with + match source#peek with | Some ('0' .. '9' | '+' | '-') -> source#advance; lex_exponent () (* TODO: error if there are no signs or digits after the 'e'? *) | _ - -> let source = source#slice_from_offset start_offset in + -> let source = source#slice start_offset in Float (start_location, float_of_string source) in let rec lex_fractional () = - match source#peek_char with + match source#peek with | Some ('0' .. '9') -> source#advance; lex_fractional () @@ -75,12 +75,12 @@ let lex_number lex_exponent_sign () | _ - -> let source = source#slice_from_offset start_offset in + -> let source = source#slice start_offset in Float (start_location, float_of_string source) in let rec lex_integer () = - match source#peek_char with + match source#peek with | Some ('0' .. '9') -> source#advance; lex_integer () @@ -94,7 +94,7 @@ let lex_number lex_exponent_sign () | _ - -> let source = source#slice_from_offset start_offset in + -> let source = source#slice start_offset in Integer (start_location, Z.of_string source) in @@ -110,16 +110,16 @@ let lex_symbol : sexp = let mksym start_location start_offset escaped = - if Int.equal start_offset source#current_offset + if Int.equal start_offset source#offset then epsilon start_location else - let raw_name = source#slice_from_offset start_offset in + let raw_name = source#slice start_offset in let name = if escaped then unescape raw_name else raw_name in hSymbol (start_location, name) in let rec loop start_location start_offset prec lf (escaped : bool) = - match source#peek_char with + match source#peek with | None -> lf (mksym start_location start_offset escaped) @@ -130,16 +130,16 @@ let lex_symbol | CKinner prec' -> let left = mksym start_location start_offset escaped in - let op_location = source#current_location doc in + let op_location = source#location doc in (* To be considered `inner`, an operator char needs to have something on its LHS or its RHS, otherwise, treat it as a normal char. `.` can be the normal function composition operator as well. *) - let lhs_p = start_offset != source#current_offset in + let lhs_p = start_offset != source#offset in source#advance; let rhs_p = - (match source#peek_char with + (match source#peek with | None -> false | Some c' -> CKseparate != token_env.(Char.code c')) in @@ -151,13 +151,13 @@ let lex_symbol then fun s -> lf (Node (op, [left; s])) else fun s -> Node (op, [lf left; s]) in - loop (source#current_location doc) source#current_offset prec' lf' false + loop (source#location doc) source#offset prec' lf' false else loop start_location start_offset prec lf escaped | CKnormal -> (source#advance; - let is_last = Option.is_none source#peek_char in + let is_last = Option.is_none source#peek in match c with (* Skip next char, in case it's a special token. For utf-8, simply advancing is risky but actually works: '\' counts as 1 @@ -178,17 +178,17 @@ let split_presymbol : sexp list = let rec loop (acc : sexp list) : sexp list = - match source#peek_char with + match source#peek with | None -> List.rev acc | Some (c) - -> let start_offset = source#current_offset in - let start_location = source#current_location doc in + -> let start_offset = source#offset in + let start_location = source#location doc in let token = match c with (* A negative number literal, or a symbol starting with '-'. *) | '-' -> (source#advance; - match source#peek_char with + match source#peek with | Some ('0' .. '9') -> lex_number source start_location start_offset | _ @@ -200,7 +200,7 @@ let split_presymbol | _ when token_env.(Char.code c) = CKseparate -> source#advance; - let name = source#slice_from_offset start_offset in + let name = source#slice start_offset in hSymbol (start_location, name) | _ ===================================== src/prelexer.ml ===================================== @@ -74,7 +74,7 @@ let prelex (source : #Source.t) : pretoken list = (doc : string) : pretoken list = - match source#peek_char with + match source#peek with | None -> (match ctx with | [] -> List.rev acc @@ -94,9 +94,9 @@ let prelex (source : #Source.t) : pretoken list = (* line's bounds seems ok: String.sub line 1 0 == "" *) | Some ('@') -> source#advance; - let start_offset = source#current_offset in + let start_offset = source#offset in consume_until_newline source; - let new_doc = String.trim (source#slice_from_offset start_offset) in + let new_doc = String.trim (source#slice start_offset) in loop ctx acc (doc ^ "\n" ^ new_doc) (* A string. *) @@ -105,26 +105,26 @@ let prelex (source : #Source.t) : pretoken list = let rec prestring chars = match source#next_char with | None | Some ('\n') - -> let location = source#current_location doc in + -> let location = source#location doc in prelexer_error location "Unterminated string"; loop ctx (Prestring (location, "") :: acc) "" | Some ('"') - -> let location = source#current_location doc in + -> let location = source#location doc in let pretoken = Prestring (location, string_implode (List.rev chars)) in loop ctx (pretoken :: acc) "" | Some ('\\') -> (match source#next_char with | None | Some ('\n') - -> let location = source#current_location doc in + -> let location = source#location doc 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#current_location doc in + -> let location = source#location doc in prelexer_error location "Unimplemented unicode escape"; prestring chars | Some (c) -> prestring (c :: chars)) @@ -134,12 +134,12 @@ let prelex (source : #Source.t) : pretoken list = | Some ('{') -> source#advance; - let ctx' = (source#current_location doc, acc) :: ctx in + let ctx' = (source#location doc, acc) :: ctx in loop ctx' [] doc | Some ('}') -> source#advance; - let location = source#current_location doc in + let location = source#location doc in (match ctx with | ((slocation, sacc) :: ctx) -> let preblock = Preblock (slocation, List.rev acc, location) in @@ -150,18 +150,18 @@ let prelex (source : #Source.t) : pretoken list = (* A pretoken. *) | Some _ - -> let start_offset = source#current_offset in + -> let start_offset = source#offset in source#advance; let rec pretok () = - match source#peek_char with + match source#peek with | None | Some ('%' | '"' | '{' | '}') - -> let location = source#current_location doc in - let text = source#slice_from_offset start_offset in + -> let location = source#location doc in + let text = source#slice start_offset in loop ctx (Pretoken (location, text) :: acc) "" | Some (c) when c <= ' ' - -> let location = source#current_location doc in - let text = source#slice_from_offset start_offset in + -> let location = source#location doc in + let text = source#slice start_offset in source#advance; loop ctx (Pretoken (location, text) :: acc) "" @@ -170,9 +170,9 @@ let prelex (source : #Source.t) : pretoken list = (match source#next_char with | Some _ -> pretok () | None - -> let location = source#current_location doc in + -> let location = source#location doc in source#advance; - let text = source#slice_from_offset start_offset in + let text = source#slice start_offset in prelexer_error location ("Unterminated escape sequence in: " ^ text); loop ctx (Pretoken (location, text) :: acc) "") ===================================== src/source.ml ===================================== @@ -43,24 +43,24 @@ let first_column_of_line = 1 (* A source object is text paired with a cursor. The text can be lazily loaded as it is accessed byte by byte, but it must be retained for future reference by error messages. *) -class virtual t (base_line : int) (base_column : int) (file_name : string) = +class virtual t (base_line : int) (base_column : int) (file : string) = object (self) val mutable line = base_line val mutable column = base_column (* A path if the text comes from a file, otherwise a meaningful identifier. *) - method file_name : string = file_name + method file : string = file (* Return the byte at the cursor, or None if the cursor is at the end of the text. *) - method virtual peek_char : char option + method virtual peek : char option (* The current location of the cursor. *) - method current_location (docstr : string) : Location.t = - {file = file_name; line; column; docstr} + method location (docstr : string) : Location.t = + {file; line; column; docstr} (* The current offset of the cursor in the file, in bytes. *) - method virtual current_offset : int + method virtual offset : int (* Slices the text, from (and including) a starting offset and to (and excluding) the curent cursor offset. @@ -68,12 +68,12 @@ object (self) 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 virtual slice_from_offset : int -> string + method virtual slice : int -> string (* Moves the cursor forward one byte *) method advance : unit = let is_utf8_head c = Char.code c < 128 || Char.code c >= 192 in - let c = self#peek_char in + let c = self#peek in self#advance_impl; match c with | Some '\n' @@ -87,7 +87,7 @@ object (self) (* Returns the char at the cursor, then advances it forward. *) method next_char : char option = - let c = self#peek_char in + let c = self#peek in self#advance; c end @@ -103,29 +103,29 @@ class source_file file_name = object (self) val mutable line_offset = 0 val mutable offset = 0 - method private peek_char_unchecked = + method private peek_unchecked = if offset < String.length source_line then source_line.[offset] else '\n' - method peek_char = + method peek = if offset <= String.length source_line - then Some self#peek_char_unchecked + then Some self#peek_unchecked else try line_offset <- line_offset + 1 + String.length source_line; source_line <- input_line in_channel; offset <- 0; - Some self#peek_char_unchecked + Some self#peek_unchecked with | End_of_file -> None method advance_impl = offset <- offset + 1 - method current_offset = line_offset + offset + method offset = line_offset + offset - method slice_from_offset start_offset = + method slice start_offset = let relative_start_offset = start_offset - line_offset in String.sub source_line relative_start_offset (offset - relative_start_offset) end @@ -141,7 +141,7 @@ object val mutable offset = 0 - method peek_char = + method peek = if offset < String.length source then Some (source.[offset]) else None @@ -149,8 +149,8 @@ object method advance_impl = offset <- offset + 1 - method current_offset = offset + method offset = offset - method slice_from_offset start_offset = + method slice start_offset = String.sub source start_offset (offset - start_offset) end View it on GitLab: https://gitlab.com/monnier/typer/-/compare/a7ac505a8249a889aa1235f6823b1c70… -- View it on GitLab: https://gitlab.com/monnier/typer/-/compare/a7ac505a8249a889aa1235f6823b1c70… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][soilih] considerate vname loc and ltype
by Soilihi BEN SOILIHI BOINA (＠BenSoilih) 27 Sep '21

27 Sep '21

Soilihi BEN SOILIHI BOINA pushed to branch soilih at Stefan / Typer Commits: 9d9ea020 by Soilih BEN SOILIH at 2021-09-27T15:05:21-06:00 considerate vname loc and ltype - - - - - 2 changed files: - src/REPL.ml - src/typer_lsp_server.ml Changes: ===================================== src/REPL.ml ===================================== @@ -150,6 +150,8 @@ let eval_interactive List.iter interactive#process_decls ldecls; print_and_clear_log (); + + List.iter Lexp.lexp_print lexprs; let values = List.map interactive#eval_expr lexprs in List.iter (Eval.print_eval_result i) values; ===================================== src/typer_lsp_server.ml ===================================== @@ -125,13 +125,12 @@ let rec nearest_lexp_of_the_list (liste : (vname * Lexp.lexp * Lexp.ltype) list) match liste with | [] -> failwith "No Lexp found!!!" - | [n] -> let (_,lxp,_) = n in - lxp + | [n] -> n | [hd;tl] -> let (_,lxp_hd,_) = hd in let (_,lxp_tl,_) = tl in if (dist (Lexp.lexp_location lxp_hd) cursor < dist (Lexp.lexp_location lxp_tl) cursor ) - then lxp_hd - else lxp_tl + then hd + else tl | hd::ml::tl -> let (_,lxp_hd,_) = hd in let (_,lxp_ml,_) = ml in if (dist (Lexp.lexp_location lxp_hd) cursor < dist (Lexp.lexp_location lxp_ml) cursor ) @@ -376,16 +375,17 @@ let update_the_context (ctx: Debruijn.lexp_context) (liste : (vname * Lexp.lexp let lstr = update_the_context ctx lst in - let rec foo (ls: (Debruijn.lexp_context * (vname * Lexp.lexp * Lexp.ltype) list) list) (cursor:Source.Location.t) : Debruijn.lexp_context * Lexp.lexp = + let rec foo (ls: (Debruijn.lexp_context * (vname * Lexp.lexp * Lexp.ltype) list) list) (cursor:Source.Location.t) : (Debruijn.lexp_context * (vname * Lexp.lexp * Lexp.ltype)) = match ls with | [] -> failwith "No Lexp found!" | hd::tl -> let (lctx_hd, hdl) = hd in - let lxp = nearest_lexp_of_the_list hdl cursor in + let v = nearest_lexp_of_the_list hdl cursor in + let (_,lxp,_) = v in let location = Lexp.lexp_location lxp in if ((location.start_line <= cursor.start_line && location.start_column <= cursor.start_column) && (location.end_line >= cursor.end_line && location.end_column >= cursor.end_column)) - then (lctx_hd,lxp) + then (lctx_hd, v) else foo tl cursor in foo lstr cursor @@ -394,18 +394,18 @@ let update_the_context (ctx: Debruijn.lexp_context) (liste : (vname * Lexp.lexp let lstr = update_the_context ctx lst in - let rec foo (ls: (Debruijn.lexp_context * (vname * Lexp.lexp * Lexp.ltype) list) list) (cursor:Source.Location.t) : Debruijn.lexp_context * Lexp.lexp = + let rec foo (ls: (Debruijn.lexp_context * (vname * Lexp.lexp * Lexp.ltype) list) list) (cursor:Source.Location.t) : (Debruijn.lexp_context * (vname * Lexp.lexp * Lexp.ltype)) = match ls with | [] -> failwith "No Lexp found!" | [n] -> let (lctx,l) = n in - let lxp = nearest_lexp_of_the_list l cursor in - (lctx,lxp) + let v = nearest_lexp_of_the_list l cursor in + (lctx,v) | [hd;tl] -> let (lctx_hd,hdl) = hd in let (lctx_tl,tll) = tl in - let lxp = nearest_lexp_of_the_list hdl cursor in - let lxp' = nearest_lexp_of_the_list tll cursor in - if (dist (Lexp.lexp_location lxp) cursor < dist (Lexp.lexp_location lxp') cursor ) + let (_,x,_) as lxp = nearest_lexp_of_the_list hdl cursor in + let (_,y,_) as lxp' = nearest_lexp_of_the_list tll cursor in + if (dist (Lexp.lexp_location x) cursor < dist (Lexp.lexp_location y) cursor ) then (lctx_hd,lxp) else ( @@ -413,9 +413,9 @@ let update_the_context (ctx: Debruijn.lexp_context) (liste : (vname * Lexp.lexp ) | hd::ml::tl -> let (lctx_hd,hdl) = hd in let (lctx_ml,mll) = ml in - let lxp = nearest_lexp_of_the_list hdl cursor in - let lxp' = nearest_lexp_of_the_list mll cursor in - if (dist (Lexp.lexp_location lxp) cursor < dist (Lexp.lexp_location lxp') cursor ) + let (_,x,_) as lxp = nearest_lexp_of_the_list hdl cursor in + let (_,y,_) as lxp' = nearest_lexp_of_the_list mll cursor in + if (dist (Lexp.lexp_location x) cursor < dist (Lexp.lexp_location y) cursor ) then (foo (hd::tl) cursor) else foo (ml::tl) cursor @@ -502,9 +502,10 @@ let update_the_context (ctx: Debruijn.lexp_context) (liste : (vname * Lexp.lexp | Lambda (ak, ((l,_) as v), t, e) -> let ctx' = Debruijn.lctx_extend ctx v Variable t in let a = browse_lexp ctx' e cursor in let b = browse_lexp ctx t cursor in - let etp = Opslexp.get_type ctx' e in - let c = (ctx,None, Lexp.mkArrow (ak,v,t,l,etp),l) in - browse_list_lexp ([a;b;c]) cursor + (*let etp = Opslexp.get_type ctx' e in + let c = (ctx,None, Lexp.mkArrow (ak,v,t,l,etp),l) in*) + let d = (ctx,None, t,l) in + browse_list_lexp ([a;b;d]) cursor | Call (f, args) -> ( @@ -789,7 +790,7 @@ let lsp_compl_from_var (ret : Debruijn.lexp_context * (((Source.Location.t * str let lst = update_the_context ctx list_list in let nlst = List.map ( fun x -> let (lctx,liste) = x in - let lxp = nearest_lexp_of_the_list liste cursor in + let (_,lxp,_) = nearest_lexp_of_the_list liste cursor in browse_lexp lctx lxp cursor ) lst in List.filter (fun x -> @@ -983,7 +984,8 @@ class lsp_server = let (list_list, _) = ast in let typer_loc = typer_pos_of_lsp_pos pos in let ctx = Debruijn.ectx_to_lctx (Elab.default_ectx) in - let (lctx,lexp) = lexp_search ctx list_list typer_loc in + let (lctx,vx) = lexp_search ctx list_list typer_loc in + let (_,lexp,_) = vx in let (l_ctx, idx,_ ,_ ) as ret = browse_lexp lctx lexp typer_loc in let loc = find_def_location l_ctx ret in let l = Lsp.Types.Location.create @@ -1000,8 +1002,11 @@ class lsp_server = let (list_list, _) = ast in let typer_loc = typer_pos_of_lsp_pos pos in let ctx = Debruijn.ectx_to_lctx (Elab.default_ectx) in - let (lctx,lexp) = lexp_search ctx list_list typer_loc in - let (l_ctx,_,l_type,location) = browse_lexp lctx lexp typer_loc in + let (lctx,vx) = lexp_search ctx list_list typer_loc in + let ((lvn,_),lexp,ltyp) = vx in + let (l_ctx_r,_,_,_) as ret = browse_lexp lctx lexp typer_loc in + let ret' = (l_ctx_r,None,ltyp,lvn) in + let (l_ctx,_,l_type,location) = browse_list_lexp [ret;ret'] typer_loc in let range = lsp_range_of_loc location in let s = Lexp.lexp_string_for_lsp l_type in let r = Lsp.Types.Hover.create @@ -1045,7 +1050,8 @@ class lsp_server = let (list_list, _) = ast in let typer_loc = typer_pos_of_lsp_pos pos in let ctx = Debruijn.ectx_to_lctx (Elab.default_ectx) in - let (lctx,lexp) = lexp_search ctx list_list typer_loc in + let (lctx,vx) = lexp_search ctx list_list typer_loc in + let (_,lexp,_) = vx in let (l_ctx,_,_,_) = browse_lexp lctx lexp typer_loc in (* @@ -1083,15 +1089,17 @@ let hoverTest (ctx:Debruijn.lexp_context) (name:string) (content:string) (posit let (list_list, _) = ast in let (l,c) = position in let pos = pos_of_tuple position in - let (lctx,lexp) = lexp_search ctx list_list pos in + let (lctx,vx) = lexp_search ctx list_list pos in + let (_,lexp,_) = vx in let (_,_, l_type,_) = browse_lexp lctx lexp pos in + let excpect = "excpected : " ^ expected ^ "\n" in let output = "output : " ^ (Lexp.lexp_string_for_lsp l_type) ^ "\n\n" in let input = "input : " ^ content ^ "\n" in let res = "result : " ^ (comp expected (Lexp.lexp_string_for_lsp l_type)) in let pos = "position : line " ^ (string_of_int l) ^ " character " ^ (string_of_int c) ^ "\n" in let sep = "################################################\n" in let oc = open_out_gen [Open_creat; Open_text; Open_append] 0o640 name in - output_string oc (sep ^ input ^ pos ^ output ^ res ^ sep ); + output_string oc (sep ^ input ^ pos ^ excpect ^ output ^ res ^ sep ); close_out oc let sep name s = @@ -1114,21 +1122,27 @@ let test () = hoverTest ctx name "f = 12.3 ;" (1,1) "##Float"; hoverTest ctx name "f = 12.3 ;" (1,6) "##Float"; sep name "LAMBDA"; - hoverTest ctx name "l = (lambda x -> _+_ x 2) ;" (1,1) "##Type"; - hoverTest ctx name "l = (lambda x -> _+_ x 2) ;" (1,8) "##Int"; + hoverTest ctx name "l = (lambda x -> _+_ x 2) ;" (1,1) "(x : ##Int) -> Int"; + hoverTest ctx name "l = (lambda x -> _+_ x 2) ;" (1,8) "(x : ##Int) -> Int"; hoverTest ctx name "l = (lambda x -> _+_ x 2) ;" (1,13) "##Int"; hoverTest ctx name "l = (lambda x -> _+_ x 2) ;" (1,19) "(Int -> (Int -> Int))"; hoverTest ctx name "l = (lambda x -> _+_ x 2) ;" (1,21) "##Int"; sep name "FUNCTION(LAMBDA)"; - hoverTest ctx name "multiply x y z = _*_ x y ;" (1,1) "##TypeLevel"; + hoverTest ctx name "multiply x y z = _*_ x y ;" (1,1) "(ℓ : ##TypeLevel) ≡> (τ : (##Type_ ℓ)) ≡> (x : ##Int) -> (y : ##Int) -> (z : τ) -> Int"; hoverTest ctx name "multiply x y z = _*_ x y ;" (1,10) "##Int"; hoverTest ctx name "multiply x y z = _*_ x y ;" (1,12) "##Int"; hoverTest ctx name "multiply x y z = _*_ x y ;" (1,14) "τ"; - hoverTest ctx name "multiply x y z = _*_ x y ;" (1,19) "(Int -> (Int -> Int))"; - hoverTest ctx name "multiply x y z = x + y + z ;" (1,19) "##Int"; - hoverTest ctx name "multiply x y z = x + y + z ;" (1,23) "##Int"; - hoverTest ctx name "multiply x y z = x + y + z ;" (1,28) "##Int"; - hoverTest ctx name "multiply x y z = _*_ x y ;" (1,26) "##Int"; + hoverTest ctx name "multiply x y z = _*_ x y ;" (1,18) "(Int -> (Int -> Int))"; + hoverTest ctx name "multiply x y z = _*_ x y ;" (1,21) "##Int"; + hoverTest ctx name "multiply x y z = _*_ x y ;" (1,23) "##Int"; + hoverTest ctx name "multiply x y z = x + y + z ;" (1,1) "(x : ##Int) -> (y : ##Int) -> (z : ##Int) -> Int"; + hoverTest ctx name "multiply x y z = x + y + z ;" (1,10) "##Int"; + hoverTest ctx name "multiply x y z = x + y + z ;" (1,12) "##Int"; + hoverTest ctx name "multiply x y z = x + y + z ;" (1,14) "##Int"; + hoverTest ctx name "multiply x y z = x + y + z ;" (1,18) "##Int"; + hoverTest ctx name "multiply x y z = x + y + z ;" (1,20) "(Int -> (Int -> Int))"; + hoverTest ctx name "multiply x y z = x + y + z ;" (1,22) "##Int"; + hoverTest ctx name "multiply x y z = x + y + z ;" (1,26) "##Int"; sep name "CALL"; hoverTest ctx name "multiply x y z = _*_ x y ; \n\n\ne = multiply 2 3 \"h\" ;" (4,1) "(ℓ : ##TypeLevel) ≡> (τ : (##Type_ ℓ)) ≡> (x : ##Int) -> (y : ##Int) -> (z : τ) -> Int"; hoverTest ctx name "multiply x y z = _*_ x y ; \n\n\ne = multiply 2 3 \"h\" ;" (4,7) "(ℓ : ##TypeLevel) ≡> (τ : (##Type_ ℓ)) ≡> (x : ##Int) -> (y : ##Int) -> (z : τ) -> Int"; @@ -1141,6 +1155,8 @@ let test () = sep name "SUSP"; hoverTest ctx name "foo = ##Int ; \n\n\nv = foo ;" (4,1) "(##Type_ ##TypeLevel.z)"; hoverTest ctx name "foo = ##Int ; \n\n\nv = foo ;" (4,6) "(##Type_ ##TypeLevel.z)"; + hoverTest ctx name "foo = ##String ; \n\n\nv = foo ;" (4,1) "(##Type_ (##TypeLevel.succ ##TypeLevel.z))"; + hoverTest ctx name "foo = ##Type ; \n\n\nv = foo ;" (4,1) "(##Type_ ##TypeLevel.z)"; sep name "LIST"; hoverTest ctx name "lst = cons 2 ( (cons 1 ) nil ) ;" (1,1) "##Type"; hoverTest ctx name "lst = cons 2 ( (cons 1 ) nil ) ;" (1,8) "(ℓ : TypeLevel) ≡> (a : (##Type_ ℓ)) ≡> (a -> ((List ℓ a) -> (List ℓ a)))"; @@ -1148,6 +1164,10 @@ let test () = hoverTest ctx name "lst = cons 2 ( (cons 1 ) nil ) ;" (1,27) "(ℓ : TypeLevel) ≡> (a : (##Type_ ℓ)) ≡> (List ℓ a)"; sep name "ARROW"; hoverTest ctx name "type Floo = bar Int Int ;" (1,1) ""; + hoverTest ctx name "floo = typecons (floo) (bar Int Int) ;\n\n\nbar = datacons floo bar ;" (4,17) ""; + hoverTest ctx name "floo = typecons (floo) (bar Int Int) ;\n\n\nbar = datacons floo bar ;" (4,29) ""; + hoverTest ctx name "v = Int -> Int ;" (1,1) ""; + sep name "INDUCTIVE"; hoverTest ctx name "type Floo = bar Int Int ;" (1,7) ""; hoverTest ctx name "type Floo = bar Int Int ;" (1,18) ""; hoverTest ctx name "type Floo = bar Int Int ;" (1,22) ""; @@ -1156,10 +1176,6 @@ let test () = hoverTest ctx name "floo = typecons (floo) (bar Int Int) ;\n\n\nbar = datacons floo bar ;" (1,26) ""; hoverTest ctx name "floo = typecons (floo) (bar Int Int) ;\n\n\nbar = datacons floo bar ;" (4,1) ""; hoverTest ctx name "floo = typecons (floo) (bar Int Int) ;\n\n\nbar = datacons floo bar ;" (4,10) ""; - hoverTest ctx name "floo = typecons (floo) (bar Int Int) ;\n\n\nbar = datacons floo bar ;" (4,17) ""; - hoverTest ctx name "floo = typecons (floo) (bar Int Int) ;\n\n\nbar = datacons floo bar ;" (4,29) ""; - hoverTest ctx name "v = Int -> Int ;" (1,1) ""; - sep name "INDUCTIVE"; hoverTest ctx name "Bool = typecons (Bool) (true) (false);" (1,1) ""; hoverTest ctx name "Bool = typecons (Bool) (true) (false);" (1,10) ""; hoverTest ctx name "Bool = typecons (Bool) (true) (false);" (1,18) ""; @@ -1195,6 +1211,9 @@ let test () = hoverTest ctx name "foo x = case x\n\n| true => \"h\"\n\n| false => \"jj\" ;" (3,13) ""; hoverTest ctx name "foo x = case x\n\n| true => \"h\"\n\n| false => \"jj\" ;" (5,4) ""; hoverTest ctx name "foo x = case x\n\n| true => \"h\"\n\n| false => \"jj\" ;" (5,14) "" + + + (*=======================================Test======================================*) @@ -1206,7 +1225,7 @@ let test () = let run () = ignore (Arg.Set Log.lsp_enabled); Logs.set_level ~all:true (Some Logs.Debug); - (*test ();*) + test (); let s = new lsp_server in let server = Linol_lwt.Jsonrpc2.create_stdio s in let task = Linol_lwt.Jsonrpc2.run server in View it on GitLab: https://gitlab.com/monnier/typer/-/commit/9d9ea020a8374265e9c72b83c66b6a59c… -- View it on GitLab: https://gitlab.com/monnier/typer/-/commit/9d9ea020a8374265e9c72b83c66b6a59c… You're receiving this email because of your account on gitlab.com.

1 0

2024

2023

2022

2021

2020

2019

2018

2017

2016

Typer Septembre 2021