diff options
| -rwxr-xr-x | extraction/convert | 6 | ||||
| -rw-r--r-- | extraction/extraction.v | 3 | ||||
| -rwxr-xr-x | extraction/fixextract | 11 | ||||
| -rw-r--r-- | lib/Camlcoq.ml | 8 |
4 files changed, 7 insertions, 21 deletions
diff --git a/extraction/convert b/extraction/convert deleted file mode 100755 index 94ec38e..0000000 --- a/extraction/convert +++ /dev/null @@ -1,6 +0,0 @@ -#!/usr/bin/perl -pi - -s/\bList\b/CoqList/g; -s/\bString\b/CoqString/g; -s/^open Int$/open CoqInt/; - diff --git a/extraction/extraction.v b/extraction/extraction.v index d74e192..137ddb0 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -82,6 +82,9 @@ Extract Constant Asm.ireg_eq => "fun (x: ireg) (y: ireg) -> x = y". Extract Constant Asm.freg_eq => "fun (x: freg) (y: freg) -> x = y". Extract Constant Asm.preg_eq => "fun (x: preg) (y: preg) -> x = y". +(* Avoid name clashes *) +Extraction Blacklist List String Int. + (* Go! *) Cd "extraction". Recursive Extraction Library Compiler. diff --git a/extraction/fixextract b/extraction/fixextract index 1ee3c48..86ebdbd 100755 --- a/extraction/fixextract +++ b/extraction/fixextract @@ -1,15 +1,4 @@ #!/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/lib/Camlcoq.ml b/lib/Camlcoq.ml index 3660a10..c7abdcc 100644 --- a/lib/Camlcoq.ml +++ b/lib/Camlcoq.ml @@ -90,15 +90,15 @@ let char_of_ascii (Ascii.Ascii(a0, a1, a2, a3, a4, a5, a6, a7)) = let coqstring_length s = let rec len accu = function - | CoqString.EmptyString -> accu - | CoqString.CoqString(_, s) -> len (accu + 1) s + | String0.EmptyString -> accu + | String0.String(_, s) -> len (accu + 1) s in len 0 s let camlstring_of_coqstring s = let r = String.create (coqstring_length s) in let rec fill pos = function - | CoqString.EmptyString -> r - | CoqString.CoqString(c, s) -> r.[pos] <- char_of_ascii c; fill (pos + 1) s + | String0.EmptyString -> r + | String0.String(c, s) -> r.[pos] <- char_of_ascii c; fill (pos + 1) s in fill 0 s (* Timing facility *) |