413 let val (eqs, noneqs) = List.partition (fn (Lineq(_,ty,_,_)) => ty=Eq) nontriv in |
413 let val (eqs, noneqs) = List.partition (fn (Lineq(_,ty,_,_)) => ty=Eq) nontriv in |
414 if not (null eqs) then |
414 if not (null eqs) then |
415 let val c = |
415 let val c = |
416 fold (fn Lineq(_,_,l,_) => fn cs => union (op =) l cs) eqs [] |
416 fold (fn Lineq(_,_,l,_) => fn cs => union (op =) l cs) eqs [] |
417 |> filter (fn i => i <> 0) |
417 |> filter (fn i => i <> 0) |
418 |> sort (int_ord o pairself abs) |
418 |> sort (int_ord o apply2 abs) |
419 |> hd |
419 |> hd |
420 val (eq as Lineq(_,_,ceq,_),othereqs) = |
420 val (eq as Lineq(_,_,ceq,_),othereqs) = |
421 extract_first (fn Lineq(_,_,l,_) => member (op =) l c) eqs |
421 extract_first (fn Lineq(_,_,l,_) => member (op =) l c) eqs |
422 val v = find_index (fn v => v = c) ceq |
422 val v = find_index (fn v => v = c) ceq |
423 val (ioth,roth) = List.partition (fn (Lineq(_,_,l,_)) => nth l v = 0) |
423 val (ioth,roth) = List.partition (fn (Lineq(_,_,l,_)) => nth l v = 0) |