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

8 files changed, 23 insertions, 24 deletions

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