387 fold (fn Lineq(_,_,l,_) => fn cs => union (op =) l cs) eqs [] |
387 fold (fn Lineq(_,_,l,_) => fn cs => union (op =) l cs) eqs [] |
388 |> filter (fn i => i <> 0) |
388 |> filter (fn i => i <> 0) |
389 |> sort (int_ord o pairself abs) |
389 |> sort (int_ord o pairself abs) |
390 |> hd |
390 |> hd |
391 val (eq as Lineq(_,_,ceq,_),othereqs) = |
391 val (eq as Lineq(_,_,ceq,_),othereqs) = |
392 extract_first (fn Lineq(_,_,l,_) => c mem l) eqs |
392 extract_first (fn Lineq(_,_,l,_) => member (op =) l c) eqs |
393 val v = find_index (fn v => v = c) ceq |
393 val v = find_index (fn v => v = c) ceq |
394 val (ioth,roth) = List.partition (fn (Lineq(_,_,l,_)) => nth l v = 0) |
394 val (ioth,roth) = List.partition (fn (Lineq(_,_,l,_)) => nth l v = 0) |
395 (othereqs @ noneqs) |
395 (othereqs @ noneqs) |
396 val others = map (elim_var v eq) roth @ ioth |
396 val others = map (elim_var v eq) roth @ ioth |
397 in elim(others,(v,nontriv)::hist) end |
397 in elim(others,(v,nontriv)::hist) end |