Found ** in Ocaml, but not for exponentiation

Question

In a book about logics (https://www.cl.cam.ac.uk/~jrh13/atp/OCaml/real.ml), I find this kind of code:

let integer_qelim =
   simplify ** evalc **
   lift_qelim linform (cnnf posineq ** evalc) cooper;;

I have seen ** before, but it was for exponentiation purposes, whereas here I do not think it is used for that, as the datatypes are not numeric. I would say it is some king of function combinator, but no idea.

I think this book was written for a version 3.06, but an updated code for 4 (https://github.com/newca12/ocaml-atp) maintains this, so ** is still used in that way that I do not understand.

Answer 1

In OCaml, you can bind to operators any behavior, e.g.,

let ( ** ) x y = print_endline x; print_endline y

so that "hello" ** "world" would print

hello
world

In the code that you reference, the (**) operator is bound to function composition:

let ( ** ) = fun f g x -> f(g x)

Answer 2

That's an utility-function defined in lib.ml:

let ( ** ) = fun f g x -> f(g x);;

It's a composition-operator, often referred to as compose in other examples.

You can use it like this:

let a x = x^"a" in
let b x = x^"b" in
let c x = x^"c" in
let foo = a ** b ** c in
foo "input-";;
- : string = "input-cba"

You could write it as

let foo x = a (b (c x))

or

let foo x = a @@ b @@ c x

or

let foo x = c x |> b |> a

as well.