@@ -10,88 +10,69 @@ import Debug.Trace
10-- which can be filled in, by matching one term's normal form against another.
10-- which can be filled in, by matching one term's normal form against another.
11-- Returns a list of hole names paired with the term which solves them.
11-- Returns a list of hole names paired with the term which solves them.
13−-- FIXME! Needs to be cleverer: when we solve a variable, fill it in and normalise
14−-- to help the rest of the unification
16unify :: Context -> Env -> TT Name -> TT Name -> TC [(Name, TT Name)]
13unify :: Context -> Env -> TT Name -> TT Name -> TC [(Name, TT Name)]
17unify ctxt env topx topy
14unify 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
19 OK v -> return v
16 OK v -> return v
20 Error e -> tfail $ CantUnify topx topy e
17 Error e -> tfail $ CantUnify topx topy e
19+ injective (P (DCon _ _) _ _) = True
20+ injective (P (TCon _) _ _) = True
21+ injective (App f a) = injective f
22− un' bnames (P Bound x _) (P Bound y _)
24+ un' fn bnames (P Bound x _) (P Bound y _)
23 | (x,y) `elem` bnames = return []
25 | (x,y) `elem` bnames = return []
24− un' bnames (P Bound x _) tm
26+ un' fn bnames (P Bound x _) tm
27+ | (not fn || injective tm)
25− | holeIn env x = return [(x, tm)]
28+ && holeIn env x = return [(x, tm)]
26− un' bnames tm (P Bound y _)
29+ un' fn bnames tm (P Bound y _)
30+ | (not fn || injective tm)
27− | holeIn env y = return [(y, tm)]
31+ && holeIn env y = return [(y, tm)]
28− un' bnames (V i) (P Bound x _)
32+ un' fn bnames (V i) (P Bound x _)
29 | fst (bnames!!i) == x || snd (bnames!!i) == x = return []
33 | 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)
31 | fst (bnames!!i) == x || snd (bnames!!i) == x = return []
35 | fst (bnames!!i) == x || snd (bnames!!i) == x = return []
33− un' bnames x@(App _ _) y@(App _ _)
37+ un' fn bnames (App fx ax) (App fy ay)
34− = uApp bnames (unApply x) (unApply y)
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'
35− un' bnames x (Bind n (Lam t) (App y (P Bound n' _)))
44+ un' fn bnames x (Bind n (Lam t) (App y (P Bound n' _)))
36− | n == n' = un' bnames x y
45+ | n == n' = un' False bnames x y
37− un' bnames (Bind n (Lam t) (App x (P Bound n' _))) y
46+ un' fn bnames (Bind n (Lam t) (App x (P Bound n' _))) y
38− | n == n' = un' bnames x y
47+ | n == n' = un' False bnames x y
39− un' bnames (Bind x bx sx) (Bind y by sy)
48+ un' fn bnames (Bind x bx sx) (Bind y by sy)
40 = do h1 <- uB bnames bx by
49 = do h1 <- uB bnames bx by
41− h2 <- un' ((x,y):bnames) sx sy
50+ h2 <- un' False ((x,y):bnames) sx sy
42 combine bnames h1 h2
51 combine bnames h1 h2
43− un' bnames x y | x == y = return []
52+ un' fn bnames x y
44− | otherwise = fail $ "Can't unify " ++ show x ++ " and " ++ show y
54+ | otherwise = fail $ "Can't unify " ++ show x ++ " and " ++ show y
45− ++ " " ++ show bnames ++ " " ++ show env
55+ ++ " " ++ show bnames ++ " " ++ show env
47 uB bnames (Let tx vx) (Let ty vy)
57 uB bnames (Let tx vx) (Let ty vy)
48− = do h1 <- un' bnames tx ty
58+ = do h1 <- un' False bnames tx ty
49− h2 <- un' bnames ty vy
59+ h2 <- un' False bnames ty vy
50 combine bnames h1 h2
60 combine bnames h1 h2
51 uB bnames (Guess tx vx) (Guess ty vy)
61 uB bnames (Guess tx vx) (Guess ty vy)
52− = do h1 <- un' bnames tx ty
62+ = do h1 <- un' False bnames tx ty
53− h2 <- un' bnames ty vy
63+ h2 <- un' False bnames ty vy
54 combine bnames h1 h2
64 combine bnames h1 h2
55− uB bnames (Lam tx) (Lam ty) = un' bnames tx ty
65+ uB bnames (Lam tx) (Lam ty) = un' False bnames tx ty
56− uB bnames (Pi tx) (Pi ty) = un' bnames tx ty
66+ uB bnames (Pi tx) (Pi ty) = un' False bnames tx ty
57− uB bnames (Hole tx) (Hole ty) = un' bnames tx ty
67+ uB bnames (Hole tx) (Hole ty) = un' False bnames tx ty
58− uB bnames (PVar tx) (PVar ty) = un' bnames tx ty
68+ uB bnames (PVar tx) (PVar ty) = un' False bnames tx ty
59 uB bnames _ _ = fail "Can't unify"
69 uB bnames _ _ = fail "Can't unify"
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
70− uApp bnames (xf, xargs) (yf, yargs)
71− = do un' bnames xf yf -- ignore result
72− uArgs bnames [] xargs yargs
74− okToUnify (DCon _ _) = True
75− okToUnify (TCon _) = True
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"
90 combine bnames as [] = return as
71 combine bnames as [] = return as
91 combine bnames as ((n, t) : bs)
72 combine bnames as ((n, t) : bs)
92 = case lookup n as of
73 = case lookup n as of
93 Nothing -> combine bnames (as ++ [(n,t)]) bs
74 Nothing -> combine bnames (as ++ [(n,t)]) bs
94− Just t' -> do un' bnames t t'
75+ Just t' -> do un' False bnames t t'
95 combine bnames as bs
76 combine bnames as bs
97holeIn :: Env -> Name -> Bool
78holeIn :: Env -> Name -> Bool