git.iko.soy/Idris-dev
on 2402885 help sign in
Idris-dev/src/Core/Unify.hs
92 lines 3.4 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.
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)]
17unify ctxt env topx topy
18 = case un' [] (normalise ctxt env topx) (normalise ctxt env topy) of
19 OK v -> return v
20 _ -> tfail $ CantUnify topx topy
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 uArgs bnames h xargs yargs
62 uApp bnames (xf, xargs) (yf, yargs)
63 = do un' bnames xf yf -- ignore result
64 uArgs bnames [] xargs yargs
66 okToUnify (DCon _ _) = True
67 okToUnify (TCon _) = True
68 okToUnify _ = False
70 uArgs bnames h [] [] = return h
71 uArgs bnames h (x:xs) (y:ys) =
72 case un' bnames x y of
73 OK h' -> do next <- combine bnames h h'
74 uArgs bnames next xs ys
75 _ -> do let x' = normalise ctxt env (substNames h x)
76 let y' = normalise ctxt env (substNames h y)
77 h' <- un' bnames x' y'
78 next <- combine bnames h h'
79 uArgs bnames next xs ys
81 combine bnames as [] = return as
82 combine bnames as ((n, t) : bs)
83 = case lookup n as of
84 Nothing -> combine bnames (as ++ [(n,t)]) bs
85 Just t' -> do un' bnames t t'
86 combine bnames as bs
88holeIn :: Env -> Name -> Bool
89holeIn env n = case lookup n env of
90 Just (Hole _) -> True
91 _ -> False