{-# OPTIONS_GHC -fglasgow-exts -fallow-undecidable-instances #-}
--  glasgow-exts:          multi-param typeclasses
--  undecidable-instances: default instance for SubstParams (see below)

-- 
-- Copyright (C) 2005 Stefan Wehr - http://www.stefanwehr.de
--
-- This program is free software; you can redistribute it and/or
-- modify it under the terms of the GNU General Public License as
-- published by the Free Software Foundation; either version 2 of
-- the License, or (at your option) any later version.
-- 
-- This program is distributed in the hope that it will be useful,
-- but WITHOUT ANY WARRANTY; without even the implied warranty of
-- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
-- General Public License for more details.
-- 
-- You should have received a copy of the GNU General Public License
-- along with this program; if not, write to the Free Software
-- Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
-- 02111-1307, USA.
-- 

module Phrac.Substitution (
    Subst, Substitution(..),
    showSubst, nullSubst, (+->), removeFromSubst, removeListFromSubst, 
    composeSubst,
    mergeSubst, substLookup, substFromAssocs,
) where

import List
import Maybe

import qualified Phrac.Map as Map
import Phrac.Pretty

data Subst a b = Subst [(a, b)]

-- The SubstParams class is only a shortcut for the constraints
-- in the class context. Only one instance will ever exists, because
-- we do not export the class at all. For this instance, we need
-- the flag -fallow-undecidable-instances
class (Pretty a, Pretty b, Ord a, Eq b) => SubstParams a b where
instance (Pretty a, Pretty b, Ord a, Eq b) => SubstParams a b where


-- The class substitution states that a substitution from a to b can
-- be applied to values of type c.
class SubstParams a b => Substitution a b c where
    applySubst :: Subst a b -> c -> c

instance Substitution a b c => Substitution a b [c] where
    applySubst s ts = map (applySubst s) ts

instance Substitution a b c => Substitution a b (Map.Map k c) where
    applySubst s m = Map.map (applySubst s) m

instance (Substitution a b c, Substitution a b d) 
    => Substitution a b (c, d) where
    applySubst s (c, d) = (applySubst s c, applySubst s d)
    
showSubst :: (SubstParams a b) => Subst a b -> String
showSubst (Subst s) = 
    "{" ++
    (concat . intersperse ", ")
    (map (\ (v,t) -> showPpr v ++ " |--> " ++ showPpr t) s)
    ++ "}"

nullSubst :: (SubstParams a b) => Subst a b
nullSubst = Subst []

(+->) :: (SubstParams a b) => a -> b -> Subst a b
(+->) id t = Subst [(id,t)]

removeFromSubst :: (SubstParams a b) => a -> Subst a b -> Subst a b
removeFromSubst id (Subst l) = Subst (remove id l)
    where remove _ [] = []
          remove id ((id',t):rest)
              | id == id' = rest
              | otherwise = (id',t) : remove id rest

removeListFromSubst :: (SubstParams a b) => [a] -> Subst a b -> Subst a b
removeListFromSubst l s = foldr removeFromSubst s l

composeSubst :: (Substitution a b b) => Subst a b -> Subst a b -> Subst a b
composeSubst s1@(Subst s1') (Subst s2') = 
    Subst $ [(u, applySubst s1 t) | (u,t) <- s2'] ++ s1'

mergeSubst :: (SubstParams a b, Monad m)
               => Subst a b -> Subst a b -> m (Subst a b)
mergeSubst s1@(Subst s1') s2@(Subst s2') = 
    if agree 
       then return (Subst (s1' ++ s2'))
            else fail ("merging substitutions failed. s1 = " ++
                       showSubst s1 ++ ", s2 = " ++ showSubst s2)
    where agree = all (\v -> fromJust (substLookup v s1)
                             == fromJust (substLookup v s2))
                      (map fst s1' `intersect` map fst s2')


substLookup :: (Monad m, SubstParams a b) => a -> Subst a b -> m b
substLookup x (Subst l) = 
    case lookup x l of
      Just y -> return y
      Nothing -> fail ("key " ++ showPpr x ++ " not found in substitution "
                       ++ showSubst (Subst l))

substFromAssocs :: [(a,b)] -> Subst a b
substFromAssocs l = Subst l