git.iko.soy/Idris-dev
on be2b9bc help sign in
Idris-dev/src/Core/Unify.hs
84 lines 3.2 kB history raw
1{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, DeriveFunctor #-}
3module Core.Unify(unify) where
5import Core.TT
6import Core.Evaluate
8import Control.Monad
10-- Unification is applied inside the theorem prover. We're looking for holes
11-- which can be filled in, by matching one term's normal form against another.
12-- Returns a list of hole names paired with the term which solves them.
14unify :: Context -> Env -> TT Name -> TT Name -> TC [(Name, TT Name)]
15unify ctxt env x y
16 = case un' [] x y of -- try without normalising first, for speed
17 OK v -> return v
18 _ -> case un' [] (normalise ctxt env x) (normalise ctxt env y) of
19 OK v -> return v
20 _ -> fail $ "Can't unify " ++ showEnv env x ++ " and " ++ showEnv env y
21 where
22 un' bnames (P Bound x _) (P Bound y _)
23 | (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)]
29 un' bnames x@(App _ _) y@(App _ _)
30 = uApp bnames (unApply x) (unApply y)
31 un' bnames x (Bind n (Lam t) (App y (P Bound n' _)))
32 | n == n' = un' bnames x y
33 un' bnames (Bind n (Lam t) (App x (P Bound n' _))) y
34 | n == n' = un' bnames x y
35 un' bnames (Bind x bx sx) (Bind y by sy)
36 = do h1 <- uB bnames bx by
37 h2 <- un' ((x,y):bnames) sx sy
38 combine bnames h1 h2
39 un' bnames x y | x == y = return []
40 | otherwise = fail "Can't unify"
42 uB bnames (Let tx vx) (Let ty vy)
43 = do h1 <- un' bnames tx ty
44 h2 <- un' bnames ty vy
45 combine bnames h1 h2
46 uB bnames (Guess tx vx) (Guess ty vy)
47 = do h1 <- un' bnames tx ty
48 h2 <- un' bnames ty vy
49 combine bnames h1 h2
50 uB bnames (Lam tx) (Lam ty) = un' bnames tx ty
51 uB bnames (Pi tx) (Pi ty) = un' bnames tx ty
52 uB bnames (Hole tx) (Hole ty) = un' bnames tx ty
53 uB bnames (PVar tx) (PVar ty) = un' bnames tx ty
54 uB bnames _ _ = fail "Can't unify"
56 uApp bnames (xp@(P xnt x xty), xargs) (yp@(P ynt y yty), yargs)
57 | (x == y && all okToUnify [xnt, ynt]) ||
58 (holeIn env x && okToUnify ynt) ||
59 (okToUnify xnt && holeIn env y)
60 = do h <- un' bnames xp yp
61 hargs <- zipWithM (un' bnames) xargs yargs
62 h' <- foldM (combine bnames) [] hargs
63 combine bnames h h'
64 uApp bnames (xf, xargs) (yf, yargs)
65 = do un' bnames xf yf -- ignore result
66 hargs <- zipWithM (un' bnames) xargs yargs
67 foldM (combine bnames) [] hargs
69 okToUnify (DCon _ _) = True
70 okToUnify (TCon _) = True
71 okToUnify _ = False
73 combine bnames as [] = return as
74 combine bnames as ((n, t) : bs)
75 = case lookup n as of
76 Nothing -> combine bnames (as ++ [(n,t)]) bs
77 Just t' -> do un' bnames t t'
78 combine bnames as bs
80holeIn :: Env -> Name -> Bool
81holeIn env n = case lookup n env of
82 Just (Hole _) -> True
83 _ -> False