Simon Génier pushed to branch compiler-phase-simpl at Stefan / Typer

Commits: a37a2df4 by Simon Génier at 2022-09-02T14:21:37-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.

Since I'm a coward, I'm leaving it disabled by default. Use `-O` to enable it.

- - - - -

9 changed files:

- src/elab.ml - src/lexp.ml - + src/simpl.ml - src/subst.ml - tests/dune - tests/lexp_test.ml - + tests/lexp_test_support.ml - + tests/simpl_test.ml - typer.ml

Changes:

===================================== src/elab.ml ===================================== @@ -71,6 +71,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 @@ -2088,7 +2089,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/lexp.ml ===================================== @@ -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 @@ -489,8 +491,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 @@ -810,11 +810,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/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 (info, 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 (info, head', tail') + + | Lexp.Case (location, subject, ty, branches, default), _ + -> let simpl_branch (location, names, body) = + let branch_subst = + ssink + (Sexp.dummy_sinfo, 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 ===================================== @@ -13,6 +13,7 @@ positivity_test samples_test sexp_test + simpl_test unify_test) (deps (alias %{project_root}/btl/typer_stdlib) (alias %{project_root}/samples/typer_samples))

===================================== 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/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 ()

===================================== 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 =

View it on GitLab: https://gitlab.com/monnier/typer/-/commit/a37a2df4759660bc0aae55746dd80a4583...