| Line No. | Rev | Author | Line |
|---|---|---|---|
| 1 | 1 | paulosilva | |
| 2 | {-# LANGUAGE FlexibleContexts #-} | ||
| 3 | {-# OPTIONS_GHC -Wall #-} | ||
| 4 | |||
| 5 | ------------------------------------------------------------------------------- | ||
| 6 | |||
| 7 | {- | | ||
| 8 | Module : Language.Type.Unification | ||
| 9 | Description : Unification algorithm for the polymorphic type representation. | ||
| 10 | Copyright : (c) Paulo Silva | ||
| 11 | License : LGPL | ||
| 12 | |||
| 13 | Maintainer : paufil@di.uminho.pt | ||
| 14 | Stability : experimental | ||
| 15 | Portability : portable | ||
| 16 | |||
| 17 | -} | ||
| 18 | |||
| 19 | ------------------------------------------------------------------------------- | ||
| 20 | |||
| 21 | module Language.Type.Unification ( | ||
| 22 | unify | ||
| 23 | ) where | ||
| 24 | |||
| 25 | import Control.GalcError | ||
| 26 | import Control.Monad.Error | ||
| 27 | import Data.Existential | ||
| 28 | import Language.Type.Constraint | ||
| 29 | import Language.Type.Equality | ||
| 30 | import Language.Type.Syntax | ||
| 31 | import Language.Type.Utils | ||
| 32 | import Prelude hiding (all,fail) | ||
| 33 | |||
| 34 | ------------------------------------------------------------------------------- | ||
| 35 | |||
| 36 | 7 | paulosilva | unify :: (MonadError GalcError m) |
| 37 | 3 | paulosilva | => [Constraint] -> m [Constraint] |
| 38 | 1 | paulosilva | unify [] = return [] |
| 39 | unify ((s :=: t):c) | ||
| 40 | | isTVar s && isTVar t && beq s t = -- delete rule (variables) | ||
| 41 | unify c | ||
| 42 | | isBasicType s && isBasicType t && beq s t = -- delete rule (base types) | ||
| 43 | unify c | ||
| 44 | | isTVar t && not (isTVar s) = -- orient rule | ||
| 45 | unify $ (t :=: s):c | ||
| 46 | | isConstructor s && isConstructor t = do -- decompose rule | ||
| 47 | cns <- decompose s t | ||
| 48 | unify $ cns++c | ||
| 49 | | isTVar s && not (occursIn s t) = do -- eliminate rule | ||
| 50 | c' <- substitution [s :=: t] c | ||
| 51 | sbs <- unify c' | ||
| 52 | 7 | paulosilva | Hide t' <- typeRewriteE sbs t |
| 53 | 1 | paulosilva | return $ (s :=: t'):sbs |
| 54 | | otherwise = | ||
| 55 | throwError $ UnificationError (show s, show t) -- typing error | ||
| 56 | |||
| 57 | ------------------------------------------------------------------------------- | ||
| 58 | |||
| 59 | 7 | paulosilva | substitution :: MonadError GalcError m |
| 60 | 3 | paulosilva | => [Constraint] -> [Constraint] -> m [Constraint] |
| 61 | 7 | paulosilva | substitution subst = mapM aux |
| 62 | where aux (t1 :=: t2) = do | ||
| 63 | Hide t1' <- typeRewriteE subst t1 | ||
| 64 | Hide t2' <- typeRewriteE subst t2 | ||
| 65 | return $ t1' :=: t2' | ||
| 66 | 1 | paulosilva | |
| 67 | ------------------------------------------------------------------------------- | ||
| 68 | |||
| 69 | 7 | paulosilva | decompose :: MonadError GalcError m => Type a -> Type b -> m [Constraint] |
| 70 | 1 | paulosilva | decompose (Prod a b) (Prod a' b') = return [a :=: a', b :=: b'] |
| 71 | decompose (Either a b) (Either a' b') = return [a :=: a', b :=: b'] | ||
| 72 | decompose (Maybe a) (Maybe a') = return [a :=: a'] | ||
| 73 | decompose (List a) (List a') = return [a :=: a'] | ||
| 74 | decompose (Set a) (Set a') = return [a :=: a'] | ||
| 75 | decompose (Map a b) (Map a' b') = return [a :=: a', b :=: b'] | ||
| 76 | decompose (Fun a b) (Fun a' b') = return [a :=: a', b :=: b'] | ||
| 77 | decompose (Rel a b) (Rel a' b') = return [a :=: a', b :=: b'] | ||
| 78 | decompose (Ord a) (Ord a') = return [a :=: a'] | ||
| 79 | decompose (GC a b) (GC a' b') = return [a :=: a', b :=: b'] | ||
| 80 | 7 | paulosilva | decompose t1 t2 = throwError $ DecomposeError (show t1) (show t2) |
| 81 | 1 | paulosilva | |
| 82 | ------------------------------------------------------------------------------- | ||
| 83 |