<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="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">Users@cakeml.org</a><br>
<a href="https://lists.cakeml.org/listinfo/users" rel="noreferrer" target="_blank">https://lists.cakeml.org/<wbr>listinfo/users</a><br>
</blockquote></div><br></div>