move src/Experiments/NewPipeline/ to src/

1 files changed, 21 insertions, 21 deletions

diff --git a/Makefile b/Makefile
index 6e9ccbb4d..56cbed38a 100644
--- a/Makefile
+++ b/Makefile
@@ -78,12 +78,12 @@ UNMADE_C_FILES := \
 # files that are treated specially
 SPECIAL_VOFILES := \
 	src/Specific/%Display.vo \
-	src/Experiments/NewPipeline/ExtractionOCaml/%.vo \
-	src/Experiments/NewPipeline/ExtractionHaskell/%.vo
+	src/ExtractionOCaml/%.vo \
+	src/ExtractionHaskell/%.vo
 SPECIFIC_GENERATED_VOFILES := src/Specific/solinas%.vo src/Specific/montgomery%.vo
 # add files to this list to prevent them from being built as final
 # targets by the "lite" target
-NEW_PIPELINE_FILTER := src/Experiments/NewPipeline/%
+NEW_PIPELINE_FILTER := src/%
 LITE_UNMADE_VOFILES := src/Curves/Weierstrass/AffineProofs.vo \
 	src/Curves/Weierstrass/Jacobian.vo \
 	src/Curves/Weierstrass/Projective.vo \
@@ -92,12 +92,12 @@ LITE_UNMADE_VOFILES := src/Curves/Weierstrass/AffineProofs.vo \
 	src/Specific/NISTP256/AMD128/fe%.vo \
 	src/Specific/X25519/C64/ladderstep.vo \
 	src/Specific/X25519/C32/fe%.vo \
-	src/Experiments/NewPipeline/RewriterWf1.vo \
-	src/Experiments/NewPipeline/RewriterWf2.vo \
-	src/Experiments/NewPipeline/RewriterRulesGood.vo \
-	src/Experiments/NewPipeline/RewriterProofs.vo \
-	src/Experiments/NewPipeline/Toplevel2.vo \
-	src/Experiments/NewPipeline/SlowPrimeSynthesisExamples.vo \
+	src/RewriterWf1.vo \
+	src/RewriterWf2.vo \
+	src/RewriterRulesGood.vo \
+	src/RewriterProofs.vo \
+	src/Toplevel2.vo \
+	src/SlowPrimeSynthesisExamples.vo \
 	src/Experiments/SimplyTypedArithmetic.vo \
 	$(SPECIFIC_GENERATED_VOFILES)
 NOBIGMEM_UNMADE_VOFILES := \
@@ -114,12 +114,12 @@ NO_CURVES_PROOFS_UNMADE_VOFILES := src/Curves/Weierstrass/AffineProofs.vo \
 NO_CURVES_PROOFS_NON_SPECIFIC_UNMADE_VOFILES := $(filter $(NO_CURVES_PROOFS_UNMADE_VOFILES) src/Specific/%.vo,$(VOFILES))
 REAL_SPECIFIC_GENERATED_VOFILES := $(filter $(SPECIFIC_GENERATED_VOFILES),$(VOFILES))
 NEW_PIPELINE_PRE_VOFILES := $(filter $(NEW_PIPELINE_FILTER),$(REGULAR_VOFILES))
-PRE_STANDALONE_PRE_VOFILES := $(filter src/Experiments/NewPipeline/Standalone%.vo,$(REGULAR_VOFILES))
+PRE_STANDALONE_PRE_VOFILES := $(filter src/Standalone%.vo,$(REGULAR_VOFILES))
 UTIL_PRE_VOFILES := $(filter bbv/%.vo src/Algebra/%.vo src/Tactics/%.vo src/Util/%.vo,$(REGULAR_VOFILES))
 COQ_WITHOUT_NEW_PIPELINE_VOFILES := $(filter-out $(NEW_PIPELINE_FILTER),$(REGULAR_VOFILES))
 SOME_EARLY_VOFILES := \
-	src/Experiments/NewPipeline/Arithmetic.vo \
-	src/Experiments/NewPipeline/Rewriter.vo \
+	src/Arithmetic.vo \
+	src/Rewriter.vo \
 	src/Experiments/SimplyTypedArithmetic.vo
 
 SELECTED_PATTERN := \
@@ -543,33 +543,33 @@ STANDALONE := \
 	saturated_solinas \
 	word_by_word_montgomery
 
-$(STANDALONE:%=src/Experiments/NewPipeline/ExtractionOCaml/%.ml) : %.ml : %.v src/Experiments/NewPipeline/StandaloneOCamlMain.vo
+$(STANDALONE:%=src/ExtractionOCaml/%.ml) : %.ml : %.v src/StandaloneOCamlMain.vo
 	$(SHOW)'COQC $< > $@'
 	$(HIDE)$(TIMER_FULL) $(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) $< > $@.tmp
 	$(HIDE)sed 's/\r\n/\n/g; s/\r//g' $@.tmp > $@ && rm -f $@.tmp
 
-$(STANDALONE:%=src/Experiments/NewPipeline/ExtractionHaskell/%.hs) : %.hs : %.v src/Experiments/NewPipeline/StandaloneHaskellMain.vo src/Experiments/NewPipeline/haskell.sed
+$(STANDALONE:%=src/ExtractionHaskell/%.hs) : %.hs : %.v src/StandaloneHaskellMain.vo src/haskell.sed
 	$(SHOW)'COQC $< > $@'
 	$(HIDE)$(TIMER_FULL) $(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) $< > $@.tmp
-	$(HIDE)sed 's/\r\n/\n/g; s/\r//g' $@.tmp | sed -f src/Experiments/NewPipeline/haskell.sed > $@ && rm -f $@.tmp
+	$(HIDE)sed 's/\r\n/\n/g; s/\r//g' $@.tmp | sed -f src/haskell.sed > $@ && rm -f $@.tmp
 
 # pass -w -20 to disable the unused argument warning
-$(STANDALONE:%=src/Experiments/NewPipeline/ExtractionOCaml/%) : % : %.ml
+$(STANDALONE:%=src/ExtractionOCaml/%) : % : %.ml
 	$(TIMER_FULL) ocamlopt -w -20 -o $@ $<
 
-$(STANDALONE:%=src/Experiments/NewPipeline/ExtractionHaskell/%) : % : %.hs
+$(STANDALONE:%=src/ExtractionHaskell/%) : % : %.hs
 	$(TIMER_FULL) $(GHC) $(GHCFLAGS) -o $@ $<
 
 standalone: standalone-haskell standalone-ocaml
 
-standalone-haskell: $(STANDALONE:%=src/Experiments/NewPipeline/ExtractionHaskell/%)
-standalone-ocaml: $(STANDALONE:%=src/Experiments/NewPipeline/ExtractionOCaml/%)
+standalone-haskell: $(STANDALONE:%=src/ExtractionHaskell/%)
+standalone-ocaml: $(STANDALONE:%=src/ExtractionOCaml/%)
 
 UNSATURATED_SOLINAS_C_FILES := curve25519_64.c curve25519_32.c p521_64.c p521_32.c # p224_solinas_64.c
 WORD_BY_WORD_MONTGOMERY_C_FILES := p256_64.c p256_32.c p384_64.c p384_32.c secp256k1_64.c secp256k1_32.c p224_64.c p224_32.c
 FUNCTIONS_FOR_25519 := carry_mul carry_square carry_scmul121666 carry add sub opp selectznz to_bytes from_bytes
-UNSATURATED_SOLINAS := src/Experiments/NewPipeline/ExtractionOCaml/unsaturated_solinas
-WORD_BY_WORD_MONTGOMERY := src/Experiments/NewPipeline/ExtractionOCaml/word_by_word_montgomery
+UNSATURATED_SOLINAS := src/ExtractionOCaml/unsaturated_solinas
+WORD_BY_WORD_MONTGOMERY := src/ExtractionOCaml/word_by_word_montgomery
 ALL_C_FILES := $(UNSATURATED_SOLINAS_C_FILES) $(WORD_BY_WORD_MONTGOMERY_C_FILES)
 .PHONY: c-files
 c-files: $(ALL_C_FILES)