From 1bce6b0f9f8cd614038a6e7fc21fb984724204a4 Mon Sep 17 00:00:00 2001 From: xleroy Date: Mon, 29 Dec 2008 13:12:08 +0000 Subject: Extract Coq lists to Caml lists. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@929 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- caml/CMparser.mly | 54 ++++++++++++++++++++-------------------- caml/CMtypecheck.ml | 14 +++++------ caml/Camlcoq.ml | 19 --------------- caml/Cil2Csyntax.ml | 65 ++++++++++++++++++++----------------------------- caml/Coloringaux.ml | 8 +++--- caml/Driver.ml | 2 +- caml/Linearizeaux.ml | 4 +-- caml/PrintCsyntax.ml | 38 ++++++++++++++--------------- caml/PrintPPC.ml | 32 ++++++++++++------------ caml/RTLgenaux.ml | 4 +-- caml/RTLtypingaux.ml | 12 ++++----- extraction/.depend | 4 +-- extraction/extraction.v | 2 ++ 13 files changed, 112 insertions(+), 146 deletions(-) diff --git a/caml/CMparser.mly b/caml/CMparser.mly index 0b3eafd8..25fb0321 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 1ac00654..d761f759 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 e9089cf3..98fd79c8 100644 --- a/caml/Camlcoq.ml +++ b/caml/Camlcoq.ml @@ -77,25 +77,6 @@ let extern_atom a = with Not_found -> Printf.sprintf "" (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 7224610c..41fe1d4f 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 984fbb34..f11738df 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 dacc9dcb..8fffcaa0 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 02a95241..2f2333fb 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 6aaa5397..bb25339a 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 "@[{@ "; - 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 "@[%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 "@["; 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 f4f29402..94c3a7b3 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 d9203808..4c1fc05c 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 6c43227b..ff704ebe 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 83dc5dcb..a8ae227f 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 69034bc1..cdb1fd63 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". -- cgit