@@ -2363,6 +2363,8 @@ impl PartialPath {
23632363}
23642364
23652365impl Node {
2366+ /// Update the given partial path pre- and postconditions with the effect of
2367+ /// appending this node to that partial path.
23662368 fn apply_to_partial_stacks (
23672369 & self ,
23682370 graph : & StackGraph ,
@@ -2462,6 +2464,144 @@ impl Node {
24622464 }
24632465 Ok ( ( ) )
24642466 }
2467+
2468+ /// Ensure the given closed precondition stacks are half-open for this end node.
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 (
2490+ & self ,
2491+ partials : & mut PartialPaths ,
2492+ symbol_stack : & mut PartialSymbolStack ,
2493+ scope_stack : & mut PartialScopeStack ,
2494+ ) {
2495+ match self {
2496+ Node :: DropScopes ( _) => {
2497+ * scope_stack = PartialScopeStack :: empty ( ) ;
2498+ }
2499+ Node :: JumpTo ( _) => { }
2500+ Node :: PopScopedSymbol ( node) => {
2501+ let symbol = symbol_stack. pop_front ( partials) . unwrap ( ) ;
2502+ debug_assert_eq ! ( symbol. symbol, node. symbol) ;
2503+ * scope_stack = symbol. scopes . into_option ( ) . unwrap ( ) ;
2504+ }
2505+ Node :: PopSymbol ( node) => {
2506+ let symbol = symbol_stack. pop_front ( partials) . unwrap ( ) ;
2507+ debug_assert_eq ! ( symbol. symbol, node. symbol) ;
2508+ }
2509+ Node :: PushScopedSymbol ( _) => { }
2510+ Node :: PushSymbol ( _) => { }
2511+ Node :: Root ( _) => { }
2512+ Node :: Scope ( _) => { }
2513+ }
2514+ }
2515+
2516+ /// Ensure the given closed postcondition stacks are half-open for this start node.
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 (
2538+ & self ,
2539+ partials : & mut PartialPaths ,
2540+ symbol_stack : & mut PartialSymbolStack ,
2541+ _scope_stack : & mut PartialScopeStack ,
2542+ ) {
2543+ match self {
2544+ Self :: DropScopes ( _) => { }
2545+ Self :: JumpTo ( _) => { }
2546+ Self :: PopScopedSymbol ( _) => { }
2547+ Self :: PopSymbol ( _) => { }
2548+ Self :: PushScopedSymbol ( node) => {
2549+ let symbol = symbol_stack. pop_front ( partials) . unwrap ( ) ;
2550+ debug_assert_eq ! ( symbol. symbol, node. symbol) ;
2551+ }
2552+ Self :: PushSymbol ( node) => {
2553+ let symbol = symbol_stack. pop_front ( partials) . unwrap ( ) ;
2554+ debug_assert_eq ! ( symbol. symbol, node. symbol) ;
2555+ }
2556+ Self :: Root ( _) => { }
2557+ Self :: Scope ( _) => { }
2558+ }
2559+ }
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+ }
24652605}
24662606
24672607impl PartialPaths {
@@ -2569,57 +2709,32 @@ impl Path {
25692709 return Err ( PathResolutionError :: IncorrectSourceNode ) ;
25702710 }
25712711
2572- // If the join node operates on the stack, the effect is present in both sides.
2573- // For correct joining, we must undo the effect on one of the sides. We match
2574- // the end node of the lhs, and the start node of the rhs separately, depending
2575- // on whether we must manipulate the lhs postcondition or rhs precondition,
2576- // respectively. The reason we cannot use only one of the lhs end or rhs start
2577- // node is that the variables used in them may differ.
2578- let mut lhs_symbol_stack = self . symbol_stack ;
2579- 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 ;
25802715 let mut rhs_symbol_stack_precondition = partial_path. symbol_stack_precondition ;
25812716 let mut rhs_scope_stack_precondition = partial_path. scope_stack_precondition ;
2582- match & graph[ self . end_node ] {
2583- Node :: DropScopes ( _) => { }
2584- Node :: JumpTo ( _) => { }
2585- Node :: PopScopedSymbol ( _) => { }
2586- Node :: PopSymbol ( _) => { }
2587- Node :: PushScopedSymbol ( _) => {
2588- lhs_symbol_stack. pop_front ( paths) . unwrap ( ) ;
2589- }
2590- Node :: PushSymbol ( _) => {
2591- lhs_symbol_stack. pop_front ( paths) . unwrap ( ) ;
2592- }
2593- Node :: Root ( _) => { }
2594- Node :: Scope ( _) => { }
2595- }
2596- match & graph[ partial_path. start_node ] {
2597- Node :: DropScopes ( _) => {
2598- rhs_scope_stack_precondition = PartialScopeStack :: empty ( ) ;
2599- }
2600- Node :: JumpTo ( _) => { }
2601- Node :: PopScopedSymbol ( _) => {
2602- let symbol = rhs_symbol_stack_precondition. pop_front ( partials) . unwrap ( ) ;
2603- rhs_scope_stack_precondition = symbol. scopes . into_option ( ) . unwrap ( ) ;
2604- }
2605- Node :: PopSymbol ( _) => {
2606- rhs_symbol_stack_precondition. pop_front ( partials) . unwrap ( ) ;
2607- }
2608- Node :: PushScopedSymbol ( _) => { }
2609- Node :: PushSymbol ( _) => { }
2610- Node :: Root ( _) => { }
2611- Node :: Scope ( _) => { }
2612- }
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+ ) ;
26132727
26142728 let mut symbol_bindings = SymbolStackBindings :: new ( ) ;
26152729 let mut scope_bindings = ScopeStackBindings :: new ( ) ;
26162730
2617- 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) ?;
26182733 rhs_symbol_stack_precondition. match_stack (
26192734 graph,
26202735 paths,
26212736 partials,
2622- lhs_symbol_stack ,
2737+ lhs_symbol_stack_postcondition ,
26232738 & mut symbol_bindings,
26242739 & mut scope_bindings,
26252740 ) ?;
@@ -2673,47 +2788,21 @@ impl PartialPath {
26732788 return Err ( PathResolutionError :: IncorrectSourceNode ) ;
26742789 }
26752790
2676- // If the join node operates on the stack, the effect is present in both sides.
2677- // For correct joining, we must undo the effect on one of the sides. We match
2678- // the end node of the lhs, and the start node of the rhs separately, depending
2679- // on whether we must manipulate the lhs postcondition or rhs precondition,
2680- // respectively. The reason we cannot use only one of the lhs end or rhs start
2681- // 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.
26822792 let mut lhs_symbol_stack_postcondition = lhs. symbol_stack_postcondition ;
2683- let lhs_scope_stack_postcondition = lhs. scope_stack_postcondition ;
2793+ let mut lhs_scope_stack_postcondition = lhs. scope_stack_postcondition ;
26842794 let mut rhs_symbol_stack_precondition = rhs. symbol_stack_precondition ;
26852795 let mut rhs_scope_stack_precondition = rhs. scope_stack_precondition ;
2686- match & graph[ lhs. end_node ] {
2687- Node :: DropScopes ( _) => { }
2688- Node :: JumpTo ( _) => { }
2689- Node :: PopScopedSymbol ( _) => { }
2690- Node :: PopSymbol ( _) => { }
2691- Node :: PushScopedSymbol ( _) => {
2692- lhs_symbol_stack_postcondition. pop_front ( partials) . unwrap ( ) ;
2693- }
2694- Node :: PushSymbol ( _) => {
2695- lhs_symbol_stack_postcondition. pop_front ( partials) . unwrap ( ) ;
2696- }
2697- Node :: Root ( _) => { }
2698- Node :: Scope ( _) => { }
2699- }
2700- match & graph[ rhs. start_node ] {
2701- Node :: DropScopes ( _) => {
2702- rhs_scope_stack_precondition = PartialScopeStack :: empty ( ) ;
2703- }
2704- Node :: JumpTo ( _) => { }
2705- Node :: PopScopedSymbol ( _) => {
2706- let symbol = rhs_symbol_stack_precondition. pop_front ( partials) . unwrap ( ) ;
2707- rhs_scope_stack_precondition = symbol. scopes . into_option ( ) . unwrap ( ) ;
2708- }
2709- Node :: PopSymbol ( _) => {
2710- rhs_symbol_stack_precondition. pop_front ( partials) . unwrap ( ) ;
2711- }
2712- Node :: PushScopedSymbol ( _) => { }
2713- Node :: PushSymbol ( _) => { }
2714- Node :: Root ( _) => { }
2715- Node :: Scope ( _) => { }
2716- }
2796+ graph[ lhs. end_node ] . halfopen_closed_partial_postcondition (
2797+ partials,
2798+ & mut lhs_symbol_stack_postcondition,
2799+ & mut lhs_scope_stack_postcondition,
2800+ ) ;
2801+ graph[ rhs. start_node ] . halfopen_closed_partial_precondition (
2802+ partials,
2803+ & mut rhs_symbol_stack_precondition,
2804+ & mut rhs_scope_stack_precondition,
2805+ ) ;
27172806
27182807 let mut symbol_bindings = PartialSymbolStackBindings :: new ( ) ;
27192808 let mut scope_bindings = PartialScopeStackBindings :: new ( ) ;
0 commit comments