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

[Git][monnier/typer][soilih] 2 commits: diagnostics
by Soilihi BEN SOILIHI BOINA (＠BenSoilih) 31 Mar '21

31 Mar '21

Soilihi BEN SOILIHI BOINA pushed to branch soilih at Stefan / Typer Commits: cc0bd4d8 by Soilih BEN SOILIH at 2021-03-30T20:58:46-06:00 diagnostics - - - - - 1b7204e3 by Soilih BEN SOILIH at 2021-03-31T10:23:12-06:00 Errors handling - - - - - 5 changed files: - + .vscode/launch.json - emacs/typer-mode.el - src/REPL.ml - src/dune - src/typer_lsp_server.ml Changes: ===================================== .vscode/launch.json ===================================== @@ -0,0 +1,15 @@ +{ + // Use IntelliSense to learn about possible attributes. + // Hover to view descriptions of existing attributes. + // For more information, visit: https://go.microsoft.com/fwlink/?linkid=830387 + "version": "0.2.0", + "configurations": [ + { + "type": "pwa-chrome", + "request": "launch", + "name": "Launch Chrome against localhost", + "url": "http://localhost:8080", + "webRoot": "${workspaceFolder}" + } + ] +} \ No newline at end of file ===================================== emacs/typer-mode.el ===================================== @@ -279,5 +279,18 @@ (easy-menu-add typer-mode-menu) ) + +(defvar typer-lsp-server-command '("typer-lsp-server")) + + (with-eval-after-load 'lsp-mode + (lsp-register-client + (make-lsp-client :new-connection + (lsp-stdio-connection + (lambda () typer-lsp-server-command)) + :major-modes '(typer-mode) + :priority -1 + :server-id 'typer-ls))) + + (provide 'typer-mode) ;;; typer-mode.el ends here ===================================== src/REPL.ml ===================================== @@ -54,7 +54,7 @@ module OL = Opslexp module EL = Elexp let arg_batch = ref false -let lsp_server = ref false +let lsp_server = ref true let print_input_line i = print_string " In["; @@ -207,8 +207,9 @@ let help_msg = let readstring (str:string) = let ectx = Elab.default_ectx in (*let rctx = Elab.default_rctx in*) - let (list, _) = Elab.lexp_decl_str str ectx in - list + Elab.lexp_decl_str str ectx ; + let ret = Log.typer_log in + ret let readfiles files (i, lctx, rctx) prt = ===================================== src/dune ===================================== @@ -1,9 +1,9 @@ ;; -*- lisp-data -*- (executable - (name REPL) + (name REPL ) ;; (public_name typer) (libraries "zarith" "str" "linol" "linol-lwt" "lsp" "jsonrpc" ) -) \ No newline at end of file +) ===================================== src/typer_lsp_server.ml ===================================== @@ -36,15 +36,45 @@ Diagnostics includes all the warnings, errors and messages that the processing of a document are expected to be able to return. *) +open Log +open Util +type state_after_processing = log_entry list -type state_after_processing = unit +let log_entry_to_list (tab:log_entry list) : ((string * int * int * string) * log_level * string) list = + List.map (fun x -> let location = Option.get x.loc in + ((location.file,location.line,location.column,location.docstr) + ,x.level,x.msg) + ) tab -let process_some_input_file (_file_contents : string) : state_after_processing = - () +let log_level_to_severity (level:log_level) : Lsp.Types.DiagnosticSeverity.t = + match level with + | Error -> Lsp.Types.DiagnosticSeverity.Error + | Warning -> Lsp.Types.DiagnosticSeverity.Warning + | Info -> Lsp.Types.DiagnosticSeverity.Information + | _ -> Lsp.Types.DiagnosticSeverity.Hint -let diagnostics (_state : state_after_processing ) : Lsp.Types.Diagnostic.t list = - [] + +let process_some_input_file (_file_contents : string) : state_after_processing = + REPL.readstring _file_contents +let diagnostics (_state : state_after_processing) : Lsp.Types.Diagnostic.t list = +let log_tab = log_entry_to_list _state in +List.map (fun x -> + let (loc, lev, msg) = x in + let (_ (* file *), line, column, _ (* docstr *) ) = loc in + let severity = log_level_to_severity lev in + let message = msg in + let start_pos = Lsp.Types.Position.create ~line:line ~character:column in + let end_pos = Lsp.Types.Position.create ~line:line ~character:(column + 1) in + let range = Lsp.Types.Range.create ~start:start_pos ~end_:end_pos in + let diagnostic = Lsp.Types.Diagnostic.create () + ~range:range + ~severity:severity + ~source:"typerlsp" + ~message:message + in + diagnostic +) log_tab (* Lsp server class This is the main point of interaction beetween the code checking documents View it on GitLab: https://gitlab.com/monnier/typer/-/compare/a4a9cf9e4aea9600b10c2c96551d7130… -- View it on GitLab: https://gitlab.com/monnier/typer/-/compare/a4a9cf9e4aea9600b10c2c96551d7130… You're receiving this email because of your account on gitlab.com.

1 0

Demande d'informations
by Soilih BEN SOILIH 26 Mar '21

26 Mar '21

Bonjour tout le monde, J'espère que vous allez bien ! Alors, en fait, j'essaie d'écrire une fonction qui prend une chaîne de caractère ( qui sera en soi le contenu d'un fichier dans l'application) et l'évalue puis me retourne un tableau contenant les erreurs, les warning..etc et l'arbre de syntaxe abstraite. Pour faire cela, il y'a ces quelques fonctions que je vois qui peuvent m'être utiles : - eval_decls_toplevel (dans eval.ml) - eval_expr_str ( dans elab.ml ) - eval_decl_str ( dans elab.ml ) - lexp_p_decls ( dans elab.ml ) - lexp_decl_str ( dans elab.ml ) - lexp_expr_str ( dans elab.ml ) Alors j'ai deux questions : - Que représente la liste des "tokens" que prend en paramètre la fonction lexp_p_decls ? - Le contexte qui est utilisé par eval_decls_toplevel en paramètre, c'est le contexte d'élaboration ( ectx)? Merci beaucoup, bien à vous !

2 2

[Git][monnier/typer][soilih] 3 commits: commit
by Soilihi BEN SOILIHI BOINA (＠BenSoilih) 26 Mar '21

26 Mar '21

Soilihi BEN SOILIHI BOINA pushed to branch soilih at Stefan / Typer Commits: 91c0bb50 by Soilih BEN SOILIH at 2021-03-13T22:36:05-07:00 commit - - - - - 74b6b623 by Soilih BEN SOILIH at 2021-03-22T09:15:37-06:00 first commit - - - - - a4a9cf9e by Soilih BEN SOILIH at 2021-03-26T21:48:38-06:00 fonction readstring - - - - - 4 changed files: - + samples/soilih.typer - src/REPL.ml - src/dune - src/typer_lsp_server.ml Changes: ===================================== samples/soilih.typer ===================================== @@ -0,0 +1 @@ +let a = 3 b = 4 in a + b ; \ No newline at end of file ===================================== src/REPL.ml ===================================== @@ -204,6 +204,12 @@ let help_msg = %help (%h) : print help " +let readstring (str:string) = + let ectx = Elab.default_ectx in + (*let rctx = Elab.default_rctx in*) + let (list, _) = Elab.lexp_decl_str str ectx in + list + let readfiles files (i, lctx, rctx) prt = (* Read specified files *) @@ -223,6 +229,7 @@ let readfiles files (i, lctx, rctx) prt = (i, lctx, rctx) files + (* Specials commands %[command-name] [args] *) let rec repl i clxp rctx = let repl = repl (i + 1) in @@ -301,8 +308,10 @@ let parse_args () = Arg.parse arg_defs (fun s -> arg_files:= s::!arg_files) "" let main () = + parse_args (); - if (!lsp_server = true) = true then Typer_lsp_server.run () + + if !lsp_server then Typer_lsp_server.run () else (); let ectx = Elab.default_ectx in @@ -334,6 +343,5 @@ let main () = if not !arg_batch then (* Initiate REPL. This will allow us to inspect interpreted code *) repl i ectx rctx - - -let _ = main () + +let _ = main () ===================================== src/dune ===================================== @@ -2,6 +2,8 @@ (executable (name REPL) ;; (public_name typer) - (libraries "zarith" "str" "linol" "linol-lwt" - "lsp" "jsonrpc") + (libraries "zarith" "str" + "linol" "linol-lwt" + "lsp" "jsonrpc" + ) ) \ No newline at end of file ===================================== src/typer_lsp_server.ml ===================================== @@ -43,9 +43,8 @@ type state_after_processing = unit let process_some_input_file (_file_contents : string) : state_after_processing = () -let diagnostics (_state : state_after_processing) : Lsp.Types.Diagnostic.t list = - [] - +let diagnostics (_state : state_after_processing ) : Lsp.Types.Diagnostic.t list = + [] (* Lsp server class This is the main point of interaction beetween the code checking documents View it on GitLab: https://gitlab.com/monnier/typer/-/compare/62dad5517d55bb95270ec9a0e57365d3… -- View it on GitLab: https://gitlab.com/monnier/typer/-/compare/62dad5517d55bb95270ec9a0e57365d3… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][gambit] 5 commits: [Myers] Add nth_opt and reverse.
by Simon Génier (＠ilovemonoids) 25 Mar '21

25 Mar '21

Simon Génier pushed to branch gambit at Stefan / Typer Commits: 952f92e3 by Simon Génier at 2021-03-19T09:45:17-04:00 [Myers] Add nth_opt and reverse. - - - - - 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. - - - - - bf44f885 by Simon Génier at 2021-03-25T12:10:43-04:00 Add a backend to compile Typer to Scheme. - - - - - bf91885c by Simon Génier at 2021-03-25T13:51:05-04:00 Backends maintain their lctx as mutable attributes. - - - - - 16 changed files: - GNUmakefile - src/REPL.ml - + src/backend.ml - src/debug_util.ml - src/dune - src/elab.ml - src/eval.ml - + src/frontend.ml - + src/gambit.ml - src/lexer.ml - src/lexp.ml - + src/main.ml - src/myers.ml - src/option.ml - src/prelexer.ml - + src/source.ml Changes: ===================================== GNUmakefile ===================================== @@ -54,8 +54,8 @@ typer: # ============================ # Build typer # ============================ - $(OCAMLBUILD) src/REPL.$(COMPILE_MODE) -I src $(OBFLAGS) - @$(MV) $(BUILDDIR)/src/REPL.$(COMPILE_MODE) $(BUILDDIR)/typer + $(OCAMLBUILD) src/main.$(COMPILE_MODE) -I src $(OBFLAGS) + @$(MV) $(BUILDDIR)/src/main.$(COMPILE_MODE) $(BUILDDIR)/typer tests-build: # ============================ ===================================== src/REPL.ml ===================================== @@ -36,300 +36,171 @@ this program. If not, see <http://www.gnu.org/licenses/>. *) * * -------------------------------------------------------------------------- *) -open Util -open Fmt - -open Prelexer -open Lexer -open Sexp -open Lexp +open Printf +open Backend +open Debruijn open Eval +open Lexp -open Grammar +let error = Log.log_error ~section:"REPL" -open Env -open Debruijn -module OL = Opslexp -module EL = Elexp +let print_and_clear_log () = + Log.print_and_clear_log (); + flush stdout -let arg_batch = ref false +let handle_stopped_compilation msg = + Log.print_and_clear_log (); + print_endline msg; + flush stdout let print_input_line i = - print_string " In["; - ralign_print_int i 2; - print_string "] >> " - -let ieval_error = Log.log_error ~section:"IEVAL" + printf " In[%02d] >> " i -let print_and_clear_log () = - if (not Log.typer_log_config.Log.print_at_log) then - Log.print_and_clear_log () +(* Read stdin for input. -let handle_stopped_compilation msg = - print_and_clear_log (); - print_string msg; print_newline (); - flush stdout - -(* Read stdin for input. Returns only when the last char is ';' - * We can use '%' to prevent parsing - * If return is pressed and the last char is not ';' then - * indentation will be added *) + Returns only when the last char is ';'. We can use '%' to prevent parsing. If + return is pressed and the last char is not ';' then indentation will be + added. *) let rec read_input i = - print_input_line i; - flush stdout; + print_input_line i; + flush stdout; - let rec loop str i = - flush stdout; - let line = input_line stdin in - let s = String.length str in - let n = String.length line in - if s = 0 && n = 0 then read_input i else - (if n = 0 then ( - print_string " . "; - print_string (make_line ' ' (i * 4)); - loop str (i + 1)) - else - let str = if s > 0 then String.concat "\n" [str; line] else line in - if line.[n - 1] = ';' || line.[0] = '%' then - str - else ( - print_string " . "; - print_string (make_line ' ' (i * 4)); - loop str (i + 1))) in - - loop "" i - -(* Interactive mode is not usual typer - It makes things easier to test out code *) -type lexpr = lexp - -(* Grouping declaration together will enable us to support mutually recursive - * declarations while bringing us closer to normal typer *) -let ipexp_parse (sxps: sexp list): (sexp list * sexp list) = - let rec pxp_parse sxps dacc pacc = - match sxps with - | [] -> (List.rev dacc), (List.rev pacc) - | sxp::tl -> match sxp with - (* Declaration *) - | Node (Symbol (_, ("_=_" | "_:_")), [Symbol _s; _t]) -> - pxp_parse tl (sxp :: dacc) pacc - - (* f arg1 arg2 = function body; *) - | Node (Symbol (_, "_=_"), [Node (Symbol _s, _args); _t]) -> - pxp_parse tl (sxp :: dacc) pacc - - (* Expression *) - | _ -> pxp_parse tl dacc (sxp::pacc) in - pxp_parse sxps [] [] - - -let ierase_type - (lctx : DB.lexp_context) - (ldecls, lexprs : ldecl list list * lexpr list) - : (vname * EL.elexp) list list * EL.elexp list = - - let lctx', eldecls = Listx.fold_left_map OL.clean_decls lctx ldecls in - let elexprs = List.map (OL.erase_type lctx') lexprs in - eldecls, elexprs - -let ilexp_parse pexps lctx: ((ldecl list list * lexpr list) * elab_context) = - let pdecls, pexprs = pexps in - (* FIXME We take the parsed input here but we should take the - unparsed tokens directly instead *) - let ldecls, lctx = Elab.lexp_p_decls pdecls [] lctx in - let lexprs = Elab.lexp_parse_all pexprs lctx in - List.iter (fun lxp -> ignore (OL.check (ectx_to_lctx lctx) lxp)) - lexprs; - (ldecls, lexprs), lctx - -let ieval f str 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 sxps = lex default_stt pres in - (* FIXME: This is too eager: it prevents one declaration from changing - * the grammar used in subsequent declarations. *) - let nods = sexp_parse_all_to_list (ectx_to_grm ectx) sxps (Some ";") in - - (* Different from usual typer *) - let pxps = ipexp_parse nods in - let lxps, ectx' = ilexp_parse pxps ectx in - let elxps = ierase_type (ectx_to_lctx ectx) lxps in - let v, rctx = ieval' elxps rctx in - v, ectx', rctx - -let raw_eval f str ectx rctx = - let pres = (f str) 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 - (* At this point, `elxps` is a `(vname * elexp) list list`, where: - * - each `(vname * elexp)` is a definition - * - each `(vname * elexp) list` is a list of definitions which can - * refer to each other (i.e. they can be mutually recursive). - * - hence the overall "list of lists" is a sequence of such - * blocs of mutually-recursive definitions. *) - let rctx = eval_decls_toplevel elxps rctx in - (* 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 - - %quit (%q) : leave REPL - %help (%h) : print help -" - -let help_msg = + let rec loop str i = + flush stdout; + let line = input_line stdin in + let s = String.length str in + let n = String.length line in + if s = 0 && n = 0 then read_input i else + (if n = 0 then ( + print_string " . "; + print_string (String.make (i * 4) ' '); + loop str (i + 1)) + else + let str = if s > 0 then String.concat "\n" [str; line] else line in + if line.[n - 1] = ';' || line.[0] = '%' then + str + else ( + print_string " . "; + print_string (String.make (i * 4) ' '); + loop str (i + 1))) in + + loop "" i + +let help_message = " %quit (%q) : leave REPL %who (%w) : print runtime environment %info (%i) : print elaboration environment %calltrace (%ct): print eval trace of last call - %elabtrace (%et): print elaboration trace %typertrace (%tt): print typer trace %readfile : read a Typer file %help (%h) : print help " - -let readfiles files (i, lctx, rctx) prt = - (* Read specified files *) - List.fold_left (fun (i, lctx, rctx) file -> - - (if prt then ( - 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)) - with - Sys_error _ -> ( - ieval_error ("file \"" ^ file ^ "\" does not exist."); - (i, lctx, rctx)) - ) - (i, lctx, rctx) files - - -(* Specials commands %[command-name] [args] *) -let rec repl i clxp rctx = - let repl = repl (i + 1) in - let ipt = try read_input i with End_of_file -> "%quit" in - match ipt with - (* Check special keywords *) - | "%quit" | "%q" -> () - | "%help" | "%h" -> (print_string help_msg; repl clxp rctx) - | "%calltrace" | "%ct" -> (print_eval_trace None; repl clxp rctx) - | "%typertrace" | "%tt" -> (print_typer_trace None; repl clxp rctx) - | "%lcollisions" | "%cl" -> (get_stats_hashtbl (WHC.stats hc_table)) - - (* command with arguments *) - | _ when (ipt.[0] = '%' && ipt.[1] != ' ') -> ( - match (str_split ipt ' ') with - | "%readfile"::args -> - let (_i, clxp, rctx) = - try - readfiles args (i, clxp, rctx) false - with Log.Stop_Compilation msg -> - (handle_stopped_compilation msg; (i,clxp,rctx)) - in - repl clxp rctx; - | "%who"::args | "%w"::args -> ( - let _ = match args with - | ["all"] -> dump_rte_ctx rctx - | _ -> print_rte_ctx rctx in - repl clxp rctx) - | "%info"::args | "%i"::args -> ( - let _ = match args with - | ["all"] -> dump_lexp_ctx (ectx_to_lctx clxp) - | _ -> print_lexp_ctx (ectx_to_lctx clxp) in - repl clxp rctx) - - | cmd::_ -> - ieval_error (" \"" ^ cmd ^ "\" is not a correct repl command"); - repl clxp rctx - | _ -> repl 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 +let process_file + (backend : #backend) + (ectx : elab_context) + (file_name : string) + : elab_context = + + try + let source = new Source.source_file file_name in + let decls, ectx' = Frontend.decls_of_source source ectx in + List.iter backend#process_decls decls; + ectx' + with + | Sys_error _ + -> (error ("file \"" ^ file_name ^ "\" does not exist."); + ectx) + +let process_interactive + (interactive : #interactive_backend) + (i : int) + (ectx : elab_context) + (input : string) + : elab_context = + + let source = new Source.source_string input in + let decls, exprs, ectx' = Frontend.decls_of_interactive source ectx in + + List.iter interactive#process_decls decls; + print_and_clear_log (); + + let values = List.map interactive#eval_expr exprs in + List.iter (print_eval_result i) values; + print_and_clear_log (); + + ectx' + +let rec repl + (i : int) + (interactive : interactive_backend) + (ectx : elab_context) + : unit = + + let input = try read_input i with End_of_file -> "%quit" in + + let ectx = + match input with + (* Check special keywords *) + | "%quit" | "%q" + -> exit 0 + | "%help" | "%h" + -> print_string help_message; + ectx + | "%calltrace" | "%ct" + -> print_eval_trace None; + ectx + | "%typertrace" | "%tt" + -> print_typer_trace None; + ectx + | "%lcollisions" | "%cl" + -> Util.get_stats_hashtbl (WHC.stats hc_table); + ectx + + (* command with arguments *) + | _ when input.[0] = '%' && input.[1] != ' ' + -> (match String.split_on_char ' ' input with + | "%readfile" :: args + -> (try + let ectx = + List.fold_left (process_file interactive) ectx args + in + print_and_clear_log (); + ectx with - | Log.Stop_Compilation msg -> - (handle_stopped_compilation msg; repl clxp rctx) - | Log.Internal_error msg -> - (handle_stopped_compilation ("Internal error: " ^ msg); - repl clxp rctx) - | Log.User_error msg -> - (handle_stopped_compilation ("Fatal user error: " ^ msg); - repl clxp rctx) - -let arg_files = ref [] - - -(* ./typer [options] files *) -let arg_defs = [ - ("--batch", Arg.Set arg_batch, "Don't run the interactive loop"); - ("--verbosity", - Arg.String Log.set_typer_log_level_str, "Set the logging level"); - ("-v", Arg.Unit Log.increment_log_level, "Increment verbosity"); - ("-Vfull-lctx", - Arg.Set Debruijn.log_full_lctx, - "Print the full lexp context on error."); - (* ("--debug", Arg.Set arg_debug, "Print the Elexp representation") *) - (*"-I", - Arg.String (fun f -> searchpath := f::!searchpath), - "Append a directory to the search path"*) -] - -let parse_args () = - Arg.parse arg_defs (fun s -> arg_files:= s::!arg_files) "" - -let main () = - parse_args (); - - let ectx = Elab.default_ectx in - let rctx = Elab.default_rctx in - - if not !arg_batch then - (print_string (make_title " TYPER REPL "); - print_string welcome_msg; - print_string (make_sep '-'); - flush stdout); - - let (i, ectx, rctx) = ( - try - let res = - readfiles (List.rev !arg_files) (1, ectx, rctx) (not !arg_batch) in - print_and_clear_log (); res - with - | Log.Stop_Compilation msg -> - handle_stopped_compilation msg; exit 1 - | (Log.Internal_error msg) as e -> - handle_stopped_compilation ("Internal error: " ^ msg); - raise e - | Log.User_error msg -> - handle_stopped_compilation ("Fatal user error: " ^ msg); exit 1 - ) in - - flush stdout; - - if not !arg_batch then - (* Initiate REPL. This will allow us to inspect interpreted code *) - repl i ectx rctx - - -let _ = main () + | Log.Stop_Compilation msg + -> handle_stopped_compilation msg; + ectx) + | "%who" :: args | "%w" :: args + -> (match args with + | ["all"] -> interactive#dump_rte_ctx + | _ -> interactive#print_rte_ctx); + ectx + | "%info" :: args | "%i" :: args + -> (match args with + | ["all"] -> dump_lexp_ctx (ectx_to_lctx ectx) + | _ -> print_lexp_ctx (ectx_to_lctx ectx)); + ectx + + | cmd :: _ + -> error ("\"" ^ cmd ^ "\" is not a correct repl command"); + ectx + + | _ + -> ectx) + + (* eval input *) + | _ + -> (try process_interactive interactive i ectx input with + | Log.Stop_Compilation msg + -> handle_stopped_compilation msg; + ectx + | Log.Internal_error msg + -> handle_stopped_compilation ("Internal error: " ^ msg); + ectx + | Log.User_error msg + -> handle_stopped_compilation ("Fatal user error: " ^ msg); + ectx) + + in repl (i + 1) interactive ectx ===================================== src/backend.ml ===================================== @@ -0,0 +1,81 @@ +(* 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/>. *) + +(* A backend is a consumer of fully eleborated and checked lexps. This module + provides a superclass for all backends as well their implementations. *) + +open Lexp + +type value = Env.value_type + +class virtual backend = object + (* Processes (interpret or compile, depending on the backend) a block of + mutually recursive declarations. *) + method virtual process_decls : ldecls -> unit + + method interactive : interactive_backend option = None +end + +(* Backends may optionaly allow interactive evaluation, i.e. lexps can be + immediately evaluated as opposed compiled for evaluation later. *) +and virtual interactive_backend = object (self) + inherit backend + + method! interactive = Some (self :> interactive_backend) + + method virtual eval_expr : lexp -> value + + method virtual print_rte_ctx : unit + + method virtual dump_rte_ctx : unit +end + +class ast_interpreter lctx = object + inherit interactive_backend + + val mutable rctx = Eval.from_lctx lctx + val mutable lctx = lctx + + method process_decls ldecls = + let lctx', eldecls = Opslexp.clean_decls lctx ldecls in + rctx <- Eval.eval_decls eldecls rctx; + lctx <- lctx' + + method eval_expr lexp = + let elexp = Opslexp.erase_type lctx lexp in + Eval.debug_eval elexp rctx + + method print_rte_ctx = Env.print_rte_ctx rctx + + method dump_rte_ctx = Env.dump_rte_ctx rctx +end + +class gambit_compiler lctx output = object + inherit backend + + val mutable sctx = Gambit.ScmContext.of_lctx lctx + val mutable lctx = lctx + + method process_decls ldecls = + let lctx', sctx', sdecls = Gambit.scheme_of_decls lctx sctx ldecls in + sctx <- sctx'; + lctx <- lctx'; + Gambit.Scm.print output sdecls; +end ===================================== src/debug_util.ml ===================================== @@ -277,7 +277,7 @@ let main () = let clean_lxp = List.map OL.clean_decls lexps in (* Eval declaration *) - let rctx = Elab.default_rctx in + let rctx = Eval.from_ectx Elab.default_ectx in print_string yellow; let rctx = (try eval_decls_toplevel clean_lxp rctx; with e -> ===================================== src/dune ===================================== @@ -1,6 +1,6 @@ ;; -*- lisp-data -*- (executable - (name REPL) + (name main) ;; (public_name typer) (libraries "zarith" "str") ) ===================================== 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 @@ -1903,8 +1905,6 @@ let default_ectx Log.print_and_clear_log (); raise e -let default_rctx = EV.from_ectx default_ectx - (* String Parsing * --------------------------------------------------------- *) @@ -1912,7 +1912,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 +1921,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 @@ -487,7 +489,14 @@ and eval_var ctx lxp v = ("Variable: " ^ L.maybename (snd name) ^ (str_idx idx) ^ " was not found ") (* unef: unevaluated function (to make the trace readable) *) -and eval_call loc unef i f args = +and eval_call + loc + (unef : elexp) + (i : eval_debug_info) + (f : value_type) + (args : value_type list) + : value_type = + match f, args with (* return result of eval *) | _, [] -> f @@ -1145,14 +1154,13 @@ let from_lctx (lctx: lexp_context): runtime_env = | CVempty -> Myers.nil | CVlet (loname, def, _, lctx) -> let rctx = from_lctx lctx in - Myers.cons (loname, - ref (match def with - | LetDef (_, e) - -> if closed_p rctx (OL.fv e) then - eval (OL.erase_type lctx e) rctx - else Vundefined - | _ -> Vundefined)) - rctx + let value = + match def with + | LetDef (_, e) when closed_p rctx (OL.fv e) + -> eval (OL.erase_type lctx e) rctx + | _ -> Vundefined + in + Myers.cons (loname, ref value) rctx | CVfix (defs, lctx) -> let fvs = List.fold_left (fun fvs (_, e, _) ===================================== src/frontend.ml ===================================== @@ -0,0 +1,75 @@ +(* 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/>. *) + +open Debruijn +open Lexer +open Lexp +open Opslexp +open Prelexer +open Sexp + +let decls_of_source + (source : Source.t) + (ectx : elab_context) + : ldecls list * elab_context = + + let pretokens = prelex source in + let tokens = lex Grammar.default_stt pretokens in + let ldecls, ectx' = Elab.lexp_p_decls [] tokens ectx in + (ldecls, ectx') + +(** Elaborate Typer source from an interactive session. The difference with + normal Typer is that expressions are also accepted in addition to + declarations. + + Note that all declarations are hoisted before expressions. *) +let decls_of_interactive + (source : Source.t) + (ectx : elab_context) + : ldecls list * lexp list * elab_context = + + let classify_sexps nodes = + let rec loop sexps decls exprs = + match sexps with + | [] -> (List.rev decls, List.rev exprs) + | sexp :: sexps + -> (match sexp with + | Node (Symbol (_, ("_=_" | "_:_")), [Symbol _; _]) + -> loop sexps (sexp :: decls) exprs + | Node (Symbol (_, ("_=_")), [Node _; _]) + -> loop sexps (sexp :: decls) exprs + | _ + -> loop sexps decls (sexp :: exprs)) + in loop nodes [] [] + in + + let pretokens = prelex source in + let tokens = lex Grammar.default_stt pretokens in + (* FIXME: This is too eager: it prevents one declaration from changing + * the grammar used in subsequent declarations. *) + let sexps = sexp_parse_all_to_list (ectx_to_grm ectx) tokens (Some ";") in + let decls, exprs = classify_sexps sexps in + + let ldecls, ectx' = Elab.lexp_p_decls decls [] ectx in + + let lexprs = Elab.lexp_parse_all exprs ectx' in + List.iter (fun lexpr -> ignore (check (ectx_to_lctx ectx') lexpr)) lexprs; + + (ldecls, lexprs, ectx') ===================================== src/gambit.ml ===================================== @@ -0,0 +1,278 @@ +(* 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/>. *) + +open Printf + +open Debruijn +open Elexp + +type ldecls = Lexp.ldecls +type lexp = Lexp.lexp + +module Scm = struct + type t = + | Symbol of string + | List of t list + | String of string + | Integer of Z.t + | Float of float + + let begin' : t = Symbol "begin" + let case : t = Symbol "case" + let define : t = Symbol "define" + let double_right_arrow : t = Symbol "=>" + let else' : t = Symbol "else" + let lambda : t = Symbol "lambda" + let let' : t = Symbol "let" + let letrec : t = Symbol "letrec" + let quote : t = Symbol "quote" + let prim_vector : t = Symbol "##vector" + let prim_vector_ref : t = Symbol "##vector-ref" + + let is_valid_bare_symbol (name : string) : bool = + let length = String.length name in + let rec loop i = + if Int.equal length i + then true + else + match name.[i] with + | '|' | '\'' | ' ' | '(' | ')' -> false + | _ -> loop (i + 1) + in loop 0 + + let escape_symbol (name : string) : string = + if is_valid_bare_symbol name + then name + else + let buffer = Buffer.create (String.length name) in + Buffer.add_char buffer '|'; + let encode_char = function + | '|' -> Buffer.add_string buffer {|\||} + | c -> Buffer.add_char buffer c + in + String.iter encode_char name; + Buffer.add_char buffer '|'; + Buffer.contents buffer + + let symbol (name : string) : t = + Symbol (escape_symbol name) + + let rec string_of_exp (exp : t) : string = + match exp with + | Symbol (name) -> name + | List (elements) + -> "(" ^ String.concat " " (List.map string_of_exp elements) ^ ")" + | String (value) + -> let length = String.length value in + let buffer = Buffer.create length in + let encode_char = function + | '\x00' .. '\x06' as c + -> (Buffer.add_string buffer "\\x"; + Buffer.add_string buffer (Printf.sprintf "%02d" (Char.code c))) + | '\x07' -> Buffer.add_string buffer "\\a" + | '\x08' -> Buffer.add_string buffer "\\b" + | '\x09' -> Buffer.add_string buffer "\\t" + | '\\' -> Buffer.add_string buffer "\\\\" + | '"' -> Buffer.add_string buffer "\\\"" + | c -> Buffer.add_char buffer c + in + String.iter encode_char value; + Buffer.contents buffer + | Integer (value) -> Z.to_string value + | Float (value) -> string_of_float value + + let print (output : out_channel) (exp : t) : unit = + output_string output (string_of_exp exp); + output_char output '\n' +end + +let gensym : string -> string = + let counter = ref 0 in + fun name -> + let i = !counter in + counter := i + 1; + let name = sprintf "%s%%%d" name i in + Scm.escape_symbol name + +module ScmContext = struct + (* Maps Debruijn indices to Scheme variable names. *) + type t = string Myers.myers + + let nil : t = Myers.nil + + let of_lctx (lctx : lexp_context) : t = + let f ((_, name), _, _) = Option.get name in + Myers.map f lctx + + let intro (sctx : t) (_, name : vname) : t * string = + let name = gensym (Option.value ~default:"g" name) in + (Myers.cons name sctx, name) + + let intro_binding (sctx : t) (name, elexp : vname * elexp) = + let sctx, name = intro sctx name in + (sctx, (name, elexp)) + + let lookup (sctx : t) (index : int) : string option = + Myers.nth_opt index sctx +end + +let rec scheme_of_expr (sctx : ScmContext.t) (elexp : elexp) : Scm.t = + match elexp with + | Elexp.Imm (Sexp.String (_, s)) -> Scm.String s + + | Elexp.Imm (Sexp.Integer (_, i)) -> Scm.Integer i + + | Elexp.Imm (Sexp.Float (_, f)) -> Scm.Float f + + | Elexp.Builtin (_, "Sexp.node") -> Scm.Symbol "cons" + + | Elexp.Builtin (_, "Sexp.symbol") -> Scm.Symbol "string->symbol" + + | Elexp.Builtin (_, name) -> failwith ("TODO: Built-in \"" ^ name ^ "\"") + + | Elexp.Var (_, index) + -> (match ScmContext.lookup sctx index with + | None -> Scm.Symbol "TODO" + | Some name -> Scm.Symbol name) + + | Elexp.Let (_, bindings, body) + -> if List.length bindings = 0 + then scheme_of_expr sctx body + else + let sctx, bindings = + Listx.fold_left_map ScmContext.intro_binding sctx bindings + in + let scheme_of_binding (name, elexp) = + Scm.List [Scm.Symbol name; scheme_of_expr sctx elexp] + in + Scm.List [Scm.letrec; + Scm.List (List.map scheme_of_binding bindings); + scheme_of_expr sctx body] + + | Elexp.Lambda (name, body) + -> let sctx', name = ScmContext.intro sctx name in + Scm.List [Scm.lambda; + Scm.List [Scm.Symbol name]; + scheme_of_expr sctx' body] + + | Elexp.Call (head, tail) + -> let scm_head = scheme_of_expr sctx head in + let scm_tail = List.map (scheme_of_expr sctx) tail in + Scm.List (scm_head :: scm_tail) + + | Elexp.Cons (arity, (_, name)) + -> let rec make_vars i vars = + match i with + | 0 -> vars + | _ -> make_vars (i - 1) (Scm.Symbol (gensym "") :: vars) + in + let vars = make_vars arity [] in + let vector_expr = + Scm.List (Scm.prim_vector + :: Scm.List [Scm.quote; Scm.symbol name] + :: List.rev vars) + in + let rec make_curried_lambda vars body = + match vars with + | [] -> body + | var :: vars' + -> let body' = Scm.List [Scm.lambda; Scm.List [var]; body] in + make_curried_lambda vars' body' + in + make_curried_lambda vars vector_expr + + | Elexp.Case (_, target, branches, default_branch) + -> let target_name = + match target with + | Elexp.Var _ -> scheme_of_expr sctx target + | _ -> Scm.Symbol (gensym "target") + in + let scm_default_branch = + match default_branch with + | None -> [] + | Some (name, body) + -> let sctx, name = ScmContext.intro sctx name in + (* (else => (lambda (name) body)) *) + [Scm.List [Scm.else'; + Scm.double_right_arrow; + Scm.List [Scm.lambda; + Scm.List [Scm.Symbol name]; + scheme_of_expr sctx body]]] + in + let add_branch cons_name (_, field_names, branch_body) scm_branches = + let make_binding (sctx, bindings, i) (location, name) = + match name with + | Some "_" -> sctx, bindings, Z.succ i + | _ + -> let sctx, name = ScmContext.intro sctx (location, name) in + let binding = Scm.List [Scm.Symbol name; + Scm.List [Scm.prim_vector_ref; + target_name; + Scm.Integer i]] + in + sctx, binding :: bindings, Z.succ i + in + let sctx, bindings, _ = List.fold_left make_binding (sctx, [], Z.one) field_names in + let scm_branch = + Scm.List [Scm.List [Scm.symbol cons_name]; + if Int.equal (List.length bindings) 0 + then scheme_of_expr sctx branch_body + else + Scm.List [Scm.let'; + Scm.List (List.rev bindings); + scheme_of_expr sctx branch_body]] + in + scm_branch :: scm_branches + in + let scm_branches = + List.rev_append (SMap.fold add_branch branches []) scm_default_branch + in + let scm_case = + Scm.List (Scm.case + :: Scm.List [Scm.prim_vector_ref; + target_name; + Scm.Integer Z.zero] + :: scm_branches) + in + (match target with + | Elexp.Var _ -> scm_case + | _ + -> Scm.List [Scm.let'; + Scm.List [Scm.List [target_name; + scheme_of_expr sctx target]]; + scm_case]) + + | Elexp.Type _ -> Scm.Symbol "lets-hope-its-ok-if-i-erase-this" + + | _ -> failwith ("[gambit] unsupported elexp: " ^ elexp_string elexp) + +let scheme_of_decl (sctx : ScmContext.t) (name, elexp : string * elexp) : Scm.t = + Scm.List ([Scm.define; Scm.Symbol name; scheme_of_expr sctx elexp]) + +let scheme_of_decls + (lctx : lexp_context) + (sctx : ScmContext.t) + (ldecls : ldecls) + : lexp_context * ScmContext.t * Scm.t = + + let lctx', eldecls = Opslexp.clean_decls lctx ldecls in + let sctx', eldecls = Listx.fold_left_map ScmContext.intro_binding sctx eldecls in + let sdecls = Scm.List (Scm.begin' :: List.map (scheme_of_decl sctx') eldecls) in + (lctx', sctx', sdecls) ===================================== 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/lexp.ml ===================================== @@ -118,6 +118,7 @@ type ltype = lexp | SLlub of lexp * lexp type ldecl = vname * lexp * ltype +type ldecls = ldecl list type varbind = | Variable ===================================== src/main.ml ===================================== @@ -0,0 +1,109 @@ +(* 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/>. *) + +open Printf + +open Backend +open Debruijn +open Elab +open Fmt + +let arg_batch = ref false +let arg_files = ref [] +let backend_name = ref "interpreter" + +(* ./typer [options] files *) +let arg_defs = + [("--batch", Arg.Set arg_batch, "Don't run the interactive loop"); + + ("--verbosity", + Arg.String Log.set_typer_log_level_str, + "Set the logging level"); + + ("-v", Arg.Unit Log.increment_log_level, "Increment verbosity"); + + ("--backend", + Arg.Symbol (["interpreter"; "gambit"], fun name -> backend_name := name), + "Select the backend"); + ] + +let welcome_message = +" Typer 0.0.0 - Interpreter - (c) 2016-2021 + + %quit (%q) : leave REPL + %help (%h) : print help +" + +let main () = + Arg.parse arg_defs (fun file -> arg_files := file :: !arg_files) ""; + + let is_batch = !arg_batch in + let file_names = List.rev !arg_files in + let backend = + match !backend_name with + | "interpreter" + -> (new ast_interpreter (ectx_to_lctx default_ectx) :> backend) + | "gambit" + -> (new gambit_compiler (ectx_to_lctx default_ectx) stdout :> backend) + | backend_name + -> (print_string ("unknown backend: " ^ backend_name); + exit 1) + in + + let interactive = backend#interactive in + let process_file = + if is_batch && Option.is_some interactive + then + fun (ectx, i) file_name + -> let ectx = REPL.process_file backend ectx file_name in + ectx, i + else + (print_string (make_title " TYPER REPL "); + print_string welcome_message; + print_string (make_sep '='); + flush stdout; + fun (ectx, i) file_name + -> printf " In[%02d] >> %%readfile %s\n" i file_name; + let ectx = REPL.process_file backend ectx file_name in + ectx, i + 1) + in + + let ectx, i = + try + let ectx, i = List.fold_left process_file (default_ectx, 0) file_names in + REPL.print_and_clear_log (); + ectx, i + with + | Log.Stop_Compilation msg + -> REPL.handle_stopped_compilation msg; + exit 1 + | Log.Internal_error msg as e + -> REPL.handle_stopped_compilation ("Internal error: " ^ msg); + raise e + | Log.User_error msg + -> REPL.handle_stopped_compilation ("Fatal user error: " ^ msg); + exit 1 + in + + match is_batch, backend#interactive with + | false, Some interactive -> REPL.repl i interactive ectx + | _ -> () + +let _ = main () ===================================== src/myers.ml ===================================== @@ -75,6 +75,11 @@ let rec nthcdr n l = let nth n l = car (nthcdr n l) +let nth_opt (n : int) (l : 'a myers) : 'a option = + match nthcdr n l with + | Mnil -> None + | Mcons (x, _, _, _) -> Some x + (* While `nth` is O(log N), `set_nth` is O(N)! :-( *) let rec set_nth n v l = match (n, l) with | 0, Mcons (_, cdr, s, tail) -> Mcons (v, cdr, s, tail) @@ -136,3 +141,6 @@ let rec fold_right f l i = match l with let map f l = fold_right (fun x l' -> cons (f x) l') l nil let iteri f l = fold_left (fun i x -> f i x; i + 1) 0 l + +let reverse (l : 'a myers) : 'a myers = + fold_left (fun cdr car -> cons car cdr) nil l ===================================== src/option.ml ===================================== @@ -30,3 +30,13 @@ let get (o : 'a option) : 'a = match o with | Some v -> v | None -> invalid_arg "expected Some" + +let value ~(default : 'a) (o : 'a option) : 'a = + match o with + | Some v -> v + | None -> default + +let is_some (o : 'a option) : bool = + match o with + | Some _ -> true + | None -> false ===================================== 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/0ea08dd805eb30bc45e0977ce3ba2de3… -- View it on GitLab: https://gitlab.com/monnier/typer/-/compare/0ea08dd805eb30bc45e0977ce3ba2de3… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][source-object] [Source] Do not buffer more than one line.
by Simon Génier (＠ilovemonoids) 24 Mar '21

24 Mar '21

Simon Génier pushed to branch source-object at Stefan / Typer Commits: e3fb3f5e by Simon Génier at 2021-03-24T19:54:15-04:00 [Source] Do not buffer more than one line. - - - - - 1 changed file: - src/source.ml Changes: ===================================== src/source.ml ===================================== @@ -35,7 +35,11 @@ class virtual t = object (self) method virtual current_offset : int (* Slices the text, from (and including) a starting offset and to (and - excluding) the curent cursor offset. *) + 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 *) @@ -53,32 +57,36 @@ class source_file file_name = object (self) inherit t val in_channel = open_in file_name - val bytes = Bytes.create read_buffer_length - val buffer = Buffer.create 4096 + val mutable end_of_line = false + val mutable line = "" + val mutable line_offset = 0 val mutable offset = 0 - val mutable length = 0 method private peek_char_unchecked = - Some (Buffer.nth buffer offset) + if offset < String.length line + then line.[offset] + else '\n' method peek_char = - if offset < length - then self#peek_char_unchecked + if offset <= String.length line + then Some self#peek_char_unchecked else - match input in_channel bytes 0 read_buffer_length with - | 0 -> None - | read_length - -> Buffer.add_subbytes buffer bytes 0 read_length; - length <- length + read_length; - self#peek_char_unchecked + 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 = offset + method current_offset = line_offset + offset method slice_from_offset start_offset = - Buffer.sub buffer start_offset (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 View it on GitLab: https://gitlab.com/monnier/typer/-/commit/e3fb3f5ed2217d547b61829b4422c5d20… -- View it on GitLab: https://gitlab.com/monnier/typer/-/commit/e3fb3f5ed2217d547b61829b4422c5d20… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer] Pushed new branch source-object
by Simon Génier (＠ilovemonoids) 24 Mar '21

24 Mar '21

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

1 0

[Git][monnier/typer] Deleted branch source-object
by Simon Génier (＠ilovemonoids) 24 Mar '21

24 Mar '21

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

1 0

[Git][monnier/typer] Pushed new branch source-object
by Simon Génier (＠ilovemonoids) 22 Mar '21

22 Mar '21

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

1 0

[Git][monnier/typer][master] [Myers] Add nth_opt and reverse.
by Simon Génier 19 Mar '21

19 Mar '21

Simon Génier pushed to branch master at Stefan / Typer Commits: 952f92e3 by Simon Génier at 2021-03-19T09:45:17-04:00 [Myers] Add nth_opt and reverse. - - - - - 1 changed file: - src/myers.ml Changes: ===================================== src/myers.ml ===================================== @@ -75,6 +75,11 @@ let rec nthcdr n l = let nth n l = car (nthcdr n l) +let nth_opt (n : int) (l : 'a myers) : 'a option = + match nthcdr n l with + | Mnil -> None + | Mcons (x, _, _, _) -> Some x + (* While `nth` is O(log N), `set_nth` is O(N)! :-( *) let rec set_nth n v l = match (n, l) with | 0, Mcons (_, cdr, s, tail) -> Mcons (v, cdr, s, tail) @@ -136,3 +141,6 @@ let rec fold_right f l i = match l with let map f l = fold_right (fun x l' -> cons (f x) l') l nil let iteri f l = fold_left (fun i x -> f i x; i + 1) 0 l + +let reverse (l : 'a myers) : 'a myers = + fold_left (fun cdr car -> cons car cdr) nil l View it on GitLab: https://gitlab.com/monnier/typer/-/commit/952f92e33c473c43327ee180f49e04668… -- View it on GitLab: https://gitlab.com/monnier/typer/-/commit/952f92e33c473c43327ee180f49e04668… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][opt-inline] Inline let-binding to vars and built-ins.
by Simon Génier 14 Mar '21

14 Mar '21

Simon Génier pushed to branch opt-inline at Stefan / Typer Commits: 50eca407 by Simon Génier at 2021-03-14T22:34:09-04:00 Inline let-binding to vars and built-ins. - - - - - 3 changed files: - src/frontend.ml - + src/inline.ml - src/myers.ml Changes: ===================================== src/frontend.ml ===================================== @@ -33,7 +33,13 @@ let decls_of_source let pretokens = prelex source in let tokens = lex Grammar.default_stt pretokens in let ldecls, ectx' = Elab.lexp_p_decls [] tokens ectx in - (ldecls, ectx') + let _, ldecls' = + Listx.fold_left_map + Inline.inline_decls + (Inline.InlContext.ictx_of_lctx (ectx_to_lctx ectx)) + ldecls + in + (ldecls', ectx') (** Elaborate Typer source from an interactive session. The difference with normal Typer is that expressions are also accepted in addition to ===================================== src/inline.ml ===================================== @@ -0,0 +1,137 @@ +(* 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/>. *) + +open Lexp + +type symbol = Sexp.symbol +module SMap = Util.SMap +let dummy_location = Util.dummy_location + +type inl_action = + | Opaque + | InlineBuiltin of lexp + | InlineVar of vname * int + +module InlContext = struct + type t = (vname * inl_action) Myers.myers + + let intro_opaque (ictx : t) (name : vname) : t = + Myers.cons (name, Opaque) ictx + + let intro (ictx : t) (name : vname) (lexp : lexp) : t = + match Lexp.nosusp lexp with + | (Lexp.Var (name', index), _) + -> Myers.cons (name, InlineVar (name', index)) ictx + | (Lexp.Builtin _, _ as lexp') + -> Myers.cons (name, InlineBuiltin lexp') ictx + | _ -> intro_opaque ictx name + + let intro_decl (ictx : t) (name, value, _ : ldecl) : t = + intro ictx name value + + let intro_decls (ictx : t) (ldecls : ldecls) : t = + List.fold_left intro_decl ictx ldecls + + let ictx_of_lctx (lctx : Debruijn.lexp_context) : t = + let rec loop lctx ictx = + match lctx with + | Myers.Mnil -> Myers.reverse ictx + | Myers.Mcons ((name, LetDef (offset, value), _), tail, _, _) + -> loop tail (intro ictx name (mkSusp value (S.shift (1 - offset)))) + | Myers.Mcons ((name, _, _), tail, _, _) + -> loop tail (intro_opaque ictx name) + in + loop lctx Myers.nil + + let lookup (ictx : t) ((_, expected_name), index : vref) : inl_action = + match Myers.nth_opt index ictx with + | Some ((_, actual_name), _) when actual_name <> expected_name + -> Log.log_fatal + (Printf.sprintf + {|expected "%s", but got "%s"\n|} + (maybename expected_name) + (maybename actual_name)) + | Some (_, action) -> action + | _ -> Opaque +end + +let rec inline (ictx : InlContext.t) (lexp : lexp) : lexp = + match Lexp.nosusp lexp with + | Lexp.Var (_, index as vref), _ + -> (match InlContext.lookup ictx vref with + | InlineBuiltin lexp' + -> lexp' + | InlineVar (name, index') + -> mkVar (name, index + index') + | _ -> lexp) + + | Lexp.Let (location, bindings, body), _ + -> let ictx' = InlContext.intro_decls ictx bindings in + let inline_binding (name, value, ty) = + let value' = inline ictx' value in + (name, value', ty) + in + let bindings' = List.map inline_binding bindings in + let body' = inline ictx' body in + Lexp.mkLet (location, bindings', body') + + | Lexp.Lambda (kind, arg_name, arg_ty, body), _ + -> let ictx' = InlContext.intro_opaque ictx arg_name in + let body' = inline ictx' body in + Lexp.mkLambda (kind, arg_name, arg_ty, body') + + | Lexp.Call (head, tail), _ + -> let inline_arg (kind, value) = (kind, inline ictx value) in + Lexp.mkCall (inline ictx head, List.map inline_arg tail) + + | Lexp.Case (location, subject, return_ty, branches, default), _ + -> let inline_branch (location, names, body) = + let branch_ictx = + InlContext.intro_opaque + (List.fold_left + (fun ictx (_, name) -> InlContext.intro_opaque ictx name) + ictx + names) + (dummy_location, None) + in + let body' = inline branch_ictx body in + (location, names, body') + in + let subject' = inline ictx subject in + let branches' = SMap.map inline_branch branches in + let default' = + match default with + | None -> None + | Some (default_name, default_body) + -> let ictx' = InlContext.intro ictx default_name subject' in + Some (default_name, inline ictx' default_body) + in + Lexp.mkCase (location, subject', return_ty, branches', default') + + | lexp' -> lexp' + +let inline_decls + (ictx : InlContext.t) + (ldecls : ldecls) + : InlContext.t * ldecls = + + let ictx' = InlContext.intro_decls ictx ldecls in + let inline_decl (name, lexp, ty) = (name, inline ictx' lexp, ty) in + (ictx', List.map inline_decl ldecls) ===================================== src/myers.ml ===================================== @@ -141,3 +141,6 @@ let rec fold_right f l i = match l with let map f l = fold_right (fun x l' -> cons (f x) l') l nil let iteri f l = fold_left (fun i x -> f i x; i + 1) 0 l + +let reverse (m : 'a myers) : 'a myers = + fold_left (fun tail head -> cons head tail) nil m View it on GitLab: https://gitlab.com/monnier/typer/-/commit/50eca4074475daa5c450509ffd6d60175… -- View it on GitLab: https://gitlab.com/monnier/typer/-/commit/50eca4074475daa5c450509ffd6d60175… You're receiving this email because of your account on gitlab.com.

1 0

2024

2023

2022

2021

2020

2019

2018

2017

2016

Typer Mars 2021