Tracking bugs of the extraction plugin

.markdown

https://github.com/coq/coq/labels/part%3A%20extraction

• Module typing: #10367, #5795, #5274, #1957

• Inlining constants declared in opaque module breaks module abstraction and typing: #4351

• Value restriction: #10502, #7954, #6614, #5705, #4875

• Name conflicts, blacklist, and fresh name generation: #7017, #5397, #3846, #2904

• Exponential behavior caused by generalized iota reduction: #7830

• Record projection: #7348

• Unused definitions: #4650

• Haskell+module producing duplication: #8152, #5754

• Other bugs: #11359, #11148, #9416, #8331, #7870, #7302, #7191, #5668, #4749, #4741, #4449, #4227

• Feature requests: #8042, #5652, #5541, #5518, #5515, #5106, #4427, #4189, #3847, #2747, #2157

1957.v

(* Module typing: issues #10367, #5795, #5274, and #1957 *)
Require Extraction.

(*************)
(* Example 1 *)
(*************)

Module Type S1.
Parameter T : bool -> Type.
Parameter x : T true.
End S1.

(*
`M1.x` should have type `M1.T true` but have type `bool`. They are convertible
in Coq but not unifiable in OCaml. `environment_until` in `extract_env.ml` takes
bodies of opaque definitions and does something wrong.
*)
Module M1 : S1.
Definition T (b : bool) := if b then bool else nat.
Definition x := true.
End M1.

Extraction "m1" M1.
Fail Extraction TestCompile M1.
(*
       In module M1:
       Modules do not match:
         sig type coq_T = __ val x : bool end
       is not included in
         S1
       In module M1:
       Values do not match: val x : bool is not included in val x : coq_T
*)

(* Even if one put the right type annotation `x : T true` this does fail. *)
Module M1' : S1.
Definition T (b : bool) := if b then bool else nat.
Definition x : T true := true.
End M1'.

Print M1'.
Eval compute in M1'.T.

Extraction M1'.
Fail Extraction TestCompile M1'.

(*
Once the module typing is checked inside the kernel, the types of
implementations should be convertible to their signatures. So casting
implementations with their signature and then extraction with preventing some
type reduction would work (full fix), and `Obj.magic`s would be inserted
appropriately, but the computation of such the type might be complicated
especially in the case of functors.
*)

(*
One may write a module implementation in a non-topologically sorted order.
So we should reorder them.
*)
Module M1'' : S1.
Definition x := true.
Definition T (b : bool) := if b then bool else nat.
End M1''.

Extraction M1''.
Fail Extraction TestCompile M1''.

(*************)
(* Example 2 *)
(*************)

Module Type S2.
Parameter T : Type.
Parameter x : T.
End S2.

Module M2 : S2.
Definition T := Prop.
Definition x : T := True.
End M2.

Extraction M2.
Fail Extraction TestCompile M2.
(*
       In module M2:
       Modules do not match:
         sig type coq_T = __ type x = __ end
       is not included in
         S2
       In module M2:
       The value `x' is required but not provided
 *)

(*************)
(* Example 3 *)
(*************)

Module Type S3.
Parameter T : bool -> Type.
Parameter x : T true.
End S3.

Module M3.
Definition T (b : bool) := if b then bool else nat.
Definition x := false.
End M3.

Module F3 (M : S3).
Definition T (b : bool) := (M.T b * M.T b)%type.
Definition x : T true := (M.x, M.x).
End F3.

Module M3' := F3 M3.

Extraction M3'.
Fail Extraction TestCompile M3'.

(*************)
(* Example 4 *)
(*************)

Module Type S4.
Parameter T : Type.
Parameter x : T.
End S4.

Module M4.
Definition T := Prop.
Definition x := True.
End M4.

Module F4 (M : S4).
Definition T := (M.T * M.T)%type.
Definition x := (M.x, M.x).
End F4.

Module M4' := F4 M4.

Extraction M4'.
Fail Extraction TestCompile M4'.

5705.v

Require Extraction.

Module Foo.

Variant bool : Type := true | false.

(*
Inferred type of `skip_fun` is `'a -> 'a` but its body is not a value and so
type is monomorphized to `'_a -> '_a`. This doesn't match with `bool -> bool`
unless implementation contains the explicit type annotation.
*)
Definition skip_fun : bool -> bool :=
  let f A (x : A) := x in f _ (f _).

End Foo.

Recursive Extraction Foo.
Extraction TestCompile Foo.
(*
       In module Foo:
       Values do not match:
         val skip_fun : '_weak1 -> '_weak1
       is not included in
         val skip_fun : bool -> bool
*)

7830.v

Require Extraction.
Extraction Language OCaml.

Inductive T : Set := X | Y | Z.

Fixpoint u (k : nat) (n : T) : nat :=
  match k with
    | 0 => 0
    | S k =>
      match
        match n with
        | X => (tt, X)
        | _ => (tt, n)
        end
      with
      | (_, _) => u k n
      end
  end.
Definition careful := Eval cbv in fun n => u 10 n.

Print careful.

Unset Extraction Optimize.
Recursive Extraction careful.
(*
let careful n =
  let Pair (_, _) = match n with
                    | X -> Pair (Tt, X)
                    | Y -> Pair (Tt, n)
                    | Z -> Pair (Tt, n) in
...
  let Pair (_, _) = match n with
                    | X -> Pair (Tt, X)
                    | Y -> Pair (Tt, n)
                    | Z -> Pair (Tt, n) in O
*)
Set Extraction Optimize.
Recursive Extraction careful. (* exponential *)