diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-04-14 19:36:17 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-04-14 19:36:33 -0400 |
| commit | 62058145e881e9f96da18ee970182a95af957882 (patch) | |
| tree | 8f6e737c44750ad776918a10c0fcfc7cea77a41a /src/Compilers/CommonSubexpressionEliminationInterp.v | |
| parent | aa0052b9469c876947cbe7ed007ae8113b711fdc (diff) | |
Add support for cse-modulo-normalization
Diffstat (limited to 'src/Compilers/CommonSubexpressionEliminationInterp.v')
| -rw-r--r-- | src/Compilers/CommonSubexpressionEliminationInterp.v | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/src/Compilers/CommonSubexpressionEliminationInterp.v b/src/Compilers/CommonSubexpressionEliminationInterp.v index 7126b0c72..2d9115eb6 100644 --- a/src/Compilers/CommonSubexpressionEliminationInterp.v +++ b/src/Compilers/CommonSubexpressionEliminationInterp.v @@ -39,8 +39,9 @@ Section symbolic. (interp_op : forall s d (opc : op s d), interp_flat_type interp_base_type s -> interp_flat_type interp_base_type d) (symbolize_op : forall s d, op s d -> op_code) (denote_op : forall s d, op_code -> option (op s d)). - Local Notation symbolic_expr := (symbolic_expr base_type_code op_code). + Context (normalize_symbolic_op_arguments : op_code -> symbolic_expr -> symbolic_expr). + Local Notation symbolic_expr_beq := (@symbolic_expr_beq base_type_code op_code base_type_code_beq op_code_beq). Local Notation symbolic_expr_lb := (@internal_symbolic_expr_dec_lb base_type_code op_code base_type_code_beq op_code_beq base_type_code_lb op_code_lb). Local Notation symbolic_expr_bl := (@internal_symbolic_expr_dec_bl base_type_code op_code base_type_code_beq op_code_beq base_type_code_bl op_code_bl). @@ -56,9 +57,9 @@ Section symbolic. Local Notation symbolicify_smart_var := (@symbolicify_smart_var base_type_code op_code). Local Notation symbolize_exprf := (@symbolize_exprf base_type_code op_code op symbolize_op). - Local Notation csef := (@csef base_type_code op_code base_type_code_beq op_code_beq base_type_code_bl op symbolize_op). - Local Notation cse := (@cse base_type_code op_code base_type_code_beq op_code_beq base_type_code_bl op symbolize_op). - Local Notation CSE := (@CSE base_type_code op_code base_type_code_beq op_code_beq base_type_code_bl op symbolize_op). + Local Notation csef := (@csef base_type_code op_code base_type_code_beq op_code_beq base_type_code_bl op symbolize_op normalize_symbolic_op_arguments). + Local Notation cse := (@cse base_type_code op_code base_type_code_beq op_code_beq base_type_code_bl op symbolize_op normalize_symbolic_op_arguments). + Local Notation CSE := (@CSE base_type_code op_code base_type_code_beq op_code_beq base_type_code_bl op symbolize_op normalize_symbolic_op_arguments). Local Notation SymbolicExprContext := (@SymbolicExprContext base_type_code op_code base_type_code_beq op_code_beq base_type_code_bl). Local Notation SymbolicExprContextOk := (@SymbolicExprContextOk base_type_code op_code base_type_code_beq op_code_beq base_type_code_bl base_type_code_lb op_code_bl op_code_lb). Local Notation prepend_prefix := (@prepend_prefix base_type_code op). |