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
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
|
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
module HSVIS.Typecheck.Solve (
solveConstraints,
UnifyErr(..),
) where
import Control.Monad (guard, (>=>))
import Data.Bifunctor (Bifunctor(..))
import Data.Foldable (toList, foldl')
import Data.List (sortBy, minimumBy, groupBy, intercalate)
import Data.Ord (comparing)
import Data.Map.Strict (Map)
import qualified Data.Map.Strict as Map
import Debug.Trace
import Data.Bag
import HSVIS.Diagnostic (Range(..))
import HSVIS.Pretty
import Data.Function (on)
data UnifyErr v t
= UEUnequal t t Range
| UERecursive v t Range
deriving (Show)
data Constr a b = Constr a b Range
deriving (Show)
instance Bifunctor Constr where
bimap f g (Constr x y r) = Constr (f x) (g y) r
-- right-hand side of a constraint
data RConstr b = RConstr b Range
deriving (Show, Functor)
splitConstr :: Constr a b -> (a, RConstr b)
splitConstr (Constr x y r) = (x, RConstr y r)
unsplitConstr :: a -> RConstr b -> Constr a b
unsplitConstr x (RConstr y r) = Constr x y r
constrUnequal :: Constr t t -> UnifyErr v t
constrUnequal (Constr x y r) = UEUnequal x y r
constrRecursive :: Constr v t -> UnifyErr v t
constrRecursive (Constr x y r) = UERecursive x y r
rconType :: RConstr b -> b
rconType (RConstr t _) = t
-- | Returns a pair of:
-- 1. A set of unification errors;
-- 2. An assignment of the variables that had any constraints on them.
-- The producedure was successful if the set of errors is empty. Note that
-- unconstrained variables do not appear in the output.
solveConstraints
:: forall v t. (Ord v, Ord t, Show v, Pretty t)
-- | reduce: take two types and unify them, resulting in:
-- 1. A bag of resulting constraints on variables;
-- 2. A bag of errors: pairs of two types that are provably distinct but
-- need to be equal for the input types to unify.
=> (t -> t -> Range -> (Bag (v, t, Range), Bag (t, t, Range)))
-- | Free variables in a type
-> (t -> Bag v)
-- | \mapping term -> term with variables in the mapping substituted by their values
-> (Map v t -> t -> t)
-- | Detect bare-variable types
-> (t -> Maybe v)
-- | Some kind of size measure on types
-> (t -> Int)
-- | Equality constraints to solve
-> [(t, t, Range)]
-> (Map v t, Bag (UnifyErr v t))
solveConstraints reduce frees subst detect size = \tupcs ->
let cs = map (uncurry3 Constr) tupcs :: [Constr t t]
(vcs, errs) = foldMap reduce' cs
asg = Map.fromListWith (<>) (map (second pure . splitConstr) (toList vcs))
(errs', asg') = loop asg []
errs'' = fmap constrUnequal errs <> errs'
in trace ("[solver] Solving:" ++ concat ["\n- " ++ pretty a ++ " == " ++ pretty b ++ " {" ++ pretty r ++ "}" | Constr a b r <- cs]) $
trace ("[solver] Result: (with " ++ show (length errs'') ++ " errors)" ++
concat ["\n- " ++ show v ++ " = " ++ pretty t | (v, t) <- Map.assocs asg'])
(asg', errs'')
where
reduce' :: Constr t t -> (Bag (Constr v t), Bag (Constr t t))
reduce' (Constr t1 t2 r) = bimap (fmap (uncurry3 Constr)) (fmap (uncurry3 Constr)) $ reduce t1 t2 r
loop :: Map v (Bag (RConstr t)) -> [(v, t)] -> (Bag (UnifyErr v t), Map v t)
loop m eqlog = do
traceM $ "[solver] Step:" ++ concat
[case toList rhss of
[] -> "\n- " ++ show v ++ " <no RHSs>"
RConstr t r : rest ->
"\n- " ++ show v ++ " == " ++ pretty t ++ " {" ++ pretty r ++ "}" ++
concat ["\n " ++ replicate (length (show v)) ' ' ++ " == " ++ pretty t' ++ " {" ++ pretty r' ++ "}"
| RConstr t' r' <- rest]
| (v, rhss) <- Map.assocs m]
m' <- Map.traverseWithKey
(\v rhss ->
let rhss' = bagFromList (dedupRCs (toList rhss))
-- filter out recursive equations
(recs, nonrecs) = bagPartition (\c@(RConstr t _) -> if v `elem` frees t then Just c else Nothing) rhss'
-- filter out trivial equations (v = v)
(_, nonrecs') = bagPartition (detect . rconType >=> guard . (== v)) nonrecs
in (constrRecursive . unsplitConstr v <$> recs, nonrecs'))
m
let msmallestvar :: Maybe (v, RConstr t) -- var with its smallest RHS, if such a var exists
msmallestvar =
minimumByMay (comparing (size . rconType . snd))
. map (second (minimumBy (comparing (size . rconType))))
. filter (not . null . snd)
$ Map.assocs m'
case msmallestvar of
Nothing -> do
traceM $ "[solver] Log = [" ++ intercalate ", " [show v ++ " = " ++ pretty t | (v, t) <- eqlog] ++ "]"
return $ applyLog eqlog mempty
Just (var, RConstr smallrhs _) -> do
traceM $ "[solver] Retiring " ++ show var ++ " = " ++ pretty smallrhs
let (_, otherrhss) = bagPartition (guard . (== smallrhs) . rconType) (m' Map.! var)
let (newcs, errs) = foldMap (reduce' . unsplitConstr smallrhs) (dedupRCs (toList otherrhss))
(fmap constrUnequal errs, ()) -- write the errors
let m'' = Map.unionWith (<>)
(Map.map (fmap @Bag (fmap @RConstr (subst (Map.singleton var smallrhs))))
(Map.delete var m'))
(Map.fromListWith (<>) (map (second pure . splitConstr) (toList newcs)))
loop m'' ((var, smallrhs) : eqlog)
applyLog :: [(v, t)] -> Map v t -> Map v t
applyLog ((v, t) : l) m = applyLog l $ Map.insert v (subst m t) m
applyLog [] m = m
-- If there are multiple sources for the same cosntraint, only one of them is kept.
dedupRCs :: Ord t => [RConstr t] -> [RConstr t]
dedupRCs = map head . groupBy ((==) `on` rconType) . sortBy (comparing rconType)
minimumByMay :: Foldable t' => (a -> a -> Ordering) -> t' a -> Maybe a
minimumByMay cmp = foldl' min' Nothing
where min' mx y = Just $! case mx of
Nothing -> y
Just x | GT <- cmp x y -> y
| otherwise -> x
uncurry3 :: (a -> b -> c -> d) -> (a, b, c) -> d
uncurry3 f (x, y, z) = f x y z
|
