zjednywacz-hs/Zjednanie.hs

module Zjednanie (dawaj, zjednaj) where

import Drzewo

type Podstawienie = [(Nazwa, Typ)]

występuje :: Nazwa -> Typ -> Bool
występuje x (TZmiennej y) = x == y
występuje x (Strzałka u v) = występuje x u || występuje x v

-- (podmień s x t) => Podmień s za wszystkie wystąpienia zmiennej x w t
podmień :: Typ -> Nazwa -> Typ -> Typ
podmień s x t@(TZmiennej y) = if x == y then s else t
podmień s x (Strzałka u v) = Strzałka (podmień s x u) (podmień s x v)

-- podmienia
dawaj :: Podstawienie -> Typ -> Typ
dawaj s t = foldr (\ (x,e) -> podmień e x) t s

-- DOZRO: jakiś ładniejszy typ niż `Może`
zjednajJedno :: Typ -> Typ -> Maybe Podstawienie
zjednajJedno (TZmiennej x) t@(TZmiennej y) = Just (if x == y then [] else [(x, t)])
zjednajJedno (Strzałka x y) (Strzałka u v) = zjednaj [(x, u), (y, v)]
zjednajJedno (TZmiennej x) z@(Strzałka _ _) = _zj x z
zjednajJedno z@(Strzałka _ _) (TZmiennej x) = _zj x z
_zj x z = if występuje x z then Nothing {-- not unifiable: circularity --} else Just [(x,z)]

zjednaj :: [(Typ, Typ)] -> Maybe Podstawienie
zjednaj [] = Just []
zjednaj ((x, y) : t) = zjednaj t >>= (\ t2 -> (\t1 -> t1 ++ t2) <$>  zjednajJedno (dawaj t2 x) (dawaj t2 y))

{--
λ> zjednaj [(Strzałka (TZmiennej "XD") (TZmiennej "ELO"), Strzałka (TZmiennej "DD") (TZmiennej "QQ"))]
Just [("XD",TZmiennej "DD"),("ELO",TZmiennej "QQ")]
--}