1\DOC UNWIND_AUTO_CONV 2 3\TYPE {UNWIND_AUTO_CONV : conv} 4 5\SYNOPSIS 6Automatic unwinding of equations defining wire values in a standard device 7specification. 8 9\LIBRARY unwind 10 11\DESCRIBE 12{UNWIND_AUTO_CONV "?l1 ... lm. t1 /\ ... /\ tn"} returns a theorem of the form: 13{ 14 |- (?l1 ... lm. t1 /\ ... /\ tn) = (?l1 ... lm. t1' /\ ... /\ tn') 15} 16where {tj'} is {tj} rewritten with equations selected from the 17{ti}'s. 18 19The function decides which equations to use for rewriting by performing a loop 20analysis on the graph representing the dependencies of the lines. By this means 21the term can be unwound as much as possible without the risk of looping. The 22user is left to deal with the recursive equations. 23 24\FAILURE 25Fails if there is more than one equation for any line variable. 26 27\EXAMPLE 28{ 29#UNWIND_AUTO_CONV 30# "(!(x:num). l1 x = (l2 x) - 1) /\ 31# (!x. f x = (l2 (x+1)) + (l1 (x+2))) /\ 32# (!x. l2 x = 7)";; 33|- (!x. l1 x = (l2 x) - 1) /\ 34 (!x. f x = (l2(x + 1)) + (l1(x + 2))) /\ 35 (!x. l2 x = 7) = 36 (!x. l1 x = 7 - 1) /\ (!x. f x = 7 + (7 - 1)) /\ (!x. l2 x = 7) 37} 38\SEEALSO 39unwindLib.UNWIND_ONCE_CONV, unwindLib.UNWIND_CONV, 40unwindLib.UNWIND_ALL_BUT_CONV, unwindLib.UNWIND_ALL_BUT_RIGHT_RULE, 41unwindLib.UNWIND_AUTO_RIGHT_RULE. 42 43\ENDDOC 44