Août 2022 - Typer - mailman.iro.umontreal.ca

[Git][monnier/typer][location-sinfo] Assertion failed line 776
by Ismaila FALL (＠Fallismaila) 31 Aoû '22

31 Aoû '22

Ismaila FALL pushed to branch location-sinfo at Stefan / Typer Commits: 366ff7fc by Fallismaila at 2022-08-31T20:48:52+00:00 Assertion failed line 776 - - - - - 5 changed files: - src/REPL.ml - src/debruijn.ml - src/elab.ml - src/heuristic.ml - src/log.ml Changes: ===================================== src/REPL.ml ===================================== @@ -46,9 +46,7 @@ open Lexp open Prelexer open Sexp open Util -(* -open Implgenealgo -*) + module OL = Opslexp module EL = Elexp @@ -208,8 +206,8 @@ let rec repl i (interactive : #Backend.interactive) (ectx : elab_context) = | "%ctx"::args | "%c"::args -> let _ = match args with - | ["all"] -> dump_un_lexp_ctx (ectx_to_lctx ectx) - | _ -> print_un_lexp_ctx (ectx_to_lctx ectx) in + | ["all"] -> Heuristic.dump_heur_ctx (ectx) + | _ -> Heuristic.print_heur_ctx (ectx) in ectx ===================================== src/debruijn.ml ===================================== @@ -435,87 +435,14 @@ let print_lexp_ctx_n (ctx : lexp_context) (ranges : (int * int) list) = print_string (make_sep '=') -let print_lexp_ctx_un (ctx : lexp_context) (ranges : (int * int) list) = - print_string (make_title " LEXP CONTEXT "); - - make_rheader - [(Some ('l', 10), "NAME"); - (Some ('l', 10), "LEXP_UNPARSE"); - (* (Some ('l', 10), "HEURISTIC_UNPARSE"); *) - (Some ('l', 42), " TYPE")]; - - print_string (make_sep '-'); - - let _ = " | | | " in - - let print i = - try - let _, name, _, ty = - match env_lookup_by_index i ctx with - | ((_, name), LetDef (r, exp), ty) -> r, name, Some exp, ty - | ((_, name), _, ty) -> 0, name, None, ty - in - let name' = maybename name in - let short_name = - if String.length name' > 10 - then - String.sub name' 0 9 ^ "…" - else name' - in - Printf.printf " %-10s || " short_name; - - sexp_print (Heuristic.heuristic_unparse ty); - - Printf.printf " |-->|: "; - - - (* - sexp_print (Heuristic.heuristic_unparse ty ctx); - - Printf.printf " |--> "; - *) - - lexp_print ty; - print_newline (); - print_newline () - with - | Not_found - -> print_endline " | %-7d | Not_found |" - in - - let rec print_range lower i = - let i' = i - 1 in - if i' >= lower - then - (print i'; - print_range lower i') - in - - let rec print_ranges = function - | [] -> () - | (lower, upper) :: ranges' - -> (print_range lower upper; - print_ranges ranges') - in - - print_ranges ranges; - print_string (make_sep '=') - - (* Only print user defined variables *) let print_lexp_ctx (lctx : lexp_context) : unit = print_lexp_ctx_n lctx [(0, M.length lctx - !builtin_size)] -let print_un_lexp_ctx (lctx : lexp_context) : unit = - print_lexp_ctx_un lctx [(0, M.length lctx - !builtin_size)] - (* Dump the whole context *) let dump_lexp_ctx (lctx : lexp_context) : unit = print_lexp_ctx_n lctx [(0, M.length lctx)] -let dump_un_lexp_ctx (lctx : lexp_context) : unit = - print_lexp_ctx_un lctx [(0, M.length lctx)] - let summarize_lctx (lctx : lexp_context) (at : int) : unit = let ranges = if at < 7 ===================================== src/elab.ml ===================================== @@ -38,7 +38,6 @@ * -------------------------------------------------------------------------- *) open Util - open Prelexer open Lexer @@ -48,20 +47,18 @@ open Lexp open Env open Debruijn +open Grammar +open Printf + module DB = Debruijn module M = Myers module EV = Eval - -open Grammar module BI = Builtin - module Unif = Unification module Inst = Instargs - module OL = Opslexp module EL = Elexp -open Printf (* dummies *) let dloc = dummy_location ===================================== src/heuristic.ml ===================================== @@ -1,6 +1,9 @@ open Lexp open Sexp open Pexp +open Debruijn + +module OL = Opslexp (* ugly printing (sexp_print (pexp_unparse (heuristic_unparse e))) *) @@ -12,9 +15,11 @@ let rec heuristic_unparse lxp = -> sexp | Builtin ((l,name), _) -> Symbol (l, "##" ^ name) - | Var ((loc, name), _) + | Var ((loc, name), _) -> Symbol (sexp_location loc, maybename name) + (* -> let s = maybename name in - if s = "ℓ" then Inverse_subst.dsinfo else Symbol (sexp_location loc, maybename name) + if s = "ℓ" then Symbol (sexp_location loc, "") else Symbol (sexp_location loc, maybename name) + *) | Proj (l,lxp,(loc,str)) -> Node (Symbol (sexp_location l, "__.__"), [(heuristic_unparse lxp);(Symbol (loc,str))]) @@ -33,22 +38,26 @@ let rec heuristic_unparse lxp = | Arrow (loc, arg_kind, (l, oname), ltp1, ltp2) -> let ut1 = heuristic_unparse ltp1 in - if arg_kind = Aerasable then - Node (Symbol (sexp_location loc, "_≡>_"), - [(match oname with + (match arg_kind with + | Aerasable -> Node (Symbol (sexp_location loc, "_≡>_"), + [(match oname with | None -> ut1 - | Some _v -> Inverse_subst.dsinfo); - heuristic_unparse ltp2]) - else - Node (Symbol (sexp_location loc, match arg_kind with - | Anormal -> "_->_" - | Aimplicit -> "_=>_" - | _ -> "_≡>_"), - [(match oname with - | None -> ut1 (* Inverse_subst.dsinfo *) - | Some v -> Node (Symbol (sexp_location l, "_:_"), - [Symbol (sexp_location l,v); ut1])); - heuristic_unparse ltp2]) + | Some v -> Node (Symbol (sexp_location l, "_:_"), + [Symbol (sexp_location l,v); Symbol (sexp_location l, "?")])); + heuristic_unparse ltp2]) + | Anormal -> Node (Symbol (sexp_location loc, "_->_"), + [(match oname with + | None -> ut1 + | Some v -> Node (Symbol (sexp_location l, "_:_"), + [Symbol (sexp_location l,v); ut1])); + heuristic_unparse ltp2]) + | Aimplicit -> Node (Symbol (sexp_location loc, "_=>_"), + [(match oname with + | None -> ut1 (* Inverse_subst.dsinfo *) + | Some v -> Node (Symbol (sexp_location l, "_:_"), + [Symbol (sexp_location l,v); ut1])); + heuristic_unparse ltp2]) + ) | Let (loc, ldecls, body) -> (* (vdef * lexp * ltype) list *) @@ -145,7 +154,79 @@ let rec heuristic_unparse lxp = | Sort (_l, Stype sl) -> Node (Symbol (lexp_location sl, "##Type_"), [heuristic_unparse sl]) - (* - [let s = heuristic_unparse sl in - if s != l then Inverse_subst.dsinfo else s]) - *) + + +let print_heur_ctx_n (ctx : elab_context) (ranges : (int * int) list) = + print_string (Fmt.make_title " LEXP CONTEXT "); + + Fmt.make_rheader + [(Some ('l', 10), "NAME"); + (Some ('l', 10), "LEXP_UNPARSE"); + (Some ('l', 20), "LEXP"); + (Some ('l', 42), " TYPE")]; + + print_string (Fmt.make_sep '-'); + + let _ = " | | " in + + let print i = + try + let _, name, _lexp, ty = + match env_lookup_by_index i (ectx_to_lctx ctx) with + | ((_, name), LetDef (r, exp), ty) -> r, name, Some exp, ty + | ((_, name), _, ty) -> 0, name, None, ty + in + let name' = maybename name in + let short_name = + if String.length name' > 10 + then + String.sub name' 0 9 ^ "…" + else name' + in + Printf.printf " %-10s || " short_name; + + let res = heuristic_unparse ty in + sexp_print res; + + + Printf.printf " |-->|: "; + + let s = fst (Elab.elaborate ctx res None) in + lexp_print s; + (* + Printf.printf " |--> "; + + lexp_print ty; + print_newline (); + *) + print_newline () + with + | Not_found + -> print_endline " | %-7d | Not_found |" + in + + let rec print_range lower i = + let i' = i - 1 in + if i' >= lower + then + (print i'; + print_range lower i') + in + + let rec print_ranges = function + | [] -> () + | (lower, upper) :: ranges' + -> (print_range lower upper; + print_ranges ranges') + in + + print_ranges ranges; + print_string (Fmt.make_sep '=') + +(* Only print user defined variables *) +let print_heur_ctx (lctx : elab_context) : unit = + print_heur_ctx_n lctx [(0, M.length (ectx_to_lctx lctx) - !builtin_size)] + +(* Dump the whole context *) +let dump_heur_ctx (lctx : elab_context) : unit = + print_heur_ctx_n lctx [(0, M.length (ectx_to_lctx lctx))] ===================================== src/log.ml ===================================== @@ -212,7 +212,7 @@ let show_error (message : string) : unit = let handle_error ~(on_error : unit -> 'a) (action : unit -> 'a) : 'a = try action () with | Stop_compilation message - -> show_error message; + -> show_error ("internal error: " ^ message); on_error () | User_error message -> show_error ("fatal user error: " ^ message); View it on GitLab: https://gitlab.com/monnier/typer/-/commit/366ff7fcae796b0cffcb60508c7071f8b… -- View it on GitLab: https://gitlab.com/monnier/typer/-/commit/366ff7fcae796b0cffcb60508c7071f8b… You're receiving this email because of your account on gitlab.com.

1 0

Commits à réviser
by Simon Génier 28 Aoû '22

28 Aoû '22

Salut, Voici quelques vieux commits à réviser. https://gitlab.com/monnier/typer/-/commit/9e0d8f0885da4337b5c38c45d521108e4… Ce commit ajoute un flag, -Vmacro-expansion, qui demande à Typer d'imprimer le résultat d'expansion de macros sur stdout pendant la compilation. J'ai trouvé ça pratique pour déboguer certain problèmes et je crois que ça pourrait servir à d'autres. https://gitlab.com/monnier/typer/-/commit/11b723953702da0e987fb1beffefa4710… Ce commit ajoute un test de s-expression, mais c'est surtout une excuse pour améliorer les messages d'erreur de ces tests. https://gitlab.com/monnier/typer/-/commit/3c0757d51f0fcbe0d42cbd7183df5bad0… Finalement, ce commit pretty-print le code généré par le backend Gambit. Dites-moi ce que vous en pensez. Simon

2 1

[Git][monnier/typer][main] Pretty-prints the code emitted by the Gambit backend.
by Stefan (＠monnier) 28 Aoû '22

28 Aoû '22

Stefan pushed to branch main at Stefan / Typer Commits: 2a824e2d by Simon Génier at 2022-08-28T22:39:23-04:00 Pretty-prints the code emitted by the Gambit backend. It spawns Gambit as a subprocess and delegates the pretty-printing to it. We only have to worry about emitting valid code. I intend to use the inferior Gambit mechanism to also implement a REPL. - - - - - 5 changed files: - src/dune - src/gambit.ml - + src/pretty-printer.scm - tests/gambit_test.ml - typer.ml Changes: ===================================== src/dune ===================================== @@ -2,4 +2,4 @@ (library (name typerlib) - (libraries zarith str)) + (libraries str unix zarith)) ===================================== src/gambit.ml ===================================== @@ -26,6 +26,8 @@ open Elexp type ldecls = Lexp.ldecls type lexp = Lexp.lexp +let gsc_path : string ref = ref "/usr/local/Gambit/bin/gsc" + module Scm = struct type t = | Symbol of string @@ -74,11 +76,11 @@ module Scm = struct let symbol (name : string) : t = Symbol (escape_symbol name) - let rec string_of_exp (exp : t) : string = + let rec to_string (exp : t) : string = match exp with | Symbol (name) -> name | List (elements) - -> "(" ^ String.concat " " (List.map string_of_exp elements) ^ ")" + -> "(" ^ String.concat " " (List.map to_string elements) ^ ")" | String (value) -> let length = String.length value in let buffer = Buffer.create length in @@ -101,7 +103,7 @@ module Scm = struct | Float (value) -> string_of_float value let print (output : out_channel) (exp : t) : unit = - output_string output (string_of_exp exp); + output_string output (to_string exp); output_char output '\n' let describe (exp : t) : string = @@ -282,6 +284,75 @@ let rec scheme_of_expr (sctx : ScmContext.t) (elexp : elexp) : Scm.t = | _ -> failwith ("[gambit] unsupported elexp: " ^ elexp_string elexp) +class inferior script_path = + let down_reader, down_writer = Unix.pipe ~cloexec:true () in + let up_reader, up_writer = Unix.pipe ~cloexec:true () in + let _ = Unix.clear_close_on_exec down_reader in + let _ = Unix.clear_close_on_exec up_writer in + let pid = + Unix.create_process + !gsc_path + [|!gsc_path; "-i"; "-f"; script_path|] + down_reader + up_writer + Unix.stderr + in + let _ = Unix.close down_reader in + let _ = Unix.close up_writer in + + object (self) + val pid = pid + val writer_fd = down_writer + val reader_fd = up_reader + val short_buffer = Bytes.make 4 '\x00' + + method stop : unit = + Unix.close writer_fd; + let _ = Unix.waitpid [] pid in + Unix.close reader_fd + + method private read_byte : char = + self#read ~size:1 short_buffer; + Bytes.get short_buffer 0 + + method private write_byte (b : char) : unit = + Bytes.set short_buffer 0 b; + self#write ~size:1 short_buffer + + method private read_sized_string : string = + self#read ~size:4 short_buffer; + let size = Int32.to_int (Bytes.get_int32_be short_buffer 0) in + let buffer = Bytes.create size in + self#read ~size buffer; + Bytes.to_string buffer + + method private write_sized_string (string : string) : unit = + let buffer = Bytes.of_string string in + let size = Bytes.length buffer in + Bytes.set_int32_be short_buffer 0 (Int32.of_int size); + self#write ~size:4 short_buffer; + self#write ~size buffer + + method private read ~(size : int) (bytes : Bytes.t) : unit = + let n = ref 0 in + while !n < size do + n := !n + Unix.read reader_fd bytes !n (size - !n) + done + + method private write ~(size : int) (bytes : Bytes.t) : unit = + assert (Unix.write writer_fd bytes 0 size = size) + end + +class pretty_printer = + object (self) + inherit inferior "src/pretty-printer.scm" + + method pp (expr : Scm.t) : string = + let source = Scm.to_string expr in + self#write_sized_string source; + self#read_sized_string + end + let scheme_of_decl (sctx : ScmContext.t) (name, elexp : string * elexp) : Scm.t = Scm.List ([Scm.define; Scm.Symbol name; scheme_of_expr sctx elexp]) @@ -290,13 +361,19 @@ class gambit_compiler lctx output = object val mutable sctx = ScmContext.of_lctx lctx val mutable lctx = lctx + val pretty_printer = new pretty_printer method process_decls ldecls = let lctx', eldecls = Opslexp.clean_decls lctx ldecls in let sctx', eldecls = List.fold_left_map ScmContext.intro_binding sctx eldecls in - let sdecls = Scm.List (Scm.begin' :: List.map (scheme_of_decl sctx') eldecls) in + let sdecls = List.map (scheme_of_decl sctx') eldecls in sctx <- sctx'; lctx <- lctx'; - Scm.print output sdecls; + List.iter + (fun sdecl -> sdecl |> pretty_printer#pp |> output_string output) + sdecls + + method stop = + pretty_printer#stop end ===================================== src/pretty-printer.scm ===================================== @@ -0,0 +1,72 @@ +;;; Copyright (C) 2021-2022 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/>. + +;;; This file implments a simple protocol where Gambit will listen on stdin for +;;; s-expressions and echo the pretty-printed version of the same expression on +;;; stdout. + +;; Read an 8-bit unsigned integer or call the given continuation. +(define (read-u8-or k) + (let ((b (read-u8))) + (if (eof-object? b) (k)) + b)) + +;; Read a 32-bit unsigned integer or call the given continuation. +(define (read-u32be-or k) + (let ((b3 (read-u8-or k)) + (b2 (read-u8-or k)) + (b1 (read-u8-or k)) + (b0 (read-u8-or k))) + (bitwise-ior (arithmetic-shift b3 24) + (arithmetic-shift b2 16) + (arithmetic-shift b1 8) + b0))) + +(define (write-u32be n) + (write-u8 (bitwise-and #xff (arithmetic-shift n -24))) + (write-u8 (bitwise-and #xff (arithmetic-shift n -16))) + (write-u8 (bitwise-and #xff (arithmetic-shift n -8))) + (write-u8 (bitwise-and #xff n))) + +;; Read a string prefixed by its length encoded as a 32-bit unsigned integer. +(define (read-sized-string k) + (let* ((bytes-length (read-u32be-or k)) + (bytes (make-u8vector bytes-length))) + (read-subu8vector bytes 0 bytes-length) + (utf8->string bytes))) + +;; Write a string prefixed by its length encoded as a 32-bit unsigned integer. +(define (write-sized-string string) + (let* ((bytes (string->utf8 string)) + (bytes-length (u8vector-length bytes))) + (write-u32be bytes-length) + (write-subu8vector bytes 0 bytes-length) + (force-output (current-output-port)))) + +(call-with-current-continuation + (lambda (k) + (let loop () + (write-sized-string + (with-output-to-string + (lambda () + (with-input-from-string (read-sized-string k) + (lambda () + (pretty-print (read))))))) + (loop)))) ===================================== tests/gambit_test.ml ===================================== @@ -31,7 +31,7 @@ open Utest_lib open Gambit let fail_on_exp exp = - Printf.printf "in %s\n" (Scm.string_of_exp exp); + Printf.printf "in %s\n" (Scm.to_string exp); false let type_error expected actual = ===================================== typer.ml ===================================== @@ -61,7 +61,10 @@ let compile_main argv = let backend = new Gambit.gambit_compiler (ectx_to_lctx ectx) stdout in let _ = - List.fold_left (Elab.process_file backend) ectx (list_input_files ()) + Fun.protect + ~finally:(fun () -> backend#stop) + (fun () + -> List.fold_left (Elab.process_file backend) ectx (list_input_files ())) in Log.print_log () View it on GitLab: https://gitlab.com/monnier/typer/-/commit/2a824e2d1539ab7a2a4ba998fbb4ac656… -- View it on GitLab: https://gitlab.com/monnier/typer/-/commit/2a824e2d1539ab7a2a4ba998fbb4ac656… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][main] Add a test for type ascription.
by Stefan (＠monnier) 28 Aoû '22

28 Aoû '22

Stefan pushed to branch main at Stefan / Typer Commits: 525e358e by Simon Génier at 2022-08-28T22:37:40-04:00 Add a test for type ascription. Also improve how discrepancies in sexp tests are reported. - - - - - 3 changed files: - src/fmt.ml - tests/sexp_test.ml - tests/utest_lib.ml Changes: ===================================== src/fmt.ml ===================================== @@ -67,12 +67,19 @@ let print_ct_tree i = loop 0 (* Colors *) -let red = "\x1b[31m" -let green = "\x1b[32m" -let yellow = "\x1b[33m" -let magenta = "\x1b[35m" -let cyan = "\x1b[36m" -let reset = "\x1b[0m" +let red_f : _ format6 = "\x1b[31m" +let green_f : _ format6 = "\x1b[32m" +let yellow_f : _ format6 = "\x1b[33m" +let magenta_f : _ format6 = "\x1b[35m" +let cyan_f : _ format6 = "\x1b[36m" +let reset_f : _ format6 = "\x1b[0m" + +let red = string_of_format red_f +let green = string_of_format green_f +let yellow = string_of_format yellow_f +let magenta = string_of_format magenta_f +let cyan = string_of_format cyan_f +let reset = string_of_format reset_f let color_string color str = color ^ str ^ reset ===================================== tests/sexp_test.ml ===================================== @@ -1,3 +1,32 @@ +(* + * Typer Compiler + * + * --------------------------------------------------------------------------- + * + * Copyright (C) 2016-2022 Free Software Foundation, Inc. + * + * 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: + * utest library utility. Tests register themselves + * + * --------------------------------------------------------------------------- *) + open Typerlib open Sexp @@ -30,16 +59,14 @@ let _ = test_sexp_add "x * x * x" (fun ret -> | _ -> failure ) -let test_sexp_eqv dcode1 dcode2 = - add_test "SEXP" dcode1 - (fun () -> - let s1 = sexp_parse_str dcode1 in - let s2 = sexp_parse_str dcode2 in - if sexp_eq_list s1 s2 - then success - else (sexp_print (List.hd s1); - sexp_print (List.hd s2); - failure)) +let test_sexp_eqv ?name actual_source expected_source = + let test () = + let actual = sexp_parse_str actual_source in + let expected = sexp_parse_str expected_source in + expect_equal_sexps ~actual ~expected + in + let name = Option.value ~default:actual_source name in + add_test "SEXP" name test let _ = test_sexp_eqv "((a) ((1.00)))" "a 1.0" let _ = test_sexp_eqv "(x + y)" "_+_ x y" @@ -52,5 +79,11 @@ let _ = test_sexp_eqv "a\\b\\c" "abc" let _ = test_sexp_eqv "(a;b)" "(_\\;_ a b)" let _ = test_sexp_eqv "a.b.c . (.)" "(__\\.__ (__\\.__ a b) c) \\. \\." +let _ = + test_sexp_eqv + ~name:"Type ascription in declaration" + "x = 4 : Int" + "(_=_ x (_:_ 4 Int))" + (* run all tests *) let _ = run_all () ===================================== tests/utest_lib.ml ===================================== @@ -3,7 +3,7 @@ * * --------------------------------------------------------------------------- * - * Copyright (C) 2011-2018 Free Software Foundation, Inc. + * Copyright (C) 2011-2022 Free Software Foundation, Inc. * * Author: Pierre Delaunay <pierre.delaunay(a)hec.ca> * Keywords: languages, lisp, dependent types. @@ -138,6 +138,50 @@ let expect_equal_values = _expect_equal_t Env.value_eq_list print_value_list let expect_equal_lexp = _expect_equal_t Lexp.eq Lexp.lexp_string let expect_conv_lexp ctx = _expect_equal_t (Opslexp.conv_p ctx) Lexp.lexp_string +let expect_equal_sexps ~expected ~actual = + let print_sexp_ok s = + Printf.printf (green_f ^^ "%s" ^^ reset_f ^^ "\n") (Sexp.sexp_string s) + in + + let print_sexp_err expected actual = + Printf.printf + ("Expected:\n" ^^ red_f ^^ "%s\n" ^^ reset_f) + (Sexp.sexp_string expected); + Printf.printf + ("Actual:\n" ^^ red_f ^^ "%s\n" ^^ reset_f) + (Sexp.sexp_string actual) + in + + let rec loop failed fine expected actual = + match expected, actual with + | l :: ll, r :: rr -> + if Sexp.sexp_equal l r + then loop failed (l :: fine) ll rr + else + (List.iter print_sexp_ok fine; + print_sexp_err l r; + loop true [] ll rr) + | _ :: _, [] -> + List.iter print_sexp_ok fine; + Printf.printf ("Missing sexps:\n" ^^ red_f); + List.iter (fun s -> s |> Sexp.sexp_string |> Printf.printf "%s\n") expected; + Printf.printf reset_f; + true + | [], _ :: _ -> + List.iter print_sexp_ok fine; + Printf.printf ("Unexpected sexps:\n" ^^ red_f); + List.iter (fun s -> s |> Sexp.sexp_string |> Printf.printf "%s\n") actual; + Printf.printf reset_f; + true + | [], [] -> + if failed + then List.iter print_sexp_ok fine; + failed + in + if loop false [] expected actual + then failure + else success + let expect_equal_lexps = let rec lexp_list_eq l r = match l, r with View it on GitLab: https://gitlab.com/monnier/typer/-/commit/525e358e957c39ca1acdd429cd978d361… -- View it on GitLab: https://gitlab.com/monnier/typer/-/commit/525e358e957c39ca1acdd429cd978d361… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer] Pushed new branch master
by Stefan (＠monnier) 27 Aoû '22

27 Aoû '22

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

1 0

[Git][monnier/typer] Deleted branch master
by Stefan (＠monnier) 27 Aoû '22

27 Aoû '22

Stefan deleted branch master at Stefan / Typer -- You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][main] 3 commits: Add Zarith dependency to opam file
by Stefan (＠monnier) 27 Aoû '22

27 Aoû '22

Stefan pushed to branch main at Stefan / Typer Commits: 50069ddc by Shon Feder at 2022-03-11T20:42:03-05:00 Add Zarith dependency to opam file Also adds "synopsis" and "description" fields, with content taken from https://www.iro.umontreal.ca/~monnier/ - - - - - 12c08fbb by Shon Feder at 2022-03-11T20:42:03-05:00 Ignore the opam switch directory - - - - - f0551384 by Stefan Monnier at 2022-08-27T14:07:24-04:00 Merge branch 'add-zarith-dependency' into 'main' See merge request monnier/typer!2 - - - - - 2 changed files: - .gitignore - opam Changes: ===================================== .gitignore ===================================== @@ -14,6 +14,9 @@ manual.?? *.info + +# opam switch directory +_opam *_build/ # Random backup/autosave files ===================================== opam ===================================== @@ -4,6 +4,12 @@ version: "0.0.0" maintainer: "Stefan Monnier <monnier(a)iro.umontreal.ca>" authors: "Stefan Monnier <monnier(a)iro.umontreal.ca>, Pierre Delaunay <pierre.delaunay(a)hec.ca>" homepage: "https://gitlab.com/monnier/typer" +synopsis: "ML+Scheme+Coq" +description: " +A programming language of the ML family, but inspired by Scheme's minimalism +and syntactic structure and built on top of a pure λ-calculus with +dependent types, similar to Coq's. +" build: [ [make] ] @@ -12,4 +18,5 @@ install: [make "install"] remove: ["ocamlfind" "remove" "typer"] depends: [ "ocamlfind" {build} + "zarith" {<= "1.12"} ] View it on GitLab: https://gitlab.com/monnier/typer/-/compare/471c1ff66c335f727485e4c54e2096f6… -- View it on GitLab: https://gitlab.com/monnier/typer/-/compare/471c1ff66c335f727485e4c54e2096f6… You're receiving this email because of your account on gitlab.com.

1 0

Branche principale?
by Simon Génier 27 Aoû '22

27 Aoû '22

Salut, Je n'avais pas touché au code de Typer depuis quelque temps et je remarque qu'il y a maintenant une branche main et aussi une branche master qui a été effacée par https://gitlab.com/monnier/typer/-/commit/f1727b0c61b851c1f7f9092b83befee1d… mais ressuscitée par https://gitlab.com/monnier/typer/-/commit/3a9417d8ad5d9375310ffde5e49724711… Laquelle est la vraie branche principale ? Simon

2 1

[Git][monnier/typer][gambit-compiler-pp] 4 commits: Pretty-prints the code emitted by the Gambit backend.
by Simon Génier (＠ilovemonoids) 26 Aoû '22

26 Aoû '22

Simon Génier pushed to branch gambit-compiler-pp at Stefan / Typer Commits: 3c0757d5 by Simon Génier at 2022-08-26T19:39:08-04:00 Pretty-prints the code emitted by the Gambit backend. It spawns Gambit as a subprocess and delegates the pretty-printing to it. We only have to worry about emitting valid code. I intend to use the inferior Gambit mechanism to also implement a REPL. - - - - - 39afb0e6 by Simon Génier at 2022-08-26T19:39:12-04:00 Adds a simplification phase. It β-reduces let bindings when the value bound is a variable or built-in, i.e. when there is - no-side effect - the value is as fast to evaluate as a variable. The hope is that it will help the readability of the code after macro expantion, without have to rewrite every macro to be smart about expanding to let-expressions. - - - - - 67f00808 by Simon Génier at 2022-08-26T19:39:12-04:00 Introduce an Op record to track operators during parsing. This makes explicit the presence or not of rhs and lhs arguments instead of implicitely tracking them via empty symbols. - - - - - 36458e61 by Simon Génier at 2022-08-26T19:39:12-04:00 Move simplification behind a flag. - - - - - 14 changed files: - src/dune - src/elab.ml - src/gambit.ml - src/lexp.ml - + src/pretty-printer.scm - src/sexp.ml - + src/simpl.ml - src/subst.ml - tests/dune - tests/gambit_test.ml - tests/lexp_test.ml - + tests/lexp_test_support.ml - + tests/simpl_test.ml - typer.ml Changes: ===================================== src/dune ===================================== @@ -2,4 +2,4 @@ (library (name typerlib) - (libraries zarith str)) + (libraries str unix zarith)) ===================================== src/elab.ml ===================================== @@ -3,7 +3,7 @@ * * --------------------------------------------------------------------------- * - * Copyright (C) 2011-2021 Free Software Foundation, Inc. + * Copyright (C) 2011-2022 Free Software Foundation, Inc. * * Author: Pierre Delaunay <pierre.delaunay(a)hec.ca> * Keywords: languages, lisp, dependent types. @@ -69,6 +69,7 @@ let parsing_internals = ref false let btl_folder = try Sys.getenv "TYPER_BUILTINS" with Not_found -> "./btl" +let optimize = ref false let fatal ?print_action ?loc fmt = Log.log_fatal ~section:"ELAB" ?print_action ?loc fmt @@ -1997,7 +1998,16 @@ let process_file let pretokens = prelex source in let tokens = lex Grammar.default_stt pretokens in let ldecls, ectx' = lexp_p_decls [] tokens ectx in - List.iter backend#process_decls ldecls; + let simpl_ldecls = + if !optimize + then + let _, ldecls = + List.fold_left_map Simpl.simpl_ldecls Subst.identity ldecls + in + ldecls + else ldecls + in + List.iter backend#process_decls simpl_ldecls; ectx' with | Sys_error _ ===================================== src/gambit.ml ===================================== @@ -26,6 +26,8 @@ open Elexp type ldecls = Lexp.ldecls type lexp = Lexp.lexp +let gsc_path : string ref = ref "/usr/local/Gambit/bin/gsc" + module Scm = struct type t = | Symbol of string @@ -74,11 +76,11 @@ module Scm = struct let symbol (name : string) : t = Symbol (escape_symbol name) - let rec string_of_exp (exp : t) : string = + let rec to_string (exp : t) : string = match exp with | Symbol (name) -> name | List (elements) - -> "(" ^ String.concat " " (List.map string_of_exp elements) ^ ")" + -> "(" ^ String.concat " " (List.map to_string elements) ^ ")" | String (value) -> let length = String.length value in let buffer = Buffer.create length in @@ -101,7 +103,7 @@ module Scm = struct | Float (value) -> string_of_float value let print (output : out_channel) (exp : t) : unit = - output_string output (string_of_exp exp); + output_string output (to_string exp); output_char output '\n' let describe (exp : t) : string = @@ -282,6 +284,75 @@ let rec scheme_of_expr (sctx : ScmContext.t) (elexp : elexp) : Scm.t = | _ -> failwith ("[gambit] unsupported elexp: " ^ elexp_string elexp) +class inferior script_path = + let down_reader, down_writer = Unix.pipe ~cloexec:true () in + let up_reader, up_writer = Unix.pipe ~cloexec:true () in + let _ = Unix.clear_close_on_exec down_reader in + let _ = Unix.clear_close_on_exec up_writer in + let pid = + Unix.create_process + !gsc_path + [|!gsc_path; "-i"; "-f"; script_path|] + down_reader + up_writer + Unix.stderr + in + let _ = Unix.close down_reader in + let _ = Unix.close up_writer in + + object (self) + val pid = pid + val writer_fd = down_writer + val reader_fd = up_reader + val short_buffer = Bytes.make 4 '\x00' + + method stop : unit = + Unix.close writer_fd; + let _ = Unix.waitpid [] pid in + Unix.close reader_fd + + method private read_byte : char = + self#read ~size:1 short_buffer; + Bytes.get short_buffer 0 + + method private write_byte (b : char) : unit = + Bytes.set short_buffer 0 b; + self#write ~size:1 short_buffer + + method private read_sized_string : string = + self#read ~size:4 short_buffer; + let size = Int32.to_int (Bytes.get_int32_be short_buffer 0) in + let buffer = Bytes.create size in + self#read ~size buffer; + Bytes.to_string buffer + + method private write_sized_string (string : string) : unit = + let buffer = Bytes.of_string string in + let size = Bytes.length buffer in + Bytes.set_int32_be short_buffer 0 (Int32.of_int size); + self#write ~size:4 short_buffer; + self#write ~size buffer + + method private read ~(size : int) (bytes : Bytes.t) : unit = + let n = ref 0 in + while !n < size do + n := !n + Unix.read reader_fd bytes !n (size - !n) + done + + method private write ~(size : int) (bytes : Bytes.t) : unit = + assert (Unix.write writer_fd bytes 0 size = size) + end + +class pretty_printer = + object (self) + inherit inferior "src/pretty-printer.scm" + + method pp (expr : Scm.t) : string = + let source = Scm.to_string expr in + self#write_sized_string source; + self#read_sized_string + end + let scheme_of_decl (sctx : ScmContext.t) (name, elexp : string * elexp) : Scm.t = Scm.List ([Scm.define; Scm.Symbol name; scheme_of_expr sctx elexp]) @@ -290,13 +361,19 @@ class gambit_compiler lctx output = object val mutable sctx = ScmContext.of_lctx lctx val mutable lctx = lctx + val pretty_printer = new pretty_printer method process_decls ldecls = let lctx', eldecls = Opslexp.clean_decls lctx ldecls in let sctx', eldecls = List.fold_left_map ScmContext.intro_binding sctx eldecls in - let sdecls = Scm.List (Scm.begin' :: List.map (scheme_of_decl sctx') eldecls) in + let sdecls = List.map (scheme_of_decl sctx') eldecls in sctx <- sctx'; lctx <- lctx'; - Scm.print output sdecls; + List.iter + (fun sdecl -> sdecl |> pretty_printer#pp |> output_string output) + sdecls + + method stop = + pretty_printer#stop end ===================================== src/lexp.ml ===================================== @@ -1,6 +1,6 @@ (* lexp.ml --- Lambda-expressions: the core language. -Copyright (C) 2011-2021 Free Software Foundation, Inc. +Copyright (C) 2011-2022 Free Software Foundation, Inc. Author: Stefan Monnier <monnier(a)iro.umontreal.ca> Keywords: languages, lisp, dependent types. @@ -20,6 +20,8 @@ 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 Printf + module U = Util module L = List module SMap = U.SMap @@ -478,8 +480,6 @@ let rec sunshift n = else (assert (n >= 0); S.cons impossible (sunshift (n - 1))) -let _ = assert (S.identity_p (scompose (S.shift 5) (sunshift 5))) - (* The quick test below seemed to indicate that about 50% of the "sink"s * are applied on top of another "sink" and hence could be combined into * a single "Lift^n" constructor. Doesn't seem high enough to justify @@ -789,11 +789,10 @@ let rec lexp_unparse lxp = (* FIXME: ¡Unify lexp_print and lexp_string! *) and lexp_string lxp = sexp_string (lexp_unparse lxp) -and subst_string s = match s with - | S.Identity o -> "↑" ^ string_of_int o - | S.Cons (l, s, 0) -> lexp_name l ^ " · " ^ subst_string s - | S.Cons (l, s, o) - -> "(↑"^ string_of_int o ^ " " ^ subst_string (S.cons l s) ^ ")" +and subst_string = function + | S.Identity o -> sprintf "↑%d" o + | S.Cons (l, s, 0) -> sprintf "%s · %s" (lexp_name l) (subst_string s) + | S.Cons (l, s, o) -> sprintf "(↑%d %s)" o (subst_string (S.cons l s)) and lexp_name e = match lexp_lexp' e with ===================================== src/pretty-printer.scm ===================================== @@ -0,0 +1,72 @@ +;;; Copyright (C) 2021-2022 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/>. + +;;; This file implments a simple protocol where Gambit will listen on stdin for +;;; s-expressions and echo the pretty-printed version of the same expression on +;;; stdout. + +;; Read an 8-bit unsigned integer or call the given continuation. +(define (read-u8-or k) + (let ((b (read-u8))) + (if (eof-object? b) (k)) + b)) + +;; Read a 32-bit unsigned integer or call the given continuation. +(define (read-u32be-or k) + (let ((b3 (read-u8-or k)) + (b2 (read-u8-or k)) + (b1 (read-u8-or k)) + (b0 (read-u8-or k))) + (bitwise-ior (arithmetic-shift b3 24) + (arithmetic-shift b2 16) + (arithmetic-shift b1 8) + b0))) + +(define (write-u32be n) + (write-u8 (bitwise-and #xff (arithmetic-shift n -24))) + (write-u8 (bitwise-and #xff (arithmetic-shift n -16))) + (write-u8 (bitwise-and #xff (arithmetic-shift n -8))) + (write-u8 (bitwise-and #xff n))) + +;; Read a string prefixed by its length encoded as a 32-bit unsigned integer. +(define (read-sized-string k) + (let* ((bytes-length (read-u32be-or k)) + (bytes (make-u8vector bytes-length))) + (read-subu8vector bytes 0 bytes-length) + (utf8->string bytes))) + +;; Write a string prefixed by its length encoded as a 32-bit unsigned integer. +(define (write-sized-string string) + (let* ((bytes (string->utf8 string)) + (bytes-length (u8vector-length bytes))) + (write-u32be bytes-length) + (write-subu8vector bytes 0 bytes-length) + (force-output (current-output-port)))) + +(call-with-current-continuation + (lambda (k) + (let loop () + (write-sized-string + (with-output-to-string + (lambda () + (with-input-from-string (read-sized-string k) + (lambda () + (pretty-print (read))))))) + (loop)))) ===================================== src/sexp.ml ===================================== @@ -23,6 +23,7 @@ this program. If not, see <http://www.gnu.org/licenses/>. *) open Util open Prelexer open Grammar +open Printf let sexp_error ?print_action loc fmt = Log.log_error ~section:"SEXP" ?print_action ~loc fmt @@ -121,6 +122,61 @@ let sexp_name s = * as appropriate. *) let empty_args_are_not_args = false +module Op = struct + type t = + { head : symbol + ; parts_rev : string list + ; lhs_p : bool + ; rhs_p : bool + } + + let null : t = + { head = (Source.Location.dummy, "") + ; parts_rev = [] + ; lhs_p = false + ; rhs_p = false + } + + let prefix (head : symbol) : t = + {head; parts_rev = []; lhs_p = false; rhs_p = true} + + let postfix (head : symbol) : t = + {head; parts_rev = []; lhs_p = true; rhs_p = false} + + let infix (head : symbol) : t = + {head; parts_rev = []; lhs_p = true; rhs_p = true} + + let compose ({head; parts_rev; lhs_p; rhs_p} : t): symbol = + let (location, head_name) = head in + let name = String.concat "_" (head_name :: List.rev parts_rev) in + let name = + match lhs_p, rhs_p with + | false, false -> name + | false, true -> sprintf "%s_" name + | true, false -> sprintf "_%s" name + | true, true -> sprintf "_%s_" name + in + (location, name) + + let mark_rhs (op : t) : t = + match op.head with + | (_, "") -> op + | _ -> {op with rhs_p = true} + + let push_inner (op : t) (part : string) : t = + let last_name = + match op.parts_rev with + | [] -> snd op.head + | last_name :: _ -> last_name + in + if String.equal part last_name + then op + else {op with parts_rev = part :: op.parts_rev} + + let push_closer (op : t) (part : string) : t = + {op with parts_rev = part :: op.parts_rev; rhs_p = false} +end + (* `op' is the operator being parsed. E.g. for let...in... * it would be either ["let"] or ["in";"let"] depending on which * part we've parsed already. @@ -128,95 +184,104 @@ let empty_args_are_not_args = false * `rargs' are the sexps that compose the arg to the right of the latest * infix symbol. They may belong to `op' or to a later infix operator * we haven't seen yet which binds more tightly. *) -let rec sexp_parse (g : grammar) (rest : sexp list) - (level : int) - (op : symbol list) - (largs : sexp list) - (rargs : sexp list) +let rec sexp_parse + (g : grammar) + (rest : sexp list) + (level : int) + (op : Op.t) + (largs : sexp list) + (rargs : sexp list) : (sexp * sexp list) = - let sexp_parse = sexp_parse g in - let compose_symbol (ss : symbol list) = match ss with - | [] -> (Log.internal_error "empty operator!") - | (l,_)::_ -> (l, String.concat "_" (List.map (fun (_,s) -> s) - (List.rev ss))) in + let sexp_parse = sexp_parse g in - let push_largs largs rargs closer = match List.rev rargs with - | [] -> if closer then dummy_epsilon :: largs else largs - | e::es -> (match es with [] -> e | _ -> Node (e, es)) :: largs in + let push_largs largs rargs closer = + match List.rev rargs with + | [] -> if closer then dummy_epsilon :: largs else largs + | e::es -> (match es with [] -> e | _ -> Node (e, es)) :: largs + in let mk_node op largs rargs closer = let args = List.rev (push_largs largs rargs closer) in - match op with - | [] -> (match args with [] -> dummy_epsilon - | [e] -> e - | e::es -> Node (e, es)) - | ss -> let headname = compose_symbol ss in - match (headname, args) with - (* FIXME: While it's uaulyl good to strip away parens, - * this makes assumptions about the grammar (i.e. there's - * a rule « exp ::= '(' exp ')' » ), and this is sometimes - * not desired (e.g. to distinguish "a b ⊢ c d" from - * "(a b) ⊢ (c d)"). *) - | ((_,"(_)"), [arg]) -> arg (* Strip away parens. *) - | _ -> Node (hSymbol (headname), args) in + let headname = Op.compose op in + match (headname, args) with + (* FIXME: While it's usually good to strip away parens, this makes + assumptions about the grammar (i.e. there's a rule + « exp ::= '(' exp ')' »), and this is sometimes not desired (e.g. to + distinguish "a b ⊢ c d" from "(a b) ⊢ (c d)"). *) + | (_, "(_)"), [arg] -> arg + | _ -> Node (hSymbol (headname), args) + in match rest with - | (((Symbol ((l,name) as s)) as e)::rest') -> - (try match SMap.find name g with - | (None, None) -> sexp_parse rest' level op largs (e::rargs) - | (None, Some rl) (* Open paren or prefix. *) - -> let (e, rest) = sexp_parse rest' rl [s] [] [] - in sexp_parse rest level op largs (e::rargs) - | (Some ll, _) when ll < level - (* A symbol that closes the currently parsed element. *) - -> ((if empty_args_are_not_args then - mk_node (match rargs with [] -> op | _ -> ((l,"")::op)) - largs rargs false - else - mk_node ((l,"")::op) largs rargs true), - rest) - | (Some ll, None) when ll > level - (* A closer without matching opener or a postfix symbol - that binds very tightly. Previously, we signaled an - error (assuming the former), but it prevented the use - tightly binding postfix operators. - - For example, it signaled spurious errors when parsing - expressions with a tightly binding postfix # operator - that implemented record construction by taking an - inductive as argument and returning the inductive's only - constructor. *) - -> sexp_parse rest' level op largs - [mk_node [(l,name);(l,"")] [] rargs true] - | (Some ll, Some rl) when ll > level - (* A new infix which binds more tightly, i.e. does not close - * the current `op' but takes its `rargs' instead. *) - -> let (e, rest) - = if empty_args_are_not_args then - sexp_parse rest' rl - (match rargs with [] -> [s] | _ -> [s;(l,"")]) - (push_largs [] rargs false) [] - else - sexp_parse rest' rl [s;(l,"")] - (push_largs [] rargs true) [] - in sexp_parse rest level op largs [e] - | (Some ll, Some rl) - -> sexp_parse rest' rl - (if ll == rl - && match op with (_,name')::_ -> name = name' - | _ -> false - then op else (s::op)) - (push_largs largs rargs true) [] - | (Some _ll, None) - -> (mk_node (s::op) largs rargs true, rest') - with Not_found -> - sexp_parse rest' level op largs (e::rargs)) - | e::rest -> sexp_parse rest level op largs (e::rargs) - | [] -> (mk_node (match rargs with [] -> op - | _ -> ((dummy_location,"")::op)) - largs rargs false, - []) + | Symbol (_, name as s) as e :: rest' -> + + begin match SMap.find name g with + | (None, None) -> + sexp_parse rest' level op largs (e :: rargs) + + | (None, Some rl) -> + (* Open paren or prefix. *) + let e, rest'' = + sexp_parse rest' rl (Op.prefix s) [] [] + in + sexp_parse rest'' level op largs (e :: rargs) + + | (Some ll, _) when ll < level -> + (* A symbol that closes the currently parsed element. *) + let op' = + match rargs with + | [] when empty_args_are_not_args -> op + | _ -> Op.mark_rhs op + in + mk_node op' largs rargs (not empty_args_are_not_args), rest + + | (Some ll, None) when ll > level -> + (* A closer without matching opener or a postfix symbol that binds very + tightly. Previously, we signaled an error (assuming the former), but + it prevented the use tightly binding postfix operators. + + For example, it signaled spurious errors when parsing expressions + with a tightly binding postfix # operator that implemented record + construction by taking an inductive as argument and returning the + inductive's only constructor. *) + let rargs' = [mk_node (Op.postfix s) [] rargs true] in + sexp_parse rest' level op largs rargs' + + | (Some ll, Some rl) when ll > level -> + (* A new infix which binds more tightly, i.e. does not close the current + `op' but takes its `rargs' instead. *) + let op' = + match rargs with + | [] when empty_args_are_not_args -> Op.prefix s + | _ -> Op.infix s + in + let e, rest'' = + sexp_parse rest' rl op' (push_largs [] rargs (not empty_args_are_not_args)) [] + in + sexp_parse rest'' level op largs [e] + + | (Some ll, Some rl) -> + let op' = if ll = rl then op else Op.push_inner op name in + sexp_parse rest' rl op' (push_largs largs rargs true) [] + + | (Some _ll, None) -> + (* Either a lone postfix or the closer of a mixfix operator. *) + mk_node (Op.push_closer op name) largs rargs true, rest' + + | exception Not_found -> + sexp_parse rest' level op largs (e :: rargs) + end + + | e :: rest -> sexp_parse rest level op largs (e :: rargs) + + | [] -> + let op' = + match rargs with + | [] -> op + | _ -> Op.mark_rhs op + in + mk_node op' largs rargs false, [] let sexp_parse_all grm tokens limit : sexp * token list = let level = match limit with @@ -225,18 +290,21 @@ let sexp_parse_all grm tokens limit : sexp * token list = match SMap.find token grm with | (Some ll, Some _) -> ll + 1 | _ -> Log.internal_error {|Can't find level of "%s"|} token - in let (e, rest) = sexp_parse grm tokens level [] [] [] in - let se = match e with - | Node (Symbol (_, ""), [e]) -> e - | Node (Symbol (_, ""), e::es) -> Node (e, es) - | _ -> (Log.internal_error "Didn't find a toplevel") in - match rest with - | [] -> (se,rest) - | Symbol (l,t) :: rest - -> if not (Some t = limit) - then sexp_error l {|Stray closing token: "%s"|} t; - (se,rest) - | _ -> (Log.internal_error "Stopped parsing before the end!") + in + let e, rest = sexp_parse grm tokens level Op.null [] [] in + let se = + match e with + | Node (Symbol (_, ""), [e]) -> e + | Node (Symbol (_, ""), e::es) -> Node (e, es) + | _ -> Log.internal_error {|Didn't find a toplevel, got: "%s"|} (sexp_string e) + in + match rest with + | [] -> (se,rest) + | Symbol (l,t) :: rest + -> if not (Some t = limit) + then sexp_error l {|Stray closing token: "%s"|} t; + (se,rest) + | _ -> Log.internal_error "Stopped parsing before the end!" (* "sexp_p" is for "parsing" and "sexp_u" is for "unparsing". *) ===================================== src/simpl.ml ===================================== @@ -0,0 +1,164 @@ +(* Copyright (C) 2022 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/>. *) + +(** A simplification pass for lexps. It β-reduces let bindings of variables and + builtins. For example, let a = b in a + b + c becomes b + b + c. + + The reason to have such a pass is not so much for performance, but to allow + us to write any macro naively, i.e. we can introduce binding in macros + without fear of “polluting” the generated code. *) + +open Lexp + +(* The secret with the simplification phase is to compute the right + substitution. In the case of a single binding, the correct substitution is + a#1 · ↑1, i.e. replace b#0 with a#1, then shift the rest of the + environment by 1 to account for the sigle remaining binding. + + let a = 1 in let a = 1 in + let b = a[1] in + a[1] + b[0] a[0] + a[0] + + For multiple non-recursive bindings, the situation is similar. In this + example, the substitution is a#2 · b#1 · ↑1, which has the same kind of + substitution for our inlined variable, followed by the identity substitution + of b#1 to b#1, and finally the shift. + + let a = 1 in let a = 1 in + let let + b = 2 b = 2 + c = a[2] + in in + b[1] + c[0] b[0] + a[1] + + What about recursive bindings? We simply don't bother with them! + + *) + +type action = + | Id of vname * int + | SubstVar of vname * int + | SubstConst of lexp + +let compute_subst (min_index : int) (ldecls : ldecls) (subst : subst) : subst = + let loop (name, lexp, _) (actions, i, removed) = + let action, removed = + match lexp with + | Lexp.Var (name, index), _ when index >= min_index + -> SubstVar (name, index), removed + 1 + | Lexp.Builtin _, _ | Lexp.Imm _, _ + -> SubstConst lexp, removed + 1 + | _ + -> Id (name, i), removed + in + action :: actions, i + 1, removed + in + let actions, total, removed = List.fold_right loop ldecls ([], 0, 0) in + let lexps = + let lexp_of_action = function + | Id (name, index) -> Lexp.mkVar (name, index) + | SubstVar (name, index) -> Lexp.mkVar (name, index - removed) + | SubstConst (lexp) -> lexp + in + List.map lexp_of_action actions + in + scompose + (List.fold_left + (fun s e -> Subst.cons e s) + (Subst.shift (total - removed)) + lexps) + subst + +let rec simpl_lexp + (subst : subst) + (lexp : lexp) + : lexp = + + match lexp with + | Lexp.Let (location, ldecls, body), _ + -> let subst', ldecls' = simpl_ldecls subst ldecls in + let body' = simpl_lexp subst' body in + begin match ldecls' with + | [] -> body' + | _ -> Lexp.mkLet (location, ldecls', body') + end + + | Lexp.Lambda (kind, arg_name, arg_ty, body), _ + -> let subst' = ssink arg_name subst in + let body' = simpl_lexp subst' body in + Lexp.mkLambda (kind, arg_name, arg_ty, body') + + | Lexp.Call (head, tail), _ + -> let head' = simpl_lexp subst head in + let tail' = + List.map + (fun (kind, value) -> kind, simpl_lexp subst value) + tail + in + Lexp.mkCall (head', tail') + + | Lexp.Case (location, subject, ty, branches, default), _ + -> let simpl_branch (location, names, body) = + let branch_subst = + ssink + (Source.Location.dummy, None) + (List.fold_left + (fun subst' (_, name) -> ssink name subst') + subst + names) + in + let body' = simpl_lexp branch_subst body in + location, names, body' + in + + let simpl_default (name, body) = + let subst' = ssink name subst in + let body' = simpl_lexp subst' body in + name, body' + in + + let subject' = simpl_lexp subst subject in + let branches' = SMap.map simpl_branch branches in + let default' = Option.map simpl_default default in + Lexp.mkCase (location, subject', ty, branches', default') + + | _ -> mkSusp lexp subst + +and simpl_ldecl + (min_index : int) + (subst : subst) + (ldecls : ldecls) + (name, lexp, ty: ldecl) + : ldecls = + + match lexp with + | Lexp.Var (_, index), _ when index >= min_index -> ldecls + | Lexp.Builtin _, _ | Lexp.Imm _, _ -> ldecls + | _ -> (name, mkSusp lexp subst, ty) :: ldecls + +and simpl_ldecls + (subst : subst) + (ldecls : ldecls) + : subst * ldecls = + + let min_index = List.length ldecls in + let subst' = compute_subst min_index ldecls subst in + let ldecls' = List.fold_left (simpl_ldecl min_index subst') [] ldecls in + subst', List.rev ldecls' ===================================== src/subst.ml ===================================== @@ -1,6 +1,6 @@ (* subst.ml --- Substitutions for Lexp -Copyright (C) 2016-2019 Free Software Foundation, Inc. +Copyright (C) 2016-2022 Free Software Foundation, Inc. Author: Stefan Monnier <monnier(a)iro.umontreal.ca> @@ -60,7 +60,7 @@ module U = Util * e[s] % Application of a substitution * * s ::= id % identity substitution - * e . s % replace #0 with `e` and use `s` for the rest + * e · s % replace #0 with `e` and use `s` for the rest * s₁ ∘ s₂ % Composition (apply s₁ *first* and then s₂!). * ↑ % dbi_index = dbi_index + 1 * @@ -72,7 +72,7 @@ module U = Util * e[s] % Application of a substitution * * s ::= id % identity substitution - * e . s % replace #0 by `e` and use `s` for the rest + * e · s % replace #0 by `e` and use `s` for the rest * s ↑n % like Abadi's "s ∘ (↑ⁿ)" * * And the composition ∘ is defined as a function rather than a constructor. @@ -148,7 +148,7 @@ let lookup (mkVar : 'b -> db_index -> 'a) else mkShift e o in lookup' 0 s v -let mkShift s (m:db_offset) = +let mkShift (s : 'a subst) (m : db_offset) : 'a subst = if m>0 then match s with Identity o -> Identity (o + m) | Cons (e, s, o) -> Cons (e, s, o + m) @@ -194,7 +194,7 @@ let compose (mkSusp : 'a -> 'a subst -> 'a) -> (* Myers's fastlane: * if o1 >= sk2 then compose_cons (o1 - sk1) s2' (o + o2') *) if o1 > 0 then compose_cons (o1 - 1) s2 (o + o2) - else + else (* Pull out o2's shift and compose the two Cons. *) let s' = cons e2 s2 in Cons (mkSusp e1 s', compose' s1 s', o + o2) ===================================== tests/dune ===================================== @@ -11,6 +11,7 @@ macro_test positivity_test sexp_test + simpl_test unify_test) (deps (alias %{project_root}/btl/typer_stdlib)) (libraries typerlib) ===================================== tests/gambit_test.ml ===================================== @@ -31,7 +31,7 @@ open Utest_lib open Gambit let fail_on_exp exp = - Printf.printf "in %s\n" (Scm.string_of_exp exp); + Printf.printf "in %s\n" (Scm.to_string exp); false let type_error expected actual = ===================================== tests/lexp_test.ml ===================================== @@ -3,7 +3,7 @@ * * --------------------------------------------------------------------------- * - * Copyright (C) 2011-2017 Free Software Foundation, Inc. + * Copyright (C) 2011-2022 Free Software Foundation, Inc. * * Author: Pierre Delaunay <pierre.delaunay(a)hec.ca> * Keywords: languages, lisp, dependent types. @@ -26,92 +26,36 @@ * --------------------------------------------------------------------------- *) open Typerlib - open Utest_lib +open Lexp_test_support +open Lexp -(* default environment *) let ectx = Elab.default_ectx let rctx = Elab.default_rctx -(* -let _ = (add_test "LEXP" "lexp_print" (fun () -> - - let dcode = " -sqr : (x : Int) -> Int; -sqr = lambda (x : Int) -> - (x * x); - -cube : (x : Int) -> Int; -cube = lambda (x : Int) -> - (x * (sqr x)); - -mult : (x : Int) -> (y : Int) -> Int; -mult = lambda (x : Int) -> - lambda (y : Int) -> - (x * y); - -twice : (y : Int) -> Int; -twice = (mult 2); - -let_fun : (x : Int) -> Int; -let_fun = lambda (x : Int) -> - let a : Int; - a = (twice x); in - let b : Int; - b = (mult 2 x); in - (a + b);" in - - let ret1, _ = lexp_decl_str dcode ectx in - - let to_str decls = - let str = _lexp_str_decls pretty_ppctx (List.flatten ret1) in - List.fold_left (fun str lxp -> str ^ "\n" ^ lxp) "" str in - - (* Cast to string *) - let str1 = (to_str ret1) ^ "\n" in - - print_string str1; - - (* read code again *) - let ret2, _ = lexp_decl_str str1 ectx in - - (* Cast to string *) - let str2 = to_str ret2 in - - if str1 = str2 then success () else failure () -)) *) - -(* -let set_to_list s = - StringSet.fold (fun g a -> g::a) s [] - -let _ = (add_test "LEXP" "Free Variable" (fun () -> - - let dcode = " - a = 2; - b = 3; - f = lambda n -> (a + n); % a is a fv - g = lambda x -> ((f b) + a + x); % f,a,b are fv - " in - - let ret = pexp_decl_str dcode in - let g = match List.rev ret with - | (_, g, _)::_ -> g - | _ -> raise (Unexpected_result "Unexpected empty list") in - - let (bound, free) = free_variable g in - - let bound = set_to_list bound in - let (free, _) = free in - - match bound with - | ["x"] ->( - match free with - | ["_+_"; "f"; "b"; "a"] -> success () - | _ -> failure ()) - | _ -> failure () - -)) *) +let test_lexp name actual expected = + let test () = + let result = expect_equal_lexps [actual] [expected] in + if result = Utest_lib.failure + then Log.print_log () + else Log.clear_log (); + result + in + add_test "LEXP" name test + +let () = + let subst = Subst.cons (make_var 0 "a") Subst.identity in + test_lexp + "Substitute variable" + (Lexp.clean (Lexp.mkSusp (make_var 0 "b") subst)) + (make_var 0 "a") + +let () = + let test () = + if Subst.identity_p (scompose (Subst.shift 5) (sunshift 5)) + then Utest_lib.success + else Utest_lib.failure + in + add_test "LEXP" "unshifts are cancelled by shifts" test -(* run all tests *) let _ = run_all () ===================================== tests/lexp_test_support.ml ===================================== @@ -0,0 +1,45 @@ +(* Copyright (C) 2022 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/>. *) + +open Typerlib + +let make_int i = + Lexp.mkImm (Sexp.Integer (Source.Location.dummy, Z.of_int i)) + +let make_sym name = + (Source.Location.dummy, name) + +let make_name name = + (Source.Location.dummy, Some name) + +let make_var index name = + Lexp.mkVar ((Source.Location.dummy, Some name), index) + +let make_builtin name ty = + Lexp.mkBuiltin (name, ty) + +let make_let decls body = + Lexp.mkLet (Source.Location.dummy, decls, body) + +let make_call head args = + Lexp.mkCall (head, List.map (fun arg -> Pexp.Anormal, arg) args) + +let make_1_plus_2 plus_index = + make_call (make_var plus_index "_+_") [make_int 1; make_int 2] ===================================== tests/simpl_test.ml ===================================== @@ -0,0 +1,103 @@ +(* Copyright (C) 2022 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/>. *) + +open Typerlib +open Utest_lib +open Debruijn +open Lexp_test_support + +let test_simpl name original expected = + let test () = + let actual = Simpl.simpl_lexp Subst.identity original in + let result = expect_equal_lexps [actual] [expected] in + if result = Utest_lib.failure + then Log.print_log () + else Log.clear_log (); + result + in + add_test "SIMPL" name test + +let () = + test_simpl + "single let of variable is eliminated" + (make_let [make_name "x", make_var 1 "y", type_int] (make_var 0 "x")) + (make_var 0 "y") + +let () = + test_simpl + "single let of builtin is eliminated" + (make_let + [make_name "x", make_builtin (make_sym "Int") type_int, type0] + (make_var 0 "x")) + (make_builtin (make_sym "Int") type0) + +let () = + test_simpl + "single let of int eliminated" + (make_let + [make_name "x", make_int 3, type_int] + (make_var 0 "x")) + (make_int 3) + +let () = + test_simpl + "first let is eliminated" + (make_let + [make_name "x", make_var 2 "y", type_int; + make_name "z", make_1_plus_2 40, type_int] + (make_var 1 "x")) + (make_let + [make_name "z", make_1_plus_2 39, type_int] + (make_var 1 "y")) + +let () = + test_simpl + "last let is eliminated" + (make_let + [make_name "z", make_1_plus_2 40, type_int; + make_name "x", make_var 2 "y", type_int] + (make_var 0 "x")) + (make_let + [make_name "z", make_1_plus_2 39, type_int] + (make_var 1 "y")) + +let () = + test_simpl + "preserves recursive variables" + (make_let + [make_name "x", make_var 0 "y", type_int; + make_name "y", make_var 1 "x", type_int] + (make_int 5)) + (make_let + [make_name "x", make_var 0 "y", type_int; + make_name "y", make_var 1 "x", type_int] + (make_int 5)) + +let () = + test_simpl + "simplification is transitive" + (make_let + [make_name "x", make_int 55, type_int] + (make_let + [make_name "y", make_var 1 "x", type_int] + (make_var 0 "y"))) + (make_int 55) + +let () = run_all () ===================================== typer.ml ===================================== @@ -45,6 +45,10 @@ let arg_defs = ("-Vmacro-expansion", Arg.Set Elab.macro_tracing_enabled, "Trace macro expansion"); + + ("-O", + Arg.Set Elab.optimize, + "Enable a simplification phase"); ] let parse_args argv usage = @@ -61,7 +65,10 @@ let compile_main argv = let backend = new Gambit.gambit_compiler (ectx_to_lctx ectx) stdout in let _ = - List.fold_left (Elab.process_file backend) ectx (list_input_files ()) + Fun.protect + ~finally:(fun () -> backend#stop) + (fun () + -> List.fold_left (Elab.process_file backend) ectx (list_input_files ())) in Log.print_log () View it on GitLab: https://gitlab.com/monnier/typer/-/compare/5c703342cab2d47bc36ca6f4ababae67… -- View it on GitLab: https://gitlab.com/monnier/typer/-/compare/5c703342cab2d47bc36ca6f4ababae67… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][gambit-compiler-pp] 5 commits: Add a test for type ascription.
by Simon Génier (＠ilovemonoids) 26 Aoû '22

26 Aoû '22

Simon Génier pushed to branch gambit-compiler-pp at Stefan / Typer Commits: 11b72395 by Simon Génier at 2022-08-26T19:24:09-04:00 Add a test for type ascription. Also improve how discrepancies in sexp tests are reported. - - - - - d05e7b22 by Simon Génier at 2022-08-26T19:24:11-04:00 Pretty-prints the code emitted by the Gambit backend. It spawns Gambit as a subprocess and delegates the pretty-printing to it. We only have to worry about emitting valid code. I intend to use the inferior Gambit mechanism to also implement a REPL. - - - - - 87ee0909 by Simon Génier at 2022-08-26T19:24:11-04:00 Adds a simplification phase. It β-reduces let bindings when the value bound is a variable or built-in, i.e. when there is - no-side effect - the value is as fast to evaluate as a variable. The hope is that it will help the readability of the code after macro expantion, without have to rewrite every macro to be smart about expanding to let-expressions. - - - - - 9297a354 by Simon Génier at 2022-08-26T19:24:11-04:00 Introduce an Op record to track operators during parsing. This makes explicit the presence or not of rhs and lhs arguments instead of implicitely tracking them via empty symbols. - - - - - 5c703342 by Simon Génier at 2022-08-26T19:24:11-04:00 Move simplification behind a flag. - - - - - 17 changed files: - src/dune - src/elab.ml - src/fmt.ml - src/gambit.ml - src/lexp.ml - + src/pretty-printer.scm - src/sexp.ml - + src/simpl.ml - src/subst.ml - tests/dune - tests/gambit_test.ml - tests/lexp_test.ml - + tests/lexp_test_support.ml - tests/sexp_test.ml - + tests/simpl_test.ml - tests/utest_lib.ml - typer.ml Changes: ===================================== src/dune ===================================== @@ -2,4 +2,4 @@ (library (name typerlib) - (libraries zarith str)) + (libraries str unix zarith)) ===================================== src/elab.ml ===================================== @@ -3,7 +3,7 @@ * * --------------------------------------------------------------------------- * - * Copyright (C) 2011-2021 Free Software Foundation, Inc. + * Copyright (C) 2011-2022 Free Software Foundation, Inc. * * Author: Pierre Delaunay <pierre.delaunay(a)hec.ca> * Keywords: languages, lisp, dependent types. @@ -69,6 +69,7 @@ let parsing_internals = ref false let btl_folder = try Sys.getenv "TYPER_BUILTINS" with Not_found -> "./btl" +let optimize = ref false let fatal ?print_action ?loc fmt = Log.log_fatal ~section:"ELAB" ?print_action ?loc fmt @@ -1997,7 +1998,16 @@ let process_file let pretokens = prelex source in let tokens = lex Grammar.default_stt pretokens in let ldecls, ectx' = lexp_p_decls [] tokens ectx in - List.iter backend#process_decls ldecls; + let simpl_ldecls = + if !optimize + then + let _, ldecls = + List.fold_left_map Simpl.simpl_ldecls Subst.identity ldecls + in + ldecls + else ldecls + in + List.iter backend#process_decls simpl_ldecls; ectx' with | Sys_error _ ===================================== src/fmt.ml ===================================== @@ -67,12 +67,19 @@ let print_ct_tree i = loop 0 (* Colors *) -let red = "\x1b[31m" -let green = "\x1b[32m" -let yellow = "\x1b[33m" -let magenta = "\x1b[35m" -let cyan = "\x1b[36m" -let reset = "\x1b[0m" +let red_f : _ format6 = "\x1b[31m" +let green_f : _ format6 = "\x1b[32m" +let yellow_f : _ format6 = "\x1b[33m" +let magenta_f : _ format6 = "\x1b[35m" +let cyan_f : _ format6 = "\x1b[36m" +let reset_f : _ format6 = "\x1b[0m" + +let red = string_of_format red_f +let green = string_of_format green_f +let yellow = string_of_format yellow_f +let magenta = string_of_format magenta_f +let cyan = string_of_format cyan_f +let reset = string_of_format reset_f let color_string color str = color ^ str ^ reset ===================================== src/gambit.ml ===================================== @@ -26,6 +26,8 @@ open Elexp type ldecls = Lexp.ldecls type lexp = Lexp.lexp +let gsc_path : string ref = ref "/usr/local/Gambit/bin/gsc" + module Scm = struct type t = | Symbol of string @@ -74,11 +76,11 @@ module Scm = struct let symbol (name : string) : t = Symbol (escape_symbol name) - let rec string_of_exp (exp : t) : string = + let rec to_string (exp : t) : string = match exp with | Symbol (name) -> name | List (elements) - -> "(" ^ String.concat " " (List.map string_of_exp elements) ^ ")" + -> "(" ^ String.concat " " (List.map to_string elements) ^ ")" | String (value) -> let length = String.length value in let buffer = Buffer.create length in @@ -101,7 +103,7 @@ module Scm = struct | Float (value) -> string_of_float value let print (output : out_channel) (exp : t) : unit = - output_string output (string_of_exp exp); + output_string output (to_string exp); output_char output '\n' let describe (exp : t) : string = @@ -282,6 +284,75 @@ let rec scheme_of_expr (sctx : ScmContext.t) (elexp : elexp) : Scm.t = | _ -> failwith ("[gambit] unsupported elexp: " ^ elexp_string elexp) +class inferior script_path = + let down_reader, down_writer = Unix.pipe ~cloexec:true () in + let up_reader, up_writer = Unix.pipe ~cloexec:true () in + let _ = Unix.clear_close_on_exec down_reader in + let _ = Unix.clear_close_on_exec up_writer in + let pid = + Unix.create_process + !gsc_path + [|!gsc_path; "-i"; "-f"; script_path|] + down_reader + up_writer + Unix.stderr + in + let _ = Unix.close down_reader in + let _ = Unix.close up_writer in + + object (self) + val pid = pid + val writer_fd = down_writer + val reader_fd = up_reader + val short_buffer = Bytes.make 4 '\x00' + + method stop : unit = + Unix.close writer_fd; + let _ = Unix.waitpid [] pid in + Unix.close reader_fd + + method private read_byte : char = + self#read ~size:1 short_buffer; + Bytes.get short_buffer 0 + + method private write_byte (b : char) : unit = + Bytes.set short_buffer 0 b; + self#write ~size:1 short_buffer + + method private read_sized_string : string = + self#read ~size:4 short_buffer; + let size = Int32.to_int (Bytes.get_int32_be short_buffer 0) in + let buffer = Bytes.create size in + self#read ~size buffer; + Bytes.to_string buffer + + method private write_sized_string (string : string) : unit = + let buffer = Bytes.of_string string in + let size = Bytes.length buffer in + Bytes.set_int32_be short_buffer 0 (Int32.of_int size); + self#write ~size:4 short_buffer; + self#write ~size buffer + + method private read ~(size : int) (bytes : Bytes.t) : unit = + let n = ref 0 in + while !n < size do + n := !n + Unix.read reader_fd bytes !n (size - !n) + done + + method private write ~(size : int) (bytes : Bytes.t) : unit = + assert (Unix.write writer_fd bytes 0 size = size) + end + +class pretty_printer = + object (self) + inherit inferior "src/pretty-printer.scm" + + method pp (expr : Scm.t) : string = + let source = Scm.to_string expr in + self#write_sized_string source; + self#read_sized_string + end + let scheme_of_decl (sctx : ScmContext.t) (name, elexp : string * elexp) : Scm.t = Scm.List ([Scm.define; Scm.Symbol name; scheme_of_expr sctx elexp]) @@ -290,13 +361,19 @@ class gambit_compiler lctx output = object val mutable sctx = ScmContext.of_lctx lctx val mutable lctx = lctx + val pretty_printer = new pretty_printer method process_decls ldecls = let lctx', eldecls = Opslexp.clean_decls lctx ldecls in let sctx', eldecls = List.fold_left_map ScmContext.intro_binding sctx eldecls in - let sdecls = Scm.List (Scm.begin' :: List.map (scheme_of_decl sctx') eldecls) in + let sdecls = List.map (scheme_of_decl sctx') eldecls in sctx <- sctx'; lctx <- lctx'; - Scm.print output sdecls; + List.iter + (fun sdecl -> sdecl |> pretty_printer#pp |> output_string output) + sdecls + + method stop = + pretty_printer#stop end ===================================== src/lexp.ml ===================================== @@ -1,6 +1,6 @@ (* lexp.ml --- Lambda-expressions: the core language. -Copyright (C) 2011-2021 Free Software Foundation, Inc. +Copyright (C) 2011-2022 Free Software Foundation, Inc. Author: Stefan Monnier <monnier(a)iro.umontreal.ca> Keywords: languages, lisp, dependent types. @@ -20,6 +20,8 @@ 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 Printf + module U = Util module L = List module SMap = U.SMap @@ -478,8 +480,6 @@ let rec sunshift n = else (assert (n >= 0); S.cons impossible (sunshift (n - 1))) -let _ = assert (S.identity_p (scompose (S.shift 5) (sunshift 5))) - (* The quick test below seemed to indicate that about 50% of the "sink"s * are applied on top of another "sink" and hence could be combined into * a single "Lift^n" constructor. Doesn't seem high enough to justify @@ -789,11 +789,10 @@ let rec lexp_unparse lxp = (* FIXME: ¡Unify lexp_print and lexp_string! *) and lexp_string lxp = sexp_string (lexp_unparse lxp) -and subst_string s = match s with - | S.Identity o -> "↑" ^ string_of_int o - | S.Cons (l, s, 0) -> lexp_name l ^ " · " ^ subst_string s - | S.Cons (l, s, o) - -> "(↑"^ string_of_int o ^ " " ^ subst_string (S.cons l s) ^ ")" +and subst_string = function + | S.Identity o -> sprintf "↑%d" o + | S.Cons (l, s, 0) -> sprintf "%s · %s" (lexp_name l) (subst_string s) + | S.Cons (l, s, o) -> sprintf "(↑%d %s)" o (subst_string (S.cons l s)) and lexp_name e = match lexp_lexp' e with ===================================== src/pretty-printer.scm ===================================== @@ -0,0 +1,44 @@ +(define (read-u8* k) + (let ((b (read-u8))) + (if (eof-object? b) (k)) + b)) + +(define (read-u32be k) + (let ((b3 (read-u8* k)) + (b2 (read-u8* k)) + (b1 (read-u8* k)) + (b0 (read-u8* k))) + (bitwise-ior (arithmetic-shift b3 24) + (arithmetic-shift b2 16) + (arithmetic-shift b1 8) + b0))) + +(define (write-u32be n) + (write-u8 (bitwise-and #xff (arithmetic-shift n -24))) + (write-u8 (bitwise-and #xff (arithmetic-shift n -16))) + (write-u8 (bitwise-and #xff (arithmetic-shift n -8))) + (write-u8 (bitwise-and #xff n))) + +(define (read-sized-string k) + (let* ((bytes-length (read-u32be k)) + (bytes (make-u8vector bytes-length))) + (read-subu8vector bytes 0 bytes-length) + (utf8->string bytes))) + +(define (write-sized-string string) + (let* ((bytes (string->utf8 string)) + (bytes-length (u8vector-length bytes))) + (write-u32be bytes-length) + (write-subu8vector bytes 0 bytes-length) + (force-output (current-output-port)))) + +(call-with-current-continuation + (lambda (k) + (let loop () + (write-sized-string + (with-output-to-string + (lambda () + (with-input-from-string (read-sized-string k) + (lambda () + (pretty-print (read))))))) + (loop)))) ===================================== src/sexp.ml ===================================== @@ -23,6 +23,7 @@ this program. If not, see <http://www.gnu.org/licenses/>. *) open Util open Prelexer open Grammar +open Printf let sexp_error ?print_action loc fmt = Log.log_error ~section:"SEXP" ?print_action ~loc fmt @@ -121,6 +122,61 @@ let sexp_name s = * as appropriate. *) let empty_args_are_not_args = false +module Op = struct + type t = + { head : symbol + ; parts_rev : string list + ; lhs_p : bool + ; rhs_p : bool + } + + let null : t = + { head = (Source.Location.dummy, "") + ; parts_rev = [] + ; lhs_p = false + ; rhs_p = false + } + + let prefix (head : symbol) : t = + {head; parts_rev = []; lhs_p = false; rhs_p = true} + + let postfix (head : symbol) : t = + {head; parts_rev = []; lhs_p = true; rhs_p = false} + + let infix (head : symbol) : t = + {head; parts_rev = []; lhs_p = true; rhs_p = true} + + let compose ({head; parts_rev; lhs_p; rhs_p} : t): symbol = + let (location, head_name) = head in + let name = String.concat "_" (head_name :: List.rev parts_rev) in + let name = + match lhs_p, rhs_p with + | false, false -> name + | false, true -> sprintf "%s_" name + | true, false -> sprintf "_%s" name + | true, true -> sprintf "_%s_" name + in + (location, name) + + let mark_rhs (op : t) : t = + match op.head with + | (_, "") -> op + | _ -> {op with rhs_p = true} + + let push_inner (op : t) (part : string) : t = + let last_name = + match op.parts_rev with + | [] -> snd op.head + | last_name :: _ -> last_name + in + if String.equal part last_name + then op + else {op with parts_rev = part :: op.parts_rev} + + let push_closer (op : t) (part : string) : t = + {op with parts_rev = part :: op.parts_rev; rhs_p = false} +end + (* `op' is the operator being parsed. E.g. for let...in... * it would be either ["let"] or ["in";"let"] depending on which * part we've parsed already. @@ -128,95 +184,104 @@ let empty_args_are_not_args = false * `rargs' are the sexps that compose the arg to the right of the latest * infix symbol. They may belong to `op' or to a later infix operator * we haven't seen yet which binds more tightly. *) -let rec sexp_parse (g : grammar) (rest : sexp list) - (level : int) - (op : symbol list) - (largs : sexp list) - (rargs : sexp list) +let rec sexp_parse + (g : grammar) + (rest : sexp list) + (level : int) + (op : Op.t) + (largs : sexp list) + (rargs : sexp list) : (sexp * sexp list) = - let sexp_parse = sexp_parse g in - let compose_symbol (ss : symbol list) = match ss with - | [] -> (Log.internal_error "empty operator!") - | (l,_)::_ -> (l, String.concat "_" (List.map (fun (_,s) -> s) - (List.rev ss))) in + let sexp_parse = sexp_parse g in - let push_largs largs rargs closer = match List.rev rargs with - | [] -> if closer then dummy_epsilon :: largs else largs - | e::es -> (match es with [] -> e | _ -> Node (e, es)) :: largs in + let push_largs largs rargs closer = + match List.rev rargs with + | [] -> if closer then dummy_epsilon :: largs else largs + | e::es -> (match es with [] -> e | _ -> Node (e, es)) :: largs + in let mk_node op largs rargs closer = let args = List.rev (push_largs largs rargs closer) in - match op with - | [] -> (match args with [] -> dummy_epsilon - | [e] -> e - | e::es -> Node (e, es)) - | ss -> let headname = compose_symbol ss in - match (headname, args) with - (* FIXME: While it's uaulyl good to strip away parens, - * this makes assumptions about the grammar (i.e. there's - * a rule « exp ::= '(' exp ')' » ), and this is sometimes - * not desired (e.g. to distinguish "a b ⊢ c d" from - * "(a b) ⊢ (c d)"). *) - | ((_,"(_)"), [arg]) -> arg (* Strip away parens. *) - | _ -> Node (hSymbol (headname), args) in + let headname = Op.compose op in + match (headname, args) with + (* FIXME: While it's usually good to strip away parens, this makes + assumptions about the grammar (i.e. there's a rule + « exp ::= '(' exp ')' »), and this is sometimes not desired (e.g. to + distinguish "a b ⊢ c d" from "(a b) ⊢ (c d)"). *) + | (_, "(_)"), [arg] -> arg + | _ -> Node (hSymbol (headname), args) + in match rest with - | (((Symbol ((l,name) as s)) as e)::rest') -> - (try match SMap.find name g with - | (None, None) -> sexp_parse rest' level op largs (e::rargs) - | (None, Some rl) (* Open paren or prefix. *) - -> let (e, rest) = sexp_parse rest' rl [s] [] [] - in sexp_parse rest level op largs (e::rargs) - | (Some ll, _) when ll < level - (* A symbol that closes the currently parsed element. *) - -> ((if empty_args_are_not_args then - mk_node (match rargs with [] -> op | _ -> ((l,"")::op)) - largs rargs false - else - mk_node ((l,"")::op) largs rargs true), - rest) - | (Some ll, None) when ll > level - (* A closer without matching opener or a postfix symbol - that binds very tightly. Previously, we signaled an - error (assuming the former), but it prevented the use - tightly binding postfix operators. - - For example, it signaled spurious errors when parsing - expressions with a tightly binding postfix # operator - that implemented record construction by taking an - inductive as argument and returning the inductive's only - constructor. *) - -> sexp_parse rest' level op largs - [mk_node [(l,name);(l,"")] [] rargs true] - | (Some ll, Some rl) when ll > level - (* A new infix which binds more tightly, i.e. does not close - * the current `op' but takes its `rargs' instead. *) - -> let (e, rest) - = if empty_args_are_not_args then - sexp_parse rest' rl - (match rargs with [] -> [s] | _ -> [s;(l,"")]) - (push_largs [] rargs false) [] - else - sexp_parse rest' rl [s;(l,"")] - (push_largs [] rargs true) [] - in sexp_parse rest level op largs [e] - | (Some ll, Some rl) - -> sexp_parse rest' rl - (if ll == rl - && match op with (_,name')::_ -> name = name' - | _ -> false - then op else (s::op)) - (push_largs largs rargs true) [] - | (Some _ll, None) - -> (mk_node (s::op) largs rargs true, rest') - with Not_found -> - sexp_parse rest' level op largs (e::rargs)) - | e::rest -> sexp_parse rest level op largs (e::rargs) - | [] -> (mk_node (match rargs with [] -> op - | _ -> ((dummy_location,"")::op)) - largs rargs false, - []) + | Symbol (_, name as s) as e :: rest' -> + + begin match SMap.find name g with + | (None, None) -> + sexp_parse rest' level op largs (e :: rargs) + + | (None, Some rl) -> + (* Open paren or prefix. *) + let e, rest'' = + sexp_parse rest' rl (Op.prefix s) [] [] + in + sexp_parse rest'' level op largs (e :: rargs) + + | (Some ll, _) when ll < level -> + (* A symbol that closes the currently parsed element. *) + let op' = + match rargs with + | [] when empty_args_are_not_args -> op + | _ -> Op.mark_rhs op + in + mk_node op' largs rargs (not empty_args_are_not_args), rest + + | (Some ll, None) when ll > level -> + (* A closer without matching opener or a postfix symbol that binds very + tightly. Previously, we signaled an error (assuming the former), but + it prevented the use tightly binding postfix operators. + + For example, it signaled spurious errors when parsing expressions + with a tightly binding postfix # operator that implemented record + construction by taking an inductive as argument and returning the + inductive's only constructor. *) + let rargs' = [mk_node (Op.postfix s) [] rargs true] in + sexp_parse rest' level op largs rargs' + + | (Some ll, Some rl) when ll > level -> + (* A new infix which binds more tightly, i.e. does not close the current + `op' but takes its `rargs' instead. *) + let op' = + match rargs with + | [] when empty_args_are_not_args -> Op.prefix s + | _ -> Op.infix s + in + let e, rest'' = + sexp_parse rest' rl op' (push_largs [] rargs (not empty_args_are_not_args)) [] + in + sexp_parse rest'' level op largs [e] + + | (Some ll, Some rl) -> + let op' = if ll = rl then op else Op.push_inner op name in + sexp_parse rest' rl op' (push_largs largs rargs true) [] + + | (Some _ll, None) -> + (* Either a lone postfix or the closer of a mixfix operator. *) + mk_node (Op.push_closer op name) largs rargs true, rest' + + | exception Not_found -> + sexp_parse rest' level op largs (e :: rargs) + end + + | e :: rest -> sexp_parse rest level op largs (e :: rargs) + + | [] -> + let op' = + match rargs with + | [] -> op + | _ -> Op.mark_rhs op + in + mk_node op' largs rargs false, [] let sexp_parse_all grm tokens limit : sexp * token list = let level = match limit with @@ -225,18 +290,21 @@ let sexp_parse_all grm tokens limit : sexp * token list = match SMap.find token grm with | (Some ll, Some _) -> ll + 1 | _ -> Log.internal_error {|Can't find level of "%s"|} token - in let (e, rest) = sexp_parse grm tokens level [] [] [] in - let se = match e with - | Node (Symbol (_, ""), [e]) -> e - | Node (Symbol (_, ""), e::es) -> Node (e, es) - | _ -> (Log.internal_error "Didn't find a toplevel") in - match rest with - | [] -> (se,rest) - | Symbol (l,t) :: rest - -> if not (Some t = limit) - then sexp_error l {|Stray closing token: "%s"|} t; - (se,rest) - | _ -> (Log.internal_error "Stopped parsing before the end!") + in + let e, rest = sexp_parse grm tokens level Op.null [] [] in + let se = + match e with + | Node (Symbol (_, ""), [e]) -> e + | Node (Symbol (_, ""), e::es) -> Node (e, es) + | _ -> Log.internal_error {|Didn't find a toplevel, got: "%s"|} (sexp_string e) + in + match rest with + | [] -> (se,rest) + | Symbol (l,t) :: rest + -> if not (Some t = limit) + then sexp_error l {|Stray closing token: "%s"|} t; + (se,rest) + | _ -> Log.internal_error "Stopped parsing before the end!" (* "sexp_p" is for "parsing" and "sexp_u" is for "unparsing". *) ===================================== src/simpl.ml ===================================== @@ -0,0 +1,164 @@ +(* Copyright (C) 2022 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/>. *) + +(** A simplification pass for lexps. It β-reduces let bindings of variables and + builtins. For example, let a = b in a + b + c becomes b + b + c. + + The reason to have such a pass is not so much for performance, but to allow + us to write any macro naively, i.e. we can introduce binding in macros + without fear of “polluting” the generated code. *) + +open Lexp + +(* The secret with the simplification phase is to compute the right + substitution. In the case of a single binding, the correct substitution is + a#1 · ↑1, i.e. replace b#0 with a#1, then shift the rest of the + environment by 1 to account for the sigle remaining binding. + + let a = 1 in let a = 1 in + let b = a[1] in + a[1] + b[0] a[0] + a[0] + + For multiple non-recursive bindings, the situation is similar. In this + example, the substitution is a#2 · b#1 · ↑1, which has the same kind of + substitution for our inlined variable, followed by the identity substitution + of b#1 to b#1, and finally the shift. + + let a = 1 in let a = 1 in + let let + b = 2 b = 2 + c = a[2] + in in + b[1] + c[0] b[0] + a[1] + + What about recursive bindings? We simply don't bother with them! + + *) + +type action = + | Id of vname * int + | SubstVar of vname * int + | SubstConst of lexp + +let compute_subst (min_index : int) (ldecls : ldecls) (subst : subst) : subst = + let loop (name, lexp, _) (actions, i, removed) = + let action, removed = + match lexp with + | Lexp.Var (name, index), _ when index >= min_index + -> SubstVar (name, index), removed + 1 + | Lexp.Builtin _, _ | Lexp.Imm _, _ + -> SubstConst lexp, removed + 1 + | _ + -> Id (name, i), removed + in + action :: actions, i + 1, removed + in + let actions, total, removed = List.fold_right loop ldecls ([], 0, 0) in + let lexps = + let lexp_of_action = function + | Id (name, index) -> Lexp.mkVar (name, index) + | SubstVar (name, index) -> Lexp.mkVar (name, index - removed) + | SubstConst (lexp) -> lexp + in + List.map lexp_of_action actions + in + scompose + (List.fold_left + (fun s e -> Subst.cons e s) + (Subst.shift (total - removed)) + lexps) + subst + +let rec simpl_lexp + (subst : subst) + (lexp : lexp) + : lexp = + + match lexp with + | Lexp.Let (location, ldecls, body), _ + -> let subst', ldecls' = simpl_ldecls subst ldecls in + let body' = simpl_lexp subst' body in + begin match ldecls' with + | [] -> body' + | _ -> Lexp.mkLet (location, ldecls', body') + end + + | Lexp.Lambda (kind, arg_name, arg_ty, body), _ + -> let subst' = ssink arg_name subst in + let body' = simpl_lexp subst' body in + Lexp.mkLambda (kind, arg_name, arg_ty, body') + + | Lexp.Call (head, tail), _ + -> let head' = simpl_lexp subst head in + let tail' = + List.map + (fun (kind, value) -> kind, simpl_lexp subst value) + tail + in + Lexp.mkCall (head', tail') + + | Lexp.Case (location, subject, ty, branches, default), _ + -> let simpl_branch (location, names, body) = + let branch_subst = + ssink + (Source.Location.dummy, None) + (List.fold_left + (fun subst' (_, name) -> ssink name subst') + subst + names) + in + let body' = simpl_lexp branch_subst body in + location, names, body' + in + + let simpl_default (name, body) = + let subst' = ssink name subst in + let body' = simpl_lexp subst' body in + name, body' + in + + let subject' = simpl_lexp subst subject in + let branches' = SMap.map simpl_branch branches in + let default' = Option.map simpl_default default in + Lexp.mkCase (location, subject', ty, branches', default') + + | _ -> mkSusp lexp subst + +and simpl_ldecl + (min_index : int) + (subst : subst) + (ldecls : ldecls) + (name, lexp, ty: ldecl) + : ldecls = + + match lexp with + | Lexp.Var (_, index), _ when index >= min_index -> ldecls + | Lexp.Builtin _, _ | Lexp.Imm _, _ -> ldecls + | _ -> (name, mkSusp lexp subst, ty) :: ldecls + +and simpl_ldecls + (subst : subst) + (ldecls : ldecls) + : subst * ldecls = + + let min_index = List.length ldecls in + let subst' = compute_subst min_index ldecls subst in + let ldecls' = List.fold_left (simpl_ldecl min_index subst') [] ldecls in + subst', List.rev ldecls' ===================================== src/subst.ml ===================================== @@ -1,6 +1,6 @@ (* subst.ml --- Substitutions for Lexp -Copyright (C) 2016-2019 Free Software Foundation, Inc. +Copyright (C) 2016-2022 Free Software Foundation, Inc. Author: Stefan Monnier <monnier(a)iro.umontreal.ca> @@ -60,7 +60,7 @@ module U = Util * e[s] % Application of a substitution * * s ::= id % identity substitution - * e . s % replace #0 with `e` and use `s` for the rest + * e · s % replace #0 with `e` and use `s` for the rest * s₁ ∘ s₂ % Composition (apply s₁ *first* and then s₂!). * ↑ % dbi_index = dbi_index + 1 * @@ -72,7 +72,7 @@ module U = Util * e[s] % Application of a substitution * * s ::= id % identity substitution - * e . s % replace #0 by `e` and use `s` for the rest + * e · s % replace #0 by `e` and use `s` for the rest * s ↑n % like Abadi's "s ∘ (↑ⁿ)" * * And the composition ∘ is defined as a function rather than a constructor. @@ -148,7 +148,7 @@ let lookup (mkVar : 'b -> db_index -> 'a) else mkShift e o in lookup' 0 s v -let mkShift s (m:db_offset) = +let mkShift (s : 'a subst) (m : db_offset) : 'a subst = if m>0 then match s with Identity o -> Identity (o + m) | Cons (e, s, o) -> Cons (e, s, o + m) @@ -194,7 +194,7 @@ let compose (mkSusp : 'a -> 'a subst -> 'a) -> (* Myers's fastlane: * if o1 >= sk2 then compose_cons (o1 - sk1) s2' (o + o2') *) if o1 > 0 then compose_cons (o1 - 1) s2 (o + o2) - else + else (* Pull out o2's shift and compose the two Cons. *) let s' = cons e2 s2 in Cons (mkSusp e1 s', compose' s1 s', o + o2) ===================================== tests/dune ===================================== @@ -11,6 +11,7 @@ macro_test positivity_test sexp_test + simpl_test unify_test) (deps (alias %{project_root}/btl/typer_stdlib)) (libraries typerlib) ===================================== tests/gambit_test.ml ===================================== @@ -31,7 +31,7 @@ open Utest_lib open Gambit let fail_on_exp exp = - Printf.printf "in %s\n" (Scm.string_of_exp exp); + Printf.printf "in %s\n" (Scm.to_string exp); false let type_error expected actual = ===================================== tests/lexp_test.ml ===================================== @@ -3,7 +3,7 @@ * * --------------------------------------------------------------------------- * - * Copyright (C) 2011-2017 Free Software Foundation, Inc. + * Copyright (C) 2011-2022 Free Software Foundation, Inc. * * Author: Pierre Delaunay <pierre.delaunay(a)hec.ca> * Keywords: languages, lisp, dependent types. @@ -26,92 +26,36 @@ * --------------------------------------------------------------------------- *) open Typerlib - open Utest_lib +open Lexp_test_support +open Lexp -(* default environment *) let ectx = Elab.default_ectx let rctx = Elab.default_rctx -(* -let _ = (add_test "LEXP" "lexp_print" (fun () -> - - let dcode = " -sqr : (x : Int) -> Int; -sqr = lambda (x : Int) -> - (x * x); - -cube : (x : Int) -> Int; -cube = lambda (x : Int) -> - (x * (sqr x)); - -mult : (x : Int) -> (y : Int) -> Int; -mult = lambda (x : Int) -> - lambda (y : Int) -> - (x * y); - -twice : (y : Int) -> Int; -twice = (mult 2); - -let_fun : (x : Int) -> Int; -let_fun = lambda (x : Int) -> - let a : Int; - a = (twice x); in - let b : Int; - b = (mult 2 x); in - (a + b);" in - - let ret1, _ = lexp_decl_str dcode ectx in - - let to_str decls = - let str = _lexp_str_decls pretty_ppctx (List.flatten ret1) in - List.fold_left (fun str lxp -> str ^ "\n" ^ lxp) "" str in - - (* Cast to string *) - let str1 = (to_str ret1) ^ "\n" in - - print_string str1; - - (* read code again *) - let ret2, _ = lexp_decl_str str1 ectx in - - (* Cast to string *) - let str2 = to_str ret2 in - - if str1 = str2 then success () else failure () -)) *) - -(* -let set_to_list s = - StringSet.fold (fun g a -> g::a) s [] - -let _ = (add_test "LEXP" "Free Variable" (fun () -> - - let dcode = " - a = 2; - b = 3; - f = lambda n -> (a + n); % a is a fv - g = lambda x -> ((f b) + a + x); % f,a,b are fv - " in - - let ret = pexp_decl_str dcode in - let g = match List.rev ret with - | (_, g, _)::_ -> g - | _ -> raise (Unexpected_result "Unexpected empty list") in - - let (bound, free) = free_variable g in - - let bound = set_to_list bound in - let (free, _) = free in - - match bound with - | ["x"] ->( - match free with - | ["_+_"; "f"; "b"; "a"] -> success () - | _ -> failure ()) - | _ -> failure () - -)) *) +let test_lexp name actual expected = + let test () = + let result = expect_equal_lexps [actual] [expected] in + if result = Utest_lib.failure + then Log.print_log () + else Log.clear_log (); + result + in + add_test "LEXP" name test + +let () = + let subst = Subst.cons (make_var 0 "a") Subst.identity in + test_lexp + "Substitute variable" + (Lexp.clean (Lexp.mkSusp (make_var 0 "b") subst)) + (make_var 0 "a") + +let () = + let test () = + if Subst.identity_p (scompose (Subst.shift 5) (sunshift 5)) + then Utest_lib.success + else Utest_lib.failure + in + add_test "LEXP" "unshifts are cancelled by shifts" test -(* run all tests *) let _ = run_all () ===================================== tests/lexp_test_support.ml ===================================== @@ -0,0 +1,45 @@ +(* Copyright (C) 2022 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/>. *) + +open Typerlib + +let make_int i = + Lexp.mkImm (Sexp.Integer (Source.Location.dummy, Z.of_int i)) + +let make_sym name = + (Source.Location.dummy, name) + +let make_name name = + (Source.Location.dummy, Some name) + +let make_var index name = + Lexp.mkVar ((Source.Location.dummy, Some name), index) + +let make_builtin name ty = + Lexp.mkBuiltin (name, ty) + +let make_let decls body = + Lexp.mkLet (Source.Location.dummy, decls, body) + +let make_call head args = + Lexp.mkCall (head, List.map (fun arg -> Pexp.Anormal, arg) args) + +let make_1_plus_2 plus_index = + make_call (make_var plus_index "_+_") [make_int 1; make_int 2] ===================================== tests/sexp_test.ml ===================================== @@ -30,16 +30,14 @@ let _ = test_sexp_add "x * x * x" (fun ret -> | _ -> failure ) -let test_sexp_eqv dcode1 dcode2 = - add_test "SEXP" dcode1 - (fun () -> - let s1 = sexp_parse_str dcode1 in - let s2 = sexp_parse_str dcode2 in - if sexp_eq_list s1 s2 - then success - else (sexp_print (List.hd s1); - sexp_print (List.hd s2); - failure)) +let test_sexp_eqv ?name actual_source expected_source = + let test () = + let actual = sexp_parse_str actual_source in + let expected = sexp_parse_str expected_source in + expect_equal_sexps ~actual ~expected + in + let name = Option.value ~default:actual_source name in + add_test "SEXP" name test let _ = test_sexp_eqv "((a) ((1.00)))" "a 1.0" let _ = test_sexp_eqv "(x + y)" "_+_ x y" @@ -52,5 +50,11 @@ let _ = test_sexp_eqv "a\\b\\c" "abc" let _ = test_sexp_eqv "(a;b)" "(_\\;_ a b)" let _ = test_sexp_eqv "a.b.c . (.)" "(__\\.__ (__\\.__ a b) c) \\. \\." +let _ = + test_sexp_eqv + ~name:"Type ascription in declaration" + "x = 4 : Int" + "(_=_ x (_:_ 4 Int))" + (* run all tests *) let _ = run_all () ===================================== tests/simpl_test.ml ===================================== @@ -0,0 +1,103 @@ +(* Copyright (C) 2022 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/>. *) + +open Typerlib +open Utest_lib +open Debruijn +open Lexp_test_support + +let test_simpl name original expected = + let test () = + let actual = Simpl.simpl_lexp Subst.identity original in + let result = expect_equal_lexps [actual] [expected] in + if result = Utest_lib.failure + then Log.print_log () + else Log.clear_log (); + result + in + add_test "SIMPL" name test + +let () = + test_simpl + "single let of variable is eliminated" + (make_let [make_name "x", make_var 1 "y", type_int] (make_var 0 "x")) + (make_var 0 "y") + +let () = + test_simpl + "single let of builtin is eliminated" + (make_let + [make_name "x", make_builtin (make_sym "Int") type_int, type0] + (make_var 0 "x")) + (make_builtin (make_sym "Int") type0) + +let () = + test_simpl + "single let of int eliminated" + (make_let + [make_name "x", make_int 3, type_int] + (make_var 0 "x")) + (make_int 3) + +let () = + test_simpl + "first let is eliminated" + (make_let + [make_name "x", make_var 2 "y", type_int; + make_name "z", make_1_plus_2 40, type_int] + (make_var 1 "x")) + (make_let + [make_name "z", make_1_plus_2 39, type_int] + (make_var 1 "y")) + +let () = + test_simpl + "last let is eliminated" + (make_let + [make_name "z", make_1_plus_2 40, type_int; + make_name "x", make_var 2 "y", type_int] + (make_var 0 "x")) + (make_let + [make_name "z", make_1_plus_2 39, type_int] + (make_var 1 "y")) + +let () = + test_simpl + "preserves recursive variables" + (make_let + [make_name "x", make_var 0 "y", type_int; + make_name "y", make_var 1 "x", type_int] + (make_int 5)) + (make_let + [make_name "x", make_var 0 "y", type_int; + make_name "y", make_var 1 "x", type_int] + (make_int 5)) + +let () = + test_simpl + "simplification is transitive" + (make_let + [make_name "x", make_int 55, type_int] + (make_let + [make_name "y", make_var 1 "x", type_int] + (make_var 0 "y"))) + (make_int 55) + +let () = run_all () ===================================== tests/utest_lib.ml ===================================== @@ -132,6 +132,50 @@ let expect_equal_float = _expect_equal_t Float.equal string_of_float let expect_equal_str = _expect_equal_t String.equal (fun g -> g) let expect_equal_values = _expect_equal_t Env.value_eq_list print_value_list +let expect_equal_sexps ~expected ~actual = + let print_sexp_ok s = + Printf.printf (green_f ^^ "%s" ^^ reset_f ^^ "\n") (Sexp.sexp_string s) + in + + let print_sexp_err expected actual = + Printf.printf + ("Expected:\n" ^^ red_f ^^ "%s\n" ^^ reset_f) + (Sexp.sexp_string expected); + Printf.printf + ("Actual:\n" ^^ red_f ^^ "%s\n" ^^ reset_f) + (Sexp.sexp_string actual) + in + + let rec loop failed fine expected actual = + match expected, actual with + | l :: ll, r :: rr -> + if Sexp.sexp_equal l r + then loop failed (l :: fine) ll rr + else + (List.iter print_sexp_ok fine; + print_sexp_err l r; + loop true [] ll rr) + | _ :: _, [] -> + List.iter print_sexp_ok fine; + Printf.printf ("Missing sexps:\n" ^^ red_f); + List.iter (fun s -> s |> Sexp.sexp_string |> Printf.printf "%s\n") expected; + Printf.printf reset_f; + true + | [], _ :: _ -> + List.iter print_sexp_ok fine; + Printf.printf ("Unexpected sexps:\n" ^^ red_f); + List.iter (fun s -> s |> Sexp.sexp_string |> Printf.printf "%s\n") actual; + Printf.printf reset_f; + true + | [], [] -> + if failed + then List.iter print_sexp_ok fine; + failed + in + if loop false [] expected actual + then failure + else success + let expect_equal_lexps = let rec lexp_list_eq l r = match l, r with ===================================== typer.ml ===================================== @@ -45,6 +45,10 @@ let arg_defs = ("-Vmacro-expansion", Arg.Set Elab.macro_tracing_enabled, "Trace macro expansion"); + + ("-O", + Arg.Set Elab.optimize, + "Enable a simplification phase"); ] let parse_args argv usage = @@ -61,7 +65,10 @@ let compile_main argv = let backend = new Gambit.gambit_compiler (ectx_to_lctx ectx) stdout in let _ = - List.fold_left (Elab.process_file backend) ectx (list_input_files ()) + Fun.protect + ~finally:(fun () -> backend#stop) + (fun () + -> List.fold_left (Elab.process_file backend) ectx (list_input_files ())) in Log.print_log () View it on GitLab: https://gitlab.com/monnier/typer/-/compare/e322bbe1fddd61f45c9a410cb1661d29… -- View it on GitLab: https://gitlab.com/monnier/typer/-/compare/e322bbe1fddd61f45c9a410cb1661d29… You're receiving this email because of your account on gitlab.com.

1 0

2024

2023

2022

2021

2020

2019

2018

2017

2016

Typer Août 2022