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

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

07 Apr '21

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

1 0

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

07 Apr '21

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

1 0

[Git][monnier/typer] Deleted branch main-module
by Simon Génier (＠ilovemonoids) 07 Apr '21

07 Apr '21

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

1 0

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

07 Apr '21

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

1 0

[Git][monnier/typer][master] 2 commits: Dunify Typer tests.
by Simon Génier (＠ilovemonoids) 07 Apr '21

07 Apr '21

Simon Génier pushed to branch master at Stefan / Typer Commits: 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' - - - - - 21 changed files: - .gitignore - GNUmakefile - README.md - + btl/dune - src/debug_util.ml → debug_util.ml - + dune - src/REPL.ml - src/dune - src/option.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)) ===================================== src/REPL.ml ===================================== @@ -327,6 +327,3 @@ let main () = if not !arg_batch then (* Initiate REPL. This will allow us to inspect interpreted code *) repl i ectx rctx - - -let _ = main () ===================================== src/dune ===================================== @@ -1,6 +1,5 @@ ;; -*- lisp-data -*- -(executable - (name REPL) - ;; (public_name typer) - (libraries "zarith" "str") - ) + +(library + (name typerlib) + (libraries zarith str)) ===================================== 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 ===================================== 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 *) @@ -258,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 @@ -270,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 @@ -459,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,20 @@ +(* 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/>. *) + +let () = Typerlib.REPL.main () View it on GitLab: https://gitlab.com/monnier/typer/-/compare/0e3dcf791673ecd47fc87ca101ce3798… -- View it on GitLab: https://gitlab.com/monnier/typer/-/compare/0e3dcf791673ecd47fc87ca101ce3798… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][gambit] [Gambit] Add tests.
by Simon Génier (＠ilovemonoids) 06 Apr '21

06 Apr '21

Simon Génier pushed to branch gambit at Stefan / Typer Commits: 4aaaf925 by Simon Génier at 2021-04-06T14:13:27-04:00 [Gambit] Add tests. - - - - - 4 changed files: - src/gambit.ml - src/listx.ml - tests/dune - + tests/gambit_test.ml Changes: ===================================== src/gambit.ml ===================================== @@ -82,6 +82,7 @@ module Scm = struct | 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"; @@ -94,6 +95,7 @@ module Scm = struct | 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 @@ -101,6 +103,23 @@ module Scm = struct 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 = ===================================== 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 ===================================== 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 () View it on GitLab: https://gitlab.com/monnier/typer/-/commit/4aaaf9258e80093455f5db33d3d865821… -- View it on GitLab: https://gitlab.com/monnier/typer/-/commit/4aaaf9258e80093455f5db33d3d865821… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][gambit] 8 commits: Merge branch 'source-object'
by Simon Génier (＠ilovemonoids) 06 Apr '21

06 Apr '21

Simon Génier pushed to branch gambit at Stefan / Typer Commits: 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. - - - - - 1337e474 by Simon Génier at 2021-04-05T14:56:38-04:00 Add a backend to compile Typer to Scheme. - - - - - c49b0498 by Simon Génier at 2021-04-05T15:20:10-04:00 Backends maintain their lctx as mutable attributes. - - - - - 52145545 by Simon Génier at 2021-04-06T14:09:54-04:00 [Gambit] Add tests. - - - - - 28 changed files: - .gitignore - GNUmakefile - README.md - + btl/dune - src/debug_util.ml → debug_util.ml - + dune - src/REPL.ml - + src/backend.ml - src/dune - src/eval.ml - + src/frontend.ml - + src/gambit.ml - src/lexp.ml - src/listx.ml - src/option.ml - + tests/dune - tests/elab_test.ml - tests/env_test.ml - tests/eval_test.ml - + tests/gambit_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,10 +278,12 @@ 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 + let rctx = Eval.from_ectx Elab.default_ectx in print_string yellow; let rctx = (try eval_decls_toplevel clean_lxp rctx; with e -> ===================================== 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)) ===================================== src/REPL.ml ===================================== @@ -36,297 +36,171 @@ this program. If not, see <http://www.gnu.org/licenses/>. *) * * -------------------------------------------------------------------------- *) -open Util -open Fmt - -open Prelexer -open Lexer -open Sexp -open Lexp +open Printf +open Backend +open Debruijn open Eval +open Lexp -open Grammar +let error = Log.log_error ~section:"REPL" -open Env -open Debruijn -module OL = Opslexp -module EL = Elexp +let print_and_clear_log () = + Log.print_and_clear_log (); + flush stdout -let arg_batch = ref false +let handle_stopped_compilation msg = + Log.print_and_clear_log (); + print_endline msg; + flush stdout let print_input_line i = - print_string " In["; - ralign_print_int i 2; - print_string "] >> " - -let ieval_error = Log.log_error ~section:"IEVAL" + printf " In[%02d] >> " i -let print_and_clear_log () = - if (not Log.typer_log_config.Log.print_at_log) then - Log.print_and_clear_log () +(* Read stdin for input. -let handle_stopped_compilation msg = - print_and_clear_log (); - print_string msg; print_newline (); - flush stdout - -(* Read stdin for input. Returns only when the last char is ';' - * We can use '%' to prevent parsing - * If return is pressed and the last char is not ';' then - * indentation will be added *) + Returns only when the last char is ';'. We can use '%' to prevent parsing. If + return is pressed and the last char is not ';' then indentation will be + added. *) let rec read_input i = - print_input_line i; - flush stdout; + print_input_line i; + flush stdout; - let rec loop str i = - flush stdout; - let line = input_line stdin in - let s = String.length str in - let n = String.length line in - if s = 0 && n = 0 then read_input i else - (if n = 0 then ( - print_string " . "; - print_string (make_line ' ' (i * 4)); - loop str (i + 1)) - else - let str = if s > 0 then String.concat "\n" [str; line] else line in - if line.[n - 1] = ';' || line.[0] = '%' then - str - else ( - print_string " . "; - print_string (make_line ' ' (i * 4)); - loop str (i + 1))) in - - loop "" i - -(* Interactive mode is not usual typer - It makes things easier to test out code *) -type lexpr = lexp - -(* Grouping declaration together will enable us to support mutually recursive - * declarations while bringing us closer to normal typer *) -let ipexp_parse (sxps: sexp list): (sexp list * sexp list) = - let rec pxp_parse sxps dacc pacc = - match sxps with - | [] -> (List.rev dacc), (List.rev pacc) - | sxp::tl -> match sxp with - (* Declaration *) - | Node (Symbol (_, ("_=_" | "_:_")), [Symbol _s; _t]) -> - pxp_parse tl (sxp :: dacc) pacc - - (* f arg1 arg2 = function body; *) - | Node (Symbol (_, "_=_"), [Node (Symbol _s, _args); _t]) -> - pxp_parse tl (sxp :: dacc) pacc - - (* Expression *) - | _ -> pxp_parse tl dacc (sxp::pacc) in - pxp_parse sxps [] [] - - -let ierase_type - (lctx : DB.lexp_context) - (ldecls, lexprs : ldecl list list * lexpr list) - : (vname * EL.elexp) list list * EL.elexp list = - - let lctx', eldecls = Listx.fold_left_map OL.clean_decls lctx ldecls in - let elexprs = List.map (OL.erase_type lctx') lexprs in - eldecls, elexprs - -let ilexp_parse pexps lctx: ((ldecl list list * lexpr list) * elab_context) = - let pdecls, pexprs = pexps in - (* FIXME We take the parsed input here but we should take the - unparsed tokens directly instead *) - let ldecls, lctx = Elab.lexp_p_decls pdecls [] lctx in - let lexprs = Elab.lexp_parse_all pexprs lctx in - List.iter (fun lxp -> ignore (OL.check (ectx_to_lctx lctx) lxp)) - lexprs; - (ldecls, lexprs), lctx - -let ieval 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 = + let rec loop str i = + flush stdout; + let line = input_line stdin in + let s = String.length str in + let n = String.length line in + if s = 0 && n = 0 then read_input i else + (if n = 0 then ( + print_string " . "; + print_string (String.make (i * 4) ' '); + loop str (i + 1)) + else + let str = if s > 0 then String.concat "\n" [str; line] else line in + if line.[n - 1] = ';' || line.[0] = '%' then + str + else ( + print_string " . "; + print_string (String.make (i * 4) ' '); + loop str (i + 1))) in + + loop "" i + +let help_message = " %quit (%q) : leave REPL %who (%w) : print runtime environment %info (%i) : print elaboration environment %calltrace (%ct): print eval trace of last call - %elabtrace (%et): print elaboration trace %typertrace (%tt): print typer trace %readfile : read a Typer file %help (%h) : print help " - -let readfiles files (i, lctx, rctx) prt = - (* Read specified files *) - List.fold_left (fun (i, lctx, rctx) file -> - - (if prt then ( - print_string " In["; ralign_print_int i 2; print_string "] >> "; - print_string ("%readfile " ^ file); print_string "\n";)); - - try - let 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 - - -(* Specials commands %[command-name] [args] *) -let rec repl i clxp rctx = - let repl = repl (i + 1) in - let ipt = try read_input i with End_of_file -> "%quit" in - match ipt with - (* Check special keywords *) - | "%quit" | "%q" -> () - | "%help" | "%h" -> (print_string help_msg; repl clxp rctx) - | "%calltrace" | "%ct" -> (print_eval_trace None; repl clxp rctx) - | "%typertrace" | "%tt" -> (print_typer_trace None; repl clxp rctx) - | "%lcollisions" | "%cl" -> (get_stats_hashtbl (WHC.stats hc_table)) - - (* command with arguments *) - | _ when (ipt.[0] = '%' && ipt.[1] != ' ') -> ( - match (str_split ipt ' ') with - | "%readfile"::args -> - let (_i, clxp, rctx) = - try - readfiles args (i, clxp, rctx) false - with Log.Stop_Compilation msg -> - (handle_stopped_compilation msg; (i,clxp,rctx)) - in - repl clxp rctx; - | "%who"::args | "%w"::args -> ( - let _ = match args with - | ["all"] -> dump_rte_ctx rctx - | _ -> print_rte_ctx rctx in - repl clxp rctx) - | "%info"::args | "%i"::args -> ( - let _ = match args with - | ["all"] -> dump_lexp_ctx (ectx_to_lctx clxp) - | _ -> print_lexp_ctx (ectx_to_lctx clxp) in - repl clxp rctx) - - | cmd::_ -> - ieval_error (" \"" ^ cmd ^ "\" is not a correct repl command"); - repl clxp rctx - | _ -> repl clxp rctx) - - (* eval input *) - | _ -> - try - let source = new Source.source_string ipt in - let (ret, clxp, rctx) = (ieval source clxp rctx) in +let process_file + (backend : #backend) + (ectx : elab_context) + (file_name : string) + : elab_context = + + try + let source = new Source.source_file file_name in + let decls, ectx' = Frontend.decls_of_source source ectx in + List.iter backend#process_decls decls; + ectx' + with + | Sys_error _ + -> (error ("file \"" ^ file_name ^ "\" does not exist."); + ectx) + +let process_interactive + (interactive : #interactive_backend) + (i : int) + (ectx : elab_context) + (input : string) + : elab_context = + + let source = new Source.source_string input in + let decls, exprs, ectx' = Frontend.decls_of_interactive source ectx in + + List.iter interactive#process_decls decls; + print_and_clear_log (); + + let values = List.map interactive#eval_expr exprs in + List.iter (print_eval_result i) values; + print_and_clear_log (); + + ectx' + +let rec repl + (i : int) + (interactive : interactive_backend) + (ectx : elab_context) + : unit = + + let input = try read_input i with End_of_file -> "%quit" in + + let ectx = + match input with + (* Check special keywords *) + | "%quit" | "%q" + -> exit 0 + | "%help" | "%h" + -> print_string help_message; + ectx + | "%calltrace" | "%ct" + -> print_eval_trace None; + ectx + | "%typertrace" | "%tt" + -> print_typer_trace None; + ectx + | "%lcollisions" | "%cl" + -> Util.get_stats_hashtbl (WHC.stats hc_table); + ectx + + (* command with arguments *) + | _ when input.[0] = '%' && input.[1] != ' ' + -> (match String.split_on_char ' ' input with + | "%readfile" :: args + -> (try + let ectx = + List.fold_left (process_file interactive) ectx args + in print_and_clear_log (); - List.iter (print_eval_result i) ret; - repl clxp rctx + ectx with - | Log.Stop_Compilation msg -> - (handle_stopped_compilation msg; repl clxp rctx) - | Log.Internal_error msg -> - (handle_stopped_compilation ("Internal error: " ^ msg); - repl clxp rctx) - | Log.User_error msg -> - (handle_stopped_compilation ("Fatal user error: " ^ msg); - repl clxp rctx) - -let arg_files = ref [] - - -(* ./typer [options] files *) -let arg_defs = [ - ("--batch", Arg.Set arg_batch, "Don't run the interactive loop"); - ("--verbosity", - Arg.String Log.set_typer_log_level_str, "Set the logging level"); - ("-v", Arg.Unit Log.increment_log_level, "Increment verbosity"); - ("-Vfull-lctx", - Arg.Set Debruijn.log_full_lctx, - "Print the full lexp context on error."); - (* ("--debug", Arg.Set arg_debug, "Print the Elexp representation") *) - (*"-I", - Arg.String (fun f -> searchpath := f::!searchpath), - "Append a directory to the search path"*) -] - -let parse_args () = - Arg.parse arg_defs (fun s -> arg_files:= s::!arg_files) "" - -let main () = - parse_args (); - - let ectx = Elab.default_ectx in - let rctx = Elab.default_rctx in - - if not !arg_batch then - (print_string (make_title " TYPER REPL "); - print_string welcome_msg; - print_string (make_sep '-'); - flush stdout); - - let (i, ectx, rctx) = ( - try - let res = - readfiles (List.rev !arg_files) (1, ectx, rctx) (not !arg_batch) in - print_and_clear_log (); res - with - | Log.Stop_Compilation msg -> - handle_stopped_compilation msg; exit 1 - | (Log.Internal_error msg) as e -> - handle_stopped_compilation ("Internal error: " ^ msg); - raise e - | Log.User_error msg -> - handle_stopped_compilation ("Fatal user error: " ^ msg); exit 1 - ) in - - flush stdout; - - if not !arg_batch then - (* Initiate REPL. This will allow us to inspect interpreted code *) - repl i ectx rctx - - -let _ = main () + | Log.Stop_Compilation msg + -> handle_stopped_compilation msg; + ectx) + | "%who" :: args | "%w" :: args + -> (match args with + | ["all"] -> interactive#dump_rte_ctx + | _ -> interactive#print_rte_ctx); + ectx + | "%info" :: args | "%i" :: args + -> (match args with + | ["all"] -> dump_lexp_ctx (ectx_to_lctx ectx) + | _ -> print_lexp_ctx (ectx_to_lctx ectx)); + ectx + + | cmd :: _ + -> error ("\"" ^ cmd ^ "\" is not a correct repl command"); + ectx + + | _ + -> ectx) + + (* eval input *) + | _ + -> (try process_interactive interactive i ectx input with + | Log.Stop_Compilation msg + -> handle_stopped_compilation msg; + ectx + | Log.Internal_error msg + -> handle_stopped_compilation ("Internal error: " ^ msg); + ectx + | Log.User_error msg + -> handle_stopped_compilation ("Fatal user error: " ^ msg); + ectx) + + in repl (i + 1) interactive ectx ===================================== src/backend.ml ===================================== @@ -0,0 +1,81 @@ +(* Copyright (C) 2021 Free Software Foundation, Inc. + * + * Author: Simon Génier <simon.genier(a)umontreal.ca> + * Keywords: languages, lisp, dependent types. + * + * This file is part of Typer. + * + * Typer is free software; you can redistribute it and/or modify it under the + * terms of the GNU General Public License as published by the Free Software + * Foundation, either version 3 of the License, or (at your option) any later + * version. + * + * Typer is distributed in the hope that it will be useful, but WITHOUT ANY + * WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS + * FOR A PARTICULAR PURPOSE. See the GNU General Public License for more + * details. + * + * You should have received a copy of the GNU General Public License along + * with this program. If not, see <http://www.gnu.org/licenses/>. *) + +(* A backend is a consumer of fully eleborated and checked lexps. This module + provides a superclass for all backends as well their implementations. *) + +open Lexp + +type value = Env.value_type + +class virtual backend = object + (* Processes (interpret or compile, depending on the backend) a block of + mutually recursive declarations. *) + method virtual process_decls : ldecls -> unit + + method interactive : interactive_backend option = None +end + +(* Backends may optionaly allow interactive evaluation, i.e. lexps can be + immediately evaluated as opposed compiled for evaluation later. *) +and virtual interactive_backend = object (self) + inherit backend + + method! interactive = Some (self :> interactive_backend) + + method virtual eval_expr : lexp -> value + + method virtual print_rte_ctx : unit + + method virtual dump_rte_ctx : unit +end + +class ast_interpreter lctx = object + inherit interactive_backend + + val mutable rctx = Eval.from_lctx lctx + val mutable lctx = lctx + + method process_decls ldecls = + let lctx', eldecls = Opslexp.clean_decls lctx ldecls in + rctx <- Eval.eval_decls eldecls rctx; + lctx <- lctx' + + method eval_expr lexp = + let elexp = Opslexp.erase_type lctx lexp in + Eval.debug_eval elexp rctx + + method print_rte_ctx = Env.print_rte_ctx rctx + + method dump_rte_ctx = Env.dump_rte_ctx rctx +end + +class gambit_compiler lctx output = object + inherit backend + + val mutable sctx = Gambit.ScmContext.of_lctx lctx + val mutable lctx = lctx + + method process_decls ldecls = + let lctx', sctx', sdecls = Gambit.scheme_of_decls lctx sctx ldecls in + sctx <- sctx'; + lctx <- lctx'; + Gambit.Scm.print output sdecls; +end ===================================== src/dune ===================================== @@ -1,6 +1,5 @@ ;; -*- lisp-data -*- -(executable - (name REPL) - ;; (public_name typer) - (libraries "zarith" "str") - ) + +(library + (name typerlib) + (libraries zarith str)) ===================================== src/eval.ml ===================================== @@ -489,7 +489,14 @@ and eval_var ctx lxp v = ("Variable: " ^ L.maybename (snd name) ^ (str_idx idx) ^ " was not found ") (* unef: unevaluated function (to make the trace readable) *) -and eval_call loc unef i f args = +and eval_call + loc + (unef : elexp) + (i : eval_debug_info) + (f : value_type) + (args : value_type list) + : value_type = + match f, args with (* return result of eval *) | _, [] -> f @@ -1147,14 +1154,13 @@ let from_lctx (lctx: lexp_context): runtime_env = | CVempty -> Myers.nil | CVlet (loname, def, _, lctx) -> let rctx = from_lctx lctx in - Myers.cons (loname, - ref (match def with - | LetDef (_, e) - -> if closed_p rctx (OL.fv e) then - eval (OL.erase_type lctx e) rctx - else Vundefined - | _ -> Vundefined)) - rctx + let value = + match def with + | LetDef (_, e) when closed_p rctx (OL.fv e) + -> eval (OL.erase_type lctx e) rctx + | _ -> Vundefined + in + Myers.cons (loname, ref value) rctx | CVfix (defs, lctx) -> let fvs = List.fold_left (fun fvs (_, e, _) @@ -1171,8 +1177,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/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,297 @@ +(* 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]) + +let scheme_of_decls + (lctx : lexp_context) + (sctx : ScmContext.t) + (ldecls : ldecls) + : lexp_context * ScmContext.t * Scm.t = + + let lctx', eldecls = Opslexp.clean_decls lctx ldecls in + let sctx', eldecls = Listx.fold_left_map ScmContext.intro_binding sctx eldecls in + let sdecls = Scm.List (Scm.begin' :: List.map (scheme_of_decl sctx') eldecls) in + (lctx', sctx', sdecls) ===================================== src/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 ===================================== @@ -30,3 +30,13 @@ let get (o : 'a option) : 'a = match o with | Some v -> v | None -> invalid_arg "expected Some" + +let value ~(default : 'a) (o : 'a option) : 'a = + match o with + | Some v -> v + | None -> default + +let is_some (o : 'a option) : bool = + match o with + | Some _ -> true + | None -> false ===================================== tests/dune ===================================== @@ -0,0 +1,16 @@ +;; -*- lisp-data -*- + +(tests + (names elab_test + env_test + eval_test + gambit_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/gambit_test.ml ===================================== @@ -0,0 +1,190 @@ +(* Copyright (C) 2020 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 () ===================================== 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,110 @@ +(* 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 Typerlib + +open Printf + +open Backend +open Debruijn +open Elab +open Fmt + +let arg_batch = ref false +let arg_files = ref [] +let backend_name = ref "interpreter" + +(* ./typer [options] files *) +let arg_defs = + [("--batch", Arg.Set arg_batch, "Don't run the interactive loop"); + + ("--verbosity", + Arg.String Log.set_typer_log_level_str, + "Set the logging level"); + + ("-v", Arg.Unit Log.increment_log_level, "Increment verbosity"); + + ("--backend", + Arg.Symbol (["interpreter"; "gambit"], fun name -> backend_name := name), + "Select the backend"); + ] + +let welcome_message = +" Typer 0.0.0 - Interpreter - (c) 2016-2021 + + %quit (%q) : leave REPL + %help (%h) : print help +" + +let main () = + Arg.parse arg_defs (fun file -> arg_files := file :: !arg_files) ""; + + let is_batch = !arg_batch in + let file_names = List.rev !arg_files in + let backend = + match !backend_name with + | "interpreter" + -> (new ast_interpreter (ectx_to_lctx default_ectx) :> backend) + | "gambit" + -> (new gambit_compiler (ectx_to_lctx default_ectx) stdout :> backend) + | backend_name + -> (print_string ("unknown backend: " ^ backend_name); + exit 1) + in + + let interactive = backend#interactive in + let process_file = + if is_batch && Option.is_some interactive + then + fun (ectx, i) file_name + -> let ectx = REPL.process_file backend ectx file_name in + ectx, i + else + (print_string (make_title " TYPER REPL "); + print_string welcome_message; + print_string (make_sep '='); + flush stdout; + fun (ectx, i) file_name + -> printf " In[%02d] >> %%readfile %s\n" i file_name; + let ectx = REPL.process_file backend ectx file_name in + ectx, i + 1) + in + + let ectx, i = + try + let ectx, i = List.fold_left process_file (default_ectx, 0) file_names in + REPL.print_and_clear_log (); + ectx, i + with + | Log.Stop_Compilation msg + -> REPL.handle_stopped_compilation msg; + exit 1 + | Log.Internal_error msg as e + -> REPL.handle_stopped_compilation ("Internal error: " ^ msg); + raise e + | Log.User_error msg + -> REPL.handle_stopped_compilation ("Fatal user error: " ^ msg); + exit 1 + in + + match is_batch, backend#interactive with + | false, Some interactive -> REPL.repl i interactive ectx + | _ -> () + +let _ = main () View it on GitLab: https://gitlab.com/monnier/typer/-/compare/bf91885c18aaea57cde096858d7afc3b… -- View it on GitLab: https://gitlab.com/monnier/typer/-/compare/bf91885c18aaea57cde096858d7afc3b… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer] Deleted branch broken-tests-2021-04
by Simon Génier (＠ilovemonoids) 05 Apr '21

05 Apr '21

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

1 0

[Git][monnier/typer][dunify-tests] Dunify Typer tests.
by Simon Génier (＠ilovemonoids) 05 Apr '21

05 Apr '21

Simon Génier pushed to branch dunify-tests at Stefan / Typer Commits: a8e4948d by Simon Génier at 2021-04-05T00:23:48-04:00 Dunify Typer tests. - - - - - 21 changed files: - .gitignore - GNUmakefile - README.md - + btl/dune - src/debug_util.ml → debug_util.ml - + dune - src/REPL.ml - src/dune - src/option.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)) ===================================== src/REPL.ml ===================================== @@ -327,6 +327,3 @@ let main () = if not !arg_batch then (* Initiate REPL. This will allow us to inspect interpreted code *) repl i ectx rctx - - -let _ = main () ===================================== src/dune ===================================== @@ -1,6 +1,5 @@ ;; -*- lisp-data -*- -(executable - (name REPL) - ;; (public_name typer) - (libraries "zarith" "str") - ) + +(library + (name typerlib) + (libraries zarith str)) ===================================== 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 ===================================== 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 *) @@ -258,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 @@ -270,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 @@ -459,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,20 @@ +(* 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/>. *) + +let () = Typerlib.REPL.main () View it on GitLab: https://gitlab.com/monnier/typer/-/commit/a8e4948deea076b2ce7eb0e93a7c2d307… -- View it on GitLab: https://gitlab.com/monnier/typer/-/commit/a8e4948deea076b2ce7eb0e93a7c2d307… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][dunify-tests] 2 commits: Merge branch 'broken-tests-2021-04'
by Simon Génier (＠ilovemonoids) 05 Apr '21

05 Apr '21

Simon Génier pushed to branch dunify-tests at Stefan / Typer Commits: 0e3dcf79 by Simon Génier at 2021-04-05T00:18:00-04:00 Merge branch 'broken-tests-2021-04' - - - - - 3ec9b2a4 by Simon Génier at 2021-04-05T00:21:49-04:00 Dunify Typer tests. - - - - - 21 changed files: - .gitignore - GNUmakefile - README.md - + btl/dune - src/debug_util.ml → debug_util.ml - + dune - src/REPL.ml - src/dune - src/option.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 ?= byte # 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_cli.$(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_cli.$(COMPILE_MODE): + $(DUNE) --profile $(DUNE_PROFILE) build ./typer_cli.$(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)) ===================================== src/REPL.ml ===================================== @@ -327,6 +327,3 @@ let main () = if not !arg_batch then (* Initiate REPL. This will allow us to inspect interpreted code *) repl i ectx rctx - - -let _ = main () ===================================== src/dune ===================================== @@ -1,6 +1,5 @@ ;; -*- lisp-data -*- -(executable - (name REPL) - ;; (public_name typer) - (libraries "zarith" "str") - ) + +(library + (name typerlib) + (libraries zarith str)) ===================================== 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 ===================================== 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 *) @@ -258,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 @@ -270,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 @@ -459,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,20 @@ +(* 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/>. *) + +let () = Typerlib.REPL.main () View it on GitLab: https://gitlab.com/monnier/typer/-/compare/19837687aad6cb2b7e0a8419d9b9387c… -- View it on GitLab: https://gitlab.com/monnier/typer/-/compare/19837687aad6cb2b7e0a8419d9b9387c… You're receiving this email because of your account on gitlab.com.

1 0