content: --  Copyright (C) 2006-2011 Angelos Charalambidis <a.charalambidis@di.uoa.gr>
  --
  --  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, 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; see the file COPYING.  If not, write to
  --  the Free Software Foundation, Inc., 51 Franklin Street, Fifth Floor,
  --  Boston, MA 02110-1301, USA.
  
  {-# LANGUAGE
      FlexibleContexts
     ,FlexibleInstances
     ,FunctionalDependencies
     ,MultiParamTypeClasses
     ,TypeSynonymInstances
  #-}
  
  module Subst where
  
  -- import Language.Hopl (Expr(..), Clause(..))
  -- import Data.Monoid (mconcat)
  import CoreLang
  import Data.List (union)
  
  type Subst a = [ (a, Expr a) ]
  
  success :: Subst a
  success = []
  
  bind :: a -> Expr a -> Subst a
  bind v e = [(v, e)]
  
  
  isTaut :: Eq a => (a, Expr a) -> Bool
  isTaut (v, Var v') = v == v'
  isTaut _ = False
  
  class (Substitutable a b) | a -> b where
          subst :: Substitutable a b => (Subst b) -> a -> a
  
  instance Eq a => (Substitutable (Expr a) a) where
          subst theta (App e1 e2)  = App (subst theta e1) (subst theta e2)
          subst theta (And e1 e2)  = And (subst theta e1) (subst theta e2)
          subst theta (Or  e1 e2)  = Or  (subst theta e1) (subst theta e2)
          subst theta (Eq  e1 e2)  = Eq  (subst theta e1) (subst theta e2)
          subst theta (Lambda x e) = maybe (Lambda x (subst theta e)) aux $ lookup x theta
              where aux (Var y) = Lambda y (subst theta e)
                    aux _ = error "Cannot substitute lambda bounds vars with expr"
          subst theta (Exists x e) = maybe (Exists x (subst theta e)) aux $ lookup x theta
              where aux (Var y) = Exists y (subst theta e)
                    aux _ = error "Cannot substitute exist bounds vars with expr"
  --        subst theta (Forall x e) = maybe (Forall x (subst theta e)) aux $ lookup x theta
  --            where aux (Var y) = Forall y (subst theta e)
  --                  aux _ = error "Cannot substitute lambda bounds vars with expr"
          subst theta e@(Var x) = maybe e id $ lookup x theta
          subst theta (Not e) = Not (subst theta e)
          subst theta (ListCons e1 e2) = ListCons (subst theta e1) (subst theta e2)
          subst theta e = e
  
  instance Eq a => (Substitutable (Subst a) a) where
           subst theta zeta = [ (v, e') | (v, e) <- theta, let e' = subst zeta e, not (isTaut (v, e')) ]
  
  
  restrict :: Eq a => [a] -> Subst a -> Subst a
  restrict ss xs = [ (v, e) | (v, e) <- xs, v `elem` ss ]
  
  combine theta zeta  = 
      let ss    = map fst theta
          zeta' = [ (v, e) | (v, e) <- zeta, v `notElem` ss ]
      in  subst theta zeta ++ zeta'
  
  
  dom theta   = map fst theta
  range theta = concatMap fv (map snd theta)
  vars theta  = dom theta `union` range theta
  
  
  isRenamingSubst s = all (\(_, x) -> isVar x) s
  
  