@@ -2068,8 +2068,8 @@ impl PartialPath {
20682068 graph[ self . end_node ] . is_jump_to ( )
20692069 }
20702070
2071- /// Returns whether a partial path is "productive" --- that is, it is not cyclic, or it consumes
2072- /// symbols from the stack, possible replacing them by different symbols .
2071+ /// Returns whether a partial path is "productive" --- that is, it is not cyclic, or its
2072+ /// pre- and postcondition are incompatible .
20732073 pub fn is_productive ( & self , graph : & StackGraph , partials : & mut PartialPaths ) -> bool {
20742074 // StackGraph ensures that there are no nodes with duplicate IDs, so we can do a simple
20752075 // comparison of node handles here.
@@ -2081,54 +2081,16 @@ impl PartialPath {
20812081 let mut rhs = self . clone ( ) ;
20822082 rhs. ensure_no_overlapping_variables ( partials, lhs) ;
20832083
2084- // If the join node operates on the stack, the effect is present in both sides.
2085- // For correct joining, we must undo the effect on one of the sides. We match
2086- // the end node of the lhs, and the start node of the rhs separately, depending
2087- // on whether we must manipulate the lhs postcondition or rhs precondition,
2088- // respectively. The reason we cannot use only one of the lhs end or rhs start
2089- // node is that the variables used in them may differ.
2090- let mut lhs_symbol_stack_postcondition = lhs. symbol_stack_postcondition ;
2091- let mut lhs_scope_stack_postcondition = lhs. scope_stack_postcondition ;
2092- let mut rhs_symbol_stack_precondition = rhs. symbol_stack_precondition ;
2093- let mut rhs_scope_stack_precondition = rhs. scope_stack_precondition ;
2094- graph[ lhs. end_node ] . halfopen_closed_postcondition (
2095- partials,
2096- & mut lhs_symbol_stack_postcondition,
2097- & mut lhs_scope_stack_postcondition,
2098- ) ;
2099- graph[ rhs. start_node ] . halfopen_closed_precondition (
2100- partials,
2101- & mut rhs_symbol_stack_precondition,
2102- & mut rhs_scope_stack_precondition,
2103- ) ;
2104-
2105- let mut symbol_bindings = PartialSymbolStackBindings :: new ( ) ;
2106- let mut scope_bindings = PartialScopeStackBindings :: new ( ) ;
2107- if lhs_symbol_stack_postcondition
2108- . unify (
2109- partials,
2110- rhs_symbol_stack_precondition,
2111- & mut symbol_bindings,
2112- & mut scope_bindings,
2113- )
2114- . is_err ( )
2115- {
2116- // symbol stacks are incompatible
2117- return true ;
2118- }
2119- if lhs_scope_stack_postcondition
2120- . unify ( partials, rhs_scope_stack_precondition, & mut scope_bindings)
2121- . is_err ( )
2122- {
2123- // scope stacks are incompatible
2124- return true ;
2125- }
2084+ let join = match Self :: compute_join ( graph, partials, lhs, & rhs) {
2085+ Ok ( join) => join,
2086+ Err ( _) => return true ,
2087+ } ;
21262088
21272089 if lhs
21282090 . symbol_stack_precondition
21292091 . variable
21302092 . into_option ( )
2131- . map_or ( false , |v| symbol_bindings. get ( v) . iter ( ) . len ( ) > 0 )
2093+ . map_or ( false , |v| join . symbol_bindings . get ( v) . iter ( ) . len ( ) > 0 )
21322094 {
21332095 // symbol stack precondition strengthened
21342096 return true ;
@@ -2138,7 +2100,7 @@ impl PartialPath {
21382100 . scope_stack_precondition
21392101 . variable
21402102 . into_option ( )
2141- . map_or ( false , |v| scope_bindings. get ( v) . iter ( ) . len ( ) > 0 )
2103+ . map_or ( false , |v| join . scope_bindings . get ( v) . iter ( ) . len ( ) > 0 )
21422104 {
21432105 // scope stack precondition strengthened
21442106 return true ;
@@ -2850,46 +2812,20 @@ impl PartialPath {
28502812 ) -> Result < ( ) , PathResolutionError > {
28512813 let lhs = self ;
28522814
2853- if lhs. end_node != rhs. start_node {
2854- return Err ( PathResolutionError :: IncorrectSourceNode ) ;
2855- }
2856-
2857- // Ensure the right post- and left precondition are half-open, so we can unify them.
2858- let mut lhs_symbol_stack_postcondition = lhs. symbol_stack_postcondition ;
2859- let mut lhs_scope_stack_postcondition = lhs. scope_stack_postcondition ;
2860- let mut rhs_symbol_stack_precondition = rhs. symbol_stack_precondition ;
2861- let mut rhs_scope_stack_precondition = rhs. scope_stack_precondition ;
2862- graph[ lhs. end_node ] . halfopen_closed_partial_postcondition (
2863- partials,
2864- & mut lhs_symbol_stack_postcondition,
2865- & mut lhs_scope_stack_postcondition,
2866- ) ;
2867- graph[ rhs. start_node ] . halfopen_closed_partial_precondition (
2868- partials,
2869- & mut rhs_symbol_stack_precondition,
2870- & mut rhs_scope_stack_precondition,
2871- ) ;
2872-
2873- let mut symbol_bindings = PartialSymbolStackBindings :: new ( ) ;
2874- let mut scope_bindings = PartialScopeStackBindings :: new ( ) ;
2875-
2876- let unified_scope_stack = lhs_scope_stack_postcondition. unify (
2877- partials,
2878- rhs_scope_stack_precondition,
2879- & mut scope_bindings,
2880- ) ?;
2881- let unified_symbol_stack = lhs_symbol_stack_postcondition. unify (
2882- partials,
2883- rhs_symbol_stack_precondition,
2884- & mut symbol_bindings,
2885- & mut scope_bindings,
2886- ) ?;
2815+ #[ cfg_attr( not( feature = "copious-debugging" ) , allow( unused_mut) ) ]
2816+ let mut join = Self :: compute_join ( graph, partials, lhs, rhs) ?;
28872817 #[ cfg( feature = "copious-debugging" ) ]
28882818 {
2889- let unified_symbol_stack = unified_symbol_stack. display ( graph, partials) . to_string ( ) ;
2890- let unified_scope_stack = unified_scope_stack. display ( graph, partials) . to_string ( ) ;
2891- let symbol_bindings = symbol_bindings. display ( graph, partials) . to_string ( ) ;
2892- let scope_bindings = scope_bindings. display ( graph, partials) . to_string ( ) ;
2819+ let unified_symbol_stack = join
2820+ . unified_symbol_stack
2821+ . display ( graph, partials)
2822+ . to_string ( ) ;
2823+ let unified_scope_stack = join
2824+ . unified_scope_stack
2825+ . display ( graph, partials)
2826+ . to_string ( ) ;
2827+ let symbol_bindings = join. symbol_bindings . display ( graph, partials) . to_string ( ) ;
2828+ let scope_bindings = join. scope_bindings . display ( graph, partials) . to_string ( ) ;
28932829 copious_debugging ! (
28942830 " via <{}> ({}) {} {}" ,
28952831 unified_symbol_stack,
@@ -2901,21 +2837,21 @@ impl PartialPath {
29012837
29022838 lhs. symbol_stack_precondition = lhs. symbol_stack_precondition . apply_partial_bindings (
29032839 partials,
2904- & symbol_bindings,
2905- & scope_bindings,
2840+ & join . symbol_bindings ,
2841+ & join . scope_bindings ,
29062842 ) ?;
29072843 lhs. symbol_stack_postcondition = rhs. symbol_stack_postcondition . apply_partial_bindings (
29082844 partials,
2909- & symbol_bindings,
2910- & scope_bindings,
2845+ & join . symbol_bindings ,
2846+ & join . scope_bindings ,
29112847 ) ?;
29122848
29132849 lhs. scope_stack_precondition = lhs
29142850 . scope_stack_precondition
2915- . apply_partial_bindings ( partials, & scope_bindings) ?;
2851+ . apply_partial_bindings ( partials, & join . scope_bindings ) ?;
29162852 lhs. scope_stack_postcondition = rhs
29172853 . scope_stack_postcondition
2918- . apply_partial_bindings ( partials, & scope_bindings) ?;
2854+ . apply_partial_bindings ( partials, & join . scope_bindings ) ?;
29192855
29202856 let mut edges = rhs. edges ;
29212857 while let Some ( edge) = edges. pop_front ( partials) {
@@ -2927,6 +2863,65 @@ impl PartialPath {
29272863
29282864 Ok ( ( ) )
29292865 }
2866+
2867+ /// Compute the bindings to join to partial paths. It is the caller's responsibility
2868+ /// to ensure non-overlapping variables, if that is required.
2869+ fn compute_join (
2870+ graph : & StackGraph ,
2871+ partials : & mut PartialPaths ,
2872+ lhs : & PartialPath ,
2873+ rhs : & PartialPath ,
2874+ ) -> Result < Join , PathResolutionError > {
2875+ if lhs. end_node != rhs. start_node {
2876+ return Err ( PathResolutionError :: IncorrectSourceNode ) ;
2877+ }
2878+
2879+ // Ensure the right post- and left precondition are half-open, so we can unify them.
2880+ let mut lhs_symbol_stack_postcondition = lhs. symbol_stack_postcondition ;
2881+ let mut lhs_scope_stack_postcondition = lhs. scope_stack_postcondition ;
2882+ let mut rhs_symbol_stack_precondition = rhs. symbol_stack_precondition ;
2883+ let mut rhs_scope_stack_precondition = rhs. scope_stack_precondition ;
2884+ graph[ lhs. end_node ] . halfopen_closed_partial_postcondition (
2885+ partials,
2886+ & mut lhs_symbol_stack_postcondition,
2887+ & mut lhs_scope_stack_postcondition,
2888+ ) ;
2889+ graph[ rhs. start_node ] . halfopen_closed_partial_precondition (
2890+ partials,
2891+ & mut rhs_symbol_stack_precondition,
2892+ & mut rhs_scope_stack_precondition,
2893+ ) ;
2894+
2895+ let mut symbol_bindings = PartialSymbolStackBindings :: new ( ) ;
2896+ let mut scope_bindings = PartialScopeStackBindings :: new ( ) ;
2897+ let unified_symbol_stack = lhs_symbol_stack_postcondition. unify (
2898+ partials,
2899+ rhs_symbol_stack_precondition,
2900+ & mut symbol_bindings,
2901+ & mut scope_bindings,
2902+ ) ?;
2903+ let unified_scope_stack = lhs_scope_stack_postcondition. unify (
2904+ partials,
2905+ rhs_scope_stack_precondition,
2906+ & mut scope_bindings,
2907+ ) ?;
2908+
2909+ Ok ( Join {
2910+ unified_symbol_stack,
2911+ unified_scope_stack,
2912+ symbol_bindings,
2913+ scope_bindings,
2914+ } )
2915+ }
2916+ }
2917+
2918+ struct Join {
2919+ #[ cfg_attr( not( feature = "copious-debugging" ) , allow( dead_code) ) ]
2920+ pub unified_symbol_stack : PartialSymbolStack ,
2921+ #[ cfg_attr( not( feature = "copious-debugging" ) , allow( dead_code) ) ]
2922+ pub unified_scope_stack : PartialScopeStack ,
2923+ pub symbol_bindings : PartialSymbolStackBindings ,
2924+ pub scope_bindings : PartialScopeStackBindings ,
29302925}
29312926
29322927//-------------------------------------------------------------------------------------------------
0 commit comments