chore: update script/apply.lean syntax
This commit is contained in:
Sebastian Ullrich
Leonardo de Moura
parent
95df68f3e4
commit
5be816244e
1 changed files with 163 additions and 173 deletions
|
|
@ -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<fn{i}>(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<fn{i}>(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<obj**>(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<obj**>(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<obj**>(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<obj**>(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<fn{i+1}>(f)({as});\n",
|
||||
emit "default: return reinterpret_cast<fnn>(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<fn{i+1}>(f)({as});
|
||||
default: return reinterpret_cast<fnn>(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<obj**>(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<obj**>(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<obj**>(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<obj**>(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<obj*> 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<fnn>(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<fnn>(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"
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue