@@ -10,88 +10,69 @@ import Debug.Trace
1010-- which can be filled in, by matching one term's normal form against another.
1111-- Returns a list of hole names paired with the term which solves them.
1212
13−-- FIXME! Needs to be cleverer: when we solve a variable, fill it in and normalise
14−-- to help the rest of the unification
15−
1613unify :: Context -> Env -> TT Name -> TT Name -> TC [(Name, TT Name)]
1714unify ctxt env topx topy
18− = case un' [] (normalise ctxt env topx) (normalise ctxt env topy) of
15+ = case un' False [] (normalise ctxt env topx) (normalise ctxt env topy) of
1916 OK v -> return v
2017 Error e -> tfail $ CantUnify topx topy e
2118 where
22− un' bnames (P Bound x _) (P Bound y _)
19+ injective (P (DCon _ _) _ _) = True
20+ injective (P (TCon _) _ _) = True
21+ injective (App f a) = injective f
22+ injective _ = False
23+
24+ un' fn bnames (P Bound x _) (P Bound y _)
2325 | (x,y) `elem` bnames = return []
24− un' bnames (P Bound x _) tm
25− | holeIn env x = return [(x, tm)]
26− un' bnames tm (P Bound y _)
27− | holeIn env y = return [(y, tm)]
28− un' bnames (V i) (P Bound x _)
26+ un' fn bnames (P Bound x _) tm
27+ | (not fn || injective tm)
28+ && holeIn env x = return [(x, tm)]
29+ un' fn bnames tm (P Bound y _)
30+ | (not fn || injective tm)
31+ && holeIn env y = return [(y, tm)]
32+ un' fn bnames (V i) (P Bound x _)
2933 | fst (bnames!!i) == x || snd (bnames!!i) == x = return []
30− un' bnames (P Bound x _) (V i)
34+ un' fn bnames (P Bound x _) (V i)
3135 | fst (bnames!!i) == x || snd (bnames!!i) == x = return []
3236
33− un' bnames x@(App _ _) y@(App _ _)
34− = uApp bnames (unApply x) (unApply y)
35− un' bnames x (Bind n (Lam t) (App y (P Bound n' _)))
36− | n == n' = un' bnames x y
37− un' bnames (Bind n (Lam t) (App x (P Bound n' _))) y
38− | n == n' = un' bnames x y
39− un' bnames (Bind x bx sx) (Bind y by sy)
37+ un' fn bnames (App fx ax) (App fy ay)
38+ = do hf <- un' True bnames fx fy
39+ let ax' = normalise ctxt env (substNames hf ax)
40+ let ay' = normalise ctxt env (substNames hf ay)
41+ ha <- un' False bnames ax' ay'
42+ combine bnames hf ha
43+
44+ un' fn bnames x (Bind n (Lam t) (App y (P Bound n' _)))
45+ | n == n' = un' False bnames x y
46+ un' fn bnames (Bind n (Lam t) (App x (P Bound n' _))) y
47+ | n == n' = un' False bnames x y
48+ un' fn bnames (Bind x bx sx) (Bind y by sy)
4049 = do h1 <- uB bnames bx by
41− h2 <- un' ((x,y):bnames) sx sy
50+ h2 <- un' False ((x,y):bnames) sx sy
4251 combine bnames h1 h2
43− un' bnames x y | x == y = return []
44− | otherwise = fail $ "Can't unify " ++ show x ++ " and " ++ show y
45− ++ " " ++ show bnames ++ " " ++ show env
52+ un' fn bnames x y
53+ | x == y = return []
54+ | otherwise = fail $ "Can't unify " ++ show x ++ " and " ++ show y
55+ ++ " " ++ show bnames ++ " " ++ show env
4656
4757 uB bnames (Let tx vx) (Let ty vy)
48− = do h1 <- un' bnames tx ty
49− h2 <- un' bnames ty vy
58+ = do h1 <- un' False bnames tx ty
59+ h2 <- un' False bnames ty vy
5060 combine bnames h1 h2
5161 uB bnames (Guess tx vx) (Guess ty vy)
52− = do h1 <- un' bnames tx ty
53− h2 <- un' bnames ty vy
62+ = do h1 <- un' False bnames tx ty
63+ h2 <- un' False bnames ty vy
5464 combine bnames h1 h2
55− uB bnames (Lam tx) (Lam ty) = un' bnames tx ty
56− uB bnames (Pi tx) (Pi ty) = un' bnames tx ty
57− uB bnames (Hole tx) (Hole ty) = un' bnames tx ty
58− uB bnames (PVar tx) (PVar ty) = un' bnames tx ty
65+ uB bnames (Lam tx) (Lam ty) = un' False bnames tx ty
66+ uB bnames (Pi tx) (Pi ty) = un' False bnames tx ty
67+ uB bnames (Hole tx) (Hole ty) = un' False bnames tx ty
68+ uB bnames (PVar tx) (PVar ty) = un' False bnames tx ty
5969 uB bnames _ _ = fail "Can't unify"
6070
61− uApp bnames (xp@(P xnt x xty), xargs) (yp@(P ynt y yty), yargs)
62− | (x == y && all okToUnify [xnt, ynt]) || -- functions x,y are injectice
63− (holeIn env x && okToUnify ynt) ||
64− (okToUnify xnt && holeIn env y)
65− = do h <- un' bnames xp yp
66− uArgs bnames h xargs yargs
67− | x == y && xargs == yargs -- only ok if arguments are equal, if functions
68− -- are not known to be injetive
69− = return []
70− uApp bnames (xf, xargs) (yf, yargs)
71− = do un' bnames xf yf -- ignore result
72− uArgs bnames [] xargs yargs
73−
74− okToUnify (DCon _ _) = True
75− okToUnify (TCon _) = True
76− okToUnify _ = False
77−
78− uArgs bnames h [] [] = return h
79− uArgs bnames h (x:xs) (y:ys) =
80− case un' bnames x y of
81− OK h' -> do next <- combine bnames h h'
82− uArgs bnames next xs ys
83− _ -> do let x' = normalise ctxt env (substNames h x)
84− let y' = normalise ctxt env (substNames h y)
85− h' <- un' bnames x' y'
86− next <- combine bnames h h'
87− uArgs bnames next xs ys
88− uArgs bnames h _ _ = fail "Can't unify; argument lists different length"
89−
9071 combine bnames as [] = return as
9172 combine bnames as ((n, t) : bs)
9273 = case lookup n as of
9374 Nothing -> combine bnames (as ++ [(n,t)]) bs
94− Just t' -> do un' bnames t t'
75+ Just t' -> do un' False bnames t t'
9576 combine bnames as bs
9677
9778holeIn :: Env -> Name -> Bool