summaryrefslogtreecommitdiff
path: root/backend
diff options
context:
space:
mode:
authorGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2011-10-18 09:40:59 +0000
committerGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2011-10-18 09:40:59 +0000
commitcdcb658c29409c8aef94ca3e22c14a90b396aea0 (patch)
tree8981d0a2312604c6b8ab8a8acb108f39f1cd1377 /backend
parentf535ac931c2b7dc65fefa83e47bb8c79ca90e92d (diff)
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
Diffstat (limited to 'backend')
-rw-r--r--backend/CMparser.mly21
-rw-r--r--backend/CMtypecheck.ml2
-rw-r--r--backend/Coloringaux.ml8
-rw-r--r--backend/PrintCminor.ml4
-rw-r--r--backend/PrintLTL.ml2
-rw-r--r--backend/PrintRTL.ml2
-rw-r--r--backend/RTLgenaux.ml2
-rw-r--r--backend/RTLtypingaux.ml6
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