summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--caml/CMparser.mly54
-rw-r--r--caml/CMtypecheck.ml14
-rw-r--r--caml/Camlcoq.ml19
-rw-r--r--caml/Cil2Csyntax.ml65
-rw-r--r--caml/Coloringaux.ml8
-rw-r--r--caml/Driver.ml2
-rw-r--r--caml/Linearizeaux.ml4
-rw-r--r--caml/PrintCsyntax.ml38
-rw-r--r--caml/PrintPPC.ml32
-rw-r--r--caml/RTLgenaux.ml4
-rw-r--r--caml/RTLtypingaux.ml12
-rw-r--r--extraction/.depend4
-rw-r--r--extraction/extraction.v2
13 files changed, 112 insertions, 146 deletions
diff --git a/caml/CMparser.mly b/caml/CMparser.mly
index 0b3eafd..25fb032 100644
--- a/caml/CMparser.mly
+++ b/caml/CMparser.mly
@@ -37,13 +37,13 @@ type rexpr =
let temp_counter = ref 0
-let temporaries = ref Coq_nil
+let temporaries = ref []
let mktemp () =
incr temp_counter;
let n = Printf.sprintf "__t%d" !temp_counter in
let id = intern_string n in
- temporaries := Coq_cons(id, !temporaries);
+ temporaries := id :: !temporaries;
id
let convert_accu = ref []
@@ -75,11 +75,11 @@ let rec convert_rexpr = function
Evar t
and convert_rexpr_list = function
- | Coq_nil -> Coq_nil
- | Coq_cons(e1, el) ->
+ | [] -> []
+ | e1 :: el ->
let c1 = convert_rexpr e1 in
let cl = convert_rexpr_list el in
- Coq_cons(c1, cl)
+ c1 :: cl
let rec prepend_seq stmts last =
match stmts with
@@ -149,9 +149,9 @@ let mkswitch expr (cases, dfl) =
convert_accu := [];
let c = convert_rexpr expr in
let rec mktable = function
- | [] -> Coq_nil
+ | [] -> []
| (key, exit) :: rem ->
- Coq_cons(Coq_pair(coqint_of_camlint key, exitnum exit), mktable rem) in
+ Coq_pair(coqint_of_camlint key, exitnum exit) :: mktable rem in
prepend_seq !convert_accu (Sswitch(c, mktable cases, exitnum dfl))
(***
@@ -174,10 +174,10 @@ let mkmatch_aux expr cases =
let ncases = Int32.of_int (List.length cases) in
let rec mktable n = function
| [] -> assert false
- | [key, action] -> Coq_nil
+ | [key, action] -> []
| (key, action) :: rem ->
- Coq_cons(Coq_pair(coqint_of_camlint key, nat_of_camlint n),
- mktable (Int32.succ n) rem) in
+ Coq_pair(coqint_of_camlint key, nat_of_camlint n)
+ :: mktable (Int32.succ n) rem in
let sw =
Sswitch(expr, mktable 0l cases, nat_of_camlint (Int32.pred ncases)) in
let rec mkblocks body n = function
@@ -329,20 +329,18 @@ prog:
;
global_declarations:
- /* empty */ { Coq_nil }
- | global_declarations global_declaration { Coq_cons($2, $1) }
+ /* empty */ { [] }
+ | global_declarations global_declaration { $2 :: $1 }
;
global_declaration:
VAR STRINGLIT LBRACKET INTLIT RBRACKET
- { Coq_pair(Coq_pair($2,
- Coq_cons(Init_space (z_of_camlint $4), Coq_nil)),
- ()) }
+ { Coq_pair(Coq_pair($2, [ Init_space (z_of_camlint $4) ]), ()) }
;
proc_list:
- /* empty */ { Coq_nil }
- | proc_list proc { Coq_cons($2, $1) }
+ /* empty */ { [] }
+ | proc_list proc { $2 :: $1 }
;
/* Procedures */
@@ -355,7 +353,7 @@ proc:
stmt_list
RBRACE
{ let tmp = !temporaries in
- temporaries := Coq_nil;
+ temporaries := [];
temp_counter := 0;
Coq_pair($1,
Internal { fn_sig = $6;
@@ -371,21 +369,21 @@ proc:
signature:
type_
- { {sig_args = Coq_nil; sig_res = Some $1} }
+ { {sig_args = []; sig_res = Some $1} }
| VOID
- { {sig_args = Coq_nil; sig_res = None} }
+ { {sig_args = []; sig_res = None} }
| type_ MINUSGREATER signature
- { let s = $3 in {s with sig_args = Coq_cons($1, s.sig_args)} }
+ { let s = $3 in {s with sig_args = $1 :: s.sig_args} }
;
parameters:
- /* empty */ { Coq_nil }
+ /* empty */ { [] }
| parameter_list { $1 }
;
parameter_list:
- IDENT { Coq_cons($1, Coq_nil) }
- | parameter_list COMMA IDENT { Coq_cons($3, $1) }
+ IDENT { $1 :: [] }
+ | parameter_list COMMA IDENT { $3 :: $1 }
;
stack_declaration:
@@ -394,7 +392,7 @@ stack_declaration:
;
var_declarations:
- /* empty */ { Coq_nil }
+ /* empty */ { [] }
| var_declarations var_declaration { CList.app $2 $1 }
;
@@ -514,13 +512,13 @@ expr:
;
expr_list:
- /* empty */ { Coq_nil }
+ /* empty */ { [] }
| expr_list_1 { $1 }
;
expr_list_1:
- expr %prec COMMA { Coq_cons($1, Coq_nil) }
- | expr COMMA expr_list_1 { Coq_cons($1, $3) }
+ expr %prec COMMA { $1 :: [] }
+ | expr COMMA expr_list_1 { $1 :: $3 }
;
memory_chunk:
diff --git a/caml/CMtypecheck.ml b/caml/CMtypecheck.ml
index 1ac0065..d761f75 100644
--- a/caml/CMtypecheck.ml
+++ b/caml/CMtypecheck.ml
@@ -35,9 +35,7 @@ let tfloat = Base Tfloat
let ty_of_typ = function Tint -> tint | Tfloat -> tfloat
-let rec ty_of_sig_args = function
- | Coq_nil -> []
- | Coq_cons(t, l) -> ty_of_typ t :: ty_of_sig_args l
+let ty_of_sig_args tyl = List.map ty_of_typ tyl
let rec repr t =
match t with
@@ -244,8 +242,8 @@ let rec type_expr env lenv e =
and type_exprlist env lenv el =
match el with
- | Coq_nil -> []
- | Coq_cons (e1, et) ->
+ | [] -> []
+ | e1 :: et ->
let te1 = type_expr env lenv e1 in
let tet = type_exprlist env lenv et in
(te1 :: tet)
@@ -352,8 +350,8 @@ let rec type_stmt env blk ret s =
let rec env_of_vars idl =
match idl with
- | Coq_nil -> []
- | Coq_cons(id1, idt) -> (id1, newvar()) :: env_of_vars idt
+ | [] -> []
+ | id1 :: idt -> (id1, newvar()) :: env_of_vars idt
let type_function id f =
try
@@ -369,4 +367,4 @@ let type_fundef (Coq_pair (id, fd)) =
| External ef -> ()
let type_program p =
- coqlist_iter type_fundef p.prog_funct; p
+ List.iter type_fundef p.prog_funct; p
diff --git a/caml/Camlcoq.ml b/caml/Camlcoq.ml
index e9089cf..98fd79c 100644
--- a/caml/Camlcoq.ml
+++ b/caml/Camlcoq.ml
@@ -77,25 +77,6 @@ let extern_atom a =
with Not_found ->
Printf.sprintf "<unknown atom %ld>" (camlint_of_positive a)
-(* Lists *)
-
-let rec coqlist_iter f = function
- Coq_nil -> ()
- | Coq_cons(a,l) -> f a; coqlist_iter f l
-
-let rec length_coqlist = function
- | Coq_nil -> 0
- | Coq_cons (x, l) -> 1 + length_coqlist l
-
-let array_of_coqlist = function
- | Coq_nil -> [||]
- | Coq_cons(hd, tl) as l ->
- let a = Array.create (length_coqlist l) hd in
- let rec fill i = function
- | Coq_nil -> a
- | Coq_cons(hd, tl) -> a.(i) <- hd; fill (i + 1) tl in
- fill 1 tl
-
(* Strings *)
let char_of_ascii (Ascii.Ascii(a0, a1, a2, a3, a4, a5, a6, a7)) =
diff --git a/caml/Cil2Csyntax.ml b/caml/Cil2Csyntax.ml
index 7224610..41fe1d4 100644
--- a/caml/Cil2Csyntax.ml
+++ b/caml/Cil2Csyntax.ml
@@ -88,12 +88,6 @@ let rec getFieldType f = function
(** ** Some functions over lists *)
-(** Apply [f] to each element of the OCaml list [l]
- and build a Coq list with the results returned by [f] *)
-let rec map_coqlist f l = match l with
- | [] -> CList.Coq_nil
- | a :: b -> CList.Coq_cons (f a, map_coqlist f b)
-
(** Keep the elements in a list from [elt] (included) to the end
(used for the translation of the [switch] statement) *)
let rec keepFrom elt = function
@@ -111,13 +105,6 @@ let rec keepUntil elt' = function
let keepBetween elt elt' l =
keepUntil elt' (keepFrom elt l)
-(** Reverse-append over Coq lists *)
-
-let rec revappend l1 l2 =
- match l1 with
- | CList.Coq_nil -> l2
- | CList.Coq_cons(hd, tl) -> revappend tl (CList.Coq_cons (hd, l2))
-
(** ** Functions used to handle locations *)
(** Update the current location *)
@@ -162,18 +149,18 @@ let typeStringLiteral s =
Tarray(Tint(I8, Unsigned), z_of_camlint(Int32.of_int(String.length s + 1)))
let global_for_string s id =
- let init = ref CList.Coq_nil in
+ let init = ref [] in
let add_char c =
- init := CList.Coq_cons(
- AST.Init_int8(coqint_of_camlint(Int32.of_int(Char.code c))),
- !init) in
+ init :=
+ AST.Init_int8(coqint_of_camlint(Int32.of_int(Char.code c)))
+ :: !init in
add_char '\000';
for i = String.length s - 1 downto 0 do add_char s.[i] done;
Datatypes.Coq_pair(Datatypes.Coq_pair(id, !init), typeStringLiteral s)
let globals_for_strings globs =
Hashtbl.fold
- (fun s id l -> CList.Coq_cons(global_for_string s id, l))
+ (fun s id l -> global_for_string s id :: l)
stringTable globs
(** ** Handling of stubs for variadic functions *)
@@ -206,7 +193,7 @@ let declare_stub_function stub_name stub_type =
| _ -> assert false
let declare_stub_functions k =
- Hashtbl.fold (fun n i k -> CList.Coq_cons(declare_stub_function n i, k))
+ Hashtbl.fold (fun n i k -> declare_stub_function n i :: k)
stub_function_table k
(** ** Generation of temporary variable names *)
@@ -346,13 +333,13 @@ and processCast t e =
(** Convert a [Cil.exp list] into an [CamlCoq.exprlist] *)
and processParamsE = function
- | [] -> Coq_nil
+ | [] -> []
| e :: l ->
let (Expr (_, t)) as e' = convertExp e in
match t with
| Tstruct _ | Tunion _ ->
unsupported "function parameter of struct or union type"
- | _ -> Coq_cons (e', processParamsE l)
+ | _ -> e' :: processParamsE l
(** Convert a [Cil.exp] into a [CabsCoq.expr] *)
@@ -546,8 +533,8 @@ let convertExpFuncall e eList =
| _ ->
unsupported "call to variadic function" in
let rec typeOfExprList = function
- | Coq_nil -> Tnil
- | Coq_cons (Expr (_, ty), rem) -> Tcons (ty, typeOfExprList rem) in
+ | [] -> Tnil
+ | Expr (_, ty) :: rem -> Tcons (ty, typeOfExprList rem) in
let targs = typeOfExprList params in
let tres = convertTyp res in
let (stub_fun_name, stub_fun_typ) =
@@ -742,8 +729,8 @@ let convertGFun fdec =
| _ -> internal_error "convertGFun: incorrect function type"
in
let s = processStmtList fdec.sbody.bstmts in (* function body -- do it first because of generated temps *)
- let args = map_coqlist convertVarinfoParam fdec.sformals in (* parameters*)
- let varList = map_coqlist convertVarinfo fdec.slocals in (* local vars *)
+ let args = List.map convertVarinfoParam fdec.sformals in (* parameters*)
+ let varList = List.map convertVarinfo fdec.slocals in (* local vars *)
if v.vname = "main" then begin
match ret with
| Tint(_, _) -> ()
@@ -758,8 +745,8 @@ let convertGFun fdec =
(** Auxiliary for [convertInit] *)
let rec initDataLen accu = function
- | CList.Coq_nil -> accu
- | CList.Coq_cons(i1, il) ->
+ | [] -> accu
+ | i1 :: il ->
let sz = match i1 with
| Init_int8 _ -> 1l
| Init_int16 _ -> 2l
@@ -811,19 +798,19 @@ let rec extract_constant e =
| _ -> ICnone
let init_data_of_string s =
- let id = ref CList.Coq_nil in
+ let id = ref [] in
let enter_char c =
let n = coqint_of_camlint(Int32.of_int(Char.code c)) in
- id := CList.Coq_cons(Init_int8 n, !id) in
+ id := Init_int8 n :: !id in
enter_char '\000';
for i = String.length s - 1 downto 0 do enter_char s.[i] done;
!id
let convertInit init =
- let k = ref Coq_nil
+ let k = ref []
and pos = ref 0 in
let emit size datum =
- k := Coq_cons(datum, !k);
+ k := datum :: !k;
pos := !pos + size in
let emit_space size =
emit size (Init_space (z_of_camlint (Int32.of_int size))) in
@@ -886,7 +873,7 @@ let convertInit init =
let convertInitInfo ty info =
match info.init with
| None ->
- CList.Coq_cons(Init_space(Csyntax.sizeof (convertTyp ty)), CList.Coq_nil)
+ [ Init_space(Csyntax.sizeof (convertTyp ty)) ]
| Some init ->
convertInit init
@@ -904,7 +891,7 @@ let convertGVar v i =
let convertExtVar v =
updateLoc(v.vdecl);
let id = intern_string v.vname in
- Datatypes.Coq_pair (Datatypes.Coq_pair(id, CList.Coq_nil),
+ Datatypes.Coq_pair (Datatypes.Coq_pair(id, []),
convertTyp v.vtype)
(** Convert a [Cil.GVarDecl] into an external function declaration *)
@@ -923,7 +910,7 @@ let convertExtFun v =
functions and the second component, of type [(ident * coq_type) coqlist],
the definitions of the global variables of the program *)
let rec processGlobals = function
- | [] -> (CList.Coq_nil, CList.Coq_nil)
+ | [] -> ([], [])
| g :: l ->
match g with
| GType _ -> processGlobals l (* typedefs are unrolled... *)
@@ -940,24 +927,24 @@ let rec processGlobals = function
| TFun (tres, Some targs, false, _) ->
let fn = convertExtFun v in
let (fList, vList) = processGlobals l in
- (CList.Coq_cons (fn, fList), vList)
+ (fn :: fList, vList)
| TFun (tres, _, _, _) ->
processGlobals l
| _ ->
let var = convertExtVar v in
let (fList, vList) = processGlobals l in
- (fList, CList.Coq_cons (var, vList))
+ (fList, var :: vList)
end
| GVar (v, init, loc) ->
updateLoc(loc);
let var = convertGVar v init in
let (fList, vList) = processGlobals l in
- (fList, CList.Coq_cons (var, vList))
+ (fList, var :: vList)
| GFun (fdec, loc) ->
updateLoc(loc);
let fn = convertGFun fdec in
let (fList, vList) = processGlobals l in
- (CList.Coq_cons (fn, fList), vList)
+ (fn :: fList, vList)
| GAsm (_, loc) ->
updateLoc(loc);
unsupported "inline assembly"
@@ -992,7 +979,7 @@ let convertFile f =
let (funList, defList) = processGlobals (cleanupGlobals f.globals) in
let funList' = declare_stub_functions funList in
let funList'' = match f.globinit with
- | Some fdec -> CList.Coq_cons (convertGFun fdec, funList')
+ | Some fdec -> convertGFun fdec :: funList'
| None -> funList' in
let defList' = globals_for_strings defList in
{ AST.prog_funct = funList'';
diff --git a/caml/Coloringaux.ml b/caml/Coloringaux.ml
index 984fbb3..f11738d 100644
--- a/caml/Coloringaux.ml
+++ b/caml/Coloringaux.ml
@@ -278,13 +278,13 @@ let class_of_type = function Tint -> 0 | Tfloat -> 1
let num_register_classes = 2
let caller_save_registers = [|
- array_of_coqlist Conventions.int_caller_save_regs;
- array_of_coqlist Conventions.float_caller_save_regs
+ Array.of_list Conventions.int_caller_save_regs;
+ Array.of_list Conventions.float_caller_save_regs
|]
let callee_save_registers = [|
- array_of_coqlist Conventions.int_callee_save_regs;
- array_of_coqlist Conventions.float_callee_save_regs
+ Array.of_list Conventions.int_callee_save_regs;
+ Array.of_list Conventions.float_callee_save_regs
|]
let num_available_registers =
diff --git a/caml/Driver.ml b/caml/Driver.ml
index dacc9dc..8fffcaa 100644
--- a/caml/Driver.ml
+++ b/caml/Driver.ml
@@ -39,7 +39,7 @@ let print_error oc msg =
let print_one_error = function
| Errors.MSG s -> output_string oc (Camlcoq.camlstring_of_coqstring s)
| Errors.CTX i -> output_string oc (Camlcoq.extern_atom i)
- in Camlcoq.coqlist_iter print_one_error msg
+ in List.iter print_one_error msg
(* For the CIL -> Csyntax translator:
diff --git a/caml/Linearizeaux.ml b/caml/Linearizeaux.ml
index 02a9524..2f2333f 100644
--- a/caml/Linearizeaux.ml
+++ b/caml/Linearizeaux.ml
@@ -51,14 +51,14 @@ let rec pos_of_int n =
module IntSet = Set.Make(struct type t = int let compare = compare end)
let enumerate_aux f reach =
- let enum = ref Coq_nil in
+ let enum = ref [] in
let emitted = Array.make (int_of_pos f.fn_nextpc) false in
let rec emit_block pending pc =
let npc = int_of_pos pc in
if emitted.(npc)
then emit_restart pending
else begin
- enum := Coq_cons(pc, !enum);
+ enum := pc :: !enum;
emitted.(npc) <- true;
match PTree.get pc f.fn_code with
| None -> assert false
diff --git a/caml/PrintCsyntax.ml b/caml/PrintCsyntax.ml
index 6aaa539..bb25339 100644
--- a/caml/PrintCsyntax.ml
+++ b/caml/PrintCsyntax.ml
@@ -205,8 +205,8 @@ and print_expr_prec p (context_prec, e) =
let rec print_expr_list p (first, el) =
match el with
- | Coq_nil -> ()
- | Coq_cons(e1, et) ->
+ | [] -> ()
+ | e1 :: et ->
if not first then fprintf p ",@ ";
print_expr p e1;
print_expr_list p (false, et)
@@ -305,12 +305,12 @@ let name_function_parameters fun_name params =
Buffer.add_string b fun_name;
Buffer.add_char b '(';
begin match params with
- | Coq_nil ->
+ | [] ->
Buffer.add_string b "void"
| _ ->
let rec add_params first = function
- | Coq_nil -> ()
- | Coq_cons(Coq_pair(id, ty), rem) ->
+ | [] -> ()
+ | Coq_pair(id, ty) :: rem ->
if not first then Buffer.add_string b ", ";
Buffer.add_string b (name_cdecl (extern_atom id) ty);
add_params false rem in
@@ -325,7 +325,7 @@ let print_function p id f =
f.fn_params)
f.fn_return);
fprintf p "@[<v 2>{@ ";
- coqlist_iter
+ List.iter
(fun (Coq_pair(id, ty)) ->
fprintf p "%s;@ " (name_cdecl (extern_atom id) ty))
f.fn_vars;
@@ -342,9 +342,9 @@ let print_fundef p (Coq_pair(id, fd)) =
let string_of_init id =
try
- let s = String.create (length_coqlist id) in
+ let s = String.create (List.length id) in
let i = ref 0 in
- coqlist_iter
+ List.iter
(function
| Init_int8 n ->
s.[!i] <- Char.chr(Int32.to_int(camlint_of_coqint n));
@@ -382,16 +382,16 @@ let print_init p = function
let print_globvar p (Coq_pair(Coq_pair(id, init), ty)) =
match init with
- | Coq_nil ->
+ | [] ->
fprintf p "extern %s;@ @ "
(name_cdecl (extern_atom id) ty)
- | Coq_cons(Init_space _, Coq_nil) ->
+ | [Init_space _] ->
fprintf p "%s;@ @ "
(name_cdecl (extern_atom id) ty)
| _ ->
fprintf p "@[<hov 2>%s = {@ "
(name_cdecl (extern_atom id) ty);
- coqlist_iter (print_init p) init;
+ List.iter (print_init p) init;
fprintf p "};@]@ @ "
(* Collect struct and union types *)
@@ -432,8 +432,8 @@ let rec collect_expr (Expr(ed, ty)) =
| Efield(e1, id) -> collect_expr e1
let rec collect_expr_list = function
- | Coq_nil -> ()
- | Coq_cons(hd, tl) -> collect_expr hd; collect_expr_list tl
+ | [] -> ()
+ | hd :: tl -> collect_expr hd; collect_expr_list tl
let rec collect_stmt = function
| Sskip -> ()
@@ -459,8 +459,8 @@ and collect_cases = function
let collect_function f =
collect_type f.fn_return;
- coqlist_iter (fun (Coq_pair(id, ty)) -> collect_type ty) f.fn_params;
- coqlist_iter (fun (Coq_pair(id, ty)) -> collect_type ty) f.fn_vars;
+ List.iter (fun (Coq_pair(id, ty)) -> collect_type ty) f.fn_params;
+ List.iter (fun (Coq_pair(id, ty)) -> collect_type ty) f.fn_vars;
collect_stmt f.fn_body
let collect_fundef (Coq_pair(id, fd)) =
@@ -472,8 +472,8 @@ let collect_globvar (Coq_pair(Coq_pair(id, init), ty)) =
collect_type ty
let collect_program p =
- coqlist_iter collect_globvar p.prog_vars;
- coqlist_iter collect_fundef p.prog_funct
+ List.iter collect_globvar p.prog_vars;
+ List.iter collect_fundef p.prog_funct
let declare_struct_or_union p (name, fld) =
fprintf p "%s;@ @ " name
@@ -494,8 +494,8 @@ let print_program p prog =
fprintf p "@[<v 0>";
StructUnionSet.iter (declare_struct_or_union p) !struct_unions;
StructUnionSet.iter (print_struct_or_union p) !struct_unions;
- coqlist_iter (print_globvar p) prog.prog_vars;
- coqlist_iter (print_fundef p) prog.prog_funct;
+ List.iter (print_globvar p) prog.prog_vars;
+ List.iter (print_fundef p) prog.prog_funct;
fprintf p "@]@."
diff --git a/caml/PrintPPC.ml b/caml/PrintPPC.ml
index f4f2940..94c3a7b 100644
--- a/caml/PrintPPC.ml
+++ b/caml/PrintPPC.ml
@@ -354,10 +354,10 @@ let print_instruction oc labels = function
if Labelset.mem lbl labels then fprintf oc "%a:\n" print_label lbl
let rec labels_of_code = function
- | Coq_nil -> Labelset.empty
- | Coq_cons((Pb lbl | Pbf(_, lbl) | Pbt(_, lbl)), c) ->
+ | [] -> Labelset.empty
+ | (Pb lbl | Pbf(_, lbl) | Pbt(_, lbl)) :: c ->
Labelset.add lbl (labels_of_code c)
- | Coq_cons(_, c) -> labels_of_code c
+ | _ :: c -> labels_of_code c
let print_function oc name code =
Hashtbl.clear current_function_labels;
@@ -365,7 +365,7 @@ let print_function oc name code =
fprintf oc " .align 2\n";
fprintf oc " .globl %a\n" print_symb name;
fprintf oc "%a:\n" print_symb name;
- coqlist_iter (print_instruction oc (labels_of_code code)) code
+ List.iter (print_instruction oc (labels_of_code code)) code
(* Generation of stub code for variadic functions, e.g. printf.
Calling conventions for variadic functions are:
@@ -401,14 +401,14 @@ let variadic_stub oc stub_name fun_name ty_args =
As an optimization, don't copy parameters that are already in
integer registers, since these stay in place. *)
let rec copy gpr fpr src_ofs dst_ofs = function
- | Coq_nil -> ()
- | Coq_cons(Tint, rem) ->
+ | [] -> ()
+ | Tint :: rem ->
if gpr > 10 then begin
fprintf oc " lwz r0, %d(r1)\n" src_ofs;
fprintf oc " stw r0, %d(r1)\n" dst_ofs
end;
copy (gpr + 1) fpr (src_ofs + 4) (dst_ofs + 4) rem
- | Coq_cons(Tfloat, rem) ->
+ | Tfloat :: rem ->
if fpr <= 10 then begin
fprintf oc " stfd f%d, %d(r1)\n" fpr dst_ofs
end else begin
@@ -421,10 +421,10 @@ let variadic_stub oc stub_name fun_name ty_args =
As an optimization, don't load parameters that are already
in the correct integer registers. *)
let rec load gpr ofs = function
- | Coq_nil -> ()
- | Coq_cons(Tint, rem) ->
+ | [] -> ()
+ | Tint :: rem ->
load (gpr + 1) (ofs + 4) rem
- | Coq_cons(Tfloat, rem) ->
+ | Tfloat :: rem ->
if gpr <= 10 then
fprintf oc " lwz r%d, %d(r1)\n" gpr ofs;
if gpr + 1 <= 10 then
@@ -503,20 +503,20 @@ let print_init oc = function
let print_init_data oc id =
init_data_queue := [];
- coqlist_iter (print_init oc) id;
+ List.iter (print_init oc) id;
let rec print_remainder () =
match !init_data_queue with
| [] -> ()
| (lbl, id) :: rem ->
init_data_queue := rem;
fprintf oc "L%d:\n" lbl;
- coqlist_iter (print_init oc) id;
+ List.iter (print_init oc) id;
print_remainder()
in print_remainder()
let print_var oc (Coq_pair(Coq_pair(name, init_data), _)) =
match init_data with
- | Coq_nil -> ()
+ | [] -> ()
| _ ->
fprintf oc " .data\n";
fprintf oc " .align 3\n";
@@ -526,7 +526,7 @@ let print_var oc (Coq_pair(Coq_pair(name, init_data), _)) =
let print_program oc p =
extfuns := IdentSet.empty;
- coqlist_iter record_extfun p.prog_funct;
- coqlist_iter (print_var oc) p.prog_vars;
- coqlist_iter (print_fundef oc) p.prog_funct
+ List.iter record_extfun p.prog_funct;
+ List.iter (print_var oc) p.prog_vars;
+ List.iter (print_fundef oc) p.prog_funct
diff --git a/caml/RTLgenaux.ml b/caml/RTLgenaux.ml
index d920380..4c1fc05 100644
--- a/caml/RTLgenaux.ml
+++ b/caml/RTLgenaux.ml
@@ -28,8 +28,8 @@ module IntSet = Set.Make(IntOrd)
let normalize_table tbl =
let rec norm seen = function
- | CList.Coq_nil -> []
- | CList.Coq_cons(Datatypes.Coq_pair(key, act), rem) ->
+ | [] -> []
+ | Datatypes.Coq_pair(key, act) :: rem ->
if IntSet.mem key seen
then norm seen rem
else (key, act) :: norm (IntSet.add key seen) rem
diff --git a/caml/RTLtypingaux.ml b/caml/RTLtypingaux.ml
index 6c43227..ff704eb 100644
--- a/caml/RTLtypingaux.ml
+++ b/caml/RTLtypingaux.ml
@@ -32,8 +32,8 @@ let set_type r ty =
let rec set_types rl tyl =
match rl, tyl with
- | Coq_nil, Coq_nil -> ()
- | Coq_cons(r1, rs), Coq_cons(ty1, tys) -> set_type r1 ty1; set_types rs tys
+ | [], [] -> ()
+ | r1 :: rs, ty1 :: tys -> set_type r1 ty1; set_types rs tys
| _, _ -> raise (Type_error "arity mismatch")
(* First pass: process constraints of the form typeof(r) = ty *)
@@ -98,16 +98,16 @@ let type_instr retty (Coq_pair(pc, i)) =
end
let type_pass1 retty instrs =
- coqlist_iter (type_instr retty) instrs
+ List.iter (type_instr retty) instrs
(* Second pass: extract move constraints typeof(r1) = typeof(r2)
and solve them iteratively *)
let rec extract_moves = function
- | Coq_nil -> []
- | Coq_cons(Coq_pair(pc, i), rem) ->
+ | [] -> []
+ | Coq_pair(pc, i) :: rem ->
match i with
- | Iop(Omove, Coq_cons(r1, Coq_nil), r2, _) ->
+ | Iop(Omove, [r1], r2, _) ->
(r1, r2) :: extract_moves rem
| Iop(Omove, _, _, _) ->
raise (Type_error "wrong Omove")
diff --git a/extraction/.depend b/extraction/.depend
index 83dc5dc..a8ae227 100644
--- a/extraction/.depend
+++ b/extraction/.depend
@@ -59,9 +59,9 @@
../caml/PrintPPC.cmx: PPC.cmx Datatypes.cmx ../caml/Camlcoq.cmx CList.cmx \
AST.cmx ../caml/PrintPPC.cmi
../caml/RTLgenaux.cmo: Switch.cmi Integers.cmi Datatypes.cmi CminorSel.cmi \
- ../caml/Camlcoq.cmo CList.cmi
+ ../caml/Camlcoq.cmo
../caml/RTLgenaux.cmx: Switch.cmx Integers.cmx Datatypes.cmx CminorSel.cmx \
- ../caml/Camlcoq.cmx CList.cmx
+ ../caml/Camlcoq.cmx
../caml/RTLtypingaux.cmo: Registers.cmi RTL.cmi Op.cmi Maps.cmi Datatypes.cmi \
../caml/Camlcoq.cmo CList.cmi AST.cmi
../caml/RTLtypingaux.cmx: Registers.cmx RTL.cmx Op.cmx Maps.cmx Datatypes.cmx \
diff --git a/extraction/extraction.v b/extraction/extraction.v
index 69034bc..cdb1fd6 100644
--- a/extraction/extraction.v
+++ b/extraction/extraction.v
@@ -10,6 +10,7 @@
(* *)
(* *********************************************************************)
+Require List.
Require Iteration.
Require Floats.
Require RTLgen.
@@ -21,6 +22,7 @@ Require Main.
Extract Inductive unit => "unit" [ "()" ].
Extract Inductive bool => "bool" [ "true" "false" ].
Extract Inductive sumbool => "bool" [ "true" "false" ].
+Extract Inductive List.list => "list" [ "[]" "(::)" ].
(* Float *)
Extract Inlined Constant Floats.float => "float".
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-22 07:02:51 +0000