diff options
| author |  xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2009-04-17 13:27:48 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2009-04-17 13:27:48 +0000 |
| commit | d1cdc0496d7d52e3ab91554dbf53fcc0e7f244eb (patch) | |
| tree | 4fb435a847b0a1f1fd0afc93eb718c459e2aa0d6 /extraction | |
| parent | ed39cb168c0ca6c979db9059d39213d4f2a59eb5 (diff) | |
Various clean-ups
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1033 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'extraction')
| -rw-r--r-- | extraction/Makefile | 48 | ||||
| -rw-r--r-- | extraction/extraction.v | 2 | ||||
| -rwxr-xr-x | extraction/fixextract | 15 | ||||
| -rwxr-xr-x | extraction/uncapitalize | 6 |
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.//' |