MacroC name c1 t1 c2 t2
MacroC will rewrite an instance of t1 to the corresponding instance of t2 using forward and reverse computation steps. For example, a macro conversion might unfolds an abstraction, unroll a recursive or inductive primitive term, and then fold up an abstraction. Specific examples can be found in the standard libraries - Look at the definitions of non-canonical abstractions. Specifically, look at ycomb_unroll or pi1_eval.
c1 and c2 must be direct computation conversions which rewrite the pattern terms t1 and t2 respectively to the same term. MacroC uses second-order matching when matching instance terms against t1. Also, any parameter variables in t1 will also be used in the match. name is used in the conversion's failure token.
For examples of the use of MacroC look at the length_unroll object in the list_1 theory.
