From 5be816244ea1ed43ce1870adf2b2f05ac92dcde2 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Mon, 7 Nov 2022 14:10:06 +0100 Subject: [PATCH] chore: update script/apply.lean syntax --- script/apply.lean | 336 ++++++++++++++++++++++------------------------ 1 file changed, 163 insertions(+), 173 deletions(-) diff --git a/script/apply.lean b/script/apply.lean index 328c59ba0b..896d3a6b22 100644 --- a/script/apply.lean +++ b/script/apply.lean @@ -1,150 +1,142 @@ -import init.lean.config init.io -open io +import Lean.Runtime -@[reducible] def m := reader_t handle io +abbrev M := ReaderT IO.FS.Stream IO -def m.run (a : m unit) (out : option string := none) : io unit := -match out with -| some out := do - h ← mk_file_handle out io.mode.write, - a.run h, - fs.close h -| none := stdout >>= a.run +def M.run (a : M Unit) (out? : Option String := none) : IO Unit := + match out? with + | some out => do + IO.FS.withFile out .write (ReaderT.run a ∘ .ofHandle) + | none => IO.getStdout >>= (ReaderT.run a) -def emit (s : string) : m unit := -⟨λ h, fs.write h s⟩ +def emit (s : String) : M Unit := do + (← read).putStr s -def mk_typedef_fn (i : nat) : m unit := -let args := string.join $ (list.repeat "obj*" i).intersperse ", " in -do emit $ sformat! "typedef obj* (*fn{i})({args}); // NOLINT\n", - emit $ sformat! "#define FN{i}(f) reinterpret_cast(closure_fun(f))\n" +def mkTypedefFn (i : Nat) : M Unit := do + let args := (List.replicate i "obj*").intersperse ", " |> String.join + emit s!"typedef obj* (*fn{i})({args}); // NOLINT\n" + emit s!"#define FN{i}(f) reinterpret_cast(closure_fun(f))\n" --- Make string: "obj* a1, obj* a2, ..., obj* an" -def mk_arg_decls (n : nat) : string := -string.join $ (n.repeat (λ i r, r ++ [sformat! "obj* a{i+1}"]) []).intersperse ", " +def genSeq (n : Nat) (f : Nat → String) (sep := ", ") : String := + List.range n |>.map f |>.intersperse sep |> .join --- Make string: "a1, a2, ..., a{n}" -def mk_args (n : nat) : string := -string.join $ (n.repeat (λ i r, r ++ [sformat! "a{i+1}"]) []).intersperse ", " +-- make string: "obj* a1, obj* a2, ..., obj* an" +def mkArgDecls (n : Nat) : String := + genSeq n (s!"obj* a{·+1}") --- Make string: "a{s}, a{s+1}, ..., a{n}" -def mk_args_from (s n : nat) : string := -string.join $ ((n-s).repeat (λ i r, r ++ [sformat! "a{s+i+1}"]) []).intersperse ", " +-- make string: "a{s+1}, ..., a{n}" +def mkArgsFrom (s n : Nat) : String := + genSeq (n-s) (s!"a{s+·+1}") --- Make string: "as[0], as[1], ..., as[n-1]" -def mk_as_args (n : nat) : string := -string.join $ (n.repeat (λ i r, r ++ [sformat! "as[{i}]"]) []).intersperse ", " +-- make string: "a1, a2, ..., a{n}" +def mkArgs (n : Nat) : String := mkArgsFrom 0 n --- Make string: "fx(0), ..., fx(n-1)" -def mk_fs_args (n : nat) : string := -string.join $ (n.repeat (λ i r, r ++ [sformat! "fx({i})"]) []).intersperse ", " +-- make string: "as[0], as[1], ..., as[n-1]" +def mkAsArgs (n : Nat) : String := + genSeq n (s!"a[{·}]") --- Make string: "inc(fx(0)); ...; inc(fx(n-1))" -def mk_inc_fs (n : nat) : string := -string.join $ (n.repeat (λ i r, r ++ [sformat! "inc(fx({i})); "]) []) +-- make string: "fx(0), ..., fx(n-1)" +def mkFsArgs (n : Nat) : String := + genSeq n (s!"fx({·})") +-- make string: "inc(fx(0)); ...; inc(fx(n-1))" +def mkIncFs (n : Nat) : String := + genSeq n (s!"inc(fx({·}))") (sep := "; ") -def mk_apply_i (n : nat) (max : nat) : m unit := -let arg_decls := mk_arg_decls n in -let args := mk_args n in -do emit $ sformat! "obj* apply_{n}(obj* f, {arg_decls}) {{\n", - emit "unsigned arity = closure_arity(f);\n", - emit "unsigned fixed = closure_num_fixed(f);\n", - emit $ sformat! "if (arity == fixed + {n}) {{\n", - emit $ sformat! " if (is_exclusive(f)) {{\n", - emit $ sformat! " switch (arity) {{\n", - max.mrepeat $ λ i, do { - let j := i + 1, - when (j ≥ n) $ - let fs := mk_fs_args (j - n) in - let sep := if j = n then "" else ", " in - emit $ sformat! " case {j}: {{ obj* r = FN{j}(f)({fs}{sep}{args}); free_closure_obj(f); return r; }\n" - }, - emit " }\n", - emit " }\n", - emit $ sformat! " switch (arity) {{\n", - max.mrepeat $ λ i, do { - let j := i + 1, - when (j ≥ n) $ - let incfs := mk_inc_fs (j - n) in - let fs := mk_fs_args (j - n) in - let sep := if j = n then "" else ", " in - emit $ sformat! " case {j}: {{ {incfs}obj* r = FN{j}(f)({fs}{sep}{args}); dec_ref(f); return r; }\n" - }, - emit " default:\n", - emit $ sformat! " lean_assert(arity > {max});\n", - emit $ sformat! " obj * as[{n}] = {{ {args} };\n", - emit " obj ** args = static_cast(LEAN_ALLOCA(arity*sizeof(obj*))); // NOLINT\n", - emit " for (unsigned i = 0; i < fixed; i++) { inc(fx(i)); args[i] = fx(i); }\n", - emit $ sformat! " for (unsigned i = 0; i < {n}; i++) args[fixed+i] = as[i];\n", - emit " obj * r = FNN(f)(args);\n", - emit " dec_ref(f);\n", - emit " return r;\n", - emit " }\n", - emit $ sformat! "} else if (arity < fixed + {n}) {{\n", - if n ≥ 2 then do - emit $ sformat! " obj * as[{n}] = {{ {args} };\n", - emit " obj ** args = static_cast(LEAN_ALLOCA(arity*sizeof(obj*))); // NOLINT\n", - emit " for (unsigned i = 0; i < fixed; i++) { inc(fx(i)); args[i] = fx(i); }\n", - emit " for (unsigned i = 0; i < arity-fixed; i++) args[fixed+i] = as[i];\n", - emit " obj * new_f = curry(f, arity, args);\n", - emit " dec_ref(f);\n", - emit $ sformat! " return apply_n(new_f, {n}+fixed-arity, as+arity-fixed);\n" - else emit " lean_assert(fixed < arity);\n lean_unreachable();\n", - emit "} else {\n", - emit $ sformat! " return fix_args(f, {{{args}});\n", - emit "}\n", - emit "}\n" +def mkApplyI (n : Nat) (max : Nat) : M Unit := do + let argDecls := mkArgDecls n + let args := mkArgs n + emit s!"obj* apply_{n}(obj* f, {argDecls}) \{ +unsigned arity = closure_arity(f); +unsigned fixed = closure_num_fixed(f); +if (arity == fixed + {n}) \{ + if (is_exclusive(f)) \{ + switch (arity) \{\n" + for j in [n:max + 1] do + let fs := mkFsArgs (j - n) + let sep := if j = n then "" else ", " + emit s!" case {j}: \{ obj* r = FN{j}(f)({fs}{sep}{args}); free_closure_obj(f); return r; }\n" + emit " } + } + switch (arity) {\n" + for j in [n:max + 1] do + let incfs := mkIncFs (j - n) + let fs := mkFsArgs (j - n) + let sep := if j = n then "" else ", " + emit s!" case {j}: \{ {incfs}obj* r = FN{j}(f)({fs}{sep}{args}); dec_ref(f); return r; }\n" + emit s!" default: + lean_assert(arity > {max}); + obj * as[{n}] = \{ {args} }; + obj ** args = static_cast(LEAN_ALLOCA(arity*sizeof(obj*))); // NOLINT + for (unsigned i = 0; i < fixed; i++) \{ inc(fx(i)); args[i] = fx(i); } + for (unsigned i = 0; i < {n}; i++) args[fixed+i] = as[i]; + obj * r = FNN(f)(args); + dec_ref(f); + return r; + } +} else if (arity < fixed + {n}) \{\n" + if n ≥ 2 then do + emit s!" obj * as[{n}] = \{ {args} }; + obj ** args = static_cast(LEAN_ALLOCA(arity*sizeof(obj*))); // NOLINT + for (unsigned i = 0; i < fixed; i++) \{ inc(fx(i)); args[i] = fx(i); } + for (unsigned i = 0; i < arity-fixed; i++) args[fixed+i] = as[i]; + obj * new_f = curry(f, arity, args); + dec_ref(f); + return apply_n(new_f, {n}+fixed-arity, as+arity-fixed);\n" + else emit s!" lean_assert(fixed < arity); + lean_unreachable(); +} else \{ + return fix_args(f, \{{args}}); +} +}\n" -def mk_curry (max : nat) : m unit := -do emit "static obj* curry(void* f, unsigned n, obj** as) {\n", - emit "switch (n) {\n", - emit "case 0: lean_unreachable();\n", - max.mrepeat $ λ i, - let as := mk_as_args (i+1) in - emit $ sformat! "case {i+1}: return reinterpret_cast(f)({as});\n", - emit "default: return reinterpret_cast(f)(as);\n", - emit "}\n", - emit "}\n", - emit "static obj* curry(obj* f, unsigned n, obj** as) { return curry(closure_fun(f), n, as); }\n" +def mkCurry (max : Nat) : M Unit := do + emit "static obj* curry(void* f, unsigned n, obj** as) { +switch (n) { +case 0: lean_unreachable();\n" + for i in [0:max] do + let as := mkAsArgs (i+1) + emit s!"case {i+1}: return reinterpret_cast(f)({as}); +default: return reinterpret_cast(f)(as); +} +} +static obj* curry(obj* f, unsigned n, obj** as) \{ return curry(closure_fun(f), n, as); }\n" -def mk_apply_n (max : nat) : m unit := -do emit "obj* apply_n(obj* f, unsigned n, obj** as) {\n", - emit "switch (n) {\n", - emit "case 0: lean_unreachable();\n", - max.mrepeat $ λ i, - let as := mk_as_args (i+1) in - emit $ sformat! "case {i+1}: return apply_{i+1}(f, {as});\n", - emit "default: return apply_m(f, n, as);\n", - emit "}\n", - emit "}\n" +def mkApplyN (max : Nat) : M Unit := do + emit "obj* apply_n(obj* f, unsigned n, obj** as) { +switch (n) { +case 0: lean_unreachable();\n" + for i in [0:max] do + let as := mkAsArgs (i+1) + emit s!"case {i+1}: return apply_{i+1}(f, {as}); +default: return apply_m(f, n, as); +} +}\n" -def mk_apply_m (max : nat) : m unit := -do emit "obj* apply_m(obj* f, unsigned n, obj** as) {\n", - emit $ sformat! "lean_assert(n > {max});\n", - emit "unsigned arity = closure_arity(f);\n", - emit "unsigned fixed = closure_num_fixed(f);\n", - emit $ sformat! "if (arity == fixed + n) {{\n", - emit " obj ** args = static_cast(LEAN_ALLOCA(arity*sizeof(obj*))); // NOLINT\n", - emit " for (unsigned i = 0; i < fixed; i++) { inc(fx(i)); args[i] = fx(i); }\n", - emit " for (unsigned i = 0; i < n; i++) args[fixed+i] = as[i];\n", - emit " obj * r = FNN(f)(args);\n", - emit " dec_ref(f);\n", - emit " return r;\n", - emit $ sformat! "} else if (arity < fixed + n) {{\n", - emit " obj ** args = static_cast(LEAN_ALLOCA(arity*sizeof(obj*))); // NOLINT\n", - emit " for (unsigned i = 0; i < fixed; i++) { inc(fx(i)); args[i] = fx(i); }\n", - emit " for (unsigned i = 0; i < arity-fixed; i++) args[fixed+i] = as[i];\n", - emit " obj * new_f = FNN(f)(args);\n", - emit " dec_ref(f);\n", - emit " return apply_n(new_f, n+fixed-arity, as+arity-fixed);\n", - emit "} else {\n", - emit " return fix_args(f, n, as);\n", - emit "}\n", - emit "}\n" +def mkApplyM (max : Nat) : M Unit := + emit s!"obj* apply_m(obj* f, unsigned n, obj** as) \{ +lean_assert(n > {max}); +unsigned arity = closure_arity(f); +unsigned fixed = closure_num_fixed(f); +if (arity == fixed + n) \{ + obj ** args = static_cast(LEAN_ALLOCA(arity*sizeof(obj*))); // NOLINT + for (unsigned i = 0; i < fixed; i++) \{ inc(fx(i)); args[i] = fx(i); } + for (unsigned i = 0; i < n; i++) args[fixed+i] = as[i]; + obj * r = FNN(f)(args); + dec_ref(f); + return r; +} else if (arity < fixed + n) \{ + obj ** args = static_cast(LEAN_ALLOCA(arity*sizeof(obj*))); // NOLINT + for (unsigned i = 0; i < fixed; i++) \{ inc(fx(i)); args[i] = fx(i); } + for (unsigned i = 0; i < arity-fixed; i++) args[fixed+i] = as[i]; + obj * new_f = FNN(f)(args); + dec_ref(f); + return apply_n(new_f, n+fixed-arity, as+arity-fixed); +} else \{ + return fix_args(f, n, as); +} +}\n" -def mk_fix_args : m unit := -emit " +def mkFixArgs : M Unit := emit " static obj* fix_args(obj* f, unsigned n, obj*const* as) { unsigned arity = closure_arity(f); unsigned fixed = closure_num_fixed(f); @@ -176,9 +168,7 @@ static inline obj* fix_args(obj* f, std::initializer_list const & l) { } " -def mk_copyright : m unit := -emit -"/* +def mkCopyright : M Unit := emit "/* Copyright (c) 2018 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. @@ -186,46 +176,46 @@ Author: Leonardo de Moura */ " -def mk_apply_cpp (max : nat) : m unit := -do mk_copyright, - emit "// DO NOT EDIT, this is an automatically generated file\n", - emit "// Generated using script: ../../gen/apply.lean\n", - emit "#include \"runtime/apply.h\"\n", - emit "namespace lean {\n", - emit "#define obj object\n", - emit "#define fx(i) closure_arg_cptr(f)[i]\n", - mk_fix_args, - max.mrepeat $ λ i, mk_typedef_fn (i+1), - emit "typedef obj* (*fnn)(obj**); // NOLINT\n", - emit "#define FNN(f) reinterpret_cast(closure_fun(f))\n", - mk_curry max, - emit "obj* apply_n(obj*, unsigned, obj**);\n", - max.mrepeat $ λ i, do { mk_apply_i (i+1) max }, - mk_apply_m max, - mk_apply_n max, - emit "}\n" +def mkApplyCpp (max : Nat) : M Unit := do + mkCopyright + emit "// DO NOT EDIT, this is an automatically generated file +// Generated using script: ../../gen/apply.lean +#include \"runtime/apply.h\" +namespace lean { +#define obj object +#define fx(i) closure_arg_cptr(f)[i]\n" + mkFixArgs + for i in [0:max] do mkTypedefFn (i+1) + emit "typedef obj* (*fnn)(obj**); // NOLINT +#define FNN(f) reinterpret_cast(closure_fun(f))\n" + mkCurry max + emit "obj* apply_n(obj*, unsigned, obj**);\n" + for i in [0:max] do mkApplyI (i+1) max + mkApplyM max + mkApplyN max + emit "}\n" --- Make string: "object* a1, object* a2, ..., object** an" -def mk_arg_decls' (n : nat) : string := -string.join $ (n.repeat (λ i r, r ++ [sformat! "object* a{i+1}"]) []).intersperse ", " +-- make string: "object* a1, object* a2, ..., object** an" +def mkArgDecls' (n : Nat) : String := + genSeq n (s!"object* a{·+1}") -def mk_apply_h (max : nat) : m unit := -do mk_copyright, - emit "// DO NOT EDIT, this is an automatically generated file\n", - emit "// Generated using script: ../../gen/apply.lean\n", - emit "#pragma once\n", - emit "#include \"runtime/object.h\"\n", - emit $ sformat! "#define LEAN_CLOSURE_MAX_ARGS {max}" - emit "namespace lean {\n", - max.mrepeat $ λ i, - let args := mk_arg_decls' (i+1) in - emit $ sformat! "object* apply_{i+1}(object* f, {args});\n", - emit "object* apply_n(object* f, unsigned n, object** args);\n", - emit $ sformat! "// pre: n > {max}\n", - emit "object* apply_m(object* f, unsigned n, object** args);\n", - emit "}\n" +def mkApplyH (max : Nat) : M Unit := do + mkCopyright + emit "// DO NOT EDIT, this is an automatically generated file +// Generated using script: ../../gen/apply.lean +#pragma once +#include \"runtime/object.h\" +#define LEAN_CLOSURE_MAX_ARGS {max}" + emit "namespace lean {\n" + for i in [0:max] do + let args := mkArgDecls' (i+1) + emit s!"object* apply_{i+1}(object* f, {args}); +object* apply_n(object* f, unsigned n, object** args); +// pre: n > {max} +object* apply_m(object* f, unsigned n, object** args); +}\n" --- #eval (mk_apply_cpp 4).run none +-- #eval (mkApplyCpp 4).run none -#eval (mk_apply_cpp lean.closure_max_args).run "..//src//runtime//apply.cpp" -#eval (mk_apply_h lean.closure_max_args).run "..//src//runtime//apply.h" +#eval (mkApplyCpp Lean.closureMaxArgs).run "../src/runtime/apply.cpp" +#eval (mkApplyH Lean.closureMaxArgs).run "../src/runtime/apply.h"