Move rust extraction (#219)

.github/coq-concert.opam.locked

@@ -20,6 +20,7 @@ depends: [
   "coq-metacoq-template" {= "8.16.dev"}
   "coq-metacoq-template-pcuic" {= "8.16.dev"}
   "coq-metacoq-utils" {= "8.16.dev"}
+  "coq-rust-extraction" {= "dev"}
   "coq-quickchick" {= "1.6.4"}
   "coq-stdpp" {= "1.8.0"}
 ]
@@ -62,4 +63,8 @@ pin-depends: [
     "coq-metacoq-utils.8.16.dev"
     "git+https://github.com/MetaCoq/metacoq.git#b96e7570a5e7fd959fe171d63398f4491fed338a"
   ]
+  [
+    "coq-rust-extraction.dev"
+    "git+https://github.com/AU-COBRA/coq-rust-extraction.git#11914d450868173dcde57fc11abc700bf55c8a0c"
+  ]
 ]

coq-concert.opam

@@ -25,6 +25,7 @@ depends: [
   "coq-metacoq-pcuic" {= "8.16.dev"}
   "coq-metacoq-safechecker" {= "8.16.dev"}
   "coq-metacoq-erasure" {= "8.16.dev"}
+  "coq-rust-extraction" {= "dev"}
   "coq-stdpp" {>= "1.6.0" & <= "1.8.0"}
 ]
 
@@ -36,6 +37,7 @@ pin-depends: [
   ["coq-metacoq-pcuic.8.16.dev" "git+https://github.com/MetaCoq/metacoq.git#b96e7570a5e7fd959fe171d63398f4491fed338a"]
   ["coq-metacoq-safechecker.8.16.dev" "git+https://github.com/MetaCoq/metacoq.git#b96e7570a5e7fd959fe171d63398f4491fed338a"]
   ["coq-metacoq-erasure.8.16.dev" "git+https://github.com/MetaCoq/metacoq.git#b96e7570a5e7fd959fe171d63398f4491fed338a"]
+  ["coq-rust-extraction.dev" "git+https://github.com/AU-COBRA/coq-rust-extraction.git#11914d450868173dcde57fc11abc700bf55c8a0c"]
 ]
 
 build: [

examples/_CoqProject

@@ -7,7 +7,6 @@
 -R ../embedding/theories ConCert.Embedding
 -R ../embedding/extraction ConCert.Embedding.Extraction
 -R ../extraction/theories ConCert.Extraction
--R ../extraction/plugin/theories ConCert.Extraction
 
 -Q eip20 ConCert.Examples.EIP20
 eip20/EIP20Token.v

examples/counter/extraction/CounterRust.v

@@ -1,7 +1,7 @@
 From ConCert.Examples.Counter Require Counter.
 From ConCert.Extraction Require Import Common.
 From ConCert.Extraction Require Import ConcordiumExtract.
-From ConCert.Extraction Require Import RustExtract.
+From RustExtraction Require Import RustExtract.
 From Coq Require Import Bool.
 From Coq Require Import String.
 From MetaCoq.Template Require Import All.

examples/stackInterpreter/StackInterpreterRustExtract.v

@@ -1,9 +1,9 @@
 From ConCert.Examples.StackInterpreter Require Import StackInterpreter.
-From ConCert.Extraction Require Import RustExtract.
+From RustExtraction Require Import RustExtract.
+From RustExtraction Require Import Printing.
 From ConCert.Extraction Require Import Common.
-From ConCert.Extraction Require Import Printing.
 From ConCert.Extraction Require Import ConcordiumExtract.
-From ConCert.Utils Require Import StringExtra.
+From RustExtraction Require Import StringExtra.
 From MetaCoq.Template Require Import All.
 From MetaCoq.TemplatePCUIC Require Import PCUICToTemplate.
 From Coq Require Import String.

extraction/CoqMakefile.local

@@ -1,7 +1,3 @@
-post-all::
-	@echo "Done extracting the extraction, processing produced files!"
-	./process_extraction.sh
-
 FILENAMES = $(notdir $(VFILES:.v=))
 DPDFILES = $(VFILES:.v=.dpd)
 DOTFILES = $(VFILES:.v=.dot)

extraction/Makefile

@@ -1,4 +1,4 @@
-all: theory plugin
+all: theory
 .PHONY: all
 
 CoqMakefile: _CoqProject
@@ -11,7 +11,6 @@ theory: CoqMakefile
 clean: CoqMakefile
 	+@make -f CoqMakefile clean
 	rm -f CoqMakefile
-	+@make -C plugin clean
 .PHONY: clean
 
 install: CoqMakefile
@@ -22,9 +21,6 @@ uninstall: CoqMakefile
 	+@make -f CoqMakefile uninstall
 .PHONY: uninstall
 
-plugin: theory
-	+make -C plugin
-.PHONY: plugin
 
 # Forward most things to Coq makefile. Use 'force' to make this phony.
 %: CoqMakefile force
@@ -35,7 +31,7 @@ all: theory process-extraction-examples
 # Do not forward these files
 Makefile _CoqProject: ;
 
-process-extraction-examples: theory plugin
+process-extraction-examples: theory
 	./process-extraction-examples.sh
 .PHONY: process-extraction-examples
 
@@ -52,19 +48,14 @@ LIGO_DIST=$(patsubst $(LIGO_SRC_DIR)/%.mligo,$(LIGO_SRC_DIR)/%.tz,$(LIGOFILES))
 CONCORDIUM_DIR=./tests/extracted-code/concordium-extract
 MIDLANG_DIR=./tests/extracted-code/midlang-extract
 
-RUST_DIR=./tests/extracted-code/rust-extract
-
 ELM_DIR=./tests/extracted-code/elm-extract
 ELM_WEB_APP_DIR=./tests/extracted-code/elm-web-extract
 
-test-extraction: test-elm test-liquidity test-ligo test-rust test-concordium
+test-extraction: test-elm test-liquidity test-ligo test-concordium
 
 test-concordium: clean-compiled-concordium
 	$(foreach dir, $(wildcard $(CONCORDIUM_DIR)/*-extracted), cd $(dir) && cargo concordium test && cd ../../../..;)
 
-test-rust: clean-compiled-rust
-	$(foreach dir, $(wildcard $(RUST_DIR)/*-extracted), cd $(dir) && cargo run && cd ../../../..;)
-
 test-elm:
 	mkdir -p $(ELM_DIR)/src
 	cd $(ELM_DIR); elm-test
@@ -91,17 +82,13 @@ clean-compiled-concordium:
 	$(foreach dir, $(wildcard $(CONCORDIUM_DIR)/*-extracted), rm -f -r $(dir)/target;)
 .PHONY: clean-compiled-concordium
 
-clean-compiled-rust:
-	$(foreach dir, $(wildcard $(RUST_DIR)/*-extracted), rm -f -r $(dir)/target;)
-.PHONY: clean-compiled-rust
-
 clean-compiled-elm:
 	rm -f -r $(ELM_WEB_APP_DIR)/elm-stuff
 	rm -f -r $(ELM_WEB_APP_DIR)/index.html
 	rm -f -r $(ELM_DIR)/elm-stuff
 .PHONY: clean-comliped-elm
 
-clean-compiled-extraction: clean-compiled-elm clean-comiped-ligo clean-compiled-liquidity clean-compiled-rust clean-compiled-concordium
+clean-compiled-extraction: clean-compiled-elm clean-comiped-ligo clean-compiled-liquidity clean-compiled-concordium
 .PHONY: clean-compiled-extraction
 
 clean-extraction-out-files:
@@ -111,7 +98,6 @@ clean-extraction-out-files:
 	rm -f $(LIGO_DIR)/*.mligo.out
 	rm -f $(CONCORDIUM_DIR)/*.rs.out
 	rm -f $(MIDLANG_DIR)/*.midlang.out
-	rm -f $(RUST_DIR)/*.rs.out
 	$(foreach dir, $(wildcard $(CONCORDIUM_DIR)/*-extracted), rm -f -r $(dir)/*.rs.out;)
 
 clean-extraction-sources:
@@ -121,7 +107,6 @@ clean-extraction-sources:
 	rm -f $(LIQUIDITY_DIR)/liquidity.log
 	rm -f $(LIGO_DIR)/tests/*.mligo
 	rm -f $(MIDLANG_DIR)/tests/*.midlang
-	find $(RUST_DIR) -name 'main.rs' -delete
 	$(foreach dir, $(wildcard $(CONCORDIUM_DIR)/*-extracted), rm -f $(dir)/src/lib.rs;)
 .PHONY:clean-extraction-sources
 

extraction/_CoqProject

@@ -10,15 +10,10 @@ theories/CameLIGOPretty.v
 theories/Common.v
 theories/ConcordiumExtract.v
 theories/ElmExtract.v
-theories/ExtractExtraction.v
 theories/LiquidityExtract.v
 theories/LiquidityPretty.v
-theories/PluginExtract.v
 theories/PrettyPrinterMonad.v
-theories/Printing.v
-theories/RustExtract.v
 theories/SpecializeChainBase.v
-theories/TopLevelFixes.v
 
 -Q tests ConCert.Extraction.Tests
 tests/Ack.v
@@ -27,5 +22,4 @@ tests/ElmExtractExamples.v
 tests/ElmExtractTests.v
 tests/ElmForms.v
 tests/RecordExtractionLiquidityTests.v
-tests/RustExtractTests.v
-tests/NumLiteralTests.v
+tests/NumLiteralTests.v