Dear Coq community,
I would like to share a project related to the Elm functional programming language.
As part of ConCert (https://github.com/AU-COBRA/ConCert ), we have developed an extraction pipeline that allows for generating Elm code.
We have several simple examples/tests here https://github.com/AU-COBRA/ConCert/blob/master/extraction/examples/ElmExtractExamples.v .
A more “domain-specific” example with a web app consisting of an input form, validation and rendering a list of users is available here:
https://github.com/AU-COBRA/ConCert/blob/master/extraction/examples/ElmForms.v
The example is inspired by a similar one from the Elm guide.
We use Coq’s subset types to encode the invariants for the part of the model that represents valid data.
Currently, we write the “logic” of the app (model and validation) in Coq, extract it and then concatenate with the hand-written view, that renders the form and calls the model functions.
Here is the result of the extraction in the online IDE Ellie:
https://ellie-app.com/cSFtmjq99Rta1
Contributions with more interesting examples are very welcome!
2 Likes
Hey this is nice, I came from google searching for this ^^
1 Like
@impression28 I’m glad you liked it The path to examples has changed a bit:
(** * Examples for extraction to Elm *)
(** The examples are writen into files that are later processed and passed to the Elm compiler as part of the building process. *)
(** Warning: this file does not work in the interactive mode due to the problems with paths for [Redirect].
We have to stick to the path, relative to the project root and in the interactive mode current directory is different. *)
From ConCert.Utils Require Import StringExtra.
From ConCert.Extraction Require Import Common.
From MetaCoq.TypedExtraction Require Import Extraction.
From ConCert.Extraction Require Import ElmExtract.
From ConCert.Extraction Require Import PrettyPrinterMonad.
From MetaCoq.TypedExtraction Require Import ResultMonad.
From MetaCoq.TypedExtraction Require Import CertifyingEta.
From ConCert.Extraction.Tests Require Import ElmExtractTests.
From ConCert.Extraction.Tests Require Import Ack.
From MetaCoq.Template Require Import Ast.
From MetaCoq.Template Require Import Kernames.
From MetaCoq.Template Require Import TemplateMonad.
From MetaCoq Require Import utils.
From Coq Require Import String.
This file has been truncated. show original
1 Like