summaryrefslogtreecommitdiff
path: root/extraction
diff options
context:
space:
mode:
Diffstat (limited to 'extraction')
-rw-r--r--extraction/Makefile48
-rw-r--r--extraction/extraction.v2
-rwxr-xr-xextraction/fixextract15
-rwxr-xr-xextraction/uncapitalize6
4 files changed, 17 insertions, 54 deletions
diff --git a/extraction/Makefile b/extraction/Makefile
deleted file mode 100644
index 0aee0be..0000000
--- a/extraction/Makefile
+++ /dev/null
@@ -1,48 +0,0 @@
-#######################################################################
-# #
-# The Compcert verified compiler #
-# #
-# Xavier Leroy, INRIA Paris-Rocquencourt #
-# #
-# Copyright Institut National de Recherche en Informatique et en #
-# Automatique. All rights reserved. This file is distributed #
-# under the terms of the INRIA Non-Commercial License Agreement. #
-# #
-#######################################################################
-
-include ../Makefile.config
-
-DIRS=lib common $(ARCH)/$(VARIANT) $(ARCH) backend cfrontend driver
-
-COQINCL=$(patsubst %,-I ../%,$(DIRS))
-COQEXEC=coqtop $(COQINCL) -batch -load-vernac-source
-
-all: Configuration.ml extraction
-
-extraction:
- rm -f [:lower:]*.mli [:lower:]*.ml
- $(COQEXEC) extraction.v
- @echo "Fixing file names..."
- @mv list.ml CoqList.ml
- @mv list.mli CoqList.mli
- @mv string.ml CoqString.ml
- @mv string.mli CoqString.mli
- @mv int.ml CoqInt.ml
- @mv int.mli CoqInt.mli
- @echo "Conversion List -> CoqList, String -> CoqString, Int -> CoqInt..."
- @./convert *.mli *.ml
- @echo "Patching files..."
- @for i in *.patch; do patch < $$i; done
-
-Configuration.ml: ../Makefile.config
- (echo 'let stdlib_path = "$(LIBDIR)"'; \
- echo 'let prepro = "$(CPREPRO)"'; \
- echo 'let asm = "$(CASM)"'; \
- echo 'let linker = "$(CLINKER)"'; \
- echo 'let arch = "$(ARCH)"'; \
- echo 'let variant = "$(VARIANT)"'; \
- echo 'let system = "$(SYSTEM)"') \
- > Configuration.ml
-
-clean:
- rm -f *.mli *.ml
diff --git a/extraction/extraction.v b/extraction/extraction.v
index 58da9c0..d74e192 100644
--- a/extraction/extraction.v
+++ b/extraction/extraction.v
@@ -22,6 +22,7 @@ Require Compiler.
Extract Inductive unit => "unit" [ "()" ].
Extract Inductive bool => "bool" [ "true" "false" ].
Extract Inductive sumbool => "bool" [ "true" "false" ].
+Extract Inductive option => "option" [ "Some" "None" ].
Extract Inductive List.list => "list" [ "[]" "(::)" ].
(* Float *)
@@ -82,4 +83,5 @@ Extract Constant Asm.freg_eq => "fun (x: freg) (y: freg) -> x = y".
Extract Constant Asm.preg_eq => "fun (x: preg) (y: preg) -> x = y".
(* Go! *)
+Cd "extraction".
Recursive Extraction Library Compiler.
diff --git a/extraction/fixextract b/extraction/fixextract
new file mode 100755
index 0000000..1ee3c48
--- /dev/null
+++ b/extraction/fixextract
@@ -0,0 +1,15 @@
+#!/bin/sh
+
+echo "Fixing file names..."
+mv list.ml CoqList.ml
+mv list.mli CoqList.mli
+mv string.ml CoqString.ml
+mv string.mli CoqString.mli
+mv int.ml CoqInt.ml
+mv int.mli CoqInt.mli
+
+echo "Conversion List -> CoqList, String -> CoqString, Int -> CoqInt..."
+./convert *.mli *.ml
+
+echo "Patching files..."
+for i in *.patch; do patch < $i; done
diff --git a/extraction/uncapitalize b/extraction/uncapitalize
deleted file mode 100755
index d724b8f..0000000
--- a/extraction/uncapitalize
+++ /dev/null
@@ -1,6 +0,0 @@
-#!/bin/sh
-echo $1 | sed -e 'h
-s/\(.\).*/\1/
-y/ABCDEFGHIJKLMNOPQRSTUVWXYZ/abcdefghijklmnopqrstuvwxyz/
-G
-s/\n.//'