... | @@ -98,7 +98,7 @@ norm [[s ~ t]] = check [[s' ~ t']] : eqs++eqt |
... | @@ -98,7 +98,7 @@ norm [[s ~ t]] = check [[s' ~ t']] : eqs++eqt |
|
(t', eqt) = flatten t
|
|
(t', eqt) = flatten t
|
|
|
|
|
|
check :: FlattenedEqInst -> [FlattenedEqInst]
|
|
check :: FlattenedEqInst -> [FlattenedEqInst]
|
|
-- Does OccursCheck + Decomp + Swap (of new-single)
|
|
-- Does OccursCheck + Decomp + Triv + Swap (of new-single)
|
|
check [[t ~ t]] = []
|
|
check [[t ~ t]] = []
|
|
check [[x ~ t]] | x `occursIn` t = fail
|
|
check [[x ~ t]] | x `occursIn` t = fail
|
|
| otherwise = [[x ~ t]]
|
|
| otherwise = [[x ~ t]]
|
... | @@ -137,7 +137,23 @@ Notes: |
... | @@ -137,7 +137,23 @@ Notes: |
|
|
|
|
|
## Solving
|
|
## Solving
|
|
|
|
|
|
**TODO** Partition the rules depending on which if the three forms of normal equalities they apply to!!!
|
|
**TODO**
|
|
|
|
|
|
|
|
- Rules applying to family equalities:
|
|
|
|
|
|
|
|
- IdenticalLHS only applies to family equalities (both local and wanteds) - MAYBE only when at least one of the equalities is a local (see email).
|
|
|
|
- Top only applies to family equalities (both locals and wanteds)
|
|
|
|
|
|
|
|
>
|
|
|
|
> We should apply IdenticalLHS first as it cheaper and potentially reduces the number of applications of Top.
|
|
|
|
|
|
|
|
- Rules applying to variable equalities:
|
|
|
|
|
|
|
|
- Unify only applies to all wanted flexible variable equalities
|
|
|
|
- Subst (= local for variable equalities) applies to all variable equalities, where local variable equalities are substituted into all equalities, but wanted variable equalities are only substituted into wanted equalities.
|
|
|
|
|
|
|
|
>
|
|
|
|
> We should first apply Unify where possible and, only when that is exhausted, apply Subst. This is as Unify is cheaper and has global impact (instantiates variables in the environment, too).
|
|
|
|
|
|
|
|
|
|
Notes:
|
|
Notes:
|
... | | ... | |