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

[Git][monnier/typer][master] 3 commits: Use the environment augmented with the new bindings for type erasure.
by Simon Génier (＠ilovemonoids) 05 Apr '21

05 Apr '21

Simon Génier pushed to branch master at Stefan / Typer Commits: 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' - - - - - 2 changed files: - src/eval.ml - tests/eval_test.ml Changes: ===================================== src/eval.ml ===================================== @@ -1171,8 +1171,9 @@ let from_lctx (lctx: lexp_context): runtime_env = let _ = (* FIXME: Evaluate those defs that we can, even if not all defs * are present! *) + let lctx' = DB.lctx_extend_rec lctx defs in if alldefs && closed_p rctx (OL.fv_hoist (List.length defs) fvs) then - List.iter (fun (e, rc) -> rc := eval (OL.erase_type lctx e) nrctx) evs + List.iter (fun (e, rc) -> rc := eval (OL.erase_type lctx' e) nrctx) evs else () in nrctx and from_lctx lctx = ===================================== tests/eval_test.ml ===================================== @@ -86,18 +86,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" View it on GitLab: https://gitlab.com/monnier/typer/-/compare/424af536858c8f2c3e00bd88f0db2572… -- View it on GitLab: https://gitlab.com/monnier/typer/-/compare/424af536858c8f2c3e00bd88f0db2572… You're receiving this email because of your account on gitlab.com.

1 0

Changements aux commandes pour compiler Typer à réviser
by Génier Simon 04 Apr '21

04 Apr '21

Bonjour, Je viens de pousser deux petites branches et j'aimerais votre avis. https://gitlab.com/monnier/typer/-/compare/master...broken-tests-2021-04 La première ne devrait être controversée, il y avait des tests brisés dans eval_test.ml. Un trio utilisait une fonction pour l'évaluation qui effaçait les types dans le mauvais environnement. Un autre test (Let3) testait ce qui était en fait du code incorrect, une déclaration qui faisait référence à un type définie dans le même bloc de déclarations. Depuis 77981fd4dc8bc6af20e1db5148a9fb14f4adc07a, seules les définitions peuvent être récursives. https://gitlab.com/monnier/typer/-/compare/broken-tests-2021-04...dunify-te… La deuxième ajoute des fichiers dune pour rouler les tests. J'ai dû faire un changement à la structure du projet. Avec le système actuel, chaque test est un exécutable indépendant qui est compilé à partir des fichiers ml que ocamlbuild trouve en suivant les dépendances. Dune par contre de supporte pas d'avoir un même fichier dans plusieurs targets. J'ai donc séparé l'essentiels des fichiers de Typer dans une bibliothèque et j'ai créé deux exécutables, typer_cli (un executable ne peut pas avoir le même nom qu'une bibliothèque) et debug_util qui, avec les tests, linkent vers cette bibliothèque. Le principal avantage est que Dune s'occupe maintenant de coordonner nos tests. Ça nous permet de ne plus avoir à maintenir tests/utest_main.ml. Le principal défaut est qu'il faut s'habituer aux nouvelles commandes. J'ai mis à jour le Makefile pour que l'adaptation soit plus facile. Qu'est-ce que vous en pensez? Simon

2 1

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

04 Apr '21

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

1 0

[Git][monnier/typer][dunify-tests] 3 commits: Use the environment augmented with the new bindings for type erasure.
by Simon Génier (＠ilovemonoids) 04 Apr '21

04 Apr '21

Simon Génier pushed to branch dunify-tests at Stefan / Typer Commits: 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. - - - - - 19837687 by Simon Génier at 2021-04-04T21:55:19-04:00 Dunify Typer tests. - - - - - 22 changed files: - .gitignore - GNUmakefile - README.md - + btl/dune - src/debug_util.ml → debug_util.ml - + dune - src/REPL.ml - src/dune - src/eval.ml - 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: ===================================== .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 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/eval.ml ===================================== @@ -1171,8 +1171,9 @@ let from_lctx (lctx: lexp_context): runtime_env = let _ = (* FIXME: Evaluate those defs that we can, even if not all defs * are present! *) + let lctx' = DB.lctx_extend_rec lctx defs in if alldefs && closed_p rctx (OL.fv_hoist (List.length defs) fvs) then - List.iter (fun (e, rc) -> rc := eval (OL.erase_type lctx e) nrctx) evs + List.iter (fun (e, rc) -> rc := eval (OL.erase_type lctx' e) nrctx) evs else () in nrctx and from_lctx lctx = ===================================== src/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 *) @@ -86,18 +84,6 @@ let _ = test_eval_eqv_named x = let a = 1; b = 2 in I in (case x | I => c);" (* == *) "3" -let _ = test_eval_eqv_named - "Let3" - - "c = 3; e = 1; f = 2; d = 4;" - - "let TrueProp : Type; - I : TrueProp; - TrueProp = typecons TrueProp I; - I = datacons TrueProp I; - x = let a = 1; b = 2 in I - in (case x | I => c);" (* == *) "3" - let _ = test_eval_eqv_named "Let-erasable" @@ -270,10 +256,10 @@ let _ = test_eval_eqv "w = 2" "declexpr w" "2" let _ = (add_test "EVAL" "Monads" (fun () -> - let dcode = " - c = IO_bind (File_open \"./_build/w_file.txt\" \"w\") - (lambda f -> File_write f \"Hello2\"); - " in + let dcode = {| + c = IO_bind (File_open "w_file.txt" "w") + (lambda f -> File_write f "Hello2"); + |} in let rctx, ectx = Elab.eval_decl_str dcode ectx rctx in @@ -282,7 +268,7 @@ let _ = (add_test "EVAL" "Monads" (fun () -> (* Eval defined lambda *) let ret = Elab.eval_expr_str rcode ectx rctx in match ret with - | [v] -> success + | [_] -> success | _ -> failure)) let _ = test_eval_eqv_named @@ -471,7 +457,7 @@ let _ = let str = "(Int_" ^ op ^ " " ^ (string_of_int a) ^ " " ^ (string_of_int b) ^ ")" in let lxp = List.hd (Elab.lexp_expr_str str ectx) in - let elxp = OL.erase_type lxp in + let elxp = OL.erase_type (Debruijn.ectx_to_lctx ectx) lxp in assert (Log.error_count () == 0); if Z.fits_int expect' then ===================================== tests/inverse_test.ml ===================================== @@ -21,23 +21,13 @@ * * -------------------------------------------------------------------------- *) -open Sexp -open Pexp +open 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(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_cli.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 () = Typer.REPL.main () View it on GitLab: https://gitlab.com/monnier/typer/-/compare/770866821edbdf2ff2a6ac82707f9693… -- View it on GitLab: https://gitlab.com/monnier/typer/-/compare/770866821edbdf2ff2a6ac82707f9693… 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) 04 Apr '21

04 Apr '21

Simon Génier pushed to branch dunify-tests at Stefan / Typer Commits: 77086682 by Simon Génier at 2021-04-04T17:11:17-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_cli.ml Changes: ===================================== .gitignore ===================================== @@ -1,5 +1,7 @@ # Files generated by OCaml's compiler +*.bc *.byte +*.exe *.annot *.cmi *.cmo ===================================== 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 [![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 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(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_cli.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 () = Typer.REPL.main () View it on GitLab: https://gitlab.com/monnier/typer/-/commit/770866821edbdf2ff2a6ac82707f96931… -- View it on GitLab: https://gitlab.com/monnier/typer/-/commit/770866821edbdf2ff2a6ac82707f96931… 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) 04 Apr '21

04 Apr '21

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 [![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 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(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_cli.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 () = Typer.REPL.main () View it on GitLab: https://gitlab.com/monnier/typer/-/commit/92965ea98a5278be89c0b9b68e16cadf8… -- View it on GitLab: https://gitlab.com/monnier/typer/-/commit/92965ea98a5278be89c0b9b68e16cadf8… You're receiving this email because of your account on gitlab.com.

1 0

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

04 Apr '21

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

1 0

[Git][monnier/typer][soilih] little bug resolution
by Soilihi BEN SOILIHI BOINA (＠BenSoilih) 03 Apr '21

03 Apr '21

Soilihi BEN SOILIHI BOINA pushed to branch soilih at Stefan / Typer Commits: 7abb48c5 by Soilih BEN SOILIH at 2021-04-03T08:12:45-06:00 little bug resolution - - - - - 2 changed files: - src/REPL.ml - src/typer_lsp_server.ml Changes: ===================================== src/REPL.ml ===================================== @@ -208,8 +208,8 @@ let readstring (str:string) = let ectx = Elab.default_ectx in (*let rctx = Elab.default_rctx in*) Elab.lexp_decl_str str ectx ; - let ret = Log.typer_log in - ret + let ref_list = Log.typer_log in + List.map (fun x -> x) !ref_list let readfiles files (i, lctx, rctx) prt = ===================================== src/typer_lsp_server.ml ===================================== @@ -57,6 +57,7 @@ let log_level_to_severity (level:log_level) : Lsp.Types.DiagnosticSeverity.t = let process_some_input_file (_file_contents : string) : state_after_processing = REPL.readstring _file_contents + let diagnostics (_state : state_after_processing) : Lsp.Types.Diagnostic.t list = let log_tab = log_entry_to_list _state in List.map (fun x -> View it on GitLab: https://gitlab.com/monnier/typer/-/commit/7abb48c554174b01d898ea7039b2e4c1b… -- View it on GitLab: https://gitlab.com/monnier/typer/-/commit/7abb48c554174b01d898ea7039b2e4c1b… You're receiving this email because of your account on gitlab.com.

1 0

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

02 Apr '21

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

1 0

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

02 Apr '21

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

1 0