1\DOC UNWIND_ONCE_CONV 2 3\TYPE {UNWIND_ONCE_CONV : ((term -> bool) -> conv)} 4 5\SYNOPSIS 6Basic conversion for parallel unwinding of equations defining wire values in a 7standard device specification. 8 9\LIBRARY unwind 10 11\DESCRIBE 12{UNWIND_ONCE_CONV p tm} unwinds the conjunction {tm} using the equations 13selected by the predicate {p}. {tm} should be a conjunction, equivalent under 14associative-commutative reordering to: 15{ 16 t1 /\ t2 /\ ... /\ tn 17} 18{p} is used to partition the terms {ti} for {1 <= i <= n} into two 19disjoint sets: 20{ 21 REW = {{ti | p ti}} 22 OBJ = {{ti | ~p ti}} 23} 24The terms {ti} for which {p} is true are then used as a set of 25rewrite rules (thus they should be equations) to do a single top-down parallel 26rewrite of the remaining terms. The rewritten terms take the place of the 27original terms in the input conjunction. For example, if {tm} is: 28{ 29 t1 /\ t2 /\ t3 /\ t4 30} 31and {REW = {{t1,t3}}} then the result is: 32{ 33 |- t1 /\ t2 /\ t3 /\ t4 = t1 /\ t2' /\ t3 /\ t4' 34} 35where {ti'} is {ti} rewritten with the equations {REW}. 36 37\FAILURE 38Never fails. 39 40\EXAMPLE 41{ 42#UNWIND_ONCE_CONV (\tm. mem (line_name tm) [`l1`;`l2`]) 43# "(!(x:num). l1 x = (l2 x) - 1) /\ 44# (!x. f x = (l2 (x+1)) + (l1 (x+2))) /\ 45# (!x. l2 x = 7)";; 46|- (!x. l1 x = (l2 x) - 1) /\ 47 (!x. f x = (l2(x + 1)) + (l1(x + 2))) /\ 48 (!x. l2 x = 7) = 49 (!x. l1 x = (l2 x) - 1) /\ 50 (!x. f x = 7 + ((l2(x + 2)) - 1)) /\ 51 (!x. l2 x = 7) 52} 53\SEEALSO 54unwindLib.UNWIND_CONV, unwindLib.UNWIND_ALL_BUT_CONV, 55unwindLib.UNWIND_AUTO_CONV, unwindLib.UNWIND_ALL_BUT_RIGHT_RULE, 56unwindLib.UNWIND_AUTO_RIGHT_RULE. 57 58\ENDDOC 59