Jean-Alexandre Barszcz pushed to branch ja/various_fixes 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.

- - - - - 5a31e992 by Simon Génier at 2020-12-05T14:46:49-05:00 Merge branch 'datacons-label'

- - - - - f5a4f23d by Jean-Alexandre Barszcz at 2020-12-08T17:56:36-05:00 Use ocaml 4.05 in the nix shell.

- - - - - db1a87c0 by Simon Génier at 2020-12-08T17:56:53-05:00 Qualify the constructors to fix warning 40.

- - - - - 6ef8ccb5 by Jean-Alexandre Barszcz at 2020-12-08T17:56:55-05:00 * src/opslexp.ml (clean_decls): Oops, make it check for metavars.

- - - - - 726a860e by Jean-Alexandre Barszcz at 2020-12-08T17:56:55-05:00 * src/elab.ml (sform_letin): Remove unnecessary scope_level bump.

- - - - - 37b1b4d9 by Jean-Alexandre Barszcz at 2020-12-08T17:56:55-05:00 * src/elab.ml (sform_letin): Make `let` bidirectional.

- - - - - 98273563 by Jean-Alexandre Barszcz at 2020-12-08T17:56:55-05:00 * src/opslexp.ml (fv): Check that the memoized value is still ok.

- - - - -

10 changed files:

- btl/builtins.typer - + btl/heap.typer - shell.nix - src/REPL.ml - src/debruijn.ml - src/elab.ml - + src/heap.ml - src/opslexp.ml - tests/unify_test.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))) +)

===================================== shell.nix ===================================== @@ -2,7 +2,7 @@ pkgs.mkShell { name = "typer"; buildInputs = - with pkgs.ocamlPackages; [ + with pkgs.ocaml-ng.ocamlPackages_4_05; [ pkgs.gnumake ocaml ocamlbuild findlib utop # tooling zarith # ocaml libraries merlin # for emacs

===================================== src/REPL.ml ===================================== @@ -66,7 +66,7 @@ let print_input_line i = let ieval_error = Log.log_error ~section:"IEVAL"

let print_and_clear_log () = - if (not Log.typer_log_config.print_at_log) then + if (not Log.typer_log_config.Log.print_at_log) then Log.print_and_clear_log ()

let handle_stopped_compilation msg =

===================================== src/debruijn.ml ===================================== @@ -99,13 +99,13 @@ let type_elabctx = mkBuiltin ((dloc, "Elab_Context"), type0) let type_eq_type = let lv = (dloc, Some "l") in let tv = (dloc, Some "t") in - mkArrow (Aerasable, lv, + mkArrow (Pexp.Aerasable, lv, type_level, dloc, - mkArrow (Aerasable, tv, + mkArrow (Pexp.Aerasable, tv, mkSort (dloc, Stype (mkVar (lv, 0))), dloc, - mkArrow (Anormal, (dloc, None), + mkArrow (Pexp.Anormal, (dloc, None), mkVar (tv, 0), dloc, - mkArrow (Anormal, (dloc, None), + mkArrow (Pexp.Anormal, (dloc, None), mkVar (tv, 1), dloc, mkSort (dloc, Stype (mkVar (lv, 3))))))) let type_eq = mkBuiltin ((dloc, "Eq"), type_eq_type) @@ -114,17 +114,17 @@ let eq_refl = let tv = (dloc, Some "t") in let xv = (dloc, Some "x") in mkBuiltin ((dloc, "Eq.refl"), - mkArrow (Aerasable, lv, + mkArrow (Pexp.Aerasable, lv, type_level, dloc, - mkArrow (Aerasable, tv, + mkArrow (Pexp.Aerasable, tv, mkSort (dloc, Stype (mkVar (lv, 0))), dloc, - mkArrow (Aerasable, xv, + mkArrow (Pexp.Aerasable, xv, mkVar (tv, 0), dloc, mkCall (type_eq, - [Aerasable, mkVar (lv, 2); - Aerasable, mkVar (tv, 1); - Anormal, mkVar (xv, 0); - Anormal, mkVar (xv, 0)]))))) + [Pexp.Aerasable, mkVar (lv, 2); + Pexp.Aerasable, mkVar (tv, 1); + Pexp.Anormal, mkVar (xv, 0); + Pexp.Anormal, mkVar (xv, 0)])))))

(* easier to debug with type annotations *)

===================================== src/elab.ml ===================================== @@ -1690,11 +1690,16 @@ let rec sform_case ctx loc sargs ot = match sargs with let sform_letin ctx loc sargs ot = match sargs with | [sdecls; sbody] -> let declss, nctx = lexp_p_decls [sdecls] [] ctx in - (* FIXME: Use `elaborate`. *) - let bdy, ltp = infer sbody (ectx_new_scope nctx) in - let s = List.fold_left (OL.lexp_defs_subst loc) S.identity declss in - (lexp_let_decls declss bdy nctx, - Inferred (mkSusp ltp s)) + let s, off = + List.fold_left (fun (s, off) decls -> + (OL.lexp_defs_subst loc s decls, off + List.length decls)) + (S.identity, 0) declss in + let ot = U.option_map (fun t -> mkSusp t (S.shift off)) ot in + let bdy, ot = elaborate nctx sbody ot in + let ot = match ot with + | Inferred t -> Inferred (mkSusp t s) + | _ -> ot in + (lexp_let_decls declss bdy nctx, ot) | _ -> sexp_error loc "Unrecognized let_in_ expression"; sform_dummy_ret ctx loc

@@ -1871,6 +1876,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

===================================== src/opslexp.ml ===================================== @@ -194,7 +194,10 @@ let rec lexp_whnf_aux e (ctx : DB.lexp_context) : lexp = let elevel = match lexp'_whnf (get_type ctx etype) ctx with | Sort (_, Stype l) -> l | _ -> Log.internal_error "" in - mkCall (DB.eq_refl, [Aerasable, elevel; Aerasable, etype; Aerasable, e]) in + mkCall (DB.eq_refl, + [Pexp.Aerasable, elevel; + Pexp.Aerasable, etype; + Pexp.Aerasable, e]) in let reduce it name aargs = let targs = match lexp_lexp' (lexp_whnf_aux it ctx) with | Inductive (_,_,fargs,_) -> fargs @@ -423,10 +426,10 @@ and conv_p' (ctx : DB.lexp_context) (vs : set_plexp) e1 e2 : bool = let tltp = mkSusp etype subst in let tlvl = mkSusp elvl subst in let eqty = mkCall (DB.type_eq, - [(Aerasable, tlvl); (* Typelevel *) - (Aerasable, tltp); (* Inductive type *) - (Anormal, hlxp); (* Lexp of the branch head *) - (Anormal, tlxp)]) in (* Target lexp *) + [(Pexp.Aerasable, tlvl); (* Typelevel *) + (Pexp.Aerasable, tltp); (* Inductive type *) + (Pexp.Anormal, hlxp); (* Lexp of the branch head *) + (Pexp.Anormal, tlxp)]) in (* Target lexp *) DB.lexp_ctx_cons ctx (DB.dloc, None) Variable eqty in (* The map module doesn't have a function to compare two maps with the key (which is needed to get the field types @@ -773,12 +776,12 @@ and check'' erased ctx e = let tltp = mkSusp etype subst in let tlvl = mkSusp elvl subst in let eqty = mkCall (DB.type_eq, - [(Aerasable, tlvl); (* Typelevel *) - (Aerasable, tltp); (* Inductive type *) - (Anormal, hlxp); (* Lexp of the branch head *) - (Anormal, tlxp)]) in (* Target lexp *) + [(Pexp.Aerasable, tlvl); (* Typelevel *) + (Pexp.Aerasable, tltp); (* Inductive type *) + (Pexp.Anormal, hlxp); (* Lexp of the branch head *) + (Pexp.Anormal, tlxp)]) in (* Target lexp *) (* The eq proof is erasable. *) - let nerased = dbset_push Aerasable nerased in + let nerased = dbset_push Pexp.Aerasable nerased in let nctx = DB.lexp_ctx_cons ctx (l, None) Variable eqty in (nerased, nctx) in SMap.iter @@ -972,11 +975,22 @@ and fv (e : lexp) : (DB.set * mv_set) = -> let (fvs, mvs) = fv_erase (fv (push_susp t s)) in (fvs, mv_set_add mvs id (sl, t, cl, name))) in - (* FIXME: Flush the memoization table whenever the metavar table - * is modified, since that can affect the output of `fv`. *) - try LMap.find fv_memo e - with Not_found - -> let r = fv' e in + let ofvs = LMap.find_opt fv_memo e in + (* The memoized value depends on the metavariable table. When it + changes, we have to recompute the free variables. Instead of + flushing the table after every association, we check that no free + metavars are actually associated. For this to work, we assume + that the table changes monotonously: metavariables can be + associated, but the associations cannot be undone. *) + match ofvs with + | Some ((_, (mvfs, _)) as fvs) + when IMap.for_all + (fun mv _ -> match metavar_lookup mv with + | MVar _ -> true + | MVal _ -> false) + mvfs + -> fvs + | _ -> let r = fv' e in LMap.add fv_memo e r; r

@@ -1183,6 +1197,9 @@ let erase_type lxp = ("Metavariables in erase_type :"); erase_type lxp

+let clean_decls decls = + List.map (fun (v, lxp, _) -> (v, (erase_type lxp))) decls +

(** Turning a set of declarations into an object. **)

===================================== tests/unify_test.ml ===================================== @@ -98,10 +98,10 @@ let _ = (fun (ectx, i) (name, lexp) -> Elab.ctx_extend ectx (dloc, Some name) Variable (shift lexp i), i + 1) (ectx, 0) - [("f", (mkArrow (Anormal, (dloc, None), nat, dloc, shift nat 1))); - ("g", (mkArrow (Anormal, (dloc, None), nat, dloc, shift nat 1))); - ("h", (mkArrow (Anormal, (dloc, Some "x"), nat, dloc, - mkArrow (Anormal, (dloc, Some "y"), shift nat 1, + [("f", (mkArrow (Pexp.Anormal, (dloc, None), nat, dloc, shift nat 1))); + ("g", (mkArrow (Pexp.Anormal, (dloc, None), nat, dloc, shift nat 1))); + ("h", (mkArrow (Pexp.Anormal, (dloc, Some "x"), nat, dloc, + mkArrow (Pexp.Anormal, (dloc, Some "y"), shift nat 1, dloc, shift nat 2)))); ("a", nat); ("b", nat)] in

===================================== 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/69b61bd608555d82434cb73a98bd7619f...