Skip to content

Instantly share code, notes, and snippets.

@joom

joom/A.v

Created September 21, 2019 02:13
Show Gist options
  • Save joom/6f7ab1d3bc840839b993c241a5f29cd1 to your computer and use it in GitHub Desktop.
Save joom/6f7ab1d3bc840839b993c241a5f29cd1 to your computer and use it in GitHub Desktop.
Download ZIP
Coq extraction in separate modules
Raw
A.v
Inductive color := red | green | blue.
Raw
B.v
Require Import A.
Definition next_color (c : color) :=
match c with
| red => green
| green => blue
| blue => red
end.
Raw
C.v
Require Import A.
Definition prev_color (c : color) :=
match c with
| red => blue
| green => red
| blue => green
end.
Raw
Extract.v
Require Import A.
Require Import B.
Require Import C.
Require Extraction.
Extraction Language Haskell.
Extraction Library A.
Extraction Library B.
Extraction Library C.
@joom
Copy link
Author

joom commented Sep 21, 2019

This is the result:

A.hs:

module A where

import qualified Prelude

data Coq_color =
   Coq_red
 | Coq_green
 | Coq_blue

color_rect :: a1 -> a1 -> a1 -> Coq_color -> a1
color_rect f f0 f1 c =
  case c of {
   Coq_red -> f;
   Coq_green -> f0;
   Coq_blue -> f1}

color_rec :: a1 -> a1 -> a1 -> Coq_color -> a1
color_rec =
  color_rect

B.hs:

module B where

import qualified Prelude
import qualified A

next_color :: A.Coq_color -> A.Coq_color
next_color c =
  case c of {
   A.Coq_red -> A.Coq_green;
   A.Coq_green -> A.Coq_blue;
   A.Coq_blue -> A.Coq_red}

C.hs:

module C where

import qualified Prelude
import qualified A

prev_color :: A.Coq_color -> A.Coq_color
prev_color c =
  case c of {
   A.Coq_red -> A.Coq_blue;
   A.Coq_green -> A.Coq_red;
   A.Coq_blue -> A.Coq_green}

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment