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@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@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@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@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@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@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@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/e322bbe1fddd61f45c9a410cb1661d29c...