1. Patrick Bahr
  2. compdata

Commits

Patrick Bahr  committed 641005b

implemented unification

  • Participants
  • Parent commits 7eed978
  • Branches typefun

Comments (0)

Files changed (4)

File alacarte.cabal

View file
                         Data.ALaCarte.Ordering,
                         Data.ALaCarte.TermRewriting, Data.ALaCarte.Automata,
                         Data.ALaCarte.Arbitrary, Data.ALaCarte.Show, Data.ALaCarte.Variables,
-                        Data.ALaCarte.Decompose													
+                        Data.ALaCarte.Decompose, Data.ALaCarte.Unification
+
   Other-Modules:        Data.ALaCarte.Derive.Utils, Data.ALaCarte.Derive.Equality,
                         Data.ALaCarte.Derive.Ordering, Data.ALaCarte.Derive.Arbitrary,
                         Data.ALaCarte.Derive.Show
 
-  Build-Depends:	base >= 4, template-haskell, containers, QuickCheck >= 2
+  Build-Depends:	base >= 4, template-haskell, containers, mtl, QuickCheck >= 2
   hs-source-dirs:	src
   ghc-options:          -W
 
 Executable test
   Main-is:		Data_Test.hs
-  Build-Depends:	base >= 4, template-haskell, containers, QuickCheck >= 2, test-framework, test-framework-quickcheck2, derive
+  Build-Depends:	base >= 4, template-haskell, containers, mtl, QuickCheck >= 2, test-framework, test-framework-quickcheck2, derive
   hs-source-dirs:	src testsuite/tests
   ghc-options:          -fhpc
   if !flag(test)

File src/Data/ALaCarte/Decompose.hs

View file
-{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, FlexibleContexts #-}
+{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, FlexibleContexts, UndecidableInstances #-}
 
 --------------------------------------------------------------------------------
 -- |
 
 {-| This class specifies the decomposability of a functorial value. -}
 
-class Decompose f v a where
+class (HasVars f v, Functor f, Foldable f) => Decompose f v where
     {-| This function decomposes a functorial value. -}
 
     decomp :: f a -> Decomp f v a
-
-instance (HasVars f v, Functor f, Foldable f) => Decompose f v a where
     decomp t = case isVar t of
                  Just v -> Var v
                  Nothing -> Fun sym args
                      where sym = fmap (const ()) t
                            args = arguments t
 
+instance (HasVars f v, Functor f, Foldable f) => Decompose f v where
+
+
 {-| This function decomposes a term. -}
 
-decompose :: (Decompose f v (Term f)) => Term f -> DecompTerm f v
+decompose :: (Decompose f v) => Term f -> DecompTerm f v
 decompose (Term t) = decomp t

File src/Data/ALaCarte/Unification.hs

View file
+{-# LANGUAGE FlexibleContexts #-}
+
+-------------------------------------------------------------------------------
+-- |
+-- Module      :  Data.ALaCarte.Unification
+-- Copyright   :  3gERP, 2010
+-- License     :  AllRightsReserved
+-- Maintainer  :  Tom Hvitved, Patrick Bahr, and Morten Ib Nielsen
+-- Stability   :  unknown
+-- Portability :  unknown
+--
+-- This module implements a simple unification algorithm using data
+-- types a la carte.
+--
+--------------------------------------------------------------------------------
+module Data.ALaCarte.Unification where
+
+import Data.ALaCarte.Term
+import Data.ALaCarte.Variables
+import Data.ALaCarte.Decompose
+import Data.ALaCarte.Sum
+
+import Control.Monad.Error
+import Control.Monad.State
+
+import qualified Data.Map as Map
+
+{-| This type represents equations between terms over a specific
+signature. -}
+
+type Equation f = (Term f,Term f)
+
+{-| This type represents list of equations. -}
+
+type Equations f = [Equation f]
+
+{-| This type represents errors that might occur during the
+unification.  -}
+
+data UnifError f v = FailedOccursCheck v (Term f)
+                   | HeadSymbolMismatch (Const f) (Const f)
+                   | UnifError String
+
+instance Error (UnifError f v) where
+    strMsg = UnifError
+
+
+failedOccursCheck :: (MonadError (UnifError f v) m) => v -> Term f -> m a
+failedOccursCheck v t = throwError $ FailedOccursCheck v t
+
+headSymbolMismatch :: (MonadError (UnifError f v) m) => Const f -> Const f -> m a
+headSymbolMismatch f g = throwError $ HeadSymbolMismatch f g
+
+applySubstEq :: (Ord v,  HasVars g v,  Functor g, g :<: f) =>
+     Subst f v -> Equation g -> Equation f
+applySubstEq s (t1,t2) = (applySubst s t1,applySubst s t2)
+
+
+{-| This function returns the most general unifier of the given
+equations using the algorithm of Martelli and Montanari. -}
+
+unify :: (MonadError (UnifError f v) m, Decompose f v, Ord v, Eq (Const f))
+      => Equations f -> m (Subst f v)
+unify = runUnifyM runUnify
+
+data UnifyState f v = UnifyState {usEqs ::Equations f, usSubst :: Subst f v}
+type UnifyM f v m a = StateT (UnifyState f v) m a
+
+runUnifyM :: MonadError (UnifError f v) m
+          => UnifyM f v m a -> Equations f -> m (Subst f v)
+runUnifyM m eqs = liftM (usSubst . snd) $
+                           runStateT m UnifyState { usEqs = eqs, usSubst = Map.empty}
+
+withNextEq :: Monad m
+           => (Equation f -> UnifyM f v m ()) -> UnifyM f v m ()
+withNextEq m = do eqs <- gets usEqs
+                  case eqs of 
+                    [] -> return ()
+                    x : xs -> modify (\s -> s {usEqs = xs})
+                           >> m x
+
+putEqs :: Monad m 
+       => Equations f -> UnifyM f v m ()
+putEqs eqs = modify addEqs
+    where addEqs s = s {usEqs = eqs ++ usEqs s}
+
+putBinding :: (Monad m, Ord v, HasVars f v, Functor f) => (v, Term f) -> UnifyM f v m ()
+putBinding bind = modify applySubst
+    where binds = Map.fromList [bind]
+          applySubst s = s { usEqs = map (applySubstEq binds) (usEqs s),
+                             usSubst = compSubst binds (usSubst s)}
+
+
+runUnify :: (MonadError (UnifError f v) m, Decompose f v, Ord v, Eq (Const f))
+         => UnifyM f v m ()
+runUnify = withNextEq (\ e -> unifyStep e >> runUnify)
+
+unifyStep :: (MonadError (UnifError f v) m, Decompose f v, Ord v, Eq (Const f)) 
+          => Equation f -> UnifyM f v m ()
+unifyStep (s,t) = case decompose s of
+                    Var v1 -> case decompose t of
+                                 Var v2 -> unless (v1 == v2) $
+                                             putBinding (v1, t)
+                                 _ -> if containsVar v1 t
+                                      then failedOccursCheck v1 t
+                                      else putBinding (v1,t)
+                    Fun s1 args1 -> case decompose t of
+                                       Var v -> if containsVar v s
+                                                 then failedOccursCheck v s
+                                                 else putBinding (v,s)
+                                       Fun s2 args2 -> if s1 == s2
+                                                        then putEqs $ zip args1 args2
+                                                        else headSymbolMismatch s1 s2

File src/Data/ALaCarte/Variables.hs

View file
 --------------------------------------------------------------------------------
 module Data.ALaCarte.Variables (
   HasVars(..),
+  Subst,
   containsVar,
   variables,
   substVars,
   substVars',
   applySubst,
-  applySubst') where
+  applySubst',
+  compSubst) where
 
 import Data.ALaCarte.Term
 import Data.ALaCarte.Algebra
 
 import Prelude hiding (or, foldl)
 
+type CxtSubst h a f v = Map v (Cxt h f a)
+
+type Subst f v = CxtSubst NoHole Nothing f v
 
 {-| This multiparameter class defines functors with variables. An
 instance @HasVar f v@ denotes that values over @f@ might contain
 
 applySubst' :: (Ord k, HasVars f1 k,Functor f1, Functor f2, Functor g, f1 :<: g, f2 :<: g)
             => Map k (Cxt h f2 a) -> Cxt h f1 a -> Cxt h g a
-applySubst' subst = applySubst (fmap deepInject subst)
+applySubst' subst = applySubst (fmap deepInject subst)
+
+
+{-| This function composes two substitutions @s1@ and @s2@. That is,
+applying the resulting substitution is equivalent to first applying
+@s2@ and then @s1@. -}
+
+compSubst :: (Ord v, HasVars f v, Functor f, f :<: g)
+          => CxtSubst h a g v -> CxtSubst h a f v -> CxtSubst h a g v
+compSubst s1 s2 = fmap (applySubst s1) s2 `Map.union` s1