1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
|
module Rewriting.UnificationSpec
( UnificationError (..)
, showUnificationError, unify, unifiable
) where
import Data.Either (isRight)
import Data.Tuple.Extra (both)
import Rewriting.Substitution (Subst, emptySubst, extendSubst)
import Rewriting.Term
data UnificationError f = Clash (Term f) (Term f) | OccurCheck VarIdx (Term f)
showUnificationError :: (f -> String) -> UnificationError f -> String
showUnificationError s (Clash t1 t2) = "Clash: " ++ (showTerm s t1)
++ " is not equal to "
++ (showTerm s t2) ++ "."
showUnificationError s (OccurCheck v t) = "OccurCheck: " ++ (showVarIdx v)
++ " occurs in " ++ (showTerm s t)
++ "."
unify :: (Eq f, Show f) => TermEqs f -> Either (UnificationError f) (Subst f)
unify = (either Left (Right . eqsToSubst)) . (unify' [])
where
eqsToSubst [] = emptySubst
eqsToSubst (eq@(l, r):eqs)
= case l of
(TermVar v) -> extendSubst (eqsToSubst eqs) v r
(TermCons _ _) ->
case r of
(TermVar v) -> extendSubst (eqsToSubst eqs) v l
(TermCons _ _) -> error ("eqsToSubst: " ++ (show eq))
unifiable :: (Eq f, Show f) => TermEqs f -> Bool
unifiable = isRight . unify
unify' :: Eq f => TermEqs f -> TermEqs f
-> Either (UnificationError f) (TermEqs f)
unify' sub [] = Right sub
unify' sub ((TermVar v, r@(TermCons _ _)):eqs) = elim sub v r eqs
unify' sub ((l@(TermCons _ _), TermVar v):eqs) = elim sub v l eqs
unify' sub ((TermVar v, r@(TermVar v')):eqs) | v == v' = unify' sub eqs
| otherwise = elim sub v r eqs
unify' sub ((l@(TermCons c1 ts1), r@(TermCons c2 ts2)):eqs)
| c1 == c2 = unify' sub ((zip ts1 ts2) ++ eqs)
| otherwise = Left (Clash l r)
elim :: Eq f => TermEqs f -> VarIdx -> Term f -> TermEqs f
-> Either (UnificationError f) (TermEqs f)
elim sub v t eqs | dependsOn (TermVar v) t = Left (OccurCheck v t)
| otherwise = unify' sub' (substitute v t eqs)
where
sub' = (TermVar v, t):(map (\(l, r) -> (l, termSubstitute v t r)) sub)
termSubstitute :: VarIdx -> Term f -> Term f -> Term f
termSubstitute v t x@(TermVar v') | v == v' = t
| otherwise = x
termSubstitute v t (TermCons c ts) = TermCons c (termsSubstitute v t ts)
termsSubstitute :: VarIdx -> Term f -> [Term f] -> [Term f]
termsSubstitute v t = map (termSubstitute v t)
substitute :: VarIdx -> Term f -> TermEqs f -> TermEqs f
substitute v t = map (substituteSingle v t)
substituteSingle :: VarIdx -> Term f -> TermEq f -> TermEq f
substituteSingle v t = both (termSubstitute v t)
dependsOn :: Eq f => Term f -> Term f -> Bool
dependsOn l r = and [not (l == r), dependsOn' l r]
where
dependsOn' t v@(TermVar _) = t == v
dependsOn' t (TermCons _ ts) = any id (map (dependsOn' t) ts)
|