Simon Génier pushed to branch datacons-label at Stefan / Typer

Commits: c0df7b8b by Simon Génier at 2020-12-02T11:36:56-05:00 Cosmetic changes to utest_main.ml.

Some of these changes bring the style more in line with the GNU coding standard that is used for Typer. - Reindent file to 2 spaces. - Break lines before a operator. - Break lines before 80 columns.

Others are my attempts to improve readability. - Use functions specialized on refs in Arg. - Remove superfluous parenthesis. - Extract large fun expressions to local let bindings.

- - - - - 077b4494 by Simon Génier at 2020-12-02T12:05:43-05:00 Utest_main now also handle Windows paths.

- - - - - a4cc1ea7 by Simon Génier at 2020-12-03T12:13:32-05:00 Merge branch 'utests-main-windows'

- - - - - 1ce7599d by Simon Génier at 2020-12-04T09:56:45-05:00 Add opaque values for identifying data constructors.

This patch add a new primitive type, ##DataconsLabel, which uniquely identifies a data constructor within a type. Its inhabitants will be consumed by Low Level Typer to write the correct header for objects. The goal is to give an abstract type that is as useful on Typer on OCaml where the labels are strings than on a future backend which will be better for Low Level Typer and where labels will likely be integers.

Values are created through the primitive ##datacons-label<-string and there is also a macro datacons-label which allows us to write a symbol directly. I choosed to use a right pointing arrow its name, against the Lisp convention. I think it makes more sense in languages with an ML syntax because function composition is made like this

c<-b . b<-a

and it also goes in the same direction as the b_of_a convention in OCaml. I also though it was OK because there where no other primitives with arrows in their names so that convention does not clash with others.

Finally, I decided to go against the name ##Discriminent because it suggests it only applies to sum types, but ##DataconsLabel is also needed for product types.

- - - - -

5 changed files:

- btl/builtins.typer - + btl/heap.typer - src/elab.ml - + src/heap.ml - tests/utest_main.ml

Changes:

===================================== btl/builtins.typer ===================================== @@ -469,4 +469,11 @@ Test_eq = Built-in "Test.eq"; Test_neq : String -> ?a -> ?a -> IO Bool; Test_neq = Built-in "Test.neq";

+%% +%% Given a string, return an opaque DataconsLabel that identifies a data +%% constructor. +%% +datacons-label<-string : String -> ##DataconsLabel; +datacons-label<-string = Built-in "datacons-label<-string"; + %%% builtins.typer ends here.

===================================== btl/heap.typer ===================================== @@ -0,0 +1,34 @@ +%%% heap --- Manipulate partially initialized objects on the heap + +%% Copyright (C) 2011-2020 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/. + +datacons-label = macro (lambda args -> + let + label = Sexp_dispatch (List_nth 0 args Sexp_error) + (lambda _ _ -> Sexp_error) + (lambda label-name -> Sexp_string label-name) + (lambda _ -> Sexp_error) + (lambda _ -> Sexp_error) + (lambda _ -> Sexp_error) + (lambda _ -> Sexp_error) + in + IO_return (quote (datacons-label<-string (uquote label))) +)

===================================== src/elab.ml ===================================== @@ -1871,6 +1871,7 @@ let default_ectx else ctx_define ctx (dloc, Some key) e t) (!BI.lmap) lctx in

+ Heap.register_builtins (); (* read base file *) let lctx = dynamic_bind parsing_internals true (fun ()

===================================== src/heap.ml ===================================== @@ -0,0 +1,40 @@ +(* Copyright (C) 2020 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/. *) + +open Env +open Lexp +open Pexp + +type location = Util.location + +let error ~(location : location) (message : string) : 'a = + Log.log_fatal ~section:"HEAP" ~loc:location message + +let dloc = Util.dummy_location +let type0 = Debruijn.type0 +let type_datacons_label = mkBuiltin ((dloc, "DataconsLabel"), type0) + +let datacons_label_of_string location depth = function + | [Vstring _ as label] -> label + | _ -> error ~location "`##datacons-label<-string` expects 1 string argument" + +let register_builtins () = + Builtin.add_builtin_cst "DataconsLabel" type_datacons_label; + Eval.add_builtin_function "datacons-label<-string" datacons_label_of_string 1

===================================== tests/utest_main.ml ===================================== @@ -3,7 +3,7 @@ * * --------------------------------------------------------------------------- * - * Copyright (C) 2011-2018 Free Software Foundation, Inc. + * Copyright (C) 2011-2020 Free Software Foundation, Inc. * * Author: Pierre Delaunay pierre.delaunay@hec.ca * Keywords: languages, lisp, dependent types. @@ -30,32 +30,34 @@ * * --------------------------------------------------------------------------- *)

-open Fmt +(** Search *_test.byte executable and run them. + Usage: + ./utest_main tests_folder root_folder *)

-let cut_name str = - String.sub str 0 (String.length str - 12) +open Fmt

let global_verbose_lvl = ref 5 -let global_sample_dir = ref "./" -let global_tests_dir = ref "./_build/tests/" +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 = [ +let arg_defs = + [ ("--verbose", - Arg.Int (fun g -> global_verbose_lvl := g), " Set verbose level"); + Arg.Set_int global_verbose_lvl, " Set verbose level"); ("--samples", - Arg.String (fun g -> global_sample_dir := g), " Set sample directory"); + Arg.Set_string global_sample_dir, " Set sample directory"); ("--tests", - Arg.String (fun g -> global_tests_dir := g), " Set tests directory"); + 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"); + global_filter := true), " Set test filter"); ("--ftitle", Arg.String (fun g -> global_ftitle := String.uppercase_ascii g; - global_filter := true), " Set test filter"); + global_filter := true), " Set test filter"); ]

@@ -69,99 +71,114 @@ 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) + 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 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) + not !global_filter || String.uppercase_ascii (cut_name str) = !global_fsection

-(* search *_test.byte executable en run them - Usage: - ./utest_main tests_folder root_folder *) 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 = - if (Filename.check_suffix name "_test.byte") || - (Filename.check_suffix name "_test.native") then true else false 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 - - List.iter (fun file -> - flush stdout; - - if must_run file then ( - tests_n := !tests_n + 1; - let command = String.concat " " (List.map Filename.quote - ((folder ^ file)::test_args)) in - exit_code := Sys.command command; - - (if !exit_code != 0 then( - (if verbose 1 then print_file_name (!tests_n) files_n file false); - failed_test := !failed_test + 1) - else - (if verbose 1 then print_file_name (!tests_n) files_n file true); - ); - - (if verbose 2 then print_newline ()); - - ); - - ) 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" + 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 ();

View it on GitLab: https://gitlab.com/monnier/typer/-/compare/90dfe88279df30b2820bd9bd66418b38e...