Changes between Version 95 and Version 96 of TypeFunctionsSolving


Ignore:
Timestamp:
Sep 29, 2008 1:36:30 PM (6 years ago)
Author:
chak
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • TypeFunctionsSolving

    v95 v96  
    201201=== Rule application: algorithm === 
    202202 
    203 The following function gets a list with all local and wanted equalities.  It returns a list of residual equalities that permit no further rule application. 
     203The four propagation rules are implemented by the following four functions: 
    204204{{{ 
    205205-- all four rule functions return Nothing if rule not applicable 
    206206applyTop         :: RewriteInst -> Maybe EqInst 
    207 applySubstFam    :: RewriteInst -> RewriteInst -> Maybe EqInst    -- return only... 
    208 applySubstVarVar :: RewriteInst -> RewriteInst -> Maybe EqInst    -- ...the modified... 
    209 applySubstVarFam :: RewriteInst -> RewriteInst -> Maybe EqInst    -- ...equality 
    210  
     207applySubstFam    :: RewriteInst -> RewriteInst -> Maybe EqInst    -- return second argument... 
     208applySubstVarVar :: RewriteInst -> RewriteInst -> Maybe EqInst    -- ...if it needs to go into... 
     209applySubstVarFam :: RewriteInst -> RewriteInst -> Maybe EqInst    -- ...the todo list 
     210}}} 
     211For `applySubstFam`, `applySubstVarVar`, and `applySubstVarFam`, if the rule is not applicable to the arguments in the given order, ''but it is applicable in the opposite order,'' return the second argument as if it had been modified.  (As a result, it will get onto the todo list, and the equalities eventually be used in the opposite order.) 
     212 
     213The following function gets a list with all local and wanted equalities.  It returns a list of residual equalities that permit no further rule application. 
     214{{{ 
    211215propagate :: [RewriteInst] -> [RewriteInst] 
    212216propagate eqs = prop eqs [] 
     
    228232 
    229233  applySubstRules eq1 eq2 
    230     | Just eq2' <- applySubstFam eq1 eq2    = (norm eq2', []) 
    231     | Just eq2' <- applySubstVarVar e1 eq2  = (norm eq2', []) 
    232     | Just eq2' <- applySubstVarFam eq1 eq2 = ([eq2'], []) 
    233     | otherwise                             = ([], [eq2]) 
     234    | Just eq2' <- applySubstFam eq1 eq2    = (norm eq2', [eq1]) 
     235    | Just eq2' <- applySubstVarVar e1 eq2  = (norm eq2', [eq1]) 
     236    | Just eq2' <- applySubstVarFam eq1 eq2 = ([eq2'], [eq1]) 
     237    | otherwise                             = ([], [eq1, eq2]) 
    234238}}} 
    235239