separate Ed25519Extraction.v, add extraction to Makefile

@JasonGross: src/Specific/GF25519Bounded.v has another constant that I
think needs a extraction-friendly version, I added a comment

1 files changed, 17 insertions, 1 deletions

diff --git a/Makefile b/Makefile
index 6a643fa7b..e1f99befe 100644
--- a/Makefile
+++ b/Makefile
@@ -12,7 +12,8 @@ HIDE := $(if $(VERBOSE),,@)
 
 .PHONY: coq clean update-_CoqProject cleanall install \
 	install-coqprime clean-coqprime coqprime \
-	specific non-specific
+	specific non-specific \
+	extraction ghc
 
 SORT_COQPROJECT = sed 's,[^/]*/,~&,g' | env LC_COLLATE=C sort | sed 's,~,,g'
 
@@ -84,6 +85,21 @@ Makefile.coq: Makefile _CoqProject
 	$(SHOW)'COQ_MAKEFILE -f _CoqProject > $@'
 	$(HIDE)$(COQBIN)coq_makefile -f _CoqProject | sed s'|^\(-include.*\)$$|ifneq ($$(filter-out $(FAST_TARGETS),$$(MAKECMDGOALS)),)~\1~else~ifeq ($$(MAKECMDGOALS),)~\1~endif~endif|g' | tr '~' '\n' | sed s'/^clean:$$/clean::/g' | sed s'/^Makefile: /Makefile-old: /g' | sed s'/^printenv:$$/printenv::/g' > $@
 
+src/Experiments/Ed25519_noimports.hs: src/Experiments/Ed25519Extraction.vo src/Experiments/Ed25519Extraction.v
+
+src/Experiments/Ed25519.hs: src/Experiments/Ed25519_noimports.hs src/Experiments/Ed25519_imports.hs
+	( cd src/Experiments && \
+		< Ed25519_noimports.hs \
+		sed "/import qualified Prelude/r Ed25519_imports.hs" | \
+	  sed 's/ Ed25519_noimports / Ed25519 /g' \
+		> Ed25519.hs )
+
+src/Experiments/Ed25519.o src/Experiments/Ed25519.core: src/Experiments/Ed25519.hs
+	( cd src/Experiments && ghc -O3 Ed25519.hs -ddump-simpl > Ed25519.core )
+
+extraction: src/Experiments/Ed25519.hs
+ghc: src/Experiments/Ed25519.core
+
 clean::
 	rm -f Makefile.coq