fact: Definition step (e : event) (st : scan_state) : scan_state := let p := point e in let '(Bscan op1 lsto op2 cls cl lhigh lx) := st in if negb (same_x p lx) then let '(first_cells, contact_cells, last_contact, last_cells, lower_edge, higher_edge) := open_cells_decomposition (op1 ++ lsto :: op2) p in let closed := closing_cells p contact_cells in let last_closed := close_cell p last_contact in let closed_cells := cls ++ cl :: closed in let (new_open_cells, newlastopen) := opening_cells_aux p (sort edge_below (outgoing e)) lower_edge higher_edge in Bscan (first_cells ++ new_open_cells) newlastopen last_cells closed_cells last_closed higher_edge (p_x (point e)) else if p >>> lhigh then let '(fc', contact_cells, last_contact, last_cells, low_edge, higher_edge) := open_cells_decomposition op2 p in let first_cells := op1 ++ lsto :: fc' in let closed := closing_cells p contact_cells in let last_closed := close_cell p last_contact in let closed_cells := cls++ cl :: closed in let (new_open_cells, newlastopen) := opening_cells_aux p (sort edge_below (outgoing e)) low_edge higher_edge in Bscan (first_cells ++ new_open_cells) newlastopen last_cells closed_cells last_closed higher_edge (p_x (point e)) else if p <<< lhigh then let new_closed := update_closed_cell cl (point e) in let (new_opens, new_lopen) := update_open_cell lsto e in Bscan (op1 ++ new_opens) new_lopen op2 cls new_closed lhigh lx else let '(fc', contact_cells, last_contact, last_cells, lower_edge, higher_edge) := open_cells_decomposition (lsto :: op2) p in let closed := closing_cells p (behead contact_cells) in let last_closed := close_cell p last_contact in let (new_opens, new_lopen) := update_open_cell_top lsto higher_edge e in Bscan (op1 ++ fc' ++ new_opens) new_lopen last_cells (closed ++ cl :: cls) last_closed higher_edge lx.
imports: mathcomp(all_ssreflect) ZArith QArith List String OrderedType OrderedTypeEx FMapAVL