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 --- 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 +++--- 8 files changed, 23 insertions(+), 24 deletions(-) (limited to 'backend') 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 -- cgit v1.2.3