summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2009-01-29 09:13:53 +0000
committerGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2009-01-29 09:13:53 +0000
commit26fcc4dbd92f367ecb20f4457cdf887eea0b6568 (patch)
tree0bec42a8bbb4c8d70e31d60e055409ef31e10da3
parentf6ecbb948ccf7f8a4e156eb29e3a41e7f2953407 (diff)
Conflict between extraction/CList and cil/obj/xxx/clist on case-insensitive file systems. Replaced CList by CoqList and likewise for CString and CInt. Removed useless references to CList in hand-written Caml code.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@951 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
-rw-r--r--arm/PrintAsm.ml1
-rw-r--r--backend/CMparser.mly11
-rw-r--r--backend/CMtypecheck.ml1
-rw-r--r--backend/Linearizeaux.ml3
-rw-r--r--backend/RTLtypingaux.ml1
-rw-r--r--cfrontend/Cil2Csyntax.ml3
-rw-r--r--cfrontend/PrintCsyntax.ml1
-rw-r--r--extraction/Makefile14
-rwxr-xr-xextraction/convert10
-rw-r--r--lib/Camlcoq.ml9
-rw-r--r--powerpc/PrintAsm.ml5
11 files changed, 25 insertions, 34 deletions
diff --git a/arm/PrintAsm.ml b/arm/PrintAsm.ml
index 16f22d6..f51a15b 100644
--- a/arm/PrintAsm.ml
+++ b/arm/PrintAsm.ml
@@ -14,7 +14,6 @@
open Printf
open Datatypes
-open CList
open Camlcoq
open AST
open Asm
diff --git a/backend/CMparser.mly b/backend/CMparser.mly
index f369f9e..c83a46e 100644
--- a/backend/CMparser.mly
+++ b/backend/CMparser.mly
@@ -15,7 +15,6 @@
%{
open Datatypes
-open CList
open Camlcoq
open BinPos
open BinInt
@@ -313,9 +312,9 @@ let mkmatch expr cases =
prog:
global_declarations proc_list EOF
- { { prog_funct = CList.rev $2;
+ { { prog_funct = List.rev $2;
prog_main = intern_string "main";
- prog_vars = CList.rev $1; } }
+ prog_vars = List.rev $1; } }
;
global_declarations:
@@ -347,8 +346,8 @@ proc:
temp_counter := 0;
Coq_pair($1,
Internal { fn_sig = $6;
- fn_params = CList.rev $3;
- fn_vars = CList.rev (CList.app tmp $9);
+ fn_params = List.rev $3;
+ fn_vars = List.rev (tmp @ $9);
fn_stackspace = $8;
fn_body = $10 }) }
| EXTERN STRINGLIT COLON signature
@@ -383,7 +382,7 @@ stack_declaration:
var_declarations:
/* empty */ { [] }
- | var_declarations var_declaration { CList.app $2 $1 }
+ | var_declarations var_declaration { $2 @ $1 }
;
var_declaration:
diff --git a/backend/CMtypecheck.ml b/backend/CMtypecheck.ml
index c4f45b2..819f269 100644
--- a/backend/CMtypecheck.ml
+++ b/backend/CMtypecheck.ml
@@ -17,7 +17,6 @@
open Printf
open Datatypes
-open CList
open Camlcoq
open AST
open Integers
diff --git a/backend/Linearizeaux.ml b/backend/Linearizeaux.ml
index d2d2f24..3fdc56f 100644
--- a/backend/Linearizeaux.ml
+++ b/backend/Linearizeaux.ml
@@ -15,7 +15,6 @@ open Coqlib
open Datatypes
open LTL
open Lattice
-open CList
open Maps
open Camlcoq
@@ -81,4 +80,4 @@ let enumerate_aux f reach =
emit_block (IntSet.remove npc pending) (pos_of_int npc)
end in
emit_block IntSet.empty f.fn_entrypoint;
- CList.rev !enum
+ List.rev !enum
diff --git a/backend/RTLtypingaux.ml b/backend/RTLtypingaux.ml
index 632f2aa..cc7edf4 100644
--- a/backend/RTLtypingaux.ml
+++ b/backend/RTLtypingaux.ml
@@ -13,7 +13,6 @@
(* Type inference for RTL *)
open Datatypes
-open CList
open Camlcoq
open Maps
open AST
diff --git a/cfrontend/Cil2Csyntax.ml b/cfrontend/Cil2Csyntax.ml
index 41fe1d4..e5ef64a 100644
--- a/cfrontend/Cil2Csyntax.ml
+++ b/cfrontend/Cil2Csyntax.ml
@@ -19,7 +19,6 @@ CIL -> CabsCoq translator
**************************************************************************)
open Cil
-open CList
open Camlcoq
open AST
open Csyntax
@@ -866,7 +865,7 @@ let convertInit init =
align al;
cvtInit init
- in cvtInit init; CList.rev !k
+ in cvtInit init; List.rev !k
(** Convert a [Cil.initinfo] into a list of [AST.init_data] *)
diff --git a/cfrontend/PrintCsyntax.ml b/cfrontend/PrintCsyntax.ml
index bb25339..5513b41 100644
--- a/cfrontend/PrintCsyntax.ml
+++ b/cfrontend/PrintCsyntax.ml
@@ -17,7 +17,6 @@
open Format
open Camlcoq
-open CList
open Datatypes
open AST
open Csyntax
diff --git a/extraction/Makefile b/extraction/Makefile
index d4163bb..ac162db 100644
--- a/extraction/Makefile
+++ b/extraction/Makefile
@@ -23,13 +23,13 @@ extraction:
rm -f [:lower:]*.mli [:lower:]*.ml
$(COQEXEC) extraction.v
@echo "Fixing file names..."
- @mv list.ml CList.ml
- @mv list.mli CList.mli
- @mv string.ml CString.ml
- @mv string.mli CString.mli
- @mv int.ml CInt.ml
- @mv int.mli CInt.mli
- @echo "Conversion List -> CList, String -> CString, Int -> CInt..."
+ @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/convert b/extraction/convert
index b3d2533..879cfe5 100755
--- a/extraction/convert
+++ b/extraction/convert
@@ -1,9 +1,9 @@
#!/usr/bin/perl -pi
-s/\bList\b/CList/g;
-s/\bString\b/CString/g;
-s/\bInt\.Z_as_Int\b/CInt.Z_as_Int/g;
-s/\bInt\.Int\b/CInt.Int/g;
-s/\bInt\.MoreInt\b/CInt.MoreInt/g;
+s/\bList\b/CoqList/g;
+s/\bString\b/CoqString/g;
+s/\bInt\.Z_as_Int\b/CoqInt.Z_as_Int/g;
+s/\bInt\.Int\b/CoqInt.Int/g;
+s/\bInt\.MoreInt\b/CoqInt.MoreInt/g;
s/^open Int$//;
diff --git a/lib/Camlcoq.ml b/lib/Camlcoq.ml
index 98fd79c..3660a10 100644
--- a/lib/Camlcoq.ml
+++ b/lib/Camlcoq.ml
@@ -13,7 +13,6 @@
(* Library of useful Caml <-> Coq conversions *)
open Datatypes
-open CList
open BinPos
open BinInt
@@ -91,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
- | CString.EmptyString -> accu
- | CString.CString(_, s) -> len (accu + 1) s
+ | CoqString.EmptyString -> accu
+ | CoqString.CoqString(_, 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
- | CString.EmptyString -> r
- | CString.CString(c, s) -> r.[pos] <- char_of_ascii c; fill (pos + 1) s
+ | CoqString.EmptyString -> r
+ | CoqString.CoqString(c, s) -> r.[pos] <- char_of_ascii c; fill (pos + 1) s
in fill 0 s
(* Timing facility *)
diff --git a/powerpc/PrintAsm.ml b/powerpc/PrintAsm.ml
index 352da05..b75d135 100644
--- a/powerpc/PrintAsm.ml
+++ b/powerpc/PrintAsm.ml
@@ -14,7 +14,6 @@
open Printf
open Datatypes
-open CList
open Camlcoq
open AST
open Asm
@@ -461,9 +460,9 @@ module Stubs_MacOS = struct
let variadic_stub oc stub_name fun_name ty_args =
(* Compute total size of arguments *)
let arg_size =
- CList.fold_left
+ List.fold_left
(fun sz ty -> match ty with Tint -> sz + 4 | Tfloat -> sz + 8)
- ty_args 0 in
+ 0 ty_args in
(* Stack size is linkage area + argument size, with a minimum of 56 bytes *)
let frame_size = max 56 (24 + arg_size) in
fprintf oc " mflr r0\n";