UNWIND_ONCE_CONV
unwindLib.UNWIND_ONCE_CONV : ((term -> bool) -> conv)
Basic conversion for parallel unwinding of equations defining wire values in a standard device specification.
UNWIND_ONCE_CONV p tm unwinds the conjunction tm using the equations
selected by the predicate p. tm should be a conjunction, equivalent
under associative-commutative reordering to:
t1 /\ t2 /\ ... /\ tn
p is used to partition the terms ti for 1 <= i <= n into two
disjoint sets:
REW = {{ti | p ti}}
OBJ = {{ti | ~p ti}}
The terms ti for which p is true are then used as a set of rewrite
rules (thus they should be equations) to do a single top-down parallel
rewrite of the remaining terms. The rewritten terms take the place of
the original terms in the input conjunction. For example, if tm is:
t1 /\ t2 /\ t3 /\ t4
and REW = {{t1,t3}} then the result is:
|- t1 /\ t2 /\ t3 /\ t4 = t1 /\ t2' /\ t3 /\ t4'
where ti' is ti rewritten with the equations REW.
Failure
Never fails.
Example
> unwindLib.UNWIND_ONCE_CONV (fn tm => mem (unwindLib.line_name tm) [`l1`,`l2`])
“(!(x:num). l1 x = (l2 x) - 1) /\
(!x. f x = (l2 (x+1)) + (l1 (x+2))) /\
(!x. l2 x = 7)”;
Exception- Type error in function application.
Function: mem (unwindLib.line_name tm) : string list -> bool
Argument: [[QUOTE " (*#loc 1 69*)l1"], [QUOTE " (*#loc 1 74*)l2"]]
: 'a frag list list
Reason:
Can't unify string (*In Basis*) with 'a frag list (*In Basis*)
(Different type constructors)
Fail "Static Errors" raised
See also
unwindLib.UNWIND_CONV,
unwindLib.UNWIND_ALL_BUT_CONV,
unwindLib.UNWIND_AUTO_CONV,
unwindLib.UNWIND_ALL_BUT_RIGHT_RULE,
unwindLib.UNWIND_AUTO_RIGHT_RULE