<div dir="ltr"><div><div>Hi again Lars,<br><br></div>Here's another simpler method to obtain the names of the basis library functions. (Magnus suggested it to me off list.) It retrieves the names, which are suggestive, but not the types (which would be even more so).<br><br></div>I put the result of running the following code at <a href="https://cakeml.org/basis-names.txt">https://cakeml.org/basis-names.txt</a> for now. (But don't expect that link to be kept up to date, or even alive.)<br><div><br>val _ = translation_extends"basisProg"<br>val () = Globals.max_print_depth := 20;<br><br>val get_dec_names_def = Define`<br>  get_dec_names (Dlet _ p _) = pat_bindings p [] ∧<br>  get_dec_names (Dletrec _ funs) = MAP FST funs ∧<br>  get_dec_names _ = []`;<br><br>val get_top_names_def = Define`<br>  get_top_names (Tdec d) = get_dec_names d ∧<br>  get_top_names (Tmod mn _ ds) = MAP ((++) (mn++".")) (FLAT (MAP get_dec_names ds))`;<br><br>val get_prog_names_def = Define`<br>  get_prog_names prog = FLAT (MAP get_top_names prog)`;<br><br>val prog_tm =<br>  get_ml_prog_state() |> remove_snocs |> clean_state |> get_thm<br>  |> concl |> strip_comb |> #2 |> el 3<br><br>val names =<br>  EVAL``get_prog_names ^prog_tm`` |> rconc<br>  |> listSyntax.dest_list |> #1<br>  |> map stringSyntax.fromHOLstring<br><br>app (fn x => (print x; print"\n")) names<br><br></div><div>Cheers,<br></div><div>Ramana<br></div></div><div class="gmail_extra"><br><div class="gmail_quote">On 20 July 2017 at 18:55, Ramana Kumar <span dir="ltr"><<a href="mailto:Ramana.Kumar@cl.cam.ac.uk" target="_blank">Ramana.Kumar@cl.cam.ac.uk</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><div><div><div><div><div><div>Hi Lars,<br><br></div>I don't think there's a list of the basis contents, and it's not trivial (off the top of my head) to generate one unfortunately.<br></div>Here's one way you could try: print the entire basis program in concrete syntax then try (maybe using some existing SML processing tools?) to get the function names from that.<br></div>You can get the basis program in a hacky way with something like this:<br><br>open preamble basisProgTheory ml_translatorLib ml_progLib astPP<br>val _ = translation_extends"basisProg"<br>val () = astPP.enable_astPP();<br>val () = Globals.max_print_depth := 20;<br>val prog_tm =<br>  get_ml_prog_state() |> remove_snocs |> clean_state |> get_thm<br>  |> concl |> strip_comb |> #2 |> el 3<br><br></div>There is no 'a -> string function. I know there is Int.toString, but for most other types you need to define your own show functions.<br><br></div>Cheers,<br></div>Ramana<br><div><div><div><br></div></div></div></div><div class="HOEnZb"><div class="h5"><div class="gmail_extra"><br><div class="gmail_quote">On 20 July 2017 at 18:41, Lars Hupel <span dir="ltr"><<a href="mailto:hupel@in.tum.de" target="_blank">hupel@in.tum.de</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Dear CakeML developers,<br>
<br>
is there any list of predefined functions/modules in CakeML? I found<br>
some using trial and error, but I'm having a hard time reading the HOL4<br>
scripts in 'basis/'.<br>
<br>
And on the off chance: Is there a function 'a -> string? Otherwise I'll<br>
have to resort to generating "show" functions myself.<br>
<br>
Cheers<br>
Lars<br>
<br>
______________________________<wbr>_________________<br>
Users mailing list<br>
<a href="mailto:Users@cakeml.org" target="_blank">Users@cakeml.org</a><br>
<a href="https://lists.cakeml.org/listinfo/users" rel="noreferrer" target="_blank">https://lists.cakeml.org/listi<wbr>nfo/users</a><br>
</blockquote></div><br></div>
</div></div></blockquote></div><br></div>