diff options
| -rw-r--r-- | arm/PrintAsm.ml | 1 | ||||
| -rw-r--r-- | backend/CMparser.mly | 11 | ||||
| -rw-r--r-- | backend/CMtypecheck.ml | 1 | ||||
| -rw-r--r-- | backend/Linearizeaux.ml | 3 | ||||
| -rw-r--r-- | backend/RTLtypingaux.ml | 1 | ||||
| -rw-r--r-- | cfrontend/Cil2Csyntax.ml | 3 | ||||
| -rw-r--r-- | cfrontend/PrintCsyntax.ml | 1 | ||||
| -rw-r--r-- | extraction/Makefile | 14 | ||||
| -rwxr-xr-x | extraction/convert | 10 | ||||
| -rw-r--r-- | lib/Camlcoq.ml | 9 | ||||
| -rw-r--r-- | powerpc/PrintAsm.ml | 5 |
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"; |