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 [] ## 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@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@iro.umontreal.ca Keywords: languages, lisp, dependent types. @@ -50,114 +50,135 @@ let inc_cp (cp:charpos) (c:char) = (* Count char positions in utf-8: don't count the non-leading bytes. *) if utf8_head_p c then cp+1 else cp
-let rec prelex (file : string) (getline : unit -> string) ln ctx acc (doc : string) +let rec consume_until_newline (source : #Source.t) : unit = + match source#next_char with + | None | Some ('\n') -> () + | Some _ -> consume_until_newline source + +let rec prelex (source : #Source.t) ln ctx acc (doc : string) : pretoken list = - try - (* let fin = open_in file in *) - let line = getline () in - let limit = String.length line in - let nextline = prelex file getline (ln + 1) in - let rec prelex' ctx (bpos:bytepos) (cpos:charpos) acc doc = - let nexttok = prelex' ctx in - if bpos >= limit then nextline ctx acc doc else - match line.[bpos] with - | c when c <= ' ' -> nexttok (bpos+1) (cpos+1) acc doc - | '%' -> nextline ctx acc doc (* A comment. *) - (* line's bounds seems ok: String.sub line 1 0 == "" *) - | '@' -> nextline ctx acc (String.concat "\n" [doc; (String.sub line 1 (limit - 1))]) - | '"' (* A string. *) - -> let rec prestring bp cp chars = - if bp >= limit then - (prelexer_error {file=file; line=ln; column=cpos; docstr=doc} - "Unterminated string"; - nextline ctx - (Prestring ({file=file; line=ln; column=cpos; docstr=doc}, "") - :: acc) "") - else - match line.[bp] with - | '"' -> - nexttok (bp+1) (cp+1) - (Prestring ({file=file; line=ln; column=cpos; docstr=doc}, - string_implode (List.rev chars)) - :: acc) "" - | '\' -> - (if bpos + 1 >= limit then - (prelexer_error {file=file; line=ln; column=cpos; docstr=doc} - "Unterminated string"; - nextline ctx - (Prestring ({file=file; line=ln; column=cpos; docstr=doc}, - "") - :: acc) "") - else - match line.[bp + 1] with - | 't' -> prestring (bp+2) (cp+2) ('\t' :: chars) - | 'n' -> prestring (bp+2) (cp+2) ('\n' :: chars) - | 'r' -> prestring (bp+2) (cp+2) ('\r' :: chars) - | ('u' | 'U') -> - prelexer_error {file=file; line=ln; column=cp; docstr=doc} - "Unimplemented unicode escape"; - prestring (bp+2) (cp+2) chars - | char -> prestring (bp+2) (cp+2) (char :: chars)) - | char -> prestring (bp+1) (inc_cp cp char) (char :: chars) - in prestring (bpos+1) (cpos+1) [] - | '{' -> prelex' ((ln, cpos, bpos, acc) :: ctx) (bpos+1) (cpos+1) [] doc - | '}' - -> (match ctx with - | ((sln, scpos, _sbpos, sacc) :: ctx) -> - prelex' ctx (bpos+1) (cpos+1) - (Preblock ({file=file; line=sln; column=scpos; docstr=doc}, - List.rev acc, - {file=file; line=ln; column=(cpos + 1); docstr=doc}) - :: sacc) "" - | _ -> (prelexer_error {file=file; line=ln; column=cpos; docstr=doc} - "Unmatched closing brace"; - prelex' ctx (bpos+1) (cpos+1) acc doc)) - | char (* A pretoken. *) - -> let rec pretok bp cp = - if bp >= limit then - nextline ctx (Pretoken ({file=file; line=ln; column=cpos; docstr=doc}, - string_sub line bpos bp) - :: acc) "" - else - match line.[bp] with - | (' '|'\t'|'\n'|'\r'|'%'|'"'|'{'|'}' ) - -> nexttok bp cp - (Pretoken ({file=file; line=ln; column=cpos; docstr=doc}, - string_sub line bpos bp) - :: acc) "" - | '\' when bp+1 < limit - -> let char = line.[bp + 1] in - pretok (bp + 2) (1 + inc_cp cp char) - | char -> pretok (bp+1) (inc_cp cp char) - in pretok (bpos+1) (inc_cp cpos char) - in prelex' ctx 0 1 acc doc (* Traditionally, column numbers start at 1 :-( *) - with End_of_file -> - match ctx with + + let nextline = prelex source (ln + 1) in + let rec prelex' ctx (cpos:charpos) acc doc = + let nexttok = prelex' ctx in + match source#peek_char with + | None + -> (match ctx with | [] -> List.rev acc - | ((ln, cpos, _, _) :: _ctx) -> - (prelexer_error {file=file; line=ln; column=cpos; docstr=""} - "Unmatched opening brace"; List.rev acc) - - -let prelex_file file = - let fin = open_in file - in prelex file (fun _ -> input_line fin) - (* Traditionally, line numbers start at 1 :-( *) - 1 [] [] "" - -let prelex_string str = - let pos = ref 0 in - let getline () = - let start = !pos in - if start >= String.length str then raise End_of_file else - let i = try String.index_from str start '\n' - with Not_found -> String.length str - 1 in - let npos = i + 1 in - pos := npos; - let line = string_sub str start npos in - (* print_string ("Read line: " ^ line); *) - line - in prelex "<string>" getline 1 [] [] "" + | ((ln, cpos, _) :: _ctx) -> + (prelexer_error {file=source#file_name; line=ln; column=cpos; docstr=""} + "Unmatched opening brace"; List.rev acc)) + + | Some ('\n') + -> source#advance; + nextline ctx acc doc + + | Some (c) when c <= ' ' + -> source#advance; + nexttok (cpos+1) acc doc + + (* A comment. *) + | Some ('%') + -> consume_until_newline source; + nextline ctx acc doc + + (* line's bounds seems ok: String.sub line 1 0 == "" *) + | Some ('@') + -> source#advance; + let start_offset = source#current_offset in + consume_until_newline source; + let new_doc = String.trim (source#slice_from_offset start_offset) in + nextline ctx acc (doc ^ "\n" ^ new_doc) + + (* A string. *) + | Some ('"') + -> source#advance; + let rec prestring cp chars = + match source#next_char with + | None | Some ('\n') + -> let location = {file=source#file_name; line=ln; column=cpos; docstr=doc} in + prelexer_error location "Unterminated string"; + nextline ctx (Prestring (location, "") :: acc) "" + + | Some ('"') + -> let location = {file=source#file_name; line=ln; column=cpos; docstr=doc} in + let pretoken = Prestring (location, string_implode (List.rev chars)) in + nexttok (cp + 1) (pretoken :: acc) "" + + | Some ('\') + -> (match source#next_char with + | None | Some ('\n') + -> let location = {file=source#file_name; line=ln; column=cp; docstr=doc} in + prelexer_error location "Unterminated escape sequence"; + nextline ctx (Prestring (location, "") :: acc) "" + | Some ('t') -> prestring (cp + 2) ('\t' :: chars) + | Some ('n') -> prestring (cp + 2) ('\n' :: chars) + | Some ('r') -> prestring (cp + 2) ('\r' :: chars) + | Some ('u') + -> let location = {file=source#file_name; line=ln; column=cp; docstr=doc} in + prelexer_error location "Unimplemented unicode escape"; + prestring (cp + 2) chars + | Some (c) -> prestring (cp + 2) (c :: chars)) + + | Some (char) -> prestring (inc_cp cp char) (char :: chars) + in prestring (cpos + 1) [] + + | Some ('{') + -> source#advance; + prelex' ((ln, cpos, acc) :: ctx) (cpos + 1) [] doc + + | Some ('}') + -> source#advance; + (match ctx with + | ((sln, scpos, sacc) :: ctx) -> + prelex' ctx (cpos+1) + (Preblock ({file=source#file_name; line=sln; column=scpos; docstr=doc}, + List.rev acc, + {file=source#file_name; line=ln; column=(cpos + 1); docstr=doc}) + :: sacc) "" + | _ -> (prelexer_error {file=source#file_name; line=ln; column=cpos; docstr=doc} + "Unmatched closing brace"; + prelex' ctx (cpos + 1) acc doc)) + + (* A pretoken. *) + | Some (c) + -> let start_offset = source#current_offset in + source#advance; + let rec pretok cp = + match source#peek_char with + | None | Some (' ' | '\t' | '%' | '"' | '{' | '}') + -> let location = {file=source#file_name; line=ln; column=cpos; docstr=doc} in + let text = source#slice_from_offset start_offset in + nexttok cp (Pretoken (location, text) :: acc) "" + + | Some ('\n') + -> let location = {file=source#file_name; line=ln; column=cpos; docstr=doc} in + let text = source#slice_from_offset start_offset in + source#advance; + nextline ctx (Pretoken (location, text) :: acc) "" + + | Some ('\') + -> source#advance; + (match source#next_char with + | Some (char) -> pretok (1 + inc_cp cp char) + | None + -> let location = {file=source#file_name; line=ln; column=cpos; docstr=doc} in + source#advance; + let text = source#slice_from_offset start_offset in + prelexer_error location ("Unterminated escape sequence in: " ^ text); + nexttok (cp + 1) (Pretoken (location, text) :: acc) "") + + | Some (c) + -> source#advance; + pretok (inc_cp cp c) + in pretok (inc_cp cpos c) + in + (* Traditionally, column numbers start at 1 :-( *) + prelex' ctx 1 acc doc + +let prelex (source : #Source.t) : pretoken list = + (* Traditionally, line numbers start at 1 :-( *) + prelex source 1 [] [] ""
let pretoken_name pretok = match pretok with
===================================== src/source.ml ===================================== @@ -0,0 +1,113 @@ +(* Copyright (C) 2021 Free Software Foundation, Inc. + * + * Author: Simon Génier simon.genier@umontreal.ca + * Keywords: languages, lisp, dependent types. + * + * This file is part of Typer. + * + * Typer is free software; you can redistribute it and/or modify it under the + * terms of the GNU General Public License as published by the Free Software + * Foundation, either version 3 of the License, or (at your option) any later + * version. + * + * Typer is distributed in the hope that it will be useful, but WITHOUT ANY + * WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS + * FOR A PARTICULAR PURPOSE. See the GNU General Public License for more + * details. + * + * You should have received a copy of the GNU General Public License along + * with this program. If not, see http://www.gnu.org/licenses/. *) + +type location = Util.location + +(* A source object is text paired with a cursor. The text can be lazily loaded + as it is accessed byte by byte, but it must be retained for future reference + by error messages. *) +class virtual t = object (self) + (* A path if the text comes from a file, otherwise a meaningful identifier. *) + method virtual file_name : string + + (* Return the byte at the cursor, or None if the cursor is at the end of + the text. *) + method virtual peek_char : char option + + (* The current offset of the cursor in the file, in bytes. *) + method virtual current_offset : int + + (* Slices the text, from (and including) a starting offset and to (and + excluding) the curent cursor offset. + + Note that the source is required only to buffer the last line read and may + raise an Invalid_argument if the slice extends before the start of the + line. *) + method virtual slice_from_offset : int -> string + + (* Moves the cursor forward one byte *) + method virtual advance : unit + + method next_char : char option = + let c = self#peek_char in + self#advance; + c +end + +let read_buffer_length = 4096 + +class source_file file_name = object (self) + inherit t + + val in_channel = open_in file_name + val mutable end_of_line = false + val mutable line = "" + val mutable line_offset = 0 + val mutable offset = 0 + + method private peek_char_unchecked = + if offset < String.length line + then line.[offset] + else '\n' + + method peek_char = + if offset <= String.length line + then Some self#peek_char_unchecked + else + try + line_offset <- line_offset + 1 + String.length line; + line <- input_line in_channel; + offset <- 0; + Some self#peek_char_unchecked + with + | End_of_file -> None + + method advance = + offset <- offset + 1 + + method current_offset = line_offset + offset + + method slice_from_offset start_offset = + let relative_start_offset = start_offset - line_offset in + String.sub line relative_start_offset (offset - relative_start_offset) + + method file_name = file_name +end + +class source_string source = object + inherit t + + val mutable offset = 0 + + method peek_char = + if offset < String.length source + then Some (source.[offset]) + else None + + method advance = + offset <- offset + 1 + + method current_offset = offset + + method slice_from_offset start_offset = + String.sub source start_offset (offset - start_offset) + + method file_name = "<string>" +end
===================================== 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@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@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/7abb48c554174b01d898ea7039b2e4c1b...
Afficher les réponses par date