From cdcb658c29409c8aef94ca3e22c14a90b396aea0 Mon Sep 17 00:00:00 2001 From: xleroy Date: Tue, 18 Oct 2011 09:40:59 +0000 Subject: Extraction: map Coq pairs to Caml pairs and Coq chars (type ascii) to Caml chars git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1732 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- arm/PrintAsm.ml | 6 +++--- backend/CMparser.mly | 21 ++++++++++----------- backend/CMtypecheck.ml | 2 +- backend/Coloringaux.ml | 8 ++++---- backend/PrintCminor.ml | 4 ++-- backend/PrintLTL.ml | 2 +- backend/PrintRTL.ml | 2 +- backend/RTLgenaux.ml | 2 +- backend/RTLtypingaux.ml | 6 +++--- cfrontend/C2C.ml | 25 ++++++++++--------------- cfrontend/PrintClight.ml | 16 ++++++++-------- cfrontend/PrintCsyntax.ml | 16 ++++++++-------- driver/Interp.ml | 25 ++++++++++++++----------- extraction/extraction.v | 7 ++----- ia32/PrintAsm.ml | 10 +++++----- lib/Camlcoq.ml | 24 ++++-------------------- powerpc/PrintAsm.ml | 6 +++--- 17 files changed, 80 insertions(+), 102 deletions(-) diff --git a/arm/PrintAsm.ml b/arm/PrintAsm.ml index 50b585e..a616cc2 100644 --- a/arm/PrintAsm.ml +++ b/arm/PrintAsm.ml @@ -201,7 +201,7 @@ let call_helper oc fn dst arg1 arg2 = let moves = Parmov.parmove2 (=) (fun _ -> IR14) [arg1; arg2] [IR0; IR1] in List.iter - (fun (Coq_pair(s, d)) -> + (fun (s, d) -> fprintf oc " mov %a, %a\n" ireg d ireg s) moves; (* Call the helper function *) @@ -689,7 +689,7 @@ let print_function oc name fn = fprintf oc " .type %a, %%function\n" print_symb name; fprintf oc " .size %a, . - %a\n" print_symb name print_symb name -let print_fundef oc (Coq_pair(name, defn)) = +let print_fundef oc (name, defn) = match defn with | Internal code -> print_function oc name code @@ -729,7 +729,7 @@ let rec log2 n = assert (n > 0); if n = 1 then 0 else 1 + log2 (n lsr 1) -let print_var oc (Coq_pair(name, v)) = +let print_var oc (name, v) = match v.gvar_init with | [] -> () | _ -> diff --git a/backend/CMparser.mly b/backend/CMparser.mly index 0b48c0f..3df3f54 100644 --- a/backend/CMparser.mly +++ b/backend/CMparser.mly @@ -141,7 +141,7 @@ let mkswitch expr (cases, dfl) = let rec mktable = function | [] -> [] | (key, exit) :: rem -> - Coq_pair(coqint_of_camlint key, exitnum exit) :: mktable rem in + (coqint_of_camlint key, exitnum exit) :: mktable rem in prepend_seq !convert_accu (Sswitch(c, mktable cases, exitnum dfl)) (*** @@ -166,7 +166,7 @@ let mkmatch_aux expr cases = | [] -> assert false | [key, action] -> [] | (key, action) :: rem -> - Coq_pair(coqint_of_camlint key, nat_of_camlint n) + (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 @@ -324,8 +324,8 @@ global_declarations: global_declaration: VAR STRINGLIT LBRACKET INTLIT RBRACKET - { Coq_pair($2, {gvar_info = (); gvar_init = [Init_space(z_of_camlint $4)]; - gvar_readonly = false; gvar_volatile = false}) } + { ($2, {gvar_info = (); gvar_init = [Init_space(z_of_camlint $4)]; + gvar_readonly = false; gvar_volatile = false}) } ; proc_list: @@ -345,14 +345,13 @@ proc: { let tmp = !temporaries in temporaries := []; temp_counter := 0; - Coq_pair($1, - Internal { fn_sig = $6; - fn_params = List.rev $3; - fn_vars = List.rev (tmp @ $9); - fn_stackspace = $8; - fn_body = $10 }) } + ($1, Internal { fn_sig = $6; + fn_params = List.rev $3; + fn_vars = List.rev (tmp @ $9); + fn_stackspace = $8; + fn_body = $10 }) } | EXTERN STRINGLIT COLON signature - { Coq_pair($2, External(EF_external($2, $4))) } + { ($2, External(EF_external($2, $4))) } ; signature: diff --git a/backend/CMtypecheck.ml b/backend/CMtypecheck.ml index 819f269..e3a6f70 100644 --- a/backend/CMtypecheck.ml +++ b/backend/CMtypecheck.ml @@ -351,7 +351,7 @@ let type_function id f = with Error s -> raise (Error (sprintf "In function %s:\n%s" (extern_atom id) s)) -let type_fundef (Coq_pair (id, fd)) = +let type_fundef (id, fd) = match fd with | Internal f -> type_function id f | External ef -> () diff --git a/backend/Coloringaux.ml b/backend/Coloringaux.ml index 34fab90..ab7d141 100644 --- a/backend/Coloringaux.ml +++ b/backend/Coloringaux.ml @@ -410,11 +410,11 @@ let build g typenv spillcosts = n in (* Fill the adjacency set and the adjacency lists; compute the degrees. *) SetRegReg.fold - (fun (Coq_pair(r1, r2)) () -> + (fun (r1, r2) () -> addEdge (find_reg_node r1) (find_reg_node r2)) g.interf_reg_reg (); SetRegMreg.fold - (fun (Coq_pair(r1, mr2)) () -> + (fun (r1, mr2) () -> addEdge (find_reg_node r1) (find_mreg_node mr2)) g.interf_reg_mreg (); (* Process the moves and insert them in worklistMoves *) @@ -427,11 +427,11 @@ let build g typenv spillcosts = n2.movelist <- m :: n2.movelist; DLinkMove.insert m worklistMoves in SetRegReg.fold - (fun (Coq_pair(r1, r2)) () -> + (fun (r1, r2) () -> add_move (find_reg_node r1) (find_reg_node r2)) g.pref_reg_reg (); SetRegMreg.fold - (fun (Coq_pair(r1, mr2)) () -> + (fun (r1, mr2) () -> let r1' = find_reg_node r1 in if List.mem mr2 !allocatable_registers then add_move r1' (find_mreg_node mr2)) diff --git a/backend/PrintCminor.ml b/backend/PrintCminor.ml index 6a74506..30884b1 100644 --- a/backend/PrintCminor.ml +++ b/backend/PrintCminor.ml @@ -223,7 +223,7 @@ let rec print_stmt p s = | Sswitch(e, cases, dfl) -> fprintf p "@[switch (%a) {" print_expr e; List.iter - (fun (Coq_pair(n, x)) -> + (fun (n, x) -> fprintf p "@ case %ld: exit %d;\n" (camlint_of_coqint n) (camlint_of_nat x)) cases; @@ -262,7 +262,7 @@ let print_function p id f = print_stmt p f.fn_body; fprintf p "@;<0 -2>}@]@ " -let print_fundef p (Coq_pair(id, fd)) = +let print_fundef p (id, fd) = match fd with | External ef -> () (* Todo? *) diff --git a/backend/PrintLTL.ml b/backend/PrintLTL.ml index 3bfd803..94f5af0 100644 --- a/backend/PrintLTL.ml +++ b/backend/PrintLTL.ml @@ -103,7 +103,7 @@ let print_function pp f = List.sort (fun (pc1, _) (pc2, _) -> Pervasives.compare pc2 pc1) (List.map - (fun (Coq_pair(pc, i)) -> (camlint_of_positive pc, i)) + (fun (pc, i) -> (camlint_of_positive pc, i)) (PTree.elements f.fn_code)) in print_succ pp f.fn_entrypoint (match instrs with (pc1, _) :: _ -> pc1 | [] -> -1l); diff --git a/backend/PrintRTL.ml b/backend/PrintRTL.ml index 620a949..985bd63 100644 --- a/backend/PrintRTL.ml +++ b/backend/PrintRTL.ml @@ -96,7 +96,7 @@ let print_function pp f = List.sort (fun (pc1, _) (pc2, _) -> Pervasives.compare pc2 pc1) (List.map - (fun (Coq_pair(pc, i)) -> (camlint_of_positive pc, i)) + (fun (pc, i) -> (camlint_of_positive pc, i)) (PTree.elements f.fn_code)) in print_succ pp f.fn_entrypoint (match instrs with (pc1, _) :: _ -> pc1 | [] -> -1l); diff --git a/backend/RTLgenaux.ml b/backend/RTLgenaux.ml index 82cb300..0822587 100644 --- a/backend/RTLgenaux.ml +++ b/backend/RTLgenaux.ml @@ -29,7 +29,7 @@ module IntSet = Set.Make(IntOrd) let normalize_table tbl = let rec norm keys accu = function | [] -> (accu, keys) - | Datatypes.Coq_pair(key, act) :: rem -> + | (key, act) :: rem -> if IntSet.mem key keys then norm keys accu rem else norm (IntSet.add key keys) ((key, act) :: accu) rem diff --git a/backend/RTLtypingaux.ml b/backend/RTLtypingaux.ml index 17acbc6..5935605 100644 --- a/backend/RTLtypingaux.ml +++ b/backend/RTLtypingaux.ml @@ -39,7 +39,7 @@ let rec set_types rl tyl = (* First pass: process constraints of the form typeof(r) = ty *) -let type_instr retty (Coq_pair(pc, i)) = +let type_instr retty (pc, i) = match i with | Inop(_) -> () @@ -48,7 +48,7 @@ let type_instr retty (Coq_pair(pc, i)) = | Iop(op, args, res, _) -> if two_address_op op && List.length args >= 1 && List.hd args <> res then raise (Type_error "two-address constraint violation"); - let (Coq_pair(targs, tres)) = type_of_operation op in + let (targs, tres) = type_of_operation op in set_types args targs; set_type res tres | Iload(chunk, addr, args, dst, _) -> set_types args (type_of_addressing addr); @@ -119,7 +119,7 @@ let type_pass1 retty instrs = let rec extract_moves = function | [] -> [] - | Coq_pair(pc, i) :: rem -> + | (pc, i) :: rem -> match i with | Iop(Omove, [r1], r2, _) -> (r1, r2) :: extract_moves rem diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index 2f50a0e..f35598c 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -132,9 +132,8 @@ let global_for_string s id = :: !init in add_char '\000'; for i = String.length s - 1 downto 0 do add_char s.[i] done; - Datatypes.Coq_pair(id, - {gvar_info = typeStringLiteral s; gvar_init = !init; - gvar_readonly = true; gvar_volatile = false}) + (id, {gvar_info = typeStringLiteral s; gvar_init = !init; + gvar_readonly = true; gvar_volatile = false}) let globals_for_strings globs = Hashtbl.fold @@ -151,8 +150,7 @@ let register_special_external name ef targs tres = let declare_special_externals k = Hashtbl.fold - (fun name fd k -> - Datatypes.Coq_pair(intern_string name, fd) :: k) + (fun name fd k -> (intern_string name, fd) :: k) special_externals_table k (** ** Handling of stubs for variadic functions *) @@ -720,7 +718,7 @@ let convertFundef env fd = (fun (id, ty) -> if Cutil.is_composite_type env ty then unsupported "function parameter of struct or union type"; - Datatypes.Coq_pair(intern_string id.name, convertTyp env ty)) + (intern_string id.name, convertTyp env ty)) fd.fd_params in let vars = List.map @@ -729,7 +727,7 @@ let convertFundef env fd = unsupported "'static' or 'extern' local variable"; if init <> None then unsupported "initialized local variable"; - Datatypes.Coq_pair(intern_string id.name, convertTyp env ty)) + (intern_string id.name, convertTyp env ty)) fd.fd_locals in let body' = convertStmt env fd.fd_body in let id' = intern_string fd.fd_name.name in @@ -739,9 +737,8 @@ let convertFundef env fd = a_type = Cutil.fundef_typ fd; a_fundef = Some fd }; Sections.define_function env id' fd.fd_ret; - Datatypes.Coq_pair(id', - Internal {fn_return = ret; fn_params = params; - fn_vars = vars; fn_body = body'}) + (id', Internal {fn_return = ret; fn_params = params; + fn_vars = vars; fn_body = body'}) (** External function declaration *) @@ -758,7 +755,7 @@ let convertFundecl env (sto, id, ty, optinit) = if List.mem_assoc id.name builtins.functions then EF_builtin(id', sg) else EF_external(id', sg) in - Datatypes.Coq_pair(id', External(ef, args, res)) + (id', External(ef, args, res)) (** Initializers *) @@ -810,10 +807,8 @@ let convertGlobvar env (sto, id, ty, optinit) = let a = Cutil.attributes_of_type env ty in let volatile = List.mem C.AVolatile a in let readonly = List.mem C.AConst a && not volatile in - Datatypes.Coq_pair(id', - {gvar_info = ty'; gvar_init = init'; - gvar_readonly = readonly; - gvar_volatile = volatile}) + (id', {gvar_info = ty'; gvar_init = init'; + gvar_readonly = readonly; gvar_volatile = volatile}) (** Convert a list of global declarations. Result is a pair [(funs, vars)] where [funs] are diff --git a/cfrontend/PrintClight.ml b/cfrontend/PrintClight.ml index ad6887c..306224b 100644 --- a/cfrontend/PrintClight.ml +++ b/cfrontend/PrintClight.ml @@ -231,17 +231,17 @@ let print_function p id f = f.fn_return); fprintf p "@[{@ "; List.iter - (fun (Coq_pair(id, ty)) -> + (fun (id, ty) -> fprintf p "%s;@ " (name_cdecl (extern_atom id) ty)) f.fn_vars; List.iter - (fun (Coq_pair(id, ty)) -> + (fun (id, ty) -> fprintf p "register %s;@ " (name_cdecl (temp_name id) ty)) f.fn_temps; print_stmt p f.fn_body; fprintf p "@;<0 -2>}@]@ @ " -let print_fundef p (Coq_pair(id, fd)) = +let print_fundef p (id, fd) = match fd with | External(_, args, res) -> fprintf p "extern %s;@ @ " @@ -314,17 +314,17 @@ and collect_cases = function let collect_function f = collect_type f.fn_return; - 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; - List.iter (fun (Coq_pair(id, ty)) -> collect_type ty) f.fn_temps; + List.iter (fun (id, ty) -> collect_type ty) f.fn_params; + List.iter (fun (id, ty) -> collect_type ty) f.fn_vars; + List.iter (fun (id, ty) -> collect_type ty) f.fn_temps; collect_stmt f.fn_body -let collect_fundef (Coq_pair(id, fd)) = +let collect_fundef (id, fd) = match fd with | External(_, args, res) -> collect_type_list args; collect_type res | Internal f -> collect_function f -let collect_globvar (Coq_pair(id, v)) = +let collect_globvar (id, v) = collect_type v.gvar_info let collect_program p = diff --git a/cfrontend/PrintCsyntax.ml b/cfrontend/PrintCsyntax.ml index 6358786..f0e9ee5 100644 --- a/cfrontend/PrintCsyntax.ml +++ b/cfrontend/PrintCsyntax.ml @@ -312,7 +312,7 @@ let name_function_parameters fun_name params = | _ -> let rec add_params first = function | [] -> () - | Coq_pair(id, ty) :: rem -> + | (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 @@ -328,13 +328,13 @@ let print_function p id f = f.fn_return); fprintf p "@[{@ "; List.iter - (fun (Coq_pair(id, ty)) -> + (fun (id, ty) -> fprintf p "%s;@ " (name_cdecl (extern_atom id) ty)) f.fn_vars; print_stmt p f.fn_body; fprintf p "@;<0 -2>}@]@ @ " -let print_fundef p (Coq_pair(id, fd)) = +let print_fundef p (id, fd) = match fd with | External(_, args, res) -> fprintf p "extern %s;@ @ " @@ -374,7 +374,7 @@ let print_init p = function let re_string_literal = Str.regexp "__stringlit_[0-9]+" -let print_globvar p (Coq_pair(id, v)) = +let print_globvar p (id, v) = let name1 = extern_atom id in let name2 = if v.gvar_readonly then "const " ^ name1 else name1 in let name3 = if v.gvar_volatile then "volatile " ^ name2 else name2 in @@ -469,16 +469,16 @@ and collect_cases = function let collect_function f = collect_type f.fn_return; - 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; + List.iter (fun (id, ty) -> collect_type ty) f.fn_params; + List.iter (fun (id, ty) -> collect_type ty) f.fn_vars; collect_stmt f.fn_body -let collect_fundef (Coq_pair(id, fd)) = +let collect_fundef (id, fd) = match fd with | External(_, args, res) -> collect_type_list args; collect_type res | Internal f -> collect_function f -let collect_globvar (Coq_pair(id, v)) = +let collect_globvar (id, v) = collect_type v.gvar_info let collect_program p = diff --git a/driver/Interp.ml b/driver/Interp.ml index 43f569c..ff097c9 100644 --- a/driver/Interp.ml +++ b/driver/Interp.ml @@ -78,7 +78,7 @@ let print_event p = function let name_of_fundef prog fd = let rec find_name = function | [] -> "" - | Coq_pair(id, fd') :: rem -> + | (id, fd') :: rem -> if fd = fd' then extern_atom id else find_name rem in find_name prog.prog_funct @@ -131,7 +131,7 @@ let compare_mem m1 m2 = if m1 == m2 then 0 else let c = compare m1.Mem.nextblock m2.Mem.nextblock in if c <> 0 then c else compare_Z_range Z0 m1.Mem.nextblock (fun b -> - let (Coq_pair(lo, hi) as bnds) = m1.Mem.bounds b in + let ((lo, hi) as bnds) = m1.Mem.bounds b in let c = compare bnds (m2.Mem.bounds b) in if c <> 0 then c else let contents1 = m1.Mem.mem_contents b and contents2 = m2.Mem.mem_contents b in if contents1 == contents2 then 0 else @@ -328,7 +328,7 @@ let rec world = Determinism.World(world_io, world_vload, world_vstore) and world_io id args = match chop_stub(extern_atom id), args with | "printf", EVptr_global(id, ofs) :: args' -> - Some(Coq_pair(EVint Integers.Int.zero, world)) + Some(EVint Integers.Int.zero, world) | _, _ -> None @@ -342,7 +342,7 @@ and world_vload chunk id ofs = | Mint32 -> EVint(coqint_of_camlint(Random.int32 0x7FFF_FFFFl)) | Mfloat32 -> EVfloat(Floats.Float.singleoffloat(Random.float 1.0)) | Mfloat64 -> EVfloat(Random.float 1.0) - in Some(Coq_pair(res, world)) + in Some(res, world) and world_vstore chunk id ofs v = assert !random_volatiles; @@ -390,7 +390,7 @@ let do_step p prog ge time s = fprintf p "@]."; exit 126 | l -> - List.iter (fun (Coq_pair(t, s')) -> do_events p ge time s t) l; + List.iter (fun (t, s') -> do_events p ge time s t) l; List.map snd l let rec explore p prog ge time ss = @@ -405,14 +405,17 @@ let rec explore p prog ge time ss = explore p prog ge (time + 1) ss' end +(* Massaging the source program *) + let unvolatile prog = - let unvolatile_globvar (Coq_pair(id, gv)) = - Coq_pair(id, - if gv.gvar_volatile - then {gv with gvar_readonly = false; gvar_volatile = false} - else gv) in + let unvolatile_globvar (id, gv) = + (id, if gv.gvar_volatile + then {gv with gvar_readonly = false; gvar_volatile = false} + else gv) in {prog with prog_vars = List.map unvolatile_globvar prog.prog_vars} +(* Execution of a whole program *) + let execute prog = Random.self_init(); let p = err_formatter in @@ -420,5 +423,5 @@ let execute prog = let prog' = if !random_volatiles then prog else unvolatile prog in begin match Cexec.do_initial_state prog' with | None -> fprintf p "ERROR: Initial state undefined@." - | Some(Coq_pair(ge, s)) -> explore p prog ge 0 (StateSet.singleton s) + | Some(ge, s) -> explore p prog ge 0 (StateSet.singleton s) end diff --git a/extraction/extraction.v b/extraction/extraction.v index 4bfac69..52706ab 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -19,11 +19,8 @@ Require Compiler. Require Initializers. (* Standard lib *) -Extract Inductive unit => "unit" [ "()" ]. -Extract Inductive bool => "bool" [ "true" "false" ]. -Extract Inductive sumbool => "bool" [ "true" "false" ]. -Extract Inductive option => "option" [ "Some" "None" ]. -Extract Inductive list => "list" [ "[]" "(::)" ]. +Require Import ExtrOcamlBasic. +Require Import ExtrOcamlString. (* Float *) Extract Inlined Constant Floats.float => "float". diff --git a/ia32/PrintAsm.ml b/ia32/PrintAsm.ml index f48b808..5ca56d7 100644 --- a/ia32/PrintAsm.ml +++ b/ia32/PrintAsm.ml @@ -114,7 +114,7 @@ let addressing oc (Addrmode(base, shift, cst)) = | Coq_inl n -> let n = camlint_of_coqint n in fprintf oc "%ld" n - | Coq_inr(Coq_pair(id, ofs)) -> + | Coq_inr(id, ofs) -> let ofs = camlint_of_coqint ofs in if ofs = 0l then symbol oc id @@ -123,8 +123,8 @@ let addressing oc (Addrmode(base, shift, cst)) = begin match base, shift with | None, None -> () | Some r1, None -> fprintf oc "(%a)" ireg r1 - | None, Some(Coq_pair(r2,sc)) -> fprintf oc "(,%a,%a)" ireg r2 coqint sc - | Some r1, Some(Coq_pair(r2,sc)) -> fprintf oc "(%a,%a,%a)" ireg r1 ireg r2 coqint sc + | None, Some(r2,sc) -> fprintf oc "(,%a,%a)" ireg r2 coqint sc + | Some r1, Some(r2,sc) -> fprintf oc "(%a,%a,%a)" ireg r1 ireg r2 coqint sc end let name_of_condition = function @@ -730,7 +730,7 @@ let print_function oc name code = jumptables := [] end -let print_fundef oc (Coq_pair(name, defn)) = +let print_fundef oc (name, defn) = match defn with | Internal code -> print_function oc name code | External ef -> () @@ -761,7 +761,7 @@ let print_init_data oc name id = else List.iter (print_init oc) id -let print_var oc (Coq_pair(name, v)) = +let print_var oc (name, v) = match v.gvar_init with | [] -> () | _ -> diff --git a/lib/Camlcoq.ml b/lib/Camlcoq.ml index 34aaa0f..cfbca6e 100644 --- a/lib/Camlcoq.ml +++ b/lib/Camlcoq.ml @@ -109,27 +109,11 @@ let extern_atom a = (* Strings *) -let char_of_ascii (Ascii.Ascii(a0, a1, a2, a3, a4, a5, a6, a7)) = - Char.chr( (if a0 then 1 else 0) - + (if a1 then 2 else 0) - + (if a2 then 4 else 0) - + (if a3 then 8 else 0) - + (if a4 then 16 else 0) - + (if a5 then 32 else 0) - + (if a6 then 64 else 0) - + (if a7 then 128 else 0)) - -let coqstring_length s = - let rec len accu = function - | 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 camlstring_of_coqstring (s: char list) = + let r = String.create (List.length s) in let rec fill pos = function - | String0.EmptyString -> r - | String0.String(c, s) -> r.[pos] <- char_of_ascii c; fill (pos + 1) s + | [] -> r + | c :: s -> r.[pos] <- c; fill (pos + 1) s in fill 0 s (* Timing facility *) diff --git a/powerpc/PrintAsm.ml b/powerpc/PrintAsm.ml index 3b90ada..91dd686 100644 --- a/powerpc/PrintAsm.ml +++ b/powerpc/PrintAsm.ml @@ -920,7 +920,7 @@ let stub_function = | MacOS -> Stubs_MacOS.stub_function | Linux|Diab -> Stubs_EABI.stub_function -let print_fundef oc (Coq_pair(name, defn)) = +let print_fundef oc (name, defn) = match defn with | Internal code -> print_function oc name code @@ -929,7 +929,7 @@ let print_fundef oc (Coq_pair(name, defn)) = | External _ -> () -let record_extfun (Coq_pair(name, defn)) = +let record_extfun (name, defn) = match defn with | Internal _ -> () | External (EF_external _) -> @@ -967,7 +967,7 @@ let print_init_data oc name id = else List.iter (print_init oc) id -let print_var oc (Coq_pair(name, v)) = +let print_var oc (name, v) = match v.gvar_init with | [] -> () | _ -> -- cgit v1.2.3