diff options
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 e0ebf71a4..0d7fa1e25 100644 --- a/src/Compilers/CommonSubexpressionEliminationInterp.v +++ b/src/Compilers/CommonSubexpressionEliminationInterp.v @@ -40,7 +40,8 @@ Section symbolic. (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). + Context (normalize_symbolic_op_arguments : op_code -> symbolic_expr -> symbolic_expr) + (inline_symbolic_expr_in_lookup : bool). 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). @@ -57,9 +58,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 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 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 inline_symbolic_expr_in_lookup). + 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 inline_symbolic_expr_in_lookup). + 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 inline_symbolic_expr_in_lookup). 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). |