git.iko.soy/Idris-dev
on ddba413 help sign in
Idris-dev/src/Core/Unify.hs
85 lines 3.2 kB history raw
1module Core.Unify(unify) where
3import Core.TT
4import Core.Evaluate
6import Control.Monad
7import Debug.Trace
9-- Unification is applied inside the theorem prover. We're looking for holes
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.
13unify :: Context -> Env -> TT Name -> TT Name -> TC [(Name, TT Name)]
14unify ctxt env topx topy
15 = case un' False [] (normalise ctxt env topx) (normalise ctxt env topy) of
16 OK v -> return (filter notTrivial v)
17 Error e -> tfail $ CantUnify topx topy e
18 where
19 notTrivial (x, P _ x' _) = x /= x'
20 notTrivial _ = True
22 injective (P (DCon _ _) _ _) = True
23 injective (P (TCon _ _) _ _) = True
24 injective (App f a) = injective f
25 injective _ = False
27 un' fn bnames (P Bound x _) (P Bound y _)
28 | (x,y) `elem` bnames = return []
29 un' fn bnames (P Bound x _) tm
30 | (not fn || injective tm)
31 && holeIn env x = return [(x, tm)]
32 un' fn bnames tm (P Bound y _)
33 | (not fn || injective tm)
34 && holeIn env y = return [(y, tm)]
35 un' fn bnames (V i) (P Bound x _)
36 | fst (bnames!!i) == x || snd (bnames!!i) == x = return []
37 un' fn bnames (P Bound x _) (V i)
38 | fst (bnames!!i) == x || snd (bnames!!i) == x = return []
40 un' fn bnames (App fx ax) (App fy ay)
41 = do hf <- un' True bnames fx fy
42 let ax' = normalise ctxt env (substNames hf ax)
43 let ay' = normalise ctxt env (substNames hf ay)
44 ha <- un' False bnames ax' ay'
45 combine bnames hf ha
47 un' fn bnames x (Bind n (Lam t) (App y (P Bound n' _)))
48 | n == n' = un' False bnames x y
49 un' fn bnames (Bind n (Lam t) (App x (P Bound n' _))) y
50 | n == n' = un' False bnames x y
51 un' fn bnames (Bind x bx sx) (Bind y by sy)
52 = do h1 <- uB bnames bx by
53 h2 <- un' False ((x,y):bnames) sx sy
54 combine bnames h1 h2
55 un' fn bnames x y
56 | x == y = return []
57 | otherwise = fail $ "Can't unify " ++ show x ++ " and " ++ show y
58 ++ " " ++ show bnames ++ " " ++ show env
60 uB bnames (Let tx vx) (Let ty vy)
61 = do h1 <- un' False bnames tx ty
62 h2 <- un' False bnames ty vy
63 combine bnames h1 h2
64 uB bnames (Guess tx vx) (Guess ty vy)
65 = do h1 <- un' False bnames tx ty
66 h2 <- un' False bnames ty vy
67 combine bnames h1 h2
68 uB bnames (Lam tx) (Lam ty) = un' False bnames tx ty
69 uB bnames (Pi tx) (Pi ty) = un' False bnames tx ty
70 uB bnames (Hole tx) (Hole ty) = un' False bnames tx ty
71 uB bnames (PVar tx) (PVar ty) = un' False bnames tx ty
72 uB bnames _ _ = fail "Can't unify"
74 combine bnames as [] = return as
75 combine bnames as ((n, t) : bs)
76 = case lookup n as of
77 Nothing -> combine bnames (as ++ [(n,t)]) bs
78 Just t' -> do un' False bnames t t'
79 combine bnames as bs
81holeIn :: Env -> Name -> Bool
82holeIn env n = case lookup n env of
83 Just (Hole _) -> True
84 _ -> False