Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Add example from https://github.com/coq/coq/issues/16172 again #23

Open
wants to merge 1 commit into
base: master
Choose a base branch
from
Open

Add example from https://github.com/coq/coq/issues/16172 again #23

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
35 changes: 35 additions & 0 deletions src/exponential_extraction.v
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,35 @@
Module Type T.
Parameter t : Type.
End T.

Module F (X:T).
(* number of occurences determines the exponential: here 4 *)
Definition t : Type := X.t * X.t * X.t * X.t.
End F.

Require Import Coq.extraction.Extraction.

Module A0. Definition t := nat. End A0.

Module A1 := F A0.
Module A2 := F A1.
Module A3 := F A2.
Module A4 := F A3.
Module A5 := F A4.
Module A6 := F A5.
Module A7 := F A6.
Module A8 := F A7.
Module A9 := F A8.

Set Boolean Equality Schemes.
Time Record Foo5 := { foo5 : A5.t }. (* 0.037s *)
Time Record Foo6 := { foo6 : A6.t }. (* 0.06 s *)
Time Record Foo7 := { foo7 : A7.t }. (* 0.248s *)
Time Record Foo8 := { foo8 : A8.t }. (* 1.015s *)
Time Record Foo9 := { foo9 : A9.t }. (* 3.811s *)

Time Redirect "A5" Recursive Extraction A5.t. (* 0.009s *)
Time Redirect "A6" Recursive Extraction A6.t. (* 0.041s *)
Time Redirect "A7" Recursive Extraction A7.t. (* 0.177s *)
Time Redirect "A8" Recursive Extraction A8.t. (* 0.744s *)
Time Redirect "A9" Recursive Extraction A9.t. (* 3.12 s *)
Loading