@@ -2466,7 +2466,27 @@ impl Node {
24662466 }
24672467
24682468 /// Ensure the given closed precondition stacks are half-open for this end node.
2469- fn halfopen_closed_precondition (
2469+ ///
2470+ /// Partial paths have closed (cf. a closed interval) pre- and postconditions, which means
2471+ /// the start node is reflected in the precondition, and the end node is reflected in the
2472+ /// postcondition. For example, a path starting with a pop node, has a precondition starting
2473+ /// with the popped symbol. Similarly, a ending with a push node, has a postcondition ending
2474+ /// with the pushed symbol.
2475+ ///
2476+ /// When concatenating two partial paths, their closed pre- and postconditions are not compatible,
2477+ /// because the effect of the join node (i.e., the node shared between the two paths) is present
2478+ /// in both the right and the left path. If two paths join at a push node, the right postcondition
2479+ /// contains the pushed symbol, while the left precondition does not contain it, behaving as if the
2480+ /// symbol was pushed twice. Similarly, when joining at a pop node, the right precondition contains
2481+ /// the popped symbol, while the right postcondition will not anymore, because it was already popped.
2482+ /// Unifying closed pre- and postconditions can result in incorrect concatenation results.
2483+ ///
2484+ /// We can make pre- and postconditions compatible again by making them half-open (cf. open intervals,
2485+ /// but half because we only undo the effect of some node types). A precondition is half-open if it
2486+ /// does not reflect the effect if a start pop node, Similarly, a postcondition is half-open if it
2487+ /// does not reflect the effect of an end push node. Unifying half-open pre- and postconditions results
2488+ /// in the correct behavior for path concatenation.
2489+ fn halfopen_closed_partial_precondition (
24702490 & self ,
24712491 partials : & mut PartialPaths ,
24722492 symbol_stack : & mut PartialSymbolStack ,
@@ -2494,7 +2514,27 @@ impl Node {
24942514 }
24952515
24962516 /// Ensure the given closed postcondition stacks are half-open for this start node.
2497- fn halfopen_closed_postcondition (
2517+ ///
2518+ /// Partial paths have closed (cf. a closed interval) pre- and postconditions, which means
2519+ /// the start node is reflected in the precondition, and the end node is reflected in the
2520+ /// postcondition. For example, a path starting with a pop node, has a precondition starting
2521+ /// with the popped symbol. Similarly, a ending with a push node, has a postcondition ending
2522+ /// with the pushed symbol.
2523+ ///
2524+ /// When concatenating two partial paths, their closed pre- and postconditions are not compatible,
2525+ /// because the effect of the join node (i.e., the node shared between the two paths) is present
2526+ /// in both the right and the left path. If two paths join at a push node, the right postcondition
2527+ /// contains the pushed symbol, while the left precondition does not contain it, behaving as if the
2528+ /// symbol was pushed twice. Similarly, when joining at a pop node, the right precondition contains
2529+ /// the popped symbol, while the right postcondition will not anymore, because it was already popped.
2530+ /// Unifying closed pre- and postconditions can result in incorrect concatenation results.
2531+ ///
2532+ /// We can make pre- and postconditions compatible again by making them half-open (cf. open intervals,
2533+ /// but half because we only undo the effect of some node types). A precondition is half-open if it
2534+ /// does not reflect the effect if a start pop node, Similarly, a postcondition is half-open if it
2535+ /// does not reflect the effect of an end push node. Unifying half-open pre- and postconditions results
2536+ /// in the correct behavior for path concatenation.
2537+ fn halfopen_closed_partial_postcondition (
24982538 & self ,
24992539 partials : & mut PartialPaths ,
25002540 symbol_stack : & mut PartialSymbolStack ,
@@ -2517,6 +2557,51 @@ impl Node {
25172557 Self :: Scope ( _) => { }
25182558 }
25192559 }
2560+
2561+ /// Ensure the given closed postcondition stacks are half-open for this start node.
2562+ ///
2563+ /// Partial paths have closed (cf. a closed interval) pre- and postconditions, which means
2564+ /// the start node is reflected in the precondition, and the end node is reflected in the
2565+ /// postcondition. For example, a path starting with a pop node, has a precondition starting
2566+ /// with the popped symbol. Similarly, a ending with a push node, has a postcondition ending
2567+ /// with the pushed symbol.
2568+ ///
2569+ /// When concatenating two partial paths, their closed pre- and postconditions are not compatible,
2570+ /// because the effect of the join node (i.e., the node shared between the two paths) is present
2571+ /// in both the right and the left path. If two paths join at a push node, the right postcondition
2572+ /// contains the pushed symbol, while the left precondition does not contain it, behaving as if the
2573+ /// symbol was pushed twice. Similarly, when joining at a pop node, the right precondition contains
2574+ /// the popped symbol, while the right postcondition will not anymore, because it was already popped.
2575+ /// Unifying closed pre- and postconditions can result in incorrect concatenation results.
2576+ ///
2577+ /// We can make pre- and postconditions compatible again by making them half-open (cf. open intervals,
2578+ /// but half because we only undo the effect of some node types). A precondition is half-open if it
2579+ /// does not reflect the effect if a start pop node, Similarly, a postcondition is half-open if it
2580+ /// does not reflect the effect of an end push node. Unifying half-open pre- and postconditions results
2581+ /// in the correct behavior for path concatenation.
2582+ fn halfopen_closed_postcondition (
2583+ & self ,
2584+ paths : & mut Paths ,
2585+ symbol_stack : & mut SymbolStack ,
2586+ _scope_stack : & mut ScopeStack ,
2587+ ) {
2588+ match self {
2589+ Self :: DropScopes ( _) => { }
2590+ Self :: JumpTo ( _) => { }
2591+ Self :: PopScopedSymbol ( _) => { }
2592+ Self :: PopSymbol ( _) => { }
2593+ Self :: PushScopedSymbol ( node) => {
2594+ let symbol = symbol_stack. pop_front ( paths) . unwrap ( ) ;
2595+ debug_assert_eq ! ( symbol. symbol, node. symbol) ;
2596+ }
2597+ Self :: PushSymbol ( node) => {
2598+ let symbol = symbol_stack. pop_front ( paths) . unwrap ( ) ;
2599+ debug_assert_eq ! ( symbol. symbol, node. symbol) ;
2600+ }
2601+ Self :: Root ( _) => { }
2602+ Self :: Scope ( _) => { }
2603+ }
2604+ }
25202605}
25212606
25222607impl PartialPaths {
@@ -2624,57 +2709,32 @@ impl Path {
26242709 return Err ( PathResolutionError :: IncorrectSourceNode ) ;
26252710 }
26262711
2627- // If the join node operates on the stack, the effect is present in both sides.
2628- // For correct joining, we must undo the effect on one of the sides. We match
2629- // the end node of the lhs, and the start node of the rhs separately, depending
2630- // on whether we must manipulate the lhs postcondition or rhs precondition,
2631- // respectively. The reason we cannot use only one of the lhs end or rhs start
2632- // node is that the variables used in them may differ.
2633- let mut lhs_symbol_stack = self . symbol_stack ;
2634- let lhs_scope_stack = self . scope_stack ;
2712+ // Ensure the right post- and left precondition are half-open, so we can unify them.
2713+ let mut lhs_symbol_stack_postcondition = self . symbol_stack ;
2714+ let mut lhs_scope_stack_postcondition = self . scope_stack ;
26352715 let mut rhs_symbol_stack_precondition = partial_path. symbol_stack_precondition ;
26362716 let mut rhs_scope_stack_precondition = partial_path. scope_stack_precondition ;
2637- match & graph[ self . end_node ] {
2638- Node :: DropScopes ( _) => { }
2639- Node :: JumpTo ( _) => { }
2640- Node :: PopScopedSymbol ( _) => { }
2641- Node :: PopSymbol ( _) => { }
2642- Node :: PushScopedSymbol ( _) => {
2643- lhs_symbol_stack. pop_front ( paths) . unwrap ( ) ;
2644- }
2645- Node :: PushSymbol ( _) => {
2646- lhs_symbol_stack. pop_front ( paths) . unwrap ( ) ;
2647- }
2648- Node :: Root ( _) => { }
2649- Node :: Scope ( _) => { }
2650- }
2651- match & graph[ partial_path. start_node ] {
2652- Node :: DropScopes ( _) => {
2653- rhs_scope_stack_precondition = PartialScopeStack :: empty ( ) ;
2654- }
2655- Node :: JumpTo ( _) => { }
2656- Node :: PopScopedSymbol ( _) => {
2657- let symbol = rhs_symbol_stack_precondition. pop_front ( partials) . unwrap ( ) ;
2658- rhs_scope_stack_precondition = symbol. scopes . into_option ( ) . unwrap ( ) ;
2659- }
2660- Node :: PopSymbol ( _) => {
2661- rhs_symbol_stack_precondition. pop_front ( partials) . unwrap ( ) ;
2662- }
2663- Node :: PushScopedSymbol ( _) => { }
2664- Node :: PushSymbol ( _) => { }
2665- Node :: Root ( _) => { }
2666- Node :: Scope ( _) => { }
2667- }
2717+ graph[ self . end_node ] . halfopen_closed_postcondition (
2718+ paths,
2719+ & mut lhs_symbol_stack_postcondition,
2720+ & mut lhs_scope_stack_postcondition,
2721+ ) ;
2722+ graph[ partial_path. start_node ] . halfopen_closed_partial_precondition (
2723+ partials,
2724+ & mut rhs_symbol_stack_precondition,
2725+ & mut rhs_scope_stack_precondition,
2726+ ) ;
26682727
26692728 let mut symbol_bindings = SymbolStackBindings :: new ( ) ;
26702729 let mut scope_bindings = ScopeStackBindings :: new ( ) ;
26712730
2672- rhs_scope_stack_precondition. match_stack ( lhs_scope_stack, & mut scope_bindings) ?;
2731+ rhs_scope_stack_precondition
2732+ . match_stack ( lhs_scope_stack_postcondition, & mut scope_bindings) ?;
26732733 rhs_symbol_stack_precondition. match_stack (
26742734 graph,
26752735 paths,
26762736 partials,
2677- lhs_symbol_stack ,
2737+ lhs_symbol_stack_postcondition ,
26782738 & mut symbol_bindings,
26792739 & mut scope_bindings,
26802740 ) ?;
@@ -2728,22 +2788,17 @@ impl PartialPath {
27282788 return Err ( PathResolutionError :: IncorrectSourceNode ) ;
27292789 }
27302790
2731- // If the join node operates on the stack, the effect is present in both sides.
2732- // For correct joining, we must undo the effect on one of the sides. We match
2733- // the end node of the lhs, and the start node of the rhs separately, depending
2734- // on whether we must manipulate the lhs postcondition or rhs precondition,
2735- // respectively. The reason we cannot use only one of the lhs end or rhs start
2736- // node is that the variables used in them may differ.
2791+ // Ensure the right post- and left precondition are half-open, so we can unify them.
27372792 let mut lhs_symbol_stack_postcondition = lhs. symbol_stack_postcondition ;
27382793 let mut lhs_scope_stack_postcondition = lhs. scope_stack_postcondition ;
27392794 let mut rhs_symbol_stack_precondition = rhs. symbol_stack_precondition ;
27402795 let mut rhs_scope_stack_precondition = rhs. scope_stack_precondition ;
2741- graph[ lhs. end_node ] . halfopen_closed_postcondition (
2796+ graph[ lhs. end_node ] . halfopen_closed_partial_postcondition (
27422797 partials,
27432798 & mut lhs_symbol_stack_postcondition,
27442799 & mut lhs_scope_stack_postcondition,
27452800 ) ;
2746- graph[ rhs. start_node ] . halfopen_closed_precondition (
2801+ graph[ rhs. start_node ] . halfopen_closed_partial_precondition (
27472802 partials,
27482803 & mut rhs_symbol_stack_precondition,
27492804 & mut rhs_scope_stack_precondition,
0 commit comments