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@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/2a824e2d1539ab7a2a4ba998fbb4ac656e...