Simon Génier pushed to branch dunify-tests at Stefan / Typer
Commits: 92965ea9 by Simon Génier at 2021-04-04T17:02:08-04:00 Dunify Typer tests.
- - - - -
20 changed files:
- 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_cli.ml
Changes:
===================================== GNUmakefile ===================================== @@ -1,96 +1,55 @@ -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) --profile dev build ./debug_util.$(COMPILE_MODE)
-test-file: - $(OCAMLBUILD) src/test.$(COMPILE_MODE) -I src $(OBFLAGS) - @$(MV) $(BUILDDIR)/src/test.$(COMPILE_MODE) $(BUILDDIR)/test +tests: + $(DUNE) --profile dev 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 +69,6 @@ run/tests: run/typer-file: @./$(BUILDDIR)/typer ./samples/test__.typer
-run/test-file: - @./$(BUILDDIR)/test - # Compile into bytecode using ocamlc in profiling mode. # Generate a ocamlprof.dump file. profiling-cp:
===================================== README.md ===================================== @@ -9,18 +9,17 @@ Status [] ## Requirement
* Ocaml 4.05 -* Ocamlfind -* Ocamlbuild -* Findlib +* Dune 2.x * Zarith
## Build
-By default ocamlbuild creates a '_build' folder which holds all the compiled files. +By default, Dune creates a '_build' folder which holds all the compiled files.
-* `make typer`: build typer interpreter './typer' -* `make debug`: build typer with debug info './debug_util' -* `make tests`: run interpreter's tests './tests/utests' +* `make typer`: build Typer interpreter (`./typer_cli.bc`). +* `COMPILE_MODE=native make typer`: build Typer interpreter (`./typer_cli.exe`). +* `make debug`: build typer with debug info (`./debug_util.bc`). +* `make tests`: run interpreter's tests.
# Directory layout
===================================== btl/dune ===================================== @@ -0,0 +1,5 @@ +;; -*- lisp-data -*- + +(alias + (name typer_stdlib) + (deps (glob_files *.typer)))
===================================== src/debug_util.ml → debug_util.ml ===================================== @@ -30,6 +30,8 @@ * * --------------------------------------------------------------------------- *)
+open Typer + (* 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_cli) + (promote (until-clean)) + (modules typer_cli) + (libraries typer) + (modes byte native)) + +(executable + (name debug_util) + (promote (until-clean)) + (modules debug_util) + (libraries typer) + (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 typer) + (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 typer) + (action + (chdir %{project_root} (run %{test}))))
===================================== tests/elab_test.ml ===================================== @@ -21,12 +21,13 @@ * * -------------------------------------------------------------------------- *)
+open Typer + 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 Typer
-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 Typer
-open Sexp -open Lexp +open Utest_lib
open Eval (* reset_eval_trace *)
@@ -282,7 +280,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 +469,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 Typer + 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 Typer
-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 Typer
-open Eval (* reset_eval_trace *) - -open Builtin open Env +open Utest_lib
(* default environment *)
===================================== tests/sexp_test.ml ===================================== @@ -1,9 +1,12 @@ +open Typer + 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 Typer
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 Typer + open Fmt open Util
@@ -63,7 +65,7 @@ exception Unexpected_result of string * 2: Print Each composing Test * 3: use debug *) -let global_verbose_lvl = ref 0 +let global_verbose_lvl = ref 2 let global_sample_dir = ref "" let global_fsection = ref "" let global_ftitle = ref "" @@ -94,7 +96,7 @@ let must_run_title str = !global_ftitle = "" || String.uppercase_ascii str = !global_ftitle
-let parse_args () = Arg.parse arg_defs (fun s -> ()) "" +let parse_args () = Arg.parse arg_defs (fun _ -> ()) ""
(* Utest printing function *) @@ -144,7 +146,7 @@ let expect_equal_lexps = _expect_equal_t lexp_list_eq string_of_lexp_list
let expect_equal_decls = - let rec decl_eq l r = + let decl_eq l r = let (_, l_vname), l_lexp, l_ltype = l in let (_, r_vname), r_lexp, r_ltype = r in Option.equal String.equal l_vname r_vname
===================================== tests/utest_main.ml deleted ===================================== @@ -1,184 +0,0 @@ -(* - * Typer Compiler - * - * --------------------------------------------------------------------------- - * - * Copyright (C) 2011-2020 Free Software Foundation, Inc. - * - * Author: Pierre Delaunay pierre.delaunay@hec.ca - * Keywords: languages, lisp, dependent types. - * - * This file is part of Typer. - * - * Typer is free software; you can redistribute it and/or modify it under the - * terms of the GNU General Public License as published by the Free Software - * Foundation, either version 3 of the License, or (at your option) any - * later version. - * - * Typer is distributed in the hope that it will be useful, but WITHOUT ANY - * WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS - * FOR A PARTICULAR PURPOSE. See the GNU General Public License for - * more details. - * - * You should have received a copy of the GNU General Public License along - * with this program. If not, see http://www.gnu.org/licenses/. - * - * --------------------------------------------------------------------------- - * - * Description: - * Basic utest program run all tests - * - * --------------------------------------------------------------------------- *) - -(** Search *_test.byte executable and run them. - Usage: - ./utest_main tests_folder root_folder *) - -open Fmt - -let global_verbose_lvl = ref 5 -let global_sample_dir = ref "." -let global_tests_dir = ref (Filename.concat "_build" "tests") -let global_fsection = ref "" -let global_ftitle = ref "" -let global_filter = ref false - -let arg_defs = - [ - ("--verbose", - Arg.Set_int global_verbose_lvl, " Set verbose level"); - ("--samples", - Arg.Set_string global_sample_dir, " Set sample directory"); - ("--tests", - Arg.Set_string global_tests_dir, " Set tests directory"); - (* Allow users to select which test to run *) - ("--fsection", - Arg.String (fun g -> global_fsection := String.uppercase_ascii g; - global_filter := true), " Set test filter"); - ("--ftitle", - Arg.String (fun g -> global_ftitle := String.uppercase_ascii g; - global_filter := true), " Set test filter"); - ] - - -let verbose n = (n <= (!global_verbose_lvl)) - -let parse_args () = Arg.parse arg_defs (fun s -> ()) "" - -let ut_string vb msg = if verbose vb then print_string msg else () - -let cut_byte str = String.sub str 0 ((String.length str) - 10) -let cut_native str = String.sub str 0 ((String.length str) - 12) - -let cut_name str = - if Filename.check_suffix str "_test.byte" - then cut_byte str - else cut_native str - -let print_file_name i n name pass = - let line_size = 80 - (String.length (cut_name name)) - 16 in - let name = cut_name name in - - (if pass then print_string green else print_string red); - print_string " ("; - ralign_print_int i 2; print_string "/"; - ralign_print_int n 2; print_string ") "; - print_string name; - print_string (make_line '.' line_size); - if pass then print_string "..OK\n" else print_string "FAIL\n"; - print_string reset - -let must_run str = - not !global_filter - || String.uppercase_ascii (cut_name str) = !global_fsection - -let main () = - parse_args (); - - print_string "\n"; - calign_print_string " Running Unit Test " 80; - print_string "\n\n"; - - (*print_string ("[ ] Test folder: " ^ folder ^ "\n"); *) - - (* get tests files *) - let folder = !global_tests_dir in - let root_folder = !global_sample_dir in - - let files = - try Sys.readdir folder - with - | e - -> (print_string ("The folder: " ^ !global_tests_dir - ^ " does not exist.\n" - ^ "Have you tried "./utests --tests= ./tests" ?\n"); - raise e) - in - - let check name = - Filename.check_suffix name "_test.byte" - || Filename.check_suffix name "_test.native" - in - - (* select files that are executable tests *) - let files = Array.fold_left - (fun acc elem -> if check elem then elem::acc else acc) - [] files in - - let files_n = List.length files in - - (if files_n = 0 then - print_string "No tests were found. Did you compiled them? \n"); - - let exit_code = ref 0 in - let failed_test = ref 0 in - let tests_n = ref 0 in - let test_args = - ["--samples"; root_folder; - "--verbose"; string_of_int !global_verbose_lvl] - @ (if not (!global_ftitle = "") then - ["--ftitle"; !global_ftitle] else []) in - - let run_file test_path = - flush stdout; - - tests_n := !tests_n + 1; - let command_parts = Filename.concat folder test_path :: test_args in - let command_parts = - if Sys.os_type = "Win32" - then - (* I wish Filename.quote could be used on Windows. - - It would be appropriate if Ocaml spawned the process through the C - API, but Sys.command passes does it through the shell, which is - cmd.exe and has its own quoting rules. Ocaml has - Filename.quote_command, which does the right thing on every platform, - but it is only available since Ocaml 4.10. Until then, let's hope the - command does not need to be escaped. *) - command_parts - else List.map Filename.quote command_parts - in - - print_endline (String.concat " " command_parts); - exit_code := Sys.command (String.concat " " command_parts); - - (if !exit_code != 0 - then - ((if verbose 1 then print_file_name !tests_n files_n test_path false); - failed_test := !failed_test + 1) - else - (if verbose 1 then print_file_name !tests_n files_n test_path true); - ); - - (if verbose 2 then print_newline ()); - in - - List.iter run_file (List.filter must_run files); - - print_string "\n\n"; - print_string " Test Ran : "; print_int !tests_n; - print_string "\n Test Failed : "; print_int !failed_test; - print_string "\n Test Passed : "; print_int (!tests_n - !failed_test); - print_endline "\n" - -let _ = main ();
===================================== typer_cli.ml ===================================== @@ -0,0 +1,20 @@ +(* Copyright (C) 2021 Free Software Foundation, Inc. + * + * Author: Simon Génier simon.genier@umontreal.ca + * Keywords: languages, lisp, dependent types. + * + * This file is part of Typer. + * + * Typer is free software; you can redistribute it and/or modify it under the + * terms of the GNU General Public License as published by the Free Software + * Foundation, either version 3 of the License, or (at your option) any later + * version. + * + * Typer is distributed in the hope that it will be useful, but WITHOUT ANY + * WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR + * A PARTICULAR PURPOSE. See the GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License along with + * this program. If not, see http://www.gnu.org/licenses/. *) + +let () = Typer.REPL.main ()
View it on GitLab: https://gitlab.com/monnier/typer/-/commit/92965ea98a5278be89c0b9b68e16cadf86...
Afficher les réponses par date