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