Changes between Version 79 and Version 80 of TypeFunctionsSolving


Ignore:
Timestamp:
Sep 5, 2008 11:07:42 AM (6 years ago)
Author:
chak
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • TypeFunctionsSolving

    v79 v80  
    8080data RewriteInst    -- normal equality 
    8181 
    82 -- !!!TODO: Adapt to new flattening!!! 
    8382norm :: EqInst -> [RewriteInst] 
    84 norm [[co :: F s1..sn ~ t]] = adjust [[co :: F s1'..sn' ~ t']] (F c1..cn |> sym c) (eqs1++..++eqsn++eqt) 
     83norm [[co :: F s1..sn ~ t]] = [[co' :: F s1'..sn' ~ t']] : eqs 
    8584  where 
    8685    (s1', c1, eqs1) = flatten s1 
    8786    .. 
    8887    (sn', cn, eqsn) = flatten sn 
    89     (t', c, eqt)   = flatten t 
     88    (t', c, eqt)    = flatten t 
     89    (co', eqs)      = adjust co (F c1..cn |> sym c) (eqs1++..++eqsn++eqt) 
    9090norm [[co :: t ~ F s1..sn]] = norm [[co' :: F s1..sn ~ t]] with co = sym co' 
    91 norm [[co :: s ~ t]] = adjust (check [[co :: s' ~ t']]) (cs |> sym ct) (eqs ++ eqt) 
     91norm [[co :: s ~ t]] = check [[co' :: s' ~ t']] ++ eqs 
    9292  where 
    9393    (s', cs, eqs) = flatten s 
    9494    (t', ct, eqt) = flatten t 
     95    (co', eqs)    = adjust co (cs |> sym ct) (eqs ++ eqt) 
    9596 
    9697check :: FlatEqInst -> [RewriteInst] 
     
    112113flatten :: Type -> (Type, Coercion, [RewriteInst]) 
    113114-- Result type has no synonym families whatsoever 
    114 flatten [[F t1..tn]] = (alpha, [[F c1..cn |> gamma]], [[gamma :: F t1'..tn' ~ alpha]] : eqt1++..++eqtn) 
     115flatten [[F t1..tn] 
     116  = (alpha, [[F c1..cn |> gamma]], [[gamma :: F t1'..tn' ~ alpha]] : eqt1++..++eqtn) 
    115117  where 
    116118    (t1', c1, eqt1) = flatten t1 
     
    124126flatten t = (t, t, []) 
    125127 
    126 adjust :: [RewriteInst] -> Coercion -> [RewriteInst] -> [RewriteInst] 
     128adjust :: EqInstCo -> Coercion -> [RewriteInst] -> (EqInstCo, [RewriteInst]) 
    127129-- Adjust coercions depending on whether we process a local or wanted equality 
    128 adjust ... 
     130adjust co co' eqs@[[co1 :: s1 ~ t1, .., con :: sn ~ tn]] 
     131  | isWanted co = (co_new, eqs) with co = co' |> co_new 
     132  | otherwise   = (co, [[id :: s1 ~ t1, .., id :: sn ~ tn]]) 
    129133}}} 
    130134 
     
    179183co1 :: x ~ t  &  co2' :: [t/x](F s1..sn) ~ s with co2 = [co1/x](F s1..sn) |> co2' 
    180184}}} 
    181  where `x` occurs in `F s1..sn`.  (`co1` may be local or wanted.) 
     185 where `x` occurs in `F s1..sn`, and `co1` may be a wanted only if `co2` is a wanted, too. 
    182186 
    183187 NB: No normalisation required.  Afterwards, !SubstVarVar or !SubstVarFam may apply to `co1` and all rules, except !SubstVarVar, may apply to `co2'`.  However, !SubstVarFam cannot again apply to `co1` and `co2'`, as `t` cannot contain `x` -- cf. the definition of normal equalities. 
     
    237241== Finalisation == 
    238242 
     243'''!!!TODO:''' complete the following. 
     244 
    239245The finalisation step instantiates as many flexible type variables as possible, but it takes care to not to affect variables occurring in the global environment.  The latter is important to obtain principle types (c.f., Andrew Kennedy's thesis).  Hence, we perform finalisation in two phases: 
    240246 1. '''Instantiation:''' For any variable equality of the form `co :: alpha ~ t` or `co :: a ~ alpha`, where `co` is wanted or `alpha` is a variable introduced by flattening, we instantiate `alpha` with `t` or `a`, respectively, and set `co := id`. 
    241247 2. '''Substitution:''' For any family equality... 
     248 
     249'''!!!TODO:''' What about unflattening the locals? 
    242250 
    243251{{{