Move elm extraction

.github/coq-concert.opam.locked

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

.github/workflows/build.yml

@@ -103,20 +103,6 @@ jobs:
           sudo chmod +x ./ligo
           sudo mv ligo /usr/local/bin/
 
-      - name: Set up Elm
-        run: |
-          curl -L -o elm.gz https://github.com/elm/compiler/releases/download/0.19.1/binary-for-linux-64-bit.gz
-          gunzip elm.gz
-          sudo chmod +x elm
-          sudo mv elm /usr/local/bin/
-      - name: Set up elm-test
-        uses: actions/setup-node@v3
-        with:
-          node-version: 16
-      - name: Set up elm-test
-        run: |
-          npm install -g elm-test@0.19.1-revision9
-
       - name: Set up Liquidity
         run: |
           sudo chmod +x ./extra/docker/liquidity

.gitignore

@@ -50,19 +50,6 @@ META.*
 *.out
 *.mligo
 
-## Elm tests
-extraction/tests/extracted-code/elm-extract/elm-stuff/
-extraction/tests/extracted-code/elm-extract/node_modules/
-extraction/tests/extracted-code/elm-extract/src/
-extraction/tests/extracted-code/elm-extract/tests/
-extraction/tests/extracted-code/elm-extract/*.html
-
-extraction/tests/extracted-code/elm-web-extract/elm-stuff/
-extraction/tests/extracted-code/elm-web-extract/node_modules/
-extraction/tests/extracted-code/elm-web-extract/src/
-extraction/tests/extracted-code/elm-web-extract/tests/
-extraction/tests/extracted-code/elm-web-extract/*.html
-
 
 ## Liquidity tests
 extraction/tests/extracted-code/liquidity-extract/*

coq-concert.opam

@@ -26,6 +26,7 @@ depends: [
   "coq-metacoq-safechecker" {= "8.16.dev"}
   "coq-metacoq-erasure" {= "8.16.dev"}
   "coq-rust-extraction" {= "dev"}
+  "coq-elm-extraction" {= "dev"}
   "coq-stdpp" {>= "1.6.0" & <= "1.8.0"}
 ]
 
@@ -38,6 +39,7 @@ pin-depends: [
   ["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"]
+  ["coq-elm-extraction.dev" "git+https://github.com/AU-COBRA/coq-elm-extraction.git#b2bc25623a2e4ca662418569273b7c5e72b975c6"]
 ]
 
 build: [

examples/counter/extraction/CounterRefTypesMidlang.v

@@ -3,9 +3,9 @@
 (** The contract uses refinement types to specify some functional correctness properties *)
 From ConCert.Execution Require Import Blockchain.
 From ConCert.Execution Require Import Serializable.
-From ConCert.Extraction Require Import Common.
-From ConCert.Extraction Require Import ElmExtract.
-From ConCert.Extraction Require Import PrettyPrinterMonad.
+From ElmExtraction Require Import Common.
+From ElmExtraction Require Import ElmExtract.
+From ElmExtraction Require Import PrettyPrinterMonad.
 From MetaCoq.Erasure.Typed Require Import Extraction.
 From MetaCoq.Erasure.Typed Require Import ResultMonad.
 From MetaCoq.Common Require Import Kernames.

examples/escrow/extraction/EscrowMidlang.v

@@ -2,13 +2,13 @@ From ConCert.Execution Require Import Blockchain.
 From ConCert.Execution Require Import Serializable.
 From ConCert.Execution Require Monad.
 From ConCert.Execution Require OptionMonad.
-From ConCert.Extraction Require Import Common.
-From ConCert.Extraction Require Import ElmExtract.
+From ElmExtraction Require Import Common.
+From ElmExtraction Require Import ElmExtract.
 From MetaCoq.Erasure.Typed Require Import CertifyingInlining.
 From MetaCoq.Erasure.Typed Require Import Extraction.
 From MetaCoq.Erasure.Typed Require Import ResultMonad.
 From ConCert.Extraction Require Import SpecializeChainBase.
-From ConCert.Extraction Require Import PrettyPrinterMonad.
+From ElmExtraction Require Import PrettyPrinterMonad.
 From ConCert.Examples.Escrow Require Import Escrow.
 From MetaCoq.Common Require Import Kernames.
 From MetaCoq.Template Require Import All.

extraction/Makefile

@@ -48,19 +48,11 @@ 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
 
-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-concordium
+test-extraction: test-liquidity test-ligo test-concordium
 
 test-concordium: clean-compiled-concordium
 	$(foreach dir, $(wildcard $(CONCORDIUM_DIR)/*-extracted), cd $(dir) && cargo concordium test && cd ../../../..;)
 
-test-elm:
-	mkdir -p $(ELM_DIR)/src
-	cd $(ELM_DIR); elm-test
-	cd $(ELM_WEB_APP_DIR); elm make src/Main.elm
-
 test-liquidity: clean-compiled-liquidity $(LIQUIDITY_DIST)
 
 $(LIQUIDITY_SRC_DIR)/%.tz:
@@ -82,27 +74,17 @@ clean-compiled-concordium:
 	$(foreach dir, $(wildcard $(CONCORDIUM_DIR)/*-extracted), rm -f -r $(dir)/target;)
 .PHONY: clean-compiled-concordium
 
-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-concordium
+clean-compiled-extraction: clean-comiped-ligo clean-compiled-liquidity clean-compiled-concordium
 .PHONY: clean-compiled-extraction
 
 clean-extraction-out-files:
-	rm -f $(ELM_WEB_APP_DIR)/*.elm.out
-	rm -f $(ELM_DIR)/*.elm.out
 	rm -f $(LIQUIDITY_DIR)/*.liq.out
 	rm -f $(LIGO_DIR)/*.mligo.out
 	rm -f $(CONCORDIUM_DIR)/*.rs.out
 	rm -f $(MIDLANG_DIR)/*.midlang.out
 	$(foreach dir, $(wildcard $(CONCORDIUM_DIR)/*-extracted), rm -f -r $(dir)/*.rs.out;)
 
 clean-extraction-sources:
-	rm -f $(ELM_DIR)/tests/*.elm
-	rm -f $(ELM_WEB_APP_DIR)/src/main.elm
 	rm -f $(LIQUIDITY_DIR)/tests/*.liq
 	rm -f $(LIQUIDITY_DIR)/liquidity.log
 	rm -f $(LIGO_DIR)/tests/*.mligo
@@ -112,4 +94,4 @@ clean-extraction-sources:
 
 clean-extraction-examples: clean-compiled-extraction clean-extraction-out-files clean-extraction-sources
 	rm ./tests/*.vo # to force recompilation of examples (a bit ad-hoc though)
-.PHONY: clean-extraction-examples clean-comiped-ligo clean-comiped-ligo test-concordium test-elm test-liquidity test-ligo test-extraction clean-extraction-out-files
+.PHONY: clean-extraction-examples clean-comiped-ligo clean-comiped-ligo test-concordium test-liquidity test-ligo test-extraction clean-extraction-out-files

extraction/README.md

@@ -62,6 +62,5 @@ Some highlights of extracted examples:
 * [CounterDepCertifiedLiquidity.v](../examples/counter/extraction/CounterDepCertifiedLiquidity.v) -- A counter contract that uses propositions to filter out the correct input. It also serves as an example application of the certifying eta-expansion.
 * [CounterRefinementTypes](../examples/counter/extraction/CounterRefTypesMidlang.v) -- A counter contract that uses refinement types for expressing partial functional correctness.
 * [CrowdfundingCertifiedExtraction.v](../examples/crowdfunding/CrowdfundingCertifiedExtraction.v) -- Machinery for extraction of a crowdfunding contract.
-* [ElmExtractTests.v](tests/ElmExtractTests.v) -- Several examples of extraction into Elm.
 * [EscrowMidlang.v](../examples/escrow/extraction/EscrowMidlang.v) -- Extraction of the escrow contract defined in [Escrow.v](../examples/escrow/Escrow.v) to Midlang.
 * [StackInterpreterExtract.v](../examples/stackInterpreter/StackInterpreterExtract.v) -- An interpreter for a simple stack-based language.

extraction/_CoqProject

@@ -9,17 +9,12 @@ theories/CameLIGOExtract.v
 theories/CameLIGOPretty.v
 theories/Common.v
 theories/ConcordiumExtract.v
-theories/ElmExtract.v
 theories/LiquidityExtract.v
 theories/LiquidityPretty.v
 theories/PrettyPrinterMonad.v
 theories/SpecializeChainBase.v
 
 -Q tests ConCert.Extraction.Tests
-tests/Ack.v
 tests/CameLIGOExtractionTests.v
-tests/ElmExtractExamples.v
-tests/ElmExtractTests.v
-tests/ElmForms.v
 tests/RecordExtractionLiquidityTests.v
 tests/NumLiteralTests.v

extraction/process-extraction-examples.sh

@@ -1,32 +1,13 @@
 #!/bin/bash
 
-ELM_PATH=./tests/extracted-code/elm-extract
-ELM_WEB_PATH=./tests/extracted-code/elm-web-extract
 LIQ_PATH=./tests/extracted-code/liquidity-extract
 LIGO_PATH=./tests/extracted-code/cameligo-extract
 MID_PATH=./tests/extracted-code/midlang-extract
 CONCORDIUM_PATH=./tests/extracted-code/concordium-extract
-ELM_TESTS=$ELM_PATH/tests
-ELM_WEB_SRC=$ELM_WEB_PATH/src
 LIQ_TESTS=$LIQ_PATH/tests
 LIGO_TESTS=$LIGO_PATH/tests
 MID_TESTS=$MID_PATH/tests
 
-echo "Processing Elm extraction"
-for f in $ELM_PATH/*.elm.out;
-do
-    if [[ ! -e "$f" ]]; then continue; fi
-    echo $f "--->" $ELM_TESTS/$(basename ${f%.out}) ;
-    sed -n 's/ *"//;/module/,/suite/p' $f > $ELM_TESTS/$(basename ${f%.out})
-done
-
-WEB_APP_OUT=UserList.elm.out
-
-echo "Processing Elm web-app extraction"
-echo $WEB_APP_OUT "+ views.elm"  "--->" $ELM_WEB_SRC/Main.elm;
-cat $ELM_WEB_PATH/$WEB_APP_OUT $ELM_WEB_SRC/views.elm > $ELM_WEB_SRC/Main.elm
-
-
 echo "Processing Liquidity extraction"
 for f in $LIQ_PATH/*.liq.out;
 do