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 --- cfrontend/C2C.ml | 25 ++++++++++--------------- cfrontend/PrintClight.ml | 16 ++++++++-------- cfrontend/PrintCsyntax.ml | 16 ++++++++-------- 3 files changed, 26 insertions(+), 31 deletions(-) (limited to 'cfrontend') diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index 2f50a0e9..f35598c7 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 ad6887c9..306224ba 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 63587869..f0e9ee54 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 = -- cgit