Is it possible to define a macro that implements another function? I’m trying to write a macro that lets you define a “main” function that takes argc and argv as expected, but also takes views for things like “you have a readable file descriptor at int 0” and “errno is unset” to represent “global” process state that can be changed and tracked linearly. Currently, I have this, which is failing to compile:
(* Set a given function to be the POSIX entry point
*
* This is equivalent to implementing main as the passed in function,
* except that in addition to argc and argv views corresponding to initial
* global program state in the POSIX environment are passed.
*
* Currently, an errno_v ( free ) proof is passed. In the future, proofs
* corresponding to open file descriptors for stdin, stdout, and stderr will
* be passed as well
*)
macdef set_posix_entrypoint ( func ) =
implement main ( argc, argv ) = let
extern praxi { v: view } __assert_view (): v
prval ev = __assert_view < errno_v ( free ) > ()
val res = ,(func) ( ev | argc, argv )
extern praxi { v: view } __unassert_view ( x: v ): ()
prval () = __unassert_view ( ev )
in res end
481(line=12, offs=3) -- 490(line=12, offs=12): error(parsing): the syntactic entity [d0exp] is needed.
(the line and offsets refer to the word “implement” above). It’s unclear to me how to continue, sorry for my ignorance!
Thanks,
Shea