Typer

Download

typer@iro.umontreal.ca

April 2021

4 participants
52 discussions

[Git][monnier/typer][master] 3 commits: Introduce source objects.
by Simon Génier (＠ilovemonoids) 02 Apr '21

02 Apr '21

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(a)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(a)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(a)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/952f92e33c473c43327ee180f49e0466… -- View it on GitLab: https://gitlab.com/monnier/typer/-/compare/952f92e33c473c43327ee180f49e0466… You're receiving this email because of your account on gitlab.com.

1 0

Quelques changements à Typer
by Génier Simon 02 Apr '21

02 Apr '21

Bonjour, J'écris ce courriel pour vous avertir de deux changements dans Typer que je fais en préparation à merger mes patch pour la compilation vers Scheme. Ce n'est pas majeur, mais ça peut causer des surprises. - Il y a plusieurs paires de fonctions, une qui agit sur un string de source Typer et l'autre, sur un fichier. Tout ça pour finalement passer une telle ou telle fermeture au prélexeur. Ma branche source-object fusionne ces fonctions pour prendre un objet source qui peut être un string ou un fichier. - Je vais extraire de REPL.ml un fichier main.ml qui sera responsable de traiter les argument à typer puis de partir le REPL si nécessaire, sinon d'invoquer le bon backend non-interactif (Gambit dans mon cas). Je vais extraire ce changement de ma branche gambit et le merger séparément. Bon typage Simon

1 0