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

3 files changed, 26 insertions, 31 deletions

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 "@[<v 2>{@ ";
   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 "@[<v 2>{@ ";
   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 =