diff options
| author | Pierre-Marie Pédrot | 2015-06-30 15:43:14 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-07-01 16:50:17 +0200 |
| commit | dab5c4c642ee9b25d488c476d55db232cf74006b (patch) | |
| tree | 134e2cf992130de5e376306393d5e12d1528a7d1 /kernel | |
| parent | 0917ce7cf48cadacc6fca48ba18b395740cccbe2 (diff) | |
Further simplification of the graph traversal in Univ.
We passed the arc to be marked as visited to the functions pushing the
neighbours on the remaining stack, but this can be actually done before
pushing them, as the [process_le] and [process_lt] functions do not rely
on the visited flag. This exposes more clearly the invariants of the
algorithm.
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/univ.ml | 25 |
1 files changed, 12 insertions, 13 deletions
diff --git a/kernel/univ.ml b/kernel/univ.ml index fce9e28d36..1d82be63b9 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -925,7 +925,8 @@ let fast_compare_neq strict g arcu arcv = if arc_is_lt arc then cmp c to_revert lt_todo le_todo else - process_lt c to_revert lt_todo le_todo arc arc.lt arc.le + let () = arc.status <- SetLt in + process_lt c (arc :: to_revert) lt_todo le_todo arc.lt arc.le | [], arc::le_todo -> if arc == arcv then (* No need to continue inspecting universes above arc: @@ -937,40 +938,38 @@ let fast_compare_neq strict g arcu arcv = if arc_is_le arc then cmp c to_revert [] le_todo else - process_le c to_revert [] le_todo arc arc.lt + let () = arc.status <- SetLe in + process_le c (arc :: to_revert) [] le_todo arc.lt arc.le - and process_lt c to_revert lt_todo le_todo arc0 lt le = match le with + and process_lt c to_revert lt_todo le_todo lt le = match le with | [] -> begin match lt with - | [] -> - let () = arc0.status <- SetLt in - cmp c (arc0 :: to_revert) lt_todo le_todo + | [] -> cmp c to_revert lt_todo le_todo | u :: lt -> let arc = repr g u in if arc == arcv then if strict then (to_revert, FastLT) else (to_revert, FastLE) - else process_lt c to_revert (arc :: lt_todo) le_todo arc0 lt le + else process_lt c to_revert (arc :: lt_todo) le_todo lt le end | u :: le -> let arc = repr g u in if arc == arcv then if strict then (to_revert, FastLT) else (to_revert, FastLE) - else process_lt c to_revert (arc :: lt_todo) le_todo arc0 lt le + else process_lt c to_revert (arc :: lt_todo) le_todo lt le - and process_le c to_revert lt_todo le_todo arc0 lt = match lt with + and process_le c to_revert lt_todo le_todo lt le = match lt with | [] -> let fold accu u = let node = repr g u in node :: accu in - let le_new = List.fold_left fold le_todo arc0.le in - let () = arc0.status <- SetLe in - cmp c (arc0 :: to_revert) lt_todo le_new + let le_new = List.fold_left fold le_todo le in + cmp c to_revert lt_todo le_new | u :: lt -> let arc = repr g u in if arc == arcv then if strict then (to_revert, FastLT) else (to_revert, FastLE) - else process_le c to_revert (arc :: lt_todo) le_todo arc0 lt + else process_le c to_revert (arc :: lt_todo) le_todo lt le in |