Jean-Alexandre Barszcz pushed to branch keep-samples-alive at Stefan / Typer

Commits: ffd27741 by Jean-Alexandre Barszcz at 2022-03-17T15:34:57-04:00 * tests/samples_test.ml : Check that the samples can be evaluated.

- - - - -

5 changed files:

- + samples/dune - + samples/unerase.typer - tests/dune - + tests/samples_test.ml - tests/utest_lib.ml

Changes:

===================================== samples/dune ===================================== @@ -0,0 +1,5 @@ +;; -*- lisp-data -*- + +(alias + (name typer_samples) + (deps (glob_files *.typer)))

===================================== samples/unerase.typer ===================================== @@ -0,0 +1,4 @@ +%Eq_unerase : Eq ?x ?y ≡> Eq ?x ?y; +Eq_unerase = + lambda x y (p : Eq x y) ≡> + Eq_cast (p := p) (f := Eq x) Eq_refl;

===================================== tests/dune ===================================== @@ -10,9 +10,11 @@ lexer_test macro_test positivity_test + samples_test sexp_test unify_test) - (deps (alias %{project_root}/btl/typer_stdlib)) + (deps (alias %{project_root}/btl/typer_stdlib) + (alias %{project_root}/samples/typer_samples)) (libraries typerlib) (action (chdir %{project_root} (run %{test}))))

===================================== tests/samples_test.ml ===================================== @@ -0,0 +1,71 @@ +(* Copyright (C) 2022 Free Software Foundation, Inc. + * + * Author: Jean-Alexandre Barszcz jean-alexandre.barszcz@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 Utest_lib +module SSet = Set.Make(String) + +let ectx = Elab.default_ectx + +let add_sample_test filename = + let error_expected = + Filename.check_suffix (Filename.remove_extension filename) "error" in + let run_sample_test () = + let backend = new Eval.ast_interpreter (Debruijn.ectx_to_lctx ectx) in + let file = Filename.concat "samples" filename in + ignore (Elab.process_file backend ectx file); + Log.stop_on_error (); + success in + add_test "SAMPLES" filename (fun () -> + if error_expected then + expect_throw (fun _ -> "successful evaluation") run_sample_test + else + run_sample_test () + ) + +(* Some samples are currently not runnable, let's skip them. *) +(* FIXME: Fix these samples. *) +let excluded_samples = + SSet.of_list [ + "autodiff.typer"; + "batch_test.typer"; + "bbst_test.typer"; + "case_test.typer"; + "defmacro.typer"; + "dependent.typer"; + "hurkens.typer"; + "io.typer"; + "list_n.typer"; + "myers_test.typer"; + "pervasive.typer"; + "polyfun_test.typer"; + "table_test.typer"; + "tuple_test.typer"; + "typer_proof.typer"; + ] + +let _ = + let samples = + List.filter (fun fn -> Filename.check_suffix fn ".typer" && + not (SSet.mem fn excluded_samples)) + (Array.to_list (Sys.readdir "samples")) in + List.iter add_sample_test samples + +let _ = run_all ()

===================================== tests/utest_lib.ml ===================================== @@ -182,6 +182,14 @@ let expect_equal_decls = in _expect_equal_t decl_list_eq string_of_decl_list

+let expect_throw to_string test = + try let value = test () in + ut_string2 (red ^ "EXPECTED an exception" ^ reset ^ "\n"); + ut_string2 (red ^ "GOT: " ^ reset ^ "\n" ^ (to_string value) ^ "\n"); + failure + with + | _ -> success + (* USAGE * * (add_test "LET" "Base Case" (fun () ->

View it on GitLab: https://gitlab.com/monnier/typer/-/commit/ffd27741d8314eefdea641d2e732d60a4e...