Simon Génier pushed to branch master at Stefan / Typer

Commits: b3875d28 by Simon Génier at 2021-03-22T15:59:01-04:00 Introduce source objects.

Source objects abstract over the text of Typer code. Does it come from a file? A string? Only the source object knows.

I extracted it from my Typer to Scheme compiler patch. By itself, I think it makes for slightly nicer code, but the real advantages are * We no longer process source text line by line. Supporting multi-line string is now as easy as removing the error. * We keep the full source text around. We can add it to locations so we are able to print the original source along an error message.

- - - - - e3fb3f5e by Simon Génier at 2021-03-24T19:54:15-04:00 [Source] Do not buffer more than one line.

- - - - - 424af536 by Simon Génier at 2021-04-02T16:11:45-04:00 Merge branch 'source-object'

- - - - -

6 changed files:

- src/REPL.ml - src/elab.ml - src/eval.ml - src/lexer.ml - src/prelexer.ml - + src/source.ml

Changes:

===================================== src/REPL.ml ===================================== @@ -143,14 +143,14 @@ let ilexp_parse pexps lctx: ((ldecl list list * lexpr list) * elab_context) = lexprs; (ldecls, lexprs), lctx

-let ieval f str ectx rctx = +let ieval source ectx rctx = let ieval' lexps rctx = let (ldecls, lexprs) = lexps in let rctx = eval_decls_toplevel ldecls rctx in let vals = eval_all lexprs rctx false in vals, rctx in

- let pres = (f str) in + let pres = prelex source in let sxps = lex default_stt pres in (* FIXME: This is too eager: it prevents one declaration from changing * the grammar used in subsequent declarations. *) @@ -163,8 +163,8 @@ let ieval f str ectx rctx = let v, rctx = ieval' elxps rctx in v, ectx', rctx

-let raw_eval f str ectx rctx = - let pres = (f str) in +let raw_eval source ectx rctx = + let pres = prelex source in let sxps = lex default_stt pres in let lxps, ectx' = Elab.lexp_p_decls [] sxps ectx in let _, elxps = Listx.fold_left_map OL.clean_decls (ectx_to_lctx ectx) lxps in @@ -178,13 +178,6 @@ let raw_eval f str ectx rctx = (* This is for consistency with ieval *) [], ectx', rctx

-let ieval_string = ieval prelex_string -let ieval_file = ieval prelex_file - -let eval_string = raw_eval prelex_string -let eval_file = raw_eval prelex_file - - let welcome_msg = " Typer 0.0.0 - Interpreter - (c) 2016

@@ -212,8 +205,10 @@ let readfiles files (i, lctx, rctx) prt = print_string " In["; ralign_print_int i 2; print_string "] >> "; print_string ("%readfile " ^ file); print_string "\n";));

- try let (ret, lctx, rctx) = eval_file file lctx rctx in - (List.iter (print_eval_result i) ret; (i + 1, lctx, rctx)) + try + let source = new Source.source_file file in + let (ret, lctx, rctx) = raw_eval source lctx rctx in + (List.iter (print_eval_result i) ret; (i + 1, lctx, rctx)) with Sys_error _ -> ( ieval_error ("file "" ^ file ^ "" does not exist."); @@ -263,10 +258,12 @@ let rec repl i clxp rctx =

(* eval input *) | _ -> - try let (ret, clxp, rctx) = (ieval_string ipt clxp rctx) in - print_and_clear_log (); - List.iter (print_eval_result i) ret; - repl clxp rctx + try + let source = new Source.source_string ipt in + let (ret, clxp, rctx) = (ieval source clxp rctx) in + print_and_clear_log (); + List.iter (print_eval_result i) ret; + repl clxp rctx with | Log.Stop_Compilation msg -> (handle_stopped_compilation msg; repl clxp rctx)

===================================== src/elab.ml ===================================== @@ -1772,8 +1772,9 @@ let in_pervasive = ref true let sform_load usr_elctx loc sargs _ot =

let read_file file_name elctx = + let source = new Source.source_file file_name in let pres = - try prelex_file file_name with + try prelex source with | Sys_error _ -> error ~loc ("Could not load `" ^ file_name ^ "`: file not found."); [] in @@ -1858,7 +1859,8 @@ let default_ectx

(* Read BTL files *) let read_file file_name elctx = - let pres = prelex_file file_name in + let source = new Source.source_file file_name in + let pres = prelex source in let sxps = lex default_stt pres in let _, lctx = lexp_p_decls [] sxps elctx in lctx in @@ -1912,7 +1914,8 @@ let lexp_expr_str str ctx = let tenv = default_stt in let grm = ectx_get_grammar ctx in let limit = Some ";" in - let pxps = sexp_parse_str str tenv grm limit in + let source = new Source.source_string str in + let pxps = sexp_parse_source source tenv grm limit in let lexps = lexp_parse_all pxps ctx in List.iter (fun lxp -> ignore (OL.check (ectx_to_lctx ctx) lxp)) lexps; @@ -1920,7 +1923,8 @@ let lexp_expr_str str ctx =

let lexp_decl_str str ctx = let tenv = default_stt in - let tokens = lex_str str tenv in + let source = new Source.source_string str in + let tokens = lex_source source tenv in lexp_p_decls [] tokens ctx

===================================== src/eval.ml ===================================== @@ -353,7 +353,9 @@ let make_float loc _depth args_val = match args_val with

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

let reader_parse loc _depth args_val = match args_val with

===================================== src/lexer.ml ===================================== @@ -1,6 +1,6 @@ (* lexer.ml --- Second half of lexical analysis of Typer.

-Copyright (C) 2011-2018 Free Software Foundation, Inc. +Copyright (C) 2011-2021 Free Software Foundation, Inc.

Author: Stefan Monnier monnier@iro.umontreal.ca Keywords: languages, lisp, dependent types. @@ -144,11 +144,11 @@ let lex tenv (pts : pretoken list) : sexp list = in gettokens pts bpos cpos (tok :: acc) in gettokens pts 0 0 []

-let lex_str (str: string) tenv = - let pretoks = prelex_string str in - lex tenv pretoks +let lex_source (source : #Source.t) tenv = + let pretoks = prelex source in + lex tenv pretoks

-let sexp_parse_str (str: string) tenv grm limit = - let toks = lex_str str tenv in - sexp_parse_all_to_list grm toks limit +let sexp_parse_source (source : #Source.t) tenv grm limit = + let toks = lex_source source tenv in + sexp_parse_all_to_list grm toks limit

===================================== src/prelexer.ml ===================================== @@ -1,6 +1,6 @@ (* prelexer.ml --- First half of lexical analysis of Typer.

-Copyright (C) 2011-2020 Free Software Foundation, Inc. +Copyright (C) 2011-2021 Free Software Foundation, Inc.

Author: Stefan Monnier monnier@iro.umontreal.ca Keywords: languages, lisp, dependent types. @@ -50,114 +50,135 @@ let inc_cp (cp:charpos) (c:char) = (* Count char positions in utf-8: don't count the non-leading bytes. *) if utf8_head_p c then cp+1 else cp

-let rec prelex (file : string) (getline : unit -> string) ln ctx acc (doc : string) +let rec consume_until_newline (source : #Source.t) : unit = + match source#next_char with + | None | Some ('\n') -> () + | Some _ -> consume_until_newline source + +let rec prelex (source : #Source.t) ln ctx acc (doc : string) : pretoken list = - try - (* let fin = open_in file in *) - let line = getline () in - let limit = String.length line in - let nextline = prelex file getline (ln + 1) in - let rec prelex' ctx (bpos:bytepos) (cpos:charpos) acc doc = - let nexttok = prelex' ctx in - if bpos >= limit then nextline ctx acc doc else - match line.[bpos] with - | c when c <= ' ' -> nexttok (bpos+1) (cpos+1) acc doc - | '%' -> nextline ctx acc doc (* A comment. *) - (* line's bounds seems ok: String.sub line 1 0 == "" *) - | '@' -> nextline ctx acc (String.concat "\n" [doc; (String.sub line 1 (limit - 1))]) - | '"' (* A string. *) - -> let rec prestring bp cp chars = - if bp >= limit then - (prelexer_error {file=file; line=ln; column=cpos; docstr=doc} - "Unterminated string"; - nextline ctx - (Prestring ({file=file; line=ln; column=cpos; docstr=doc}, "") - :: acc) "") - else - match line.[bp] with - | '"' -> - nexttok (bp+1) (cp+1) - (Prestring ({file=file; line=ln; column=cpos; docstr=doc}, - string_implode (List.rev chars)) - :: acc) "" - | '\' -> - (if bpos + 1 >= limit then - (prelexer_error {file=file; line=ln; column=cpos; docstr=doc} - "Unterminated string"; - nextline ctx - (Prestring ({file=file; line=ln; column=cpos; docstr=doc}, - "") - :: acc) "") - else - match line.[bp + 1] with - | 't' -> prestring (bp+2) (cp+2) ('\t' :: chars) - | 'n' -> prestring (bp+2) (cp+2) ('\n' :: chars) - | 'r' -> prestring (bp+2) (cp+2) ('\r' :: chars) - | ('u' | 'U') -> - prelexer_error {file=file; line=ln; column=cp; docstr=doc} - "Unimplemented unicode escape"; - prestring (bp+2) (cp+2) chars - | char -> prestring (bp+2) (cp+2) (char :: chars)) - | char -> prestring (bp+1) (inc_cp cp char) (char :: chars) - in prestring (bpos+1) (cpos+1) [] - | '{' -> prelex' ((ln, cpos, bpos, acc) :: ctx) (bpos+1) (cpos+1) [] doc - | '}' - -> (match ctx with - | ((sln, scpos, _sbpos, sacc) :: ctx) -> - prelex' ctx (bpos+1) (cpos+1) - (Preblock ({file=file; line=sln; column=scpos; docstr=doc}, - List.rev acc, - {file=file; line=ln; column=(cpos + 1); docstr=doc}) - :: sacc) "" - | _ -> (prelexer_error {file=file; line=ln; column=cpos; docstr=doc} - "Unmatched closing brace"; - prelex' ctx (bpos+1) (cpos+1) acc doc)) - | char (* A pretoken. *) - -> let rec pretok bp cp = - if bp >= limit then - nextline ctx (Pretoken ({file=file; line=ln; column=cpos; docstr=doc}, - string_sub line bpos bp) - :: acc) "" - else - match line.[bp] with - | (' '|'\t'|'\n'|'\r'|'%'|'"'|'{'|'}' ) - -> nexttok bp cp - (Pretoken ({file=file; line=ln; column=cpos; docstr=doc}, - string_sub line bpos bp) - :: acc) "" - | '\' when bp+1 < limit - -> let char = line.[bp + 1] in - pretok (bp + 2) (1 + inc_cp cp char) - | char -> pretok (bp+1) (inc_cp cp char) - in pretok (bpos+1) (inc_cp cpos char) - in prelex' ctx 0 1 acc doc (* Traditionally, column numbers start at 1 :-( *) - with End_of_file -> - match ctx with + + let nextline = prelex source (ln + 1) in + let rec prelex' ctx (cpos:charpos) acc doc = + let nexttok = prelex' ctx in + match source#peek_char with + | None + -> (match ctx with | [] -> List.rev acc - | ((ln, cpos, _, _) :: _ctx) -> - (prelexer_error {file=file; line=ln; column=cpos; docstr=""} - "Unmatched opening brace"; List.rev acc) - - -let prelex_file file = - let fin = open_in file - in prelex file (fun _ -> input_line fin) - (* Traditionally, line numbers start at 1 :-( *) - 1 [] [] "" - -let prelex_string str = - let pos = ref 0 in - let getline () = - let start = !pos in - if start >= String.length str then raise End_of_file else - let i = try String.index_from str start '\n' - with Not_found -> String.length str - 1 in - let npos = i + 1 in - pos := npos; - let line = string_sub str start npos in - (* print_string ("Read line: " ^ line); *) - line - in prelex "<string>" getline 1 [] [] "" + | ((ln, cpos, _) :: _ctx) -> + (prelexer_error {file=source#file_name; line=ln; column=cpos; docstr=""} + "Unmatched opening brace"; List.rev acc)) + + | Some ('\n') + -> source#advance; + nextline ctx acc doc + + | Some (c) when c <= ' ' + -> source#advance; + nexttok (cpos+1) acc doc + + (* A comment. *) + | Some ('%') + -> consume_until_newline source; + nextline ctx acc doc + + (* line's bounds seems ok: String.sub line 1 0 == "" *) + | Some ('@') + -> source#advance; + let start_offset = source#current_offset in + consume_until_newline source; + let new_doc = String.trim (source#slice_from_offset start_offset) in + nextline ctx acc (doc ^ "\n" ^ new_doc) + + (* A string. *) + | Some ('"') + -> source#advance; + let rec prestring cp chars = + match source#next_char with + | None | Some ('\n') + -> let location = {file=source#file_name; line=ln; column=cpos; docstr=doc} in + prelexer_error location "Unterminated string"; + nextline ctx (Prestring (location, "") :: acc) "" + + | Some ('"') + -> let location = {file=source#file_name; line=ln; column=cpos; docstr=doc} in + let pretoken = Prestring (location, string_implode (List.rev chars)) in + nexttok (cp + 1) (pretoken :: acc) "" + + | Some ('\') + -> (match source#next_char with + | None | Some ('\n') + -> let location = {file=source#file_name; line=ln; column=cp; docstr=doc} in + prelexer_error location "Unterminated escape sequence"; + nextline ctx (Prestring (location, "") :: acc) "" + | Some ('t') -> prestring (cp + 2) ('\t' :: chars) + | Some ('n') -> prestring (cp + 2) ('\n' :: chars) + | Some ('r') -> prestring (cp + 2) ('\r' :: chars) + | Some ('u') + -> let location = {file=source#file_name; line=ln; column=cp; docstr=doc} in + prelexer_error location "Unimplemented unicode escape"; + prestring (cp + 2) chars + | Some (c) -> prestring (cp + 2) (c :: chars)) + + | Some (char) -> prestring (inc_cp cp char) (char :: chars) + in prestring (cpos + 1) [] + + | Some ('{') + -> source#advance; + prelex' ((ln, cpos, acc) :: ctx) (cpos + 1) [] doc + + | Some ('}') + -> source#advance; + (match ctx with + | ((sln, scpos, sacc) :: ctx) -> + prelex' ctx (cpos+1) + (Preblock ({file=source#file_name; line=sln; column=scpos; docstr=doc}, + List.rev acc, + {file=source#file_name; line=ln; column=(cpos + 1); docstr=doc}) + :: sacc) "" + | _ -> (prelexer_error {file=source#file_name; line=ln; column=cpos; docstr=doc} + "Unmatched closing brace"; + prelex' ctx (cpos + 1) acc doc)) + + (* A pretoken. *) + | Some (c) + -> let start_offset = source#current_offset in + source#advance; + let rec pretok cp = + match source#peek_char with + | None | Some (' ' | '\t' | '%' | '"' | '{' | '}') + -> let location = {file=source#file_name; line=ln; column=cpos; docstr=doc} in + let text = source#slice_from_offset start_offset in + nexttok cp (Pretoken (location, text) :: acc) "" + + | Some ('\n') + -> let location = {file=source#file_name; line=ln; column=cpos; docstr=doc} in + let text = source#slice_from_offset start_offset in + source#advance; + nextline ctx (Pretoken (location, text) :: acc) "" + + | Some ('\') + -> source#advance; + (match source#next_char with + | Some (char) -> pretok (1 + inc_cp cp char) + | None + -> let location = {file=source#file_name; line=ln; column=cpos; docstr=doc} in + source#advance; + let text = source#slice_from_offset start_offset in + prelexer_error location ("Unterminated escape sequence in: " ^ text); + nexttok (cp + 1) (Pretoken (location, text) :: acc) "") + + | Some (c) + -> source#advance; + pretok (inc_cp cp c) + in pretok (inc_cp cpos c) + in + (* Traditionally, column numbers start at 1 :-( *) + prelex' ctx 1 acc doc + +let prelex (source : #Source.t) : pretoken list = + (* Traditionally, line numbers start at 1 :-( *) + prelex source 1 [] [] ""

let pretoken_name pretok = match pretok with

===================================== src/source.ml ===================================== @@ -0,0 +1,113 @@ +(* Copyright (C) 2021 Free Software Foundation, Inc. + * + * Author: Simon Génier simon.genier@umontreal.ca + * Keywords: languages, lisp, dependent types. + * + * This file is part of Typer. + * + * Typer is free software; you can redistribute it and/or modify it under the + * terms of the GNU General Public License as published by the Free Software + * Foundation, either version 3 of the License, or (at your option) any later + * version. + * + * Typer is distributed in the hope that it will be useful, but WITHOUT ANY + * WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS + * FOR A PARTICULAR PURPOSE. See the GNU General Public License for more + * details. + * + * You should have received a copy of the GNU General Public License along + * with this program. If not, see http://www.gnu.org/licenses/. *) + +type location = Util.location + +(* 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 = object (self) + (* A path if the text comes from a file, otherwise a meaningful identifier. *) + method virtual file_name : string + + (* Return the byte at the cursor, or None if the cursor is at the end of + the text. *) + method virtual peek_char : char option + + (* The current offset of the cursor in the file, in bytes. *) + method virtual current_offset : int + + (* Slices the text, from (and including) a starting offset 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 + + (* Moves the cursor forward one byte *) + method virtual advance : unit + + method next_char : char option = + let c = self#peek_char in + self#advance; + c +end + +let read_buffer_length = 4096 + +class source_file file_name = object (self) + inherit t + + val in_channel = open_in file_name + val mutable end_of_line = false + val mutable line = "" + val mutable line_offset = 0 + val mutable offset = 0 + + method private peek_char_unchecked = + if offset < String.length line + then line.[offset] + else '\n' + + method peek_char = + if offset <= String.length line + then Some self#peek_char_unchecked + else + try + line_offset <- line_offset + 1 + String.length line; + line <- input_line in_channel; + offset <- 0; + Some self#peek_char_unchecked + with + | End_of_file -> None + + method advance = + offset <- offset + 1 + + method current_offset = line_offset + offset + + method slice_from_offset start_offset = + let relative_start_offset = start_offset - line_offset in + String.sub line relative_start_offset (offset - relative_start_offset) + + method file_name = file_name +end + +class source_string source = object + inherit t + + val mutable offset = 0 + + method peek_char = + if offset < String.length source + then Some (source.[offset]) + else None + + method advance = + offset <- offset + 1 + + method current_offset = offset + + method slice_from_offset start_offset = + String.sub source start_offset (offset - start_offset) + + method file_name = "<string>" +end

View it on GitLab: https://gitlab.com/monnier/typer/-/compare/952f92e33c473c43327ee180f49e04668...