How do I extract efficient string code in Coq to OCaml?

Question

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.

Answer 1

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).

Answer 2

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.)

Answer 3

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).