source: driver/backendPrinter.ml @ 2854

Last change on this file since 2854 was 2854, checked in by sacerdot, 7 years ago

Pretty printing of the LTL program.

File size: 2.9 KB
Line 
1let print_keyword =
2 function
3  | Extracted.Joint_printer.KwCOMMENT      -> "COMMENT"
4  | Extracted.Joint_printer.KwMOVE         -> "MOVE"
5  | Extracted.Joint_printer.KwPOP          -> "POP"
6  | Extracted.Joint_printer.KwPUSH         -> "PUSH"
7  | Extracted.Joint_printer.KwADDRESS      -> "ADDRESS"
8  | Extracted.Joint_printer.KwOPACCS       -> "OPACCS"
9  | Extracted.Joint_printer.KwOP1          -> "OP1"
10  | Extracted.Joint_printer.KwOP2          -> "OP2"
11  | Extracted.Joint_printer.KwCLEAR_CARRY  -> "CLEAR_CARRY"
12  | Extracted.Joint_printer.KwSET_CARRY    -> "SET_CARRY"
13  | Extracted.Joint_printer.KwLOAD         -> "LOAD"
14  | Extracted.Joint_printer.KwSTORE        -> "STORE"
15  | Extracted.Joint_printer.KwCOST_LABEL   -> "COST_LABEL"
16  | Extracted.Joint_printer.KwCOND         -> "COND"
17  | Extracted.Joint_printer.KwCALL         -> "CALL"
18  | Extracted.Joint_printer.KwGOTO         -> "GOTO"
19  | Extracted.Joint_printer.KwRETURN       -> "RETURN"
20  | Extracted.Joint_printer.KwTAILCALL     -> "TAILCALL"
21  | Extracted.Joint_printer.KwFCOND        -> "FCOND"
22
23let print_opAccs =
24 function
25  | Extracted.BackEndOps.Mul -> "Mul"
26  | Extracted.BackEndOps.DivuModu -> "DivModu"
27
28let print_op1 =
29 function
30  | Extracted.BackEndOps.Cmpl -> "Cmpl"
31  | Extracted.BackEndOps.Inc -> "Inc"
32  | Extracted.BackEndOps.Rl -> "Rl"
33
34let print_op2 =
35 function
36  | Extracted.BackEndOps.Add -> "Add"
37  | Extracted.BackEndOps.Addc -> "Addc"
38  | Extracted.BackEndOps.Sub -> "Sub"
39  | Extracted.BackEndOps.And -> "And"
40  | Extracted.BackEndOps.Or -> "Or"
41  | Extracted.BackEndOps.Xor -> "Xor"
42
43(* Duplicated, also in cerco.ml! *)
44let string_of_pos n = string_of_int (Extracted.Glue.int_of_matitapos n)
45
46let printing_pass_independent_params =
47 { Extracted.Joint_printer.print_String =
48    (fun Extracted.String.EmptyString -> "EmptyString")
49 ; print_keyword = print_keyword
50 ; print_concat = (fun s1 s2 -> s1 ^ " " ^ s2)
51 ; print_empty = ""
52 ; print_newline = "\n"
53 ; print_ident = (fun n -> "fun_" ^ string_of_pos n)
54 ; print_costlabel = (fun n -> "k_" ^ string_of_pos n)
55 ; print_label = (fun n -> "l_" ^ string_of_pos n)
56 ; print_OpAccs = print_opAccs
57 ; print_Op1 = print_op1
58 ; print_Op2 = print_op2
59 }
60
61let joint_LTL_LIN_printing_params =
62 { Extracted.Joint_printer.print_pass_ind = printing_pass_independent_params
63 ; print_acc_a_reg = (fun _ -> "ACC_A")
64 ; print_acc_b_reg = (fun _ -> "ACC_B")
65 ; print_acc_a_arg = (fun _ -> "ACC_A")
66 ; print_acc_b_arg = (fun _ -> "ACC_B")
67 ; print_dpl_reg = (fun _ -> "DPL")
68 ; print_dph_reg = (fun _ -> "DPH")
69 ; print_dpl_arg = (fun _ -> "DPL")
70 ; print_dph_arg = (fun _ -> "DPH")
71 ; print_snd_arg = (fun hdw_arg -> "ACC_B")
72 ; print_pair_move = (fun pair_move -> "ACC_B")
73 ; print_call_args = (fun n -> "ACC_B")
74 ; print_call_dest = (fun _ -> "")
75 ; print_ext_seq = (fun ltl_lin_seq -> assert false )
76 }
77
78let print_LTL_program =
79 Extracted.LTL_printer.print_LTL_program joint_LTL_LIN_printing_params
Note: See TracBrowser for help on using the repository browser.