# Default inlinings of Coq Extraction

While working with Coq’s JSON extraction, Thomas and I were quite puzzled when the AST generated by extraction did not match the original Gallina syntax: Some functions were silently unfolded, even though we never told Coq to do so. With Tej’s help, we figured out what’s going on, and after some thinking, it all started to make sense.

In the following, I will use OCaml extraction instead of JSON extraction,
because the puzzlers are the same, but OCaml code is much more concise than
JSON code.
The original puzzler was the following:

Require Extraction.

Definition foo(a b: bool): bool := orb a b.

Extraction Language OCaml.

Extraction foo.

It outputs

let foo a b =

match a with

| True -> True

| False -> b
so orb got silently unfolded, even though we never told Coq to do so.
Let's try another extraction language:

let foo a b =

match a with

| True -> True

| False -> b

Extraction Language Haskell.

Extraction foo.

And suddenly we get what we want:

foo :: Bool -> Bool -> Bool

foo =

orb
What if we define our own orb?

foo :: Bool -> Bool -> Bool

foo =

orb

Definition myorb(b1 b2 : bool) := if b1 then true else b2.

Definition foo'(a b: bool): bool := myorb a b.

Extraction Language OCaml.

Extraction foo'.

We also get what we want:

let foo' =

myorb
What if we mark foo as opaque?

let foo' =

myorb

No luck:

let foo a b =

match a with

| True -> True

| False -> b
So we entered a clone of the Coq source code and played with some grep commands like

grep -R . --include='*.ml' -e '[^a-zA-Z]orb[^A-Za-z]' -C3
which eventually pointed us to the file plugins/extraction/mlutil.ml, which contains
a list of hard-coded always-inlined constants:

let manual_inline_set =

List.fold_right (fun x -> Cset_env.add (con_of_string x))

[ "Coq.Init.Wf.well_founded_induction_type";

"Coq.Init.Wf.well_founded_induction";

"Coq.Init.Wf.Acc_iter";

"Coq.Init.Wf.Fix_F";

"Coq.Init.Wf.Fix";

"Coq.Init.Datatypes.andb";

"Coq.Init.Datatypes.orb";

"Coq.Init.Logic.eq_rec_r";

"Coq.Init.Logic.eq_rect_r";

"Coq.Init.Specif.proj1_sig";

]

Cset_env.empty
So that's why orb was inlined, but myorb was not!
And further down in that file, we see

let inline r t =

not (to_keep r) (* The user DOES want to keep it *)

&& not (is_inline_custom r)

&& (to_inline r (* The user DOES want to inline it *)

|| (lang () != Haskell && not (is_projection r) &&

(is_recursor r || manual_inline r || inline_test r t)))
so there's a special case for Haskell, which is why we got the desired result in Haskell,
but not in OCaml.
Now,
In OCaml, which has strict evaluation semantics, we want to enable short-circuiting of
boolean expressions. For instance, if the Coq source contains orb somethingTrue expensiveCalculation,
the expensiveCalculation should not be evaluated in OCaml.
This can be achieved by always inlining orb, so that the OCaml code is
if somethingTrue then true else expensiveCalculation.
On the other hand, Haskell has lazy evaluation semantics, so we don't need to do anything
special in Haskell, but can just extract it to orb somethingTrue expensiveCalculation,
and expensiveCalculation will be wrapped inside a thunk which is never evaluated.
So we now understand what's going on, but how do we get our example to behave the way it
should?
It turns out that reading the manual page for Extraction helps: It tells us about the vernac command Extraction NoInline qualid, so
we can do the following:

let foo a b =

match a with

| True -> True

| False -> b

grep -R . --include='*.ml' -e '[^a-zA-Z]orb[^A-Za-z]' -C3

let manual_inline_set =

List.fold_right (fun x -> Cset_env.add (con_of_string x))

[ "Coq.Init.Wf.well_founded_induction_type";

"Coq.Init.Wf.well_founded_induction";

"Coq.Init.Wf.Acc_iter";

"Coq.Init.Wf.Fix_F";

"Coq.Init.Wf.Fix";

"Coq.Init.Datatypes.andb";

"Coq.Init.Datatypes.orb";

"Coq.Init.Logic.eq_rec_r";

"Coq.Init.Logic.eq_rect_r";

"Coq.Init.Specif.proj1_sig";

]

Cset_env.empty

let inline r t =

not (to_keep r) (* The user DOES want to keep it *)

&& not (is_inline_custom r)

&& (to_inline r (* The user DOES want to inline it *)

|| (lang () != Haskell && not (is_projection r) &&

(is_recursor r || manual_inline r || inline_test r t)))

*why*are things so surprising and non-uniform? Is this a bug or a feature? After some thinking, I concluded that it's a feature:Extraction NoInline orb.

Extraction foo.

and woohoo, we get what we want:

let foo =

orb
Problem solved!

let foo =

orb