0
$\begingroup$

I have a Gallina (Coq) program that I am extracting to OCaml. The program is a (symbolic) interpreter for a small programming language, and I defined functions to stringify the states so I can print them. Unfortunately these functions are the real bottleneck in the code: While it can take a few millis to produce a final state, it can take hours to convert them to string - states are very big inductive data structures. I suspect that the problem is due to the many string concatenation operations done recursively by code like e.g.:

Fixpoint stringify (x : state) : string :=
  match state with
  | a => "a"
  | b x y => b ++ (stringify x) ++ (stringify y)
  ...

Can you suggest a more efficient way to extract string code to OCaml, or to implement the Gallina functions?

P.S. Sorry for the sketchy description of the problem. I preferred to stay abstract rather than to provide details that might be not really relevant (I have no clear idea of which part of the stringification code is slow). If you ask me I will provide more details.

$\endgroup$
2
  • $\begingroup$ Alas, in most cases staying abstract is the wrong thing to do. How do you know you abstracted correctly? It is very likely that your concrete problem has a concrete solution. $\endgroup$ Jul 15, 2023 at 8:30
  • $\begingroup$ If it can be useful I shared my code at github.com/pietrobraione/pose. The incriminated code is at Prettyprint.v (convert state to string) and Smt.v (convert state predicate to SMTLIB). $\endgroup$ Jul 16, 2023 at 7:08

3 Answers 3

2
$\begingroup$

Indeed, if you naively concatenate strings then it may take time quadratic in the size of the final string to build it. (a nested concatenation (.. (a0 ++ a1) ++ ..) ++ an will copy each substring ai (n-i) times instead of just once.) Instead you should use a data structure that supports efficient concatenation, like trees or difference lists.

Definition dstring := string -> string.  (* difference lists *)
Definition from_string (s : string) : dstring := fun t => s ++ t.
Definition append (f g : dstring) : dstring := fun t => f (g t).
Definition to_string (f : dstring) : string := f "".

Another possible source of slowness is that Coq strings get extracted to OCaml lists instead of OCaml strings by default, but (1) that probably only has a minor effect, (2) that's what makes the "difference lists" encoding above work (otherwise you'd have to use list char explicitly).

$\endgroup$
5
  • $\begingroup$ Thank you for the explanation. I am currently extracting Coq strings to OCaml strings (I am importing extraction.ExtrOcamlNativeString.) I have changed to extract Coq strings to list char (extraction.ExtrOcamlString) and I have used the dstring type in place of Coq string, but I can't see any improvement. I will debug and try to understand what's happening. Do you see any gross mistake? $\endgroup$ Jul 15, 2023 at 8:01
  • $\begingroup$ Can you share your code? $\endgroup$
    – Li-yao Xia
    Jul 15, 2023 at 11:58
  • $\begingroup$ You find it at github.com/pietrobraione/pose. See Prettyprint.v and Smt.v. Branch dl is the implementation with difference lists (the dstring type and related stuff is in Aux.v). $\endgroup$ Jul 15, 2023 at 20:16
  • $\begingroup$ By thinking about my code I realized I was still conjoining strings in many places. So I followed the advice from Andrej Bauer and now I am pervasively using a dstring = List string type, that I never flatten. The OCaml code that prints a dstring scans the list and prints each single string. Now everything is fast, but my longest executions exhaust the stack (even with max ulimit), so maybe I shall find a tradeoff. I will post my code on the dl branch. $\endgroup$ Jul 16, 2023 at 15:42
  • $\begingroup$ Why are you even converting to strings? Just output directly using Format by traversing your data structures (and if you make the traversals tail-recursive, your stack oveflows will be gone). $\endgroup$ Jul 16, 2023 at 19:25
1
$\begingroup$

Two suggestions come to mind:

  1. Do not convert to strings in Coq. Write custom functions in OCaml and use Extract Constant, as described in the documentation. More generally, it's probably a good idea to implement non-critical code in OCaml directly, anyhow.

  2. If you have very large states to output, why are you even converting them to strings? You should write custom functions that directly output states using the OCaml Format module. (Here's a pretty involved example that handles bound variables and parentheses, with some luck you don't need all of that.)

$\endgroup$
2
  • $\begingroup$ Your last advice was the right one. I was able to radically cut times, I discuss my approach under Li-yao Xia answer. $\endgroup$ Jul 16, 2023 at 15:38
  • $\begingroup$ Do you see those little up arrows on the left? That's why we write answers. $\endgroup$ Jul 16, 2023 at 19:24
0
$\begingroup$

I am posting a followup to tell how, by applying the suggestions of Li-yao Xia (avoid quadratic explosion by storing the strings in a data structure) and of Andrej Bauer (do not even concatenate the strings, just print them) the problem was solved. A big thank you to both.

  • I defined a type dstring := list string. Since just storing the strings on some cases generates a stack overflow, I am extracting Coq strings to native OCaml strings to avoid having lots of char lists. Moreover, the concatenation function for dstrings alternates between appending the lists and concatenating the strings at the borders, so that in a dstring list the Coq strings are always kept to a length of about 30 chars.
  • The OCaml code never converts dstrings to strings, and when it needs to print them just scans the list and prints each of them.

With some other unrelated optimizations now everything runs on all the examples at a fraction of the time (seconds insteads of hours) and does not exhaust the stack. Also, by tuning the minimum length of the Coq strings in dstring I can choose my trade-off between memory consumption and execution time, that is a useful degree of freedom for the next experiments. The code is in https://github.com/pietrobraione/pose (Aux.v, Prettyprint.v, Smt.v and dll.ml).

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.