git.iko.soy/Idris-dev
on ec87a69 help sign in
Idris-dev/src/Core/Unify.hs
82 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 v
17 Error e -> tfail $ CantUnify topx topy e
18 where
19 injective (P (DCon _ _) _ _) = True
20 injective (P (TCon _) _ _) = True
21 injective (App f a) = injective f
22 injective _ = False
24 un' fn bnames (P Bound x _) (P Bound y _)
25 | (x,y) `elem` bnames = return []
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 _)
33 | fst (bnames!!i) == x || snd (bnames!!i) == x = return []
34 un' fn bnames (P Bound x _) (V i)
35 | fst (bnames!!i) == x || snd (bnames!!i) == x = return []
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
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)
49 = do h1 <- uB bnames bx by
50 h2 <- un' False ((x,y):bnames) sx sy
51 combine bnames h1 h2
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
57 uB bnames (Let tx vx) (Let ty vy)
58 = do h1 <- un' False bnames tx ty
59 h2 <- un' False bnames ty vy
60 combine bnames h1 h2
61 uB bnames (Guess tx vx) (Guess ty vy)
62 = do h1 <- un' False bnames tx ty
63 h2 <- un' False bnames ty vy
64 combine bnames h1 h2
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
69 uB bnames _ _ = fail "Can't unify"
71 combine bnames as [] = return as
72 combine bnames as ((n, t) : bs)
73 = case lookup n as of
74 Nothing -> combine bnames (as ++ [(n,t)]) bs
75 Just t' -> do un' False bnames t t'
76 combine bnames as bs
78holeIn :: Env -> Name -> Bool
79holeIn env n = case lookup n env of
80 Just (Hole _) -> True
81 _ -> False