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

Problème de compilation
by Stefan Monnier 09 Apr '21

09 Apr '21

[ Je renvoie pour Soilih, parce que j'me suis marché dessus et j'ai effacé son message. ] Bonjour tout le monde, J'espère que vous allez bien ! L'objet de mon message est qu'en fait, j'ai des problèmes de compilation. Il se passe que dune me dit que le module linol-lwt n'est pas présente or il est bien installé et je l'ai rajouté à dune. J'ai ces problèmes depuis que j'ai fait un pull de la branche extract-args-from-repl. L'erreur affichée est celle-ci : File "src/typer_lsp_server.ml", line 117, characters 64-80: 117 | method on_notif_doc_did_open ~notify_back d ~content : unit Linol_lwt.Task.m = Error: Unbound module Linol_lwt.Task Pourtant, comme on peut le voir quand j'essaie de l'installer depuis opam : <><> Synchronising pinned packages ><><><><><><><><><><><><><><><><><><><><><><> [linol-lwt.0.2] no changes from file:///home/soilih/Projet Maitrise/typer/linol [NOTE] Package linol-lwt is already installed (current version is 0.2). Voilà. Une petite précision Simon, je ne vais pas créer un autre exécutable, je vais juste rajouter la fonction run() qui démarre le serveur à l'exécutable principal si on démarre typer avec l'argument "--lsp". Donc je veux juste rajouter les bibliothèques lsp, linol-lwt, et linol au fichier dune pour qu'ils soient reconnus. Ils sont tous présent dans opam. Merci beaucoup ! Soilih

2 3

[Git][monnier/typer][backend-object] 2 commits: Merge branch 'extract-args-from-repl'
by Simon Génier (＠ilovemonoids) 09 Apr '21

09 Apr '21

Simon Génier pushed to branch backend-object at Stefan / Typer Commits: e229996a by Simon Génier at 2021-04-09T13:41:26-04:00 Merge branch 'extract-args-from-repl' - - - - - 28dc36e9 by Simon Génier at 2021-04-09T16:35:34-04:00 Introduce swappable backends for Typer. The backends themselves are objects which must implement the new backend abstract class. I also shuffled some code, mostly in the module REPL, so that is it more focused on evaluating interactive code. I move code that was more concerned with loading regular Typer code in typer.ml and elab.ml. - - - - - 8 changed files: - src/REPL.ml - + src/backend.ml - src/elab.ml - src/eval.ml - src/lexp.ml - src/listx.ml - src/option.ml - typer.ml Changes: ===================================== src/REPL.ml ===================================== @@ -36,20 +36,16 @@ this program. If not, see <http://www.gnu.org/licenses/>. *) * * -------------------------------------------------------------------------- *) -open Util +open Backend +open Debruijn +open Eval open Fmt - -open Prelexer open Lexer -open Sexp open Lexp +open Prelexer +open Sexp +open Util -open Eval - -open Grammar - -open Env -open Debruijn module OL = Opslexp module EL = Elexp @@ -58,7 +54,7 @@ let print_input_line i = ralign_print_int i 2; print_string "] >> " -let ieval_error = Log.log_error ~section:"IEVAL" +let error = Log.log_error ~section:"REPL" let print_and_clear_log () = if (not Log.typer_log_config.Log.print_at_log) then @@ -98,84 +94,6 @@ let rec read_input i = 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 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 = 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. *) - 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 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 - (* 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 help_msg = " %quit (%q) : leave REPL %who (%w) : print runtime environment @@ -187,80 +105,103 @@ let help_msg = %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 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."); - (i, lctx, rctx)) - ) - (i, lctx, rctx) files - +(* Elaborate Typer source from an interactive session. Like "normal" Typer, + declarations are grouped in blocks that are mutually recursive, but unlike + "normal" Typer, expressions are also accepted in addition to declarations. + + Note that all declarations are pulled before expressions, i.e. an expression + can refer to variable introduced by later declarations. *) +let eval_interactive + (interactive : #interactive_backend) + (i : int) + (ectx : elab_context) + (input : string) + : 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 source = new Source.source_string input 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 + + (* FIXME We take the parsed input here but we should take the unparsed tokens + directly instead *) + let ldecls, ectx' = Elab.lexp_p_decls decls [] ectx in + + let lexprs = Elab.lexp_parse_all exprs ectx' in + List.iter (fun lexpr -> ignore (OL.check (ectx_to_lctx ectx') lexpr)) lexprs; + + List.iter interactive#process_decls ldecls; + print_and_clear_log (); + + let values = List.map interactive#eval_expr lexprs in + List.iter (Eval.print_eval_result i) values; + print_and_clear_log (); + + ectx' (* Specials commands %[command-name] [args] *) -let rec repl i clxp rctx = - let repl = repl (i + 1) in +let rec repl i (interactive : #interactive_backend) (ectx : elab_context) = let ipt = try read_input i with End_of_file -> "%quit" in + let ectx = 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)) + | "%quit" | "%q" -> exit 0 + | "%help" | "%h" -> (print_string help_msg; ectx) + | "%calltrace" | "%ct" -> (print_eval_trace None; ectx) + | "%typertrace" | "%tt" -> (print_typer_trace None; ectx) + | "%lcollisions" | "%cl" -> (get_stats_hashtbl (WHC.stats hc_table); ectx) (* 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; + let ectx = List.fold_left (Elab.eval_file interactive) ectx args in + print_and_clear_log (); + ectx | "%who"::args | "%w"::args -> ( let _ = match args with - | ["all"] -> dump_rte_ctx rctx - | _ -> print_rte_ctx rctx in - repl clxp rctx) + | ["all"] -> interactive#dump_rte_ctx + | _ -> interactive#print_rte_ctx in + ectx) | "%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) + | ["all"] -> dump_lexp_ctx (ectx_to_lctx ectx) + | _ -> print_lexp_ctx (ectx_to_lctx ectx) in + ectx) | cmd::_ -> - ieval_error (" \"" ^ cmd ^ "\" is not a correct repl command"); - repl clxp rctx - | _ -> repl clxp rctx) + error (" \"" ^ cmd ^ "\" is not a correct repl command"); + ectx + | _ -> ectx) (* eval input *) | _ -> - 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 + try eval_interactive interactive i ectx ipt with | Log.Stop_Compilation msg -> - (handle_stopped_compilation msg; repl clxp rctx) + (handle_stopped_compilation msg; ectx) | Log.Internal_error msg -> (handle_stopped_compilation ("Internal error: " ^ msg); - repl clxp rctx) + ectx) | Log.User_error msg -> (handle_stopped_compilation ("Fatal user error: " ^ msg); - repl clxp rctx) + ectx) + in + repl (i + 1) interactive ectx ===================================== src/backend.ml ===================================== @@ -0,0 +1,48 @@ +(* 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. *) + +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 ===================================== src/elab.ml ===================================== @@ -1338,6 +1338,12 @@ and lexp_decls_1 pending_decls pending_defs in (Log.stop_on_error (); res)) +(* Why is the return value a list of list? + - each `(vname * lexp * ltype)` is a definition + - each `(vname * lexp * ltype) 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. *) and lexp_p_decls (sdecls : sexp list) (tokens : token list) (ctx : elab_context) : ((vname * lexp * ltype) list list * elab_context) = let rec impl sdecls tokens ctx = @@ -1943,3 +1949,21 @@ let eval_decl_str str ectx rctx = let lctx = ectx_to_lctx ectx in let _, elxps = Listx.fold_left_map (OL.clean_decls) lctx lxps in (EV.eval_decls_toplevel elxps rctx), ectx' + +let eval_file + (backend : #Backend.backend) + (ectx : elab_context) + (file_name : string) + : elab_context = + + try + let source = new Source.source_file file_name in + let pretokens = prelex source in + let tokens = lex Grammar.default_stt pretokens in + let ldecls, ectx' = lexp_p_decls [] tokens ectx in + List.iter backend#process_decls ldecls; + ectx' + with + | Sys_error _ + -> (error (Printf.sprintf {|file %s does not exist.|} file_name); + ectx) ===================================== src/eval.ml ===================================== @@ -1187,3 +1187,23 @@ let from_lctx (lctx: lexp_context): runtime_env = (* build a rctx from a ectx. *) let from_ectx (ctx: elab_context): runtime_env = from_lctx (ectx_to_lctx ctx) + +class ast_interpreter lctx = object + inherit Backend.interactive_backend + + val mutable rctx = from_lctx lctx + val mutable lctx = lctx + + method process_decls ldecls = + let lctx', eldecls = Opslexp.clean_decls lctx ldecls in + rctx <- eval_decls eldecls rctx; + lctx <- lctx' + + method eval_expr lexp = + let elexp = Opslexp.erase_type lctx lexp in + debug_eval elexp rctx + + method print_rte_ctx = Env.print_rte_ctx rctx + + method dump_rte_ctx = Env.dump_rte_ctx rctx +end ===================================== 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/listx.ml ===================================== @@ -44,3 +44,10 @@ let fold_left_map loop fold_acc (new_element :: map_acc) bs in loop i [] bs + +(* Backport from 4.12. *) +let rec equal (p : 'a -> 'a -> bool) (ls : 'a list) (rs : 'a list) : bool = + match ls, rs with + | l :: ls', r :: rs' -> p l r && equal p ls' rs' + | _ :: _, [] | [], _ :: _ -> false + | [], [] -> true ===================================== src/option.ml ===================================== @@ -35,3 +35,8 @@ 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 ===================================== typer.ml ===================================== @@ -51,22 +51,34 @@ let arg_defs = let main () = let usage = Sys.executable_name ^ " [options] <file1> [<file2>] …" in Arg.parse arg_defs add_input_file usage; - let files = List.rev !arg_files in - let is_interactive = not !arg_batch in - if is_interactive - then - (print_string (Fmt.make_title " TYPER REPL "); - print_string welcome_msg; - print_string (Fmt.make_sep '-'); - flush stdout); + let ectx = Elab.default_ectx in + let backend = new Eval.ast_interpreter (Debruijn.ectx_to_lctx ectx) in + let interactive = backend#interactive in + let file_names = List.rev !arg_files in + let is_interactive = not !arg_batch && Option.is_some interactive in - let i, ectx, rctx = + let process_file = + if is_interactive + then + (print_string (Fmt.make_title " TYPER REPL "); + print_string welcome_msg; + print_string (Fmt.make_sep '-'); + flush stdout; + fun ectx i file_name + -> Printf.printf " In[%02d] >> %%readfile %s\n" i file_name; + Elab.eval_file backend ectx file_name) + else + fun ectx _ file_name -> Elab.eval_file backend ectx file_name + in + + let ectx, i = try - let ectx = Elab.default_ectx in - let rctx = Elab.default_rctx in let res = - REPL.readfiles files (1, ectx, rctx) is_interactive + List.fold_left + (fun (ectx, i) file_name -> (process_file ectx i file_name, i + 1)) + (ectx, 0) + file_names in REPL.print_and_clear_log (); res @@ -82,7 +94,8 @@ let main () = exit 1 in - if is_interactive - then REPL.repl i ectx rctx + match is_interactive, interactive with + | true, Some (interactive) -> REPL.repl i interactive ectx + | _ -> () let () = main () View it on GitLab: https://gitlab.com/monnier/typer/-/compare/6c849ddf758619d4ef5bbc45c70a8973… -- View it on GitLab: https://gitlab.com/monnier/typer/-/compare/6c849ddf758619d4ef5bbc45c70a8973… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][soilih] 22 commits: [Myers] Add nth_opt and reverse.
by Soilihi BEN SOILIHI BOINA (＠BenSoilih) 09 Apr '21

09 Apr '21

Soilihi BEN SOILIHI BOINA pushed to branch soilih 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. - - - - - bde2d9b9 by Soilih BEN SOILIH at 2021-03-30T21:05:26-06:00 Merge branch 'master' of https://gitlab.com/monnier/typer - - - - - 424af536 by Simon Génier at 2021-04-02T16:11:45-04:00 Merge branch 'source-object' - - - - - 0590a584 by Simon Génier at 2021-04-04T21:50:28-04:00 Use the environment augmented with the new bindings for type erasure. - - - - - b3886bc0 by Simon Génier at 2021-04-04T21:51:47-04:00 Remove a test testing incorrect code. - - - - - 0e3dcf79 by Simon Génier at 2021-04-05T00:18:00-04:00 Merge branch 'broken-tests-2021-04' - - - - - a8e4948d by Simon Génier at 2021-04-05T00:23:48-04:00 Dunify Typer tests. - - - - - 6816e0aa by Simon Génier at 2021-04-07T15:35:15-04:00 Merge branch 'dunify-tests' - - - - - ceed8e81 by Simon Génier at 2021-04-07T16:05:34-04:00 Move code related to command-line argument parsing out of REPL. - - - - - be768c34 by Soilih BEN SOILIH at 2021-04-08T16:52:39-06:00 h - - - - - c0f859bc by Soilih BEN SOILIH at 2021-04-08T17:03:41-06:00 update - - - - - 94ab822b by Soilih BEN SOILIH at 2021-04-08T17:14:00-06:00 Merge branch 'extract-args-from-repl' of https://gitlab.com/monnier/typer into extract - - - - - f847a4c1 by Soilih BEN SOILIH at 2021-04-08T17:17:15-06:00 extract - - - - - f9f40536 by Soilih BEN SOILIH at 2021-04-08T18:18:36-06:00 commit - - - - - e58ae4ad by Soilih BEN SOILIH at 2021-04-08T18:28:48-06:00 bugs - - - - - 2941d939 by Soilih BEN SOILIH at 2021-04-09T13:38:10-06:00 fix merge conflict - - - - - 9836b205 by Soilih BEN SOILIH at 2021-04-09T13:40:42-06:00 merge conflict - - - - - 7ad32eb9 by Soilih BEN SOILIH at 2021-04-09T13:44:17-06:00 lsp args - - - - - 6add7c68 by Soilih BEN SOILIH at 2021-04-09T13:48:40-06:00 lsp - - - - - b2fe2a90 by Soilih BEN SOILIH at 2021-04-09T13:50:10-06:00 readstring - - - - - 29 changed files: - .gitignore - GNUmakefile - README.md - + btl/dune - src/debug_util.ml → debug_util.ml - + dune - + extract - src/REPL.ml - src/dune - src/elab.ml - src/eval.ml - src/lexer.ml - src/myers.ml - src/option.ml - src/prelexer.ml - + src/source.ml - src/typer_lsp_server.ml - + tests/dune - tests/elab_test.ml - tests/env_test.ml - tests/eval_test.ml - tests/inverse_test.ml - tests/lexp_test.ml - tests/macro_test.ml - tests/sexp_test.ml - tests/unify_test.ml - tests/utest_lib.ml - − tests/utest_main.ml - + typer.ml Changes: ===================================== .gitignore ===================================== @@ -1,5 +1,7 @@ # Files generated by OCaml's compiler +*.bc *.byte +*.exe *.annot *.cmi *.cmo ===================================== GNUmakefile ===================================== @@ -1,96 +1,58 @@ -RM=rm -f -MV=mv -OCAMLBUILD=ocamlbuild - -BUILDDIR := _build - +DUNE = dune OCAMLCP := ocamlcp -OCAMLOPT := ocamlopt -OCAMLDEP := ocamldep + +BUILDDIR := _build SRC_FILES := $(wildcard ./src/*.ml) -TEST_FILES := $(wildcard ./tests/*_test.ml) DEPSORT_FILES := $(shell ocamldep -sort -I src $(SRC_NO_DEBUG)) -OBFLAGS = -tag debug -tag profile -lib str -build-dir $(BUILDDIR) -pkg zarith -# OBFLAGS := -I $(SRCDIR) -build-dir $(BUILDDIR) -pkg str -# OBFLAGS_DEBUG := -tag debug -tag profile -tag "warn(+20)" -# OBFLAGS_RELEASE := -tag unsafe -tag inline -COMPILE_MODE = byte -# COMPILE_MODE = native +DUNE_PROFILE = dev +# DUNE_PROFILE = release + +# Set COMPILE_MODE to native to build ocaml code with ocamlopt. +COMPILE_MODE ?= bc # DEBUG ?= 1 # VERBOSE ?= 1 -all: typer debug tests-build - -# ifeq ($(OS), Windows_NT) -# Windows need '-r' and building to native can be problematic (linking error) -# So we build to byte instead -# OBFLAGS = $(OBFLAGS) -r -# endif - -# ifeq ($(DEBUG), 1) -# OBFLAGS += $(OBFLAGS_DEBUG) -# else -# OBFLAGS += $(OBFLAGS_RELEASE) -# endif +all: typer debug tests help: ## Prints help for targets with comments @grep -E '^[a-zA-Z_-]+:.*?## .*$$' $(MAKEFILE_LIST) \ | { echo -e 'typer: ## Build Typer'; sort; } \ | awk 'BEGIN {FS = ":.*?## "}; {printf "\033[36m%-30s\033[0m %s\n", $$1, $$2}' -# debug file eval -debug: - # ============================ - # Build debug utils - # ============================ - $(OCAMLBUILD) src/debug_util.$(COMPILE_MODE) -I src $(OBFLAGS) - @$(MV) $(BUILDDIR)/src/debug_util.$(COMPILE_MODE) $(BUILDDIR)/debug_util +typer: typer.$(COMPILE_MODE) -# interactive typer -typer: - # ============================ - # Build typer - # ============================ - $(OCAMLBUILD) src/REPL.$(COMPILE_MODE) -I src $(OBFLAGS) - @$(MV) $(BUILDDIR)/src/REPL.$(COMPILE_MODE) $(BUILDDIR)/typer +debug: debug_util.$(COMPILE_MODE) -tests-build: - # ============================ - # Build tests - # ============================ - @$(foreach test, $(TEST_FILES), \ - $(OCAMLBUILD) $(subst ./,,$(subst .ml,.$(COMPILE_MODE) ,$(test))) \ - -I src $(OBFLAGS);) - @$(OCAMLBUILD) tests/utest_main.$(COMPILE_MODE) -I src $(OBFLAGS) - @$(MV) $(BUILDDIR)/tests/utest_main.$(COMPILE_MODE) \ - $(BUILDDIR)/tests/utests +# interactive typer +typer.$(COMPILE_MODE): + $(DUNE) --profile $(DUNE_PROFILE) build ./typer.$(COMPILE_MODE) -tests-run: - @./$(BUILDDIR)/tests/utests --verbose 3 +debug_util.$(COMPILE_MODE): + $(DUNE) build ./debug_util.$(COMPILE_MODE) -test-file: - $(OCAMLBUILD) src/test.$(COMPILE_MODE) -I src $(OBFLAGS) - @$(MV) $(BUILDDIR)/src/test.$(COMPILE_MODE) $(BUILDDIR)/test +# By default, Dune only runs tests that failed since the last changes. This can +# be confusing if you don't know Dune, so we pass the --force flag to rerun all +# the tests no matter what. +tests: + $(DUNE) --force test # There is nothing here. I use this to test if opam integration works install: tests -tests: tests-build tests-run - # Make language doc doc-tex: texi2pdf ./doc/manual.texi --pdf --build=clean # Make implementation doc doc-ocaml: - ocamldoc -html -d $(BUILDDIR)/doc $(SRC_FILES) + ocamldoc -html -d $(BUILDDIR)/doc $(SRC_FILES) # everything is expected to be compiled in the "./$(BUILDDIR)/" folder clean: - -rm -rf $(BUILDDIR) + $(DUNE) clean .PHONY: typer debug tests @@ -110,9 +72,6 @@ run/tests: run/typer-file: @./$(BUILDDIR)/typer ./samples/test__.typer -run/test-file: - @./$(BUILDDIR)/test - # Compile into bytecode using ocamlc in profiling mode. # Generate a ocamlprof.dump file. profiling-cp: ===================================== README.md ===================================== @@ -9,18 +9,17 @@ Status [![Build Status](https://travis-ci.org/Delaunay/typer.svg?branch=master)] ## Requirement * Ocaml 4.05 -* Ocamlfind -* Ocamlbuild -* Findlib +* Dune 2.x * Zarith ## Build -By default ocamlbuild creates a '_build' folder which holds all the compiled files. +By default, Dune creates a '_build' folder which holds all the compiled files. -* `make typer`: build typer interpreter './typer' -* `make debug`: build typer with debug info './debug_util' -* `make tests`: run interpreter's tests './tests/utests' +* `make typer`: build Typer interpreter (`./typer_cli.bc`). +* `COMPILE_MODE=native make typer`: build Typer interpreter (`./typer_cli.exe`). +* `make debug`: build typer with debug info (`./debug_util.bc`). +* `make tests`: run interpreter's tests. # Directory layout ===================================== btl/dune ===================================== @@ -0,0 +1,5 @@ +;; -*- lisp-data -*- + +(alias + (name typer_stdlib) + (deps (glob_files *.typer))) ===================================== src/debug_util.ml → debug_util.ml ===================================== @@ -30,6 +30,8 @@ * * --------------------------------------------------------------------------- *) +open Typerlib + (* Utilities *) open Util open Fmt @@ -169,7 +171,8 @@ let format_source () = print_string (make_title " ERRORS "); let filename = List.hd (!arg_files) in - let pretoks = prelex_file filename in + let source = new Source.source_file filename in + let pretoks = prelex source in let toks = lex default_stt pretoks in let ctx = Elab.default_ectx in let lexps, _ = Elab.lexp_p_decls [] toks ctx in @@ -212,7 +215,8 @@ let main () = (* get pretokens*) print_string yellow; - let pretoks = prelex_file filename in + let source = new Source.source_file filename in + let pretoks = prelex source in print_string reset; (if (get_p_option "pretok") then( @@ -274,7 +278,9 @@ let main () = print_lexp_ctx (ectx_to_lctx nctx); print_string "\n")); (* Type erasure *) - let clean_lxp = List.map OL.clean_decls lexps in + let _, clean_lxp = + Listx.fold_left_map OL.clean_decls (ectx_to_lctx nctx) lexps + in (* Eval declaration *) let rctx = Elab.default_rctx in ===================================== dune ===================================== @@ -0,0 +1,15 @@ +;; -*- lisp-data -*- + +(executable + (name typer) + (promote (until-clean)) + (modules typer) + (libraries typerlib) + (modes byte native)) + +(executable + (name debug_util) + (promote (until-clean)) + (modules debug_util) + (libraries typerlib) + (modes byte native)) ===================================== extract ===================================== @@ -0,0 +1 @@ +Subproject commit ceed8e815e7c8525e093869f3c1bcea68613b85e ===================================== src/REPL.ml ===================================== @@ -35,7 +35,6 @@ this program. If not, see <http://www.gnu.org/licenses/>. *) * Out[ 3] >> 6 * * -------------------------------------------------------------------------- *) - open Util open Fmt @@ -53,9 +52,6 @@ open Debruijn module OL = Opslexp module EL = Elexp -let arg_batch = ref false -let lsp_server = ref true - let print_input_line i = print_string " In["; ralign_print_int i 2; @@ -144,14 +140,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. *) @@ -164,8 +160,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 @@ -179,20 +175,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 - - %quit (%q) : leave REPL - %help (%h) : print help -" - let help_msg = " %quit (%q) : leave REPL %who (%w) : print runtime environment @@ -204,13 +186,6 @@ let help_msg = %help (%h) : print help " -let readstring (str:string) = - let ectx = Elab.default_ectx in - (*let rctx = Elab.default_rctx in*) - Elab.lexp_decl_str str ectx ; - let ref_list = Log.typer_log in - List.map (fun x -> x) !ref_list - let readfiles files (i, lctx, rctx) prt = (* Read specified files *) @@ -220,8 +195,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."); @@ -230,7 +207,6 @@ 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 @@ -272,10 +248,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) @@ -284,65 +262,4 @@ let rec repl i clxp rctx = 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"); - ("--lsp", Arg.Set lsp_server, "Enable the LSP server"); - ("--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 (); - - if !lsp_server then Typer_lsp_server.run () - else (); - - 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 () + repl clxp rctx) \ No newline at end of file ===================================== src/dune ===================================== @@ -1,9 +1,8 @@ ;; -*- lisp-data -*- -(executable - (name REPL ) - ;; (public_name typer) - (libraries "zarith" "str" - "linol" "linol-lwt" - "lsp" "jsonrpc" - ) -) +(library + (name typerlib) + (libraries zarith str + linol linol-lwt + lsp jsonrpc + )) + ===================================== 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 @@ -1169,8 +1171,9 @@ let from_lctx (lctx: lexp_context): runtime_env = let _ = (* FIXME: Evaluate those defs that we can, even if not all defs * are present! *) + let lctx' = DB.lctx_extend_rec lctx defs in if alldefs && closed_p rctx (OL.fv_hoist (List.length defs) fvs) then - List.iter (fun (e, rc) -> rc := eval (OL.erase_type lctx e) nrctx) evs + List.iter (fun (e, rc) -> rc := eval (OL.erase_type lctx' e) nrctx) evs else () in nrctx and from_lctx lctx = ===================================== 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/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,8 @@ 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 ===================================== 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 ===================================== src/typer_lsp_server.ml ===================================== @@ -54,9 +54,14 @@ let log_level_to_severity (level:log_level) : Lsp.Types.DiagnosticSeverity.t = | Info -> Lsp.Types.DiagnosticSeverity.Information | _ -> Lsp.Types.DiagnosticSeverity.Hint +let readstring (str:string) = + let ectx = Elab.default_ectx in + (*let rctx = Elab.default_rctx in*) + ignore (Elab.lexp_decl_str str ectx); + !Log.typer_log let process_some_input_file (_file_contents : string) : state_after_processing = - REPL.readstring _file_contents + readstring _file_contents let diagnostics (_state : state_after_processing) : Lsp.Types.Diagnostic.t list = let log_tab = log_entry_to_list _state in ===================================== tests/dune ===================================== @@ -0,0 +1,15 @@ +;; -*- lisp-data -*- + +(tests + (names elab_test + env_test + eval_test + inverse_test + lexp_test + macro_test + sexp_test + unify_test) + (deps (alias %{project_root}/btl/typer_stdlib)) + (libraries typerlib) + (action + (chdir %{project_root} (run %{test})))) ===================================== tests/elab_test.ml ===================================== @@ -21,12 +21,13 @@ * * -------------------------------------------------------------------------- *) +open Typerlib + open Utest_lib let add_elab_test elab test name ?(setup="") ?(expected="") input = let run_elab_test () = - let ectx = Elab.default_ectx in - let _, ectx = Elab.lexp_decl_str setup ectx in + let _, ectx = Elab.lexp_decl_str setup Elab.default_ectx in let last_metavar = !Unification.global_last_metavar in let actual, _ = elab input ectx in if String.equal expected "" ===================================== tests/env_test.ml ===================================== @@ -25,13 +25,9 @@ * * --------------------------------------------------------------------------- *) -open Util -open Utest_lib - -open Sexp -open Lexp +open Typerlib -open Builtin +open Utest_lib open Env @@ -55,14 +51,14 @@ let _ = (add_test "ENV" "Set Variables" (fun () -> let n = (List.length var) - 1 in let rctx = List.fold_left - (fun ctx (n, t, _) -> + (fun ctx (n, _, _) -> add_rte_variable n Vundefined ctx) rctx var in print_rte_ctx rctx; let rctx, _ = List.fold_left - (fun (ctx, idx) (n, _, v) -> + (fun (ctx, idx) (n, _, _) -> (set_rte_variable idx n Vundefined ctx); (ctx, idx - 1)) (rctx, n) var in ===================================== tests/eval_test.ml ===================================== @@ -25,11 +25,9 @@ * * --------------------------------------------------------------------------- *) -open Utest_lib -open Util +open Typerlib -open Sexp -open Lexp +open Utest_lib open Eval (* reset_eval_trace *) @@ -86,18 +84,6 @@ let _ = test_eval_eqv_named x = let a = 1; b = 2 in I in (case x | I => c);" (* == *) "3" -let _ = test_eval_eqv_named - "Let3" - - "c = 3; e = 1; f = 2; d = 4;" - - "let TrueProp : Type; - I : TrueProp; - TrueProp = typecons TrueProp I; - I = datacons TrueProp I; - x = let a = 1; b = 2 in I - in (case x | I => c);" (* == *) "3" - let _ = test_eval_eqv_named "Let-erasable" @@ -270,10 +256,10 @@ let _ = test_eval_eqv "w = 2" "declexpr w" "2" let _ = (add_test "EVAL" "Monads" (fun () -> - let dcode = " - c = IO_bind (File_open \"./_build/w_file.txt\" \"w\") - (lambda f -> File_write f \"Hello2\"); - " in + let dcode = {| + c = IO_bind (File_open "w_file.txt" "w") + (lambda f -> File_write f "Hello2"); + |} in let rctx, ectx = Elab.eval_decl_str dcode ectx rctx in @@ -282,7 +268,7 @@ let _ = (add_test "EVAL" "Monads" (fun () -> (* Eval defined lambda *) let ret = Elab.eval_expr_str rcode ectx rctx in match ret with - | [v] -> success + | [_] -> success | _ -> failure)) let _ = test_eval_eqv_named @@ -471,7 +457,7 @@ let _ = let str = "(Int_" ^ op ^ " " ^ (string_of_int a) ^ " " ^ (string_of_int b) ^ ")" in let lxp = List.hd (Elab.lexp_expr_str str ectx) in - let elxp = OL.erase_type lxp in + let elxp = OL.erase_type (Debruijn.ectx_to_lctx ectx) lxp in assert (Log.error_count () == 0); if Z.fits_int expect' then ===================================== tests/inverse_test.ml ===================================== @@ -21,23 +21,13 @@ * * -------------------------------------------------------------------------- *) -open Sexp -open Pexp +open Typerlib + open Lexp -open Unification open Inverse_subst open Utest_lib -open Fmt - -open Builtin -open Env - -open Str - -open Debug - let mkShift2 shift subst = S.mkShift subst shift ===================================== tests/lexp_test.ml ===================================== @@ -25,12 +25,9 @@ * * --------------------------------------------------------------------------- *) -open Utest_lib - -open Pexp -open Lexp +open Typerlib -open Builtin +open Utest_lib (* default environment *) let ectx = Elab.default_ectx ===================================== tests/macro_test.ml ===================================== @@ -25,16 +25,10 @@ * * --------------------------------------------------------------------------- *) -open Util -open Utest_lib - -open Sexp -open Lexp +open Typerlib -open Eval (* reset_eval_trace *) - -open Builtin open Env +open Utest_lib (* default environment *) ===================================== tests/sexp_test.ml ===================================== @@ -1,9 +1,12 @@ +open Typerlib + open Sexp open Lexer open Utest_lib -let sexp_parse_str dcode - = sexp_parse_str dcode Grammar.default_stt Grammar.default_grammar (Some ";") +let sexp_parse_str dcode = + let source = new Source.source_string dcode in + sexp_parse_source source Grammar.default_stt Grammar.default_grammar (Some ";") let test_sexp_add dcode testfun = add_test "SEXP" dcode ===================================== tests/unify_test.ml ===================================== @@ -21,6 +21,7 @@ * * -------------------------------------------------------------------------- *) +open Typerlib open Lexp open Unification @@ -61,7 +62,7 @@ let unif_output (lxp1: lexp) (lxp2: lexp) ctx = let add_unif_test name ?(ectx=ectx) lxp_a lxp_b expected = add_test "UNIFICATION" name (fun () -> - let (r, cstrts) = unif_output lxp_a lxp_b (DB.ectx_to_lctx ectx) in + let (r, _) = unif_output lxp_a lxp_b (DB.ectx_to_lctx ectx) in if r = expected then success ===================================== tests/utest_lib.ml ===================================== @@ -30,6 +30,8 @@ * * --------------------------------------------------------------------------- *) +open Typerlib + open Fmt open Util @@ -63,7 +65,7 @@ exception Unexpected_result of string * 2: Print Each composing Test * 3: use debug *) -let global_verbose_lvl = ref 0 +let global_verbose_lvl = ref 2 let global_sample_dir = ref "" let global_fsection = ref "" let global_ftitle = ref "" @@ -94,7 +96,7 @@ let must_run_title str = !global_ftitle = "" || String.uppercase_ascii str = !global_ftitle -let parse_args () = Arg.parse arg_defs (fun s -> ()) "" +let parse_args () = Arg.parse arg_defs (fun _ -> ()) "" (* Utest printing function *) @@ -144,7 +146,7 @@ let expect_equal_lexps = _expect_equal_t lexp_list_eq string_of_lexp_list let expect_equal_decls = - let rec decl_eq l r = + let decl_eq l r = let (_, l_vname), l_lexp, l_ltype = l in let (_, r_vname), r_lexp, r_ltype = r in Option.equal String.equal l_vname r_vname ===================================== tests/utest_main.ml deleted ===================================== @@ -1,184 +0,0 @@ -(* - * Typer Compiler - * - * --------------------------------------------------------------------------- - * - * Copyright (C) 2011-2020 Free Software Foundation, Inc. - * - * Author: Pierre Delaunay <pierre.delaunay(a)hec.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/>. - * - * --------------------------------------------------------------------------- - * - * Description: - * Basic utest program run all tests - * - * --------------------------------------------------------------------------- *) - -(** Search *_test.byte executable and run them. - Usage: - ./utest_main tests_folder root_folder *) - -open Fmt - -let global_verbose_lvl = ref 5 -let global_sample_dir = ref "." -let global_tests_dir = ref (Filename.concat "_build" "tests") -let global_fsection = ref "" -let global_ftitle = ref "" -let global_filter = ref false - -let arg_defs = - [ - ("--verbose", - Arg.Set_int global_verbose_lvl, " Set verbose level"); - ("--samples", - Arg.Set_string global_sample_dir, " Set sample directory"); - ("--tests", - Arg.Set_string global_tests_dir, " Set tests directory"); - (* Allow users to select which test to run *) - ("--fsection", - Arg.String (fun g -> global_fsection := String.uppercase_ascii g; - global_filter := true), " Set test filter"); - ("--ftitle", - Arg.String (fun g -> global_ftitle := String.uppercase_ascii g; - global_filter := true), " Set test filter"); - ] - - -let verbose n = (n <= (!global_verbose_lvl)) - -let parse_args () = Arg.parse arg_defs (fun s -> ()) "" - -let ut_string vb msg = if verbose vb then print_string msg else () - -let cut_byte str = String.sub str 0 ((String.length str) - 10) -let cut_native str = String.sub str 0 ((String.length str) - 12) - -let cut_name str = - if Filename.check_suffix str "_test.byte" - then cut_byte str - else cut_native str - -let print_file_name i n name pass = - let line_size = 80 - (String.length (cut_name name)) - 16 in - let name = cut_name name in - - (if pass then print_string green else print_string red); - print_string " ("; - ralign_print_int i 2; print_string "/"; - ralign_print_int n 2; print_string ") "; - print_string name; - print_string (make_line '.' line_size); - if pass then print_string "..OK\n" else print_string "FAIL\n"; - print_string reset - -let must_run str = - not !global_filter - || String.uppercase_ascii (cut_name str) = !global_fsection - -let main () = - parse_args (); - - print_string "\n"; - calign_print_string " Running Unit Test " 80; - print_string "\n\n"; - - (*print_string ("[ ] Test folder: " ^ folder ^ "\n"); *) - - (* get tests files *) - let folder = !global_tests_dir in - let root_folder = !global_sample_dir in - - let files = - try Sys.readdir folder - with - | e - -> (print_string ("The folder: " ^ !global_tests_dir - ^ " does not exist.\n" - ^ "Have you tried \"./utests --tests= ./tests\" ?\n"); - raise e) - in - - let check name = - Filename.check_suffix name "_test.byte" - || Filename.check_suffix name "_test.native" - in - - (* select files that are executable tests *) - let files = Array.fold_left - (fun acc elem -> if check elem then elem::acc else acc) - [] files in - - let files_n = List.length files in - - (if files_n = 0 then - print_string "No tests were found. Did you compiled them? \n"); - - let exit_code = ref 0 in - let failed_test = ref 0 in - let tests_n = ref 0 in - let test_args = - ["--samples"; root_folder; - "--verbose"; string_of_int !global_verbose_lvl] - @ (if not (!global_ftitle = "") then - ["--ftitle"; !global_ftitle] else []) in - - let run_file test_path = - flush stdout; - - tests_n := !tests_n + 1; - let command_parts = Filename.concat folder test_path :: test_args in - let command_parts = - if Sys.os_type = "Win32" - then - (* I wish Filename.quote could be used on Windows. - - It would be appropriate if Ocaml spawned the process through the C - API, but Sys.command passes does it through the shell, which is - cmd.exe and has its own quoting rules. Ocaml has - Filename.quote_command, which does the right thing on every platform, - but it is only available since Ocaml 4.10. Until then, let's hope the - command does not need to be escaped. *) - command_parts - else List.map Filename.quote command_parts - in - - print_endline (String.concat " " command_parts); - exit_code := Sys.command (String.concat " " command_parts); - - (if !exit_code != 0 - then - ((if verbose 1 then print_file_name !tests_n files_n test_path false); - failed_test := !failed_test + 1) - else - (if verbose 1 then print_file_name !tests_n files_n test_path true); - ); - - (if verbose 2 then print_newline ()); - in - - List.iter run_file (List.filter must_run files); - - print_string "\n\n"; - print_string " Test Ran : "; print_int !tests_n; - print_string "\n Test Failed : "; print_int !failed_test; - print_string "\n Test Passed : "; print_int (!tests_n - !failed_test); - print_endline "\n" - -let _ = main (); ===================================== typer.ml ===================================== @@ -0,0 +1,96 @@ +(* 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/>. *) + +(** This file is the the entry point to the typer REPL. *) + +open Typerlib + +let welcome_msg = +" Typer 0.0.0 - Interpreter - (c) 2016-2021 + + %quit (%q) : leave REPL + %help (%h) : print help +" + +let arg_batch = ref false + +(*booléen utilisé pour démarrer le serveur. + je l'ai mis true pour les tests +*) +let lsp_server = ref true + +let arg_files = ref [] +let add_input_file file = + arg_files := file :: !arg_files + +let arg_defs = + [("--batch", Arg.Set arg_batch, "Don't run the interactive loop"); + ("--lsp", Arg.Set lsp_server, "Enable Typer LSP server"); + + ("--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."); + ] + +let main () = + let usage = Sys.executable_name ^ " [options] <file1> [<file2>] …" in + Arg.parse arg_defs add_input_file usage; + if !lsp_server then Typer_lsp_server.run () + else (); + let files = List.rev !arg_files in + let is_interactive = not !arg_batch in + + if is_interactive + then + (print_string (Fmt.make_title " TYPER REPL "); + print_string welcome_msg; + print_string (Fmt.make_sep '-'); + flush stdout); + + let i, ectx, rctx = + try + let ectx = Elab.default_ectx in + let rctx = Elab.default_rctx in + let res = + REPL.readfiles files (1, ectx, rctx) is_interactive + in + REPL.print_and_clear_log (); + res + 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 + + if is_interactive + then REPL.repl i ectx rctx + +let () = main () View it on GitLab: https://gitlab.com/monnier/typer/-/compare/7abb48c554174b01d898ea7039b2e4c1… -- View it on GitLab: https://gitlab.com/monnier/typer/-/compare/7abb48c554174b01d898ea7039b2e4c1… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer] Deleted branch extract-args-from-repl
by Simon Génier (＠ilovemonoids) 09 Apr '21

09 Apr '21

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

1 0

[Git][monnier/typer][master] 2 commits: Move code related to command-line argument parsing out of REPL.
by Simon Génier (＠ilovemonoids) 09 Apr '21

09 Apr '21

Simon Génier pushed to branch master at Stefan / Typer Commits: ceed8e81 by Simon Génier at 2021-04-07T16:05:34-04:00 Move code related to command-line argument parsing out of REPL. - - - - - e229996a by Simon Génier at 2021-04-09T13:41:26-04:00 Merge branch 'extract-args-from-repl' - - - - - 2 changed files: - src/REPL.ml - typer.ml Changes: ===================================== src/REPL.ml ===================================== @@ -53,8 +53,6 @@ open Debruijn module OL = Opslexp module EL = Elexp -let arg_batch = ref false - let print_input_line i = print_string " In["; ralign_print_int i 2; @@ -178,13 +176,6 @@ let raw_eval source ectx rctx = (* This is for consistency with ieval *) [], ectx', rctx -let welcome_msg = -" Typer 0.0.0 - Interpreter - (c) 2016 - - %quit (%q) : leave REPL - %help (%h) : print help -" - let help_msg = " %quit (%q) : leave REPL %who (%w) : print runtime environment @@ -273,57 +264,3 @@ let rec repl i 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 ===================================== typer.ml ===================================== @@ -17,4 +17,72 @@ * You should have received a copy of the GNU General Public License along with * this program. If not, see <http://www.gnu.org/licenses/>. *) -let () = Typerlib.REPL.main () +(** This file is the the entry point to the typer REPL. *) + +open Typerlib + +let welcome_msg = +" Typer 0.0.0 - Interpreter - (c) 2016-2021 + + %quit (%q) : leave REPL + %help (%h) : print help +" + +let arg_batch = ref false + +let arg_files = ref [] +let add_input_file file = + arg_files := file :: !arg_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."); + ] + +let main () = + let usage = Sys.executable_name ^ " [options] <file1> [<file2>] …" in + Arg.parse arg_defs add_input_file usage; + let files = List.rev !arg_files in + let is_interactive = not !arg_batch in + + if is_interactive + then + (print_string (Fmt.make_title " TYPER REPL "); + print_string welcome_msg; + print_string (Fmt.make_sep '-'); + flush stdout); + + let i, ectx, rctx = + try + let ectx = Elab.default_ectx in + let rctx = Elab.default_rctx in + let res = + REPL.readfiles files (1, ectx, rctx) is_interactive + in + REPL.print_and_clear_log (); + res + 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 + + if is_interactive + then REPL.repl i ectx rctx + +let () = main () View it on GitLab: https://gitlab.com/monnier/typer/-/compare/6816e0aa66886deafa267f95cc456dfb… -- View it on GitLab: https://gitlab.com/monnier/typer/-/compare/6816e0aa66886deafa267f95cc456dfb… You're receiving this email because of your account on gitlab.com.

1 0

Compilateur vers Gambit (prise 2) et autres changements
by Génier Simon 08 Apr '21

08 Apr '21

Salut, Voici quelques branches à réviser. https://gitlab.com/monnier/typer/-/compare/master...extract-args-from-repl Cette branche déplace le traitement des arguments en ligne de commande vers le fichier typer.ml (le nouveau point d'entrée). De cette façon, le module REPL ne contient que du code relié au REPL. Soilih, tu peux t'inspirer du fichier typer.ml pour créer un nouveau point d'entrée pour ton serveur LSP (n'oublie pas d'ajouter l'exécutable au fichier dune). https://gitlab.com/monnier/typer/-/compare/extract-args-from-repl...backend… J'ai extrait la création des backend dans une patch séparée. Le but de ce changement est de créer un objet backend qui permet de manipuler de façon abstraite un consommateur de Lexp. https://gitlab.com/monnier/typer/-/compare/backend-object...gambit Dans cette patch, je crée un nouveau backend qui émet du code Scheme compatible avec Gambit. https://gitlab.com/monnier/typer/-/compare/master...lexer-tests Finalement, cette patch ajoute des tests pour la phase d'analyse lexicale. C'est utile parce qu'il y a des subtilités au niveau des operateurs internes et j'ai une autre patch qui s'en vient qui fait des changements à cette phase pour préparer le changement des locations à un intervalle de caractères. Merci Simon

2 1

[Git][monnier/typer] Pushed new branch lexer-tests
by Simon Génier (＠ilovemonoids) 07 Apr '21

07 Apr '21

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

1 0

[Git][monnier/typer][gambit] Add a backend to compile Typer to Scheme.
by Simon Génier (＠ilovemonoids) 07 Apr '21

07 Apr '21

Simon Génier pushed to branch gambit at Stefan / Typer Commits: 3a38656d by Simon Génier at 2021-04-07T17:13:29-04:00 Add a backend to compile Typer to Scheme. - - - - - 4 changed files: - + src/gambit.ml - tests/dune - + tests/gambit_test.ml - typer.ml Changes: ===================================== src/gambit.ml ===================================== @@ -0,0 +1,302 @@ +(* 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 + Buffer.add_char buffer '"'; + 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.add_char buffer '"'; + 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' + + let describe (exp : t) : string = + match exp with + | Symbol _ -> "a symbol" + | List _ -> "a list" + | String _ -> "a string" + | Integer _ -> "an integer" + | Float _ -> "a float" + + let rec equal (l : t) (r : t) : bool = + match l, r with + | Symbol l, Symbol r | String l, String r + -> String.equal l r + | List ls, List rs -> Listx.equal equal ls rs + | Integer l, Integer r -> Z.equal l r + | Float l, Float r -> Float.equal l r + | _ -> false +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]) + +class gambit_compiler lctx output = object + inherit Backend.backend + + val mutable sctx = ScmContext.of_lctx lctx + val mutable lctx = lctx + + method process_decls ldecls = + 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 + + sctx <- sctx'; + lctx <- lctx'; + Scm.print output sdecls; +end ===================================== tests/dune ===================================== @@ -4,6 +4,7 @@ (names elab_test env_test eval_test + gambit_test inverse_test lexp_test macro_test ===================================== tests/gambit_test.ml ===================================== @@ -0,0 +1,190 @@ +(* 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/>. *) + +(** Tests for the compilation of Lexps to Gambit Scheme code. + + There is more support code in this file than I would have liked. This is due + to the fact that there is a lot of α-renaming and gensymming so we can't + directly compare s-expressions. Instead, I defined predicates for lists, + strings, known symbols, unknown gensymmed symbols, etc. *) + +open Typerlib + +open Utest_lib + +open Gambit + +let fail_on_exp exp = + Printf.printf "in %s\n" (Scm.string_of_exp exp); + false + +let type_error expected actual = + Printf.printf + "%sExpected %s, but got %s%s\n" + Fmt.red + expected + (Scm.describe actual) + Fmt.reset; + fail_on_exp actual + +let string expected actual = + match actual with + | Scm.String value when String.equal expected value -> true + | Scm.String _ + -> Printf.printf + "%sExpected a string equal to \"%s\"%s\n" + Fmt.red + expected + Fmt.reset; + fail_on_exp actual + | _ -> type_error "a string" actual + +let sym expected actual = + match actual with + | Scm.Symbol value when String.equal expected value -> true + | Scm.Symbol _ + -> Printf.printf + "%sExpected a symbol equal to |%s|%s\n" + Fmt.red + expected + Fmt.reset; + fail_on_exp actual + | _ -> type_error "a symbol" actual + +let has_prefix prefix value = + String.length prefix < String.length value + && String.equal prefix (String.sub value 0 (String.length prefix)) + +type var = Var of string | UniqueVar of string + +let make_var prefix = ref (Var prefix) + +let gensym var actual = + match actual with + | Scm.Symbol value + -> (match !var with + | UniqueVar prev when String.equal value prev -> true + | UniqueVar prev + -> Printf.printf + "%sExpected a symbol equal to |%s|%s\n" + Fmt.red + prev + Fmt.reset; + fail_on_exp actual + | Var prefix when has_prefix (prefix ^ "%") value + -> var := UniqueVar value; + true + | Var prefix + -> Printf.printf + "%sExpected a symbol starting with |%s|%s\n" + Fmt.red + prefix + Fmt.reset; + fail_on_exp actual) + | _ -> type_error "a symbol" actual + +(* Returns whether the s-expression is list and that that the element at an + index satifies the predicate at the same index. *) +let list (expected : (Scm.t -> bool) list) (actual : Scm.t) : bool = + match actual with + | Scm.List value + -> let rec loop i es xs = + match es, xs with + | e :: es, x :: xs + -> if e x + then loop (i + 1) es xs + else fail_on_exp actual + | _ :: _, [] | [], _ :: _ + -> Printf.printf + "%sExpected a list of %d elements, but got %d elements%s\n" + Fmt.red + (List.length expected) + (List.length value) + Fmt.reset; + fail_on_exp actual + | [], [] -> true + in + loop 0 expected value + | _ -> type_error "a list" actual + +let test_compile name source predicate = + let compile () = + let ectx = Elab.default_ectx in + let lctx = Debruijn.ectx_to_lctx ectx in + let lexps = Elab.lexp_expr_str source ectx in + let elexps = List.map (Opslexp.erase_type lctx) lexps in + let sctx = ScmContext.of_lctx lctx in + let actual = List.map (scheme_of_expr sctx) elexps in + match actual with + | head :: [] + -> if predicate head + then success + else failure + | _ + -> Printf.printf "expected 1 expression, but got %d" (List.length actual); + failure + in + Utest_lib.add_test "GAMBIT" name compile + +let () = + test_compile + "Typer string to Scheme string" + {|"Hello"|} + (string "Hello") + +let () = + let var = make_var "x" in + test_compile + "Typer lambda to Scheme lambda" + {|lambda (x : Int) -> x|} + (list [sym "lambda"; list [gensym var]; gensym var]) + +let () = + test_compile + "Typer data cons of 0 arguments to Scheme vector" + {|datacons (typecons T V) V|} + (list [sym "##vector"; list [sym "quote"; sym "V"]]) + +let () = + let var = make_var "" in + test_compile + "Typer data cons of 1 argument to Scheme function" + {|datacons (typecons T (V Int)) V|} + (list [sym "lambda"; + list [gensym var]; + list [sym "##vector"; + list [sym "quote"; sym "V"]; + gensym var]]) + +let () = + let var_0 = make_var "" in + let var_1 = make_var "" in + test_compile + "Typer data cons of 2 arguments to Scheme function" + {|datacons (typecons T (V Int Int)) V|} + (list [sym "lambda"; + list [gensym var_0]; + list [sym "lambda"; + list [gensym var_1]; + list [sym "##vector"; + list [sym "quote"; sym "V"]; + gensym var_0; + gensym var_1]]]) + +let () = Utest_lib.run_all () ===================================== typer.ml ===================================== @@ -21,6 +21,9 @@ open Typerlib +open Backend +open Debruijn + let welcome_msg = " Typer 0.0.0 - Interpreter - (c) 2016-2021 @@ -29,6 +32,7 @@ let welcome_msg = " let arg_batch = ref false +let arg_backend_name = ref "interpreter" let arg_files = ref [] let add_input_file file = @@ -46,6 +50,10 @@ let arg_defs = ("-Vfull-lctx", Arg.Set Debruijn.log_full_lctx, "Print the full lexp context on error."); + + ("--backend", + Arg.Symbol (["interpreter"; "gambit"], fun name -> arg_backend_name := name), + "Select the backend"); ] let main () = @@ -53,7 +61,12 @@ let main () = Arg.parse arg_defs add_input_file usage; let ectx = Elab.default_ectx in - let backend = new Eval.ast_interpreter (Debruijn.ectx_to_lctx ectx) in + let backend = + let lctx = ectx_to_lctx ectx in + match !arg_backend_name with + | "gambit" -> (new Gambit.gambit_compiler lctx stdout :> backend) + | _ -> (new Eval.ast_interpreter lctx :> backend) + in let interactive = backend#interactive in let file_names = List.rev !arg_files in let is_interactive = not !arg_batch && Option.is_some interactive in View it on GitLab: https://gitlab.com/monnier/typer/-/commit/3a38656d67a5df540c392ec9ad4dbea1b… -- View it on GitLab: https://gitlab.com/monnier/typer/-/commit/3a38656d67a5df540c392ec9ad4dbea1b… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][gambit] 4 commits: Merge branch 'dunify-tests'
by Simon Génier (＠ilovemonoids) 07 Apr '21

07 Apr '21

Simon Génier pushed to branch gambit at Stefan / Typer Commits: 6816e0aa by Simon Génier at 2021-04-07T15:35:15-04:00 Merge branch 'dunify-tests' - - - - - ceed8e81 by Simon Génier at 2021-04-07T16:05:34-04:00 Move code related to command-line argument parsing out of REPL. - - - - - 6c849ddf by Simon Génier at 2021-04-07T16:58:02-04:00 Introduce swappable backends for Typer. - - - - - 770e0f69 by Simon Génier at 2021-04-07T17:12:36-04:00 Add a backend to compile Typer to Scheme. - - - - - 12 changed files: - src/REPL.ml - + src/backend.ml - src/elab.ml - src/eval.ml - + src/frontend.ml - + src/gambit.ml - src/lexp.ml - src/listx.ml - src/option.ml - tests/dune - + tests/gambit_test.ml - typer.ml Changes: ===================================== src/REPL.ml ===================================== @@ -36,31 +36,25 @@ this program. If not, see <http://www.gnu.org/licenses/>. *) * * -------------------------------------------------------------------------- *) -open Util +open Backend +open Debruijn +open Eval open Fmt - -open Prelexer open Lexer -open Sexp open Lexp +open Prelexer +open Sexp +open Util -open Eval - -open Grammar - -open Env -open Debruijn module OL = Opslexp module EL = Elexp -let arg_batch = ref false - let print_input_line i = print_string " In["; ralign_print_int i 2; print_string "] >> " -let ieval_error = Log.log_error ~section:"IEVAL" +let error = Log.log_error ~section:"REPL" let print_and_clear_log () = if (not Log.typer_log_config.Log.print_at_log) then @@ -100,91 +94,6 @@ let rec read_input i = 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 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 = 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. *) - 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 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 - (* 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 welcome_msg = -" Typer 0.0.0 - Interpreter - (c) 2016 - - %quit (%q) : leave REPL - %help (%h) : print help -" - let help_msg = " %quit (%q) : leave REPL %who (%w) : print runtime environment @@ -196,134 +105,100 @@ let help_msg = %help (%h) : print help " +(** 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 eval_interactive + (interactive : #interactive_backend) + (i : int) + (ectx : elab_context) + (input : string) + : 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 source = new Source.source_string input 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 readfiles files (i, lctx, rctx) prt = - (* Read specified files *) - List.fold_left (fun (i, lctx, rctx) file -> + let lexprs = Elab.lexp_parse_all exprs ectx' in + List.iter (fun lexpr -> ignore (OL.check (ectx_to_lctx ectx') lexpr)) lexprs; - (if prt then ( - print_string " In["; ralign_print_int i 2; print_string "] >> "; - print_string ("%readfile " ^ file); print_string "\n";)); + List.iter interactive#process_decls ldecls; + print_and_clear_log (); - 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."); - (i, lctx, rctx)) - ) - (i, lctx, rctx) files + let values = List.map interactive#eval_expr lexprs in + List.iter (Eval.print_eval_result i) values; + print_and_clear_log (); + ectx' (* Specials commands %[command-name] [args] *) -let rec repl i clxp rctx = - let repl = repl (i + 1) in +let rec repl i (interactive : #interactive_backend) (ectx : elab_context) = let ipt = try read_input i with End_of_file -> "%quit" in + let ectx = 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)) + | "%quit" | "%q" -> exit 0 + | "%help" | "%h" -> (print_string help_msg; ectx) + | "%calltrace" | "%ct" -> (print_eval_trace None; ectx) + | "%typertrace" | "%tt" -> (print_typer_trace None; ectx) + | "%lcollisions" | "%cl" -> (get_stats_hashtbl (WHC.stats hc_table); ectx) (* 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; + let ectx = List.fold_left (Elab.eval_file interactive) ectx args in + print_and_clear_log (); + ectx | "%who"::args | "%w"::args -> ( let _ = match args with - | ["all"] -> dump_rte_ctx rctx - | _ -> print_rte_ctx rctx in - repl clxp rctx) + | ["all"] -> interactive#dump_rte_ctx + | _ -> interactive#print_rte_ctx in + ectx) | "%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) + | ["all"] -> dump_lexp_ctx (ectx_to_lctx ectx) + | _ -> print_lexp_ctx (ectx_to_lctx ectx) in + ectx) | cmd::_ -> - ieval_error (" \"" ^ cmd ^ "\" is not a correct repl command"); - repl clxp rctx - | _ -> repl clxp rctx) + error (" \"" ^ cmd ^ "\" is not a correct repl command"); + ectx + | _ -> ectx) (* eval input *) | _ -> - 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 + try eval_interactive interactive i ectx ipt with | Log.Stop_Compilation msg -> - (handle_stopped_compilation msg; repl clxp rctx) + (handle_stopped_compilation msg; ectx) | Log.Internal_error msg -> (handle_stopped_compilation ("Internal error: " ^ msg); - repl clxp rctx) + ectx) | 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 + ectx) + in + repl (i + 1) interactive ectx ===================================== src/backend.ml ===================================== @@ -0,0 +1,48 @@ +(* 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. *) + +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 ===================================== src/elab.ml ===================================== @@ -1943,3 +1943,21 @@ let eval_decl_str str ectx rctx = let lctx = ectx_to_lctx ectx in let _, elxps = Listx.fold_left_map (OL.clean_decls) lctx lxps in (EV.eval_decls_toplevel elxps rctx), ectx' + +let eval_file + (backend : #Backend.backend) + (ectx : elab_context) + (file_name : string) + : elab_context = + + try + let source = new Source.source_file file_name in + let pretokens = prelex source in + let tokens = lex Grammar.default_stt pretokens in + let ldecls, ectx' = lexp_p_decls [] tokens ectx in + List.iter backend#process_decls ldecls; + ectx' + with + | Sys_error _ + -> (error (Printf.sprintf {|file %s does not exist.|} file_name); + ectx) ===================================== src/eval.ml ===================================== @@ -1187,3 +1187,23 @@ let from_lctx (lctx: lexp_context): runtime_env = (* build a rctx from a ectx. *) let from_ectx (ctx: elab_context): runtime_env = from_lctx (ectx_to_lctx ctx) + +class ast_interpreter lctx = object + inherit Backend.interactive_backend + + val mutable rctx = from_lctx lctx + val mutable lctx = lctx + + method process_decls ldecls = + let lctx', eldecls = Opslexp.clean_decls lctx ldecls in + rctx <- eval_decls eldecls rctx; + lctx <- lctx' + + method eval_expr lexp = + let elexp = Opslexp.erase_type lctx lexp in + debug_eval elexp rctx + + method print_rte_ctx = Env.print_rte_ctx rctx + + method dump_rte_ctx = Env.dump_rte_ctx rctx +end ===================================== 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,302 @@ +(* 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 + Buffer.add_char buffer '"'; + 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.add_char buffer '"'; + 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' + + let describe (exp : t) : string = + match exp with + | Symbol _ -> "a symbol" + | List _ -> "a list" + | String _ -> "a string" + | Integer _ -> "an integer" + | Float _ -> "a float" + + let rec equal (l : t) (r : t) : bool = + match l, r with + | Symbol l, Symbol r | String l, String r + -> String.equal l r + | List ls, List rs -> Listx.equal equal ls rs + | Integer l, Integer r -> Z.equal l r + | Float l, Float r -> Float.equal l r + | _ -> false +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]) + +class gambit_compiler lctx output = object + inherit Backend.backend + + val mutable sctx = ScmContext.of_lctx lctx + val mutable lctx = lctx + + method process_decls ldecls = + 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 + + sctx <- sctx'; + lctx <- lctx'; + Scm.print output sdecls; +end ===================================== 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/listx.ml ===================================== @@ -44,3 +44,10 @@ let fold_left_map loop fold_acc (new_element :: map_acc) bs in loop i [] bs + +(* Backport from 4.12. *) +let rec equal (p : 'a -> 'a -> bool) (ls : 'a list) (rs : 'a list) : bool = + match ls, rs with + | l :: ls', r :: rs' -> p l r && equal p ls' rs' + | _ :: _, [] | [], _ :: _ -> false + | [], [] -> true ===================================== src/option.ml ===================================== @@ -35,3 +35,8 @@ 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 ===================================== tests/dune ===================================== @@ -4,6 +4,7 @@ (names elab_test env_test eval_test + gambit_test inverse_test lexp_test macro_test ===================================== tests/gambit_test.ml ===================================== @@ -0,0 +1,190 @@ +(* 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/>. *) + +(** Tests for the compilation of Lexps to Gambit Scheme code. + + There is more support code in this file than I would have liked. This is due + to the fact that there is a lot of α-renaming and gensymming so we can't + directly compare s-expressions. Instead, I defined predicates for lists, + strings, known symbols, unknown gensymmed symbols, etc. *) + +open Typerlib + +open Utest_lib + +open Gambit + +let fail_on_exp exp = + Printf.printf "in %s\n" (Scm.string_of_exp exp); + false + +let type_error expected actual = + Printf.printf + "%sExpected %s, but got %s%s\n" + Fmt.red + expected + (Scm.describe actual) + Fmt.reset; + fail_on_exp actual + +let string expected actual = + match actual with + | Scm.String value when String.equal expected value -> true + | Scm.String _ + -> Printf.printf + "%sExpected a string equal to \"%s\"%s\n" + Fmt.red + expected + Fmt.reset; + fail_on_exp actual + | _ -> type_error "a string" actual + +let sym expected actual = + match actual with + | Scm.Symbol value when String.equal expected value -> true + | Scm.Symbol _ + -> Printf.printf + "%sExpected a symbol equal to |%s|%s\n" + Fmt.red + expected + Fmt.reset; + fail_on_exp actual + | _ -> type_error "a symbol" actual + +let has_prefix prefix value = + String.length prefix < String.length value + && String.equal prefix (String.sub value 0 (String.length prefix)) + +type var = Var of string | UniqueVar of string + +let make_var prefix = ref (Var prefix) + +let gensym var actual = + match actual with + | Scm.Symbol value + -> (match !var with + | UniqueVar prev when String.equal value prev -> true + | UniqueVar prev + -> Printf.printf + "%sExpected a symbol equal to |%s|%s\n" + Fmt.red + prev + Fmt.reset; + fail_on_exp actual + | Var prefix when has_prefix (prefix ^ "%") value + -> var := UniqueVar value; + true + | Var prefix + -> Printf.printf + "%sExpected a symbol starting with |%s|%s\n" + Fmt.red + prefix + Fmt.reset; + fail_on_exp actual) + | _ -> type_error "a symbol" actual + +(* Returns whether the s-expression is list and that that the element at an + index satifies the predicate at the same index. *) +let list (expected : (Scm.t -> bool) list) (actual : Scm.t) : bool = + match actual with + | Scm.List value + -> let rec loop i es xs = + match es, xs with + | e :: es, x :: xs + -> if e x + then loop (i + 1) es xs + else fail_on_exp actual + | _ :: _, [] | [], _ :: _ + -> Printf.printf + "%sExpected a list of %d elements, but got %d elements%s\n" + Fmt.red + (List.length expected) + (List.length value) + Fmt.reset; + fail_on_exp actual + | [], [] -> true + in + loop 0 expected value + | _ -> type_error "a list" actual + +let test_compile name source predicate = + let compile () = + let ectx = Elab.default_ectx in + let lctx = Debruijn.ectx_to_lctx ectx in + let lexps = Elab.lexp_expr_str source ectx in + let elexps = List.map (Opslexp.erase_type lctx) lexps in + let sctx = ScmContext.of_lctx lctx in + let actual = List.map (scheme_of_expr sctx) elexps in + match actual with + | head :: [] + -> if predicate head + then success + else failure + | _ + -> Printf.printf "expected 1 expression, but got %d" (List.length actual); + failure + in + Utest_lib.add_test "GAMBIT" name compile + +let () = + test_compile + "Typer string to Scheme string" + {|"Hello"|} + (string "Hello") + +let () = + let var = make_var "x" in + test_compile + "Typer lambda to Scheme lambda" + {|lambda (x : Int) -> x|} + (list [sym "lambda"; list [gensym var]; gensym var]) + +let () = + test_compile + "Typer data cons of 0 arguments to Scheme vector" + {|datacons (typecons T V) V|} + (list [sym "##vector"; list [sym "quote"; sym "V"]]) + +let () = + let var = make_var "" in + test_compile + "Typer data cons of 1 argument to Scheme function" + {|datacons (typecons T (V Int)) V|} + (list [sym "lambda"; + list [gensym var]; + list [sym "##vector"; + list [sym "quote"; sym "V"]; + gensym var]]) + +let () = + let var_0 = make_var "" in + let var_1 = make_var "" in + test_compile + "Typer data cons of 2 arguments to Scheme function" + {|datacons (typecons T (V Int Int)) V|} + (list [sym "lambda"; + list [gensym var_0]; + list [sym "lambda"; + list [gensym var_1]; + list [sym "##vector"; + list [sym "quote"; sym "V"]; + gensym var_0; + gensym var_1]]]) + +let () = Utest_lib.run_all () ===================================== typer.ml ===================================== @@ -17,4 +17,98 @@ * You should have received a copy of the GNU General Public License along with * this program. If not, see <http://www.gnu.org/licenses/>. *) -let () = Typerlib.REPL.main () +(** This file is the the entry point to the typer REPL. *) + +open Typerlib + +open Backend +open Debruijn + +let welcome_msg = +" Typer 0.0.0 - Interpreter - (c) 2016-2021 + + %quit (%q) : leave REPL + %help (%h) : print help +" + +let arg_batch = ref false +let arg_backend_name = ref "interpreter" + +let arg_files = ref [] +let add_input_file file = + arg_files := file :: !arg_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."); + + ("--backend", + Arg.Symbol (["interpreter"; "gambit"], fun name -> arg_backend_name := name), + "Select the backend"); + ] + +let main () = + let usage = Sys.executable_name ^ " [options] <file1> [<file2>] …" in + Arg.parse arg_defs add_input_file usage; + + let ectx = Elab.default_ectx in + let backend = + let lctx = ectx_to_lctx ectx in + match !arg_backend_name with + | "gambit" -> (new Gambit.gambit_compiler lctx stdout :> backend) + | _ -> (new Eval.ast_interpreter lctx :> backend) + in + let interactive = backend#interactive in + let file_names = List.rev !arg_files in + let is_interactive = not !arg_batch && Option.is_some interactive in + + let process_file = + if is_interactive + then + (print_string (Fmt.make_title " TYPER REPL "); + print_string welcome_msg; + print_string (Fmt.make_sep '-'); + flush stdout; + fun ectx i file_name + -> Printf.printf " In[%02d] >> %%readfile %s\n" i file_name; + Elab.eval_file backend ectx file_name) + else + fun ectx _ file_name -> Elab.eval_file backend ectx file_name + in + + let ectx, i = + try + let res = + List.fold_left + (fun (ectx, i) file_name -> (process_file ectx i file_name, i + 1)) + (ectx, 0) + file_names + in + REPL.print_and_clear_log (); + res + 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_interactive, interactive with + | true, Some (interactive) -> REPL.repl i interactive ectx + | _ -> () + +let () = main () View it on GitLab: https://gitlab.com/monnier/typer/-/compare/4aaaf9258e80093455f5db33d3d86582… -- View it on GitLab: https://gitlab.com/monnier/typer/-/compare/4aaaf9258e80093455f5db33d3d86582… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][backend-object] Introduce swappable backends for Typer.
by Simon Génier (＠ilovemonoids) 07 Apr '21

07 Apr '21

Simon Génier pushed to branch backend-object at Stefan / Typer Commits: 6c849ddf by Simon Génier at 2021-04-07T16:58:02-04:00 Introduce swappable backends for Typer. - - - - - 8 changed files: - src/REPL.ml - + src/backend.ml - src/elab.ml - src/eval.ml - src/lexp.ml - src/listx.ml - src/option.ml - typer.ml Changes: ===================================== src/REPL.ml ===================================== @@ -36,20 +36,16 @@ this program. If not, see <http://www.gnu.org/licenses/>. *) * * -------------------------------------------------------------------------- *) -open Util +open Backend +open Debruijn +open Eval open Fmt - -open Prelexer open Lexer -open Sexp open Lexp +open Prelexer +open Sexp +open Util -open Eval - -open Grammar - -open Env -open Debruijn module OL = Opslexp module EL = Elexp @@ -58,7 +54,7 @@ let print_input_line i = ralign_print_int i 2; print_string "] >> " -let ieval_error = Log.log_error ~section:"IEVAL" +let error = Log.log_error ~section:"REPL" let print_and_clear_log () = if (not Log.typer_log_config.Log.print_at_log) then @@ -98,84 +94,6 @@ let rec read_input i = 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 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 = 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. *) - 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 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 - (* 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 help_msg = " %quit (%q) : leave REPL %who (%w) : print runtime environment @@ -187,80 +105,100 @@ let help_msg = %help (%h) : print help " +(** 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 eval_interactive + (interactive : #interactive_backend) + (i : int) + (ectx : elab_context) + (input : string) + : 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 source = new Source.source_string input 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 readfiles files (i, lctx, rctx) prt = - (* Read specified files *) - List.fold_left (fun (i, lctx, rctx) file -> + let lexprs = Elab.lexp_parse_all exprs ectx' in + List.iter (fun lexpr -> ignore (OL.check (ectx_to_lctx ectx') lexpr)) lexprs; - (if prt then ( - print_string " In["; ralign_print_int i 2; print_string "] >> "; - print_string ("%readfile " ^ file); print_string "\n";)); + List.iter interactive#process_decls ldecls; + print_and_clear_log (); - 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."); - (i, lctx, rctx)) - ) - (i, lctx, rctx) files + let values = List.map interactive#eval_expr lexprs in + List.iter (Eval.print_eval_result i) values; + print_and_clear_log (); + ectx' (* Specials commands %[command-name] [args] *) -let rec repl i clxp rctx = - let repl = repl (i + 1) in +let rec repl i (interactive : #interactive_backend) (ectx : elab_context) = let ipt = try read_input i with End_of_file -> "%quit" in + let ectx = 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)) + | "%quit" | "%q" -> exit 0 + | "%help" | "%h" -> (print_string help_msg; ectx) + | "%calltrace" | "%ct" -> (print_eval_trace None; ectx) + | "%typertrace" | "%tt" -> (print_typer_trace None; ectx) + | "%lcollisions" | "%cl" -> (get_stats_hashtbl (WHC.stats hc_table); ectx) (* 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; + let ectx = List.fold_left (Elab.eval_file interactive) ectx args in + print_and_clear_log (); + ectx | "%who"::args | "%w"::args -> ( let _ = match args with - | ["all"] -> dump_rte_ctx rctx - | _ -> print_rte_ctx rctx in - repl clxp rctx) + | ["all"] -> interactive#dump_rte_ctx + | _ -> interactive#print_rte_ctx in + ectx) | "%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) + | ["all"] -> dump_lexp_ctx (ectx_to_lctx ectx) + | _ -> print_lexp_ctx (ectx_to_lctx ectx) in + ectx) | cmd::_ -> - ieval_error (" \"" ^ cmd ^ "\" is not a correct repl command"); - repl clxp rctx - | _ -> repl clxp rctx) + error (" \"" ^ cmd ^ "\" is not a correct repl command"); + ectx + | _ -> ectx) (* eval input *) | _ -> - 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 + try eval_interactive interactive i ectx ipt with | Log.Stop_Compilation msg -> - (handle_stopped_compilation msg; repl clxp rctx) + (handle_stopped_compilation msg; ectx) | Log.Internal_error msg -> (handle_stopped_compilation ("Internal error: " ^ msg); - repl clxp rctx) + ectx) | Log.User_error msg -> (handle_stopped_compilation ("Fatal user error: " ^ msg); - repl clxp rctx) + ectx) + in + repl (i + 1) interactive ectx ===================================== src/backend.ml ===================================== @@ -0,0 +1,48 @@ +(* 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. *) + +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 ===================================== src/elab.ml ===================================== @@ -1943,3 +1943,21 @@ let eval_decl_str str ectx rctx = let lctx = ectx_to_lctx ectx in let _, elxps = Listx.fold_left_map (OL.clean_decls) lctx lxps in (EV.eval_decls_toplevel elxps rctx), ectx' + +let eval_file + (backend : #Backend.backend) + (ectx : elab_context) + (file_name : string) + : elab_context = + + try + let source = new Source.source_file file_name in + let pretokens = prelex source in + let tokens = lex Grammar.default_stt pretokens in + let ldecls, ectx' = lexp_p_decls [] tokens ectx in + List.iter backend#process_decls ldecls; + ectx' + with + | Sys_error _ + -> (error (Printf.sprintf {|file %s does not exist.|} file_name); + ectx) ===================================== src/eval.ml ===================================== @@ -1187,3 +1187,23 @@ let from_lctx (lctx: lexp_context): runtime_env = (* build a rctx from a ectx. *) let from_ectx (ctx: elab_context): runtime_env = from_lctx (ectx_to_lctx ctx) + +class ast_interpreter lctx = object + inherit Backend.interactive_backend + + val mutable rctx = from_lctx lctx + val mutable lctx = lctx + + method process_decls ldecls = + let lctx', eldecls = Opslexp.clean_decls lctx ldecls in + rctx <- eval_decls eldecls rctx; + lctx <- lctx' + + method eval_expr lexp = + let elexp = Opslexp.erase_type lctx lexp in + debug_eval elexp rctx + + method print_rte_ctx = Env.print_rte_ctx rctx + + method dump_rte_ctx = Env.dump_rte_ctx rctx +end ===================================== 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/listx.ml ===================================== @@ -44,3 +44,10 @@ let fold_left_map loop fold_acc (new_element :: map_acc) bs in loop i [] bs + +(* Backport from 4.12. *) +let rec equal (p : 'a -> 'a -> bool) (ls : 'a list) (rs : 'a list) : bool = + match ls, rs with + | l :: ls', r :: rs' -> p l r && equal p ls' rs' + | _ :: _, [] | [], _ :: _ -> false + | [], [] -> true ===================================== src/option.ml ===================================== @@ -35,3 +35,8 @@ 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 ===================================== typer.ml ===================================== @@ -51,22 +51,34 @@ let arg_defs = let main () = let usage = Sys.executable_name ^ " [options] <file1> [<file2>] …" in Arg.parse arg_defs add_input_file usage; - let files = List.rev !arg_files in - let is_interactive = not !arg_batch in - if is_interactive - then - (print_string (Fmt.make_title " TYPER REPL "); - print_string welcome_msg; - print_string (Fmt.make_sep '-'); - flush stdout); + let ectx = Elab.default_ectx in + let backend = new Eval.ast_interpreter (Debruijn.ectx_to_lctx ectx) in + let interactive = backend#interactive in + let file_names = List.rev !arg_files in + let is_interactive = not !arg_batch && Option.is_some interactive in - let i, ectx, rctx = + let process_file = + if is_interactive + then + (print_string (Fmt.make_title " TYPER REPL "); + print_string welcome_msg; + print_string (Fmt.make_sep '-'); + flush stdout; + fun ectx i file_name + -> Printf.printf " In[%02d] >> %%readfile %s\n" i file_name; + Elab.eval_file backend ectx file_name) + else + fun ectx _ file_name -> Elab.eval_file backend ectx file_name + in + + let ectx, i = try - let ectx = Elab.default_ectx in - let rctx = Elab.default_rctx in let res = - REPL.readfiles files (1, ectx, rctx) is_interactive + List.fold_left + (fun (ectx, i) file_name -> (process_file ectx i file_name, i + 1)) + (ectx, 0) + file_names in REPL.print_and_clear_log (); res @@ -82,7 +94,8 @@ let main () = exit 1 in - if is_interactive - then REPL.repl i ectx rctx + match is_interactive, interactive with + | true, Some (interactive) -> REPL.repl i interactive ectx + | _ -> () let () = main () View it on GitLab: https://gitlab.com/monnier/typer/-/commit/6c849ddf758619d4ef5bbc45c70a89732… -- View it on GitLab: https://gitlab.com/monnier/typer/-/commit/6c849ddf758619d4ef5bbc45c70a89732… You're receiving this email because of your account on gitlab.com.

1 0