Changes between Version 79 and Version 80 of TypeFunctionsSolving


Ignore:
Timestamp:
Sep 5, 2008 11:07:42 AM (7 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{{{