Changes between Version 57 and Version 58 of TypeFunctionsSolving


Ignore:
Timestamp:
Aug 17, 2008 10:46:15 AM (7 years ago)
Author:
chak
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • TypeFunctionsSolving

    v57 v58  
    134134== Propagation (aka Solving) == 
    135135 
    136 A significant difference to new-single is that solving is a purely local operation.  We never instantiate any flexible variables. 
     136A significant difference to `new-single` is that solving is a purely local operation.  We never instantiate any flexible variables. 
     137 
     138=== Rules === 
     139 
     140 '''Top''':: 
     141{{{ 
     142co :: F t1..tn ~ t 
     143=(Top)=> 
     144co' :: [s1/x1, .., sm/xm]s ~ t with co = g s1..sm |> co'   
     145}}} 
     146 where `g :: forall x1..xm. F u1..um ~ s` and `[s1/x1, .., sm/xm]u1 == t1`. 
     147 
     148 '''!SubstFam''':: 
     149{{{ 
     150co1 :: F t1..tn ~ t  &  co2 :: F t1..tn ~ s 
     151=(SubstFam)=> 
     152co1 :: F t1..tn ~ t  &  co2' :: t ~ s with co2 = co1 |> co2' 
     153}}} 
     154 where `co1` is local, or both `co1` and `co2` are wanted and at least one of the equalities contains a flexible variable. 
     155 
     156 '''!SubstVarVar''':: 
     157{{{ 
     158co1 :: x ~ t  &  co2 :: x ~ s 
     159=(SubstVar)=> 
     160co1 :: x ~ t  &  co2' :: t ~ s with co2 = co1 |> co2' 
     161}}} 
     162 where `co1` is local, or both `co1` and `co2` are wanted and at least one of the equalities contains a flexible variable. 
     163 
     164 '''!SubstVarFam''':: 
     165{{{ 
     166}}} 
    137167 
    138168'''TODO:'''