1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
|
(**open Camlcoq
open Datatypes
open Maps
open AST
open Abstr
open PrintAST
open Printf
let rec expr_to_list = function
| Enil -> []
| Econs (e, el) -> e :: expr_to_list el
let res pp = function
| Reg r -> fprintf pp "r%d" (P.to_int r)
| Pred r -> fprintf pp "p%d" (P.to_int r)
| Mem -> fprintf pp "M"
let rec print_expression pp = function
| Ebase r -> fprintf pp "%a'" res r
| Eop (op, el) -> fprintf pp "(%a)" (PrintOp.print_operation print_expression) (op, expr_to_list el)
| Eload (chunk, addr, el, e) ->
fprintf pp "(%s[%a][%a])"
(name_of_chunk chunk) print_expression e
(PrintOp.print_addressing print_expression) (addr, expr_to_list el)
| Estore (e, chunk, addr, el, m) ->
fprintf pp "(%s[%a][%a] = %a)"
(name_of_chunk chunk) print_expression m
(PrintOp.print_addressing print_expression) (addr, expr_to_list el)
print_expression e
| Esetpred (c, el) ->
fprintf pp "(%a)" (PrintOp.print_condition print_expression) (c, expr_to_list el)
let rec print_predicated pp = function
| NE.Coq_singleton (p, e) ->
fprintf pp "%a %a" PrintRTLBlockInstr.print_pred_option p print_expression e
| NE.Coq_cons ((p, e), pr) ->
fprintf pp "%a %a\n%a" PrintRTLBlockInstr.print_pred_option p print_expression e
print_predicated pr
*)
|
