git.iko.soy/Idris-dev
on e613365 help sign in
Idris-dev/src/Core/Unify.hs
95 lines 3.5 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 x y
18 = --case un' [] x y of -- try without normalising first, for speed
19 -- OK v -> return v
20 -- _ ->
21 case un' [] (normalise ctxt env x) (normalise ctxt env y) of
22 OK v -> return v
23 _ -> fail $ "Can't unify " ++ showEnv env x ++ " and " ++ showEnv env y
24 where
25 un' bnames (P Bound x _) (P Bound y _)
26 | (x,y) `elem` bnames = return []
27 un' bnames (P Bound x _) tm
28 | holeIn env x = return [(x, tm)]
29 un' bnames tm (P Bound y _)
30 | holeIn env y = return [(y, tm)]
32 un' bnames x@(App _ _) y@(App _ _)
33 = uApp bnames (unApply x) (unApply y)
34 un' bnames x (Bind n (Lam t) (App y (P Bound n' _)))
35 | n == n' = un' bnames x y
36 un' bnames (Bind n (Lam t) (App x (P Bound n' _))) y
37 | n == n' = un' bnames x y
38 un' bnames (Bind x bx sx) (Bind y by sy)
39 = do h1 <- uB bnames bx by
40 h2 <- un' ((x,y):bnames) sx sy
41 combine bnames h1 h2
42 un' bnames x y | x == y = return []
43 | otherwise = fail "Can't unify"
45 uB bnames (Let tx vx) (Let ty vy)
46 = do h1 <- un' bnames tx ty
47 h2 <- un' bnames ty vy
48 combine bnames h1 h2
49 uB bnames (Guess tx vx) (Guess ty vy)
50 = do h1 <- un' bnames tx ty
51 h2 <- un' bnames ty vy
52 combine bnames h1 h2
53 uB bnames (Lam tx) (Lam ty) = un' bnames tx ty
54 uB bnames (Pi tx) (Pi ty) = un' bnames tx ty
55 uB bnames (Hole tx) (Hole ty) = un' bnames tx ty
56 uB bnames (PVar tx) (PVar ty) = un' bnames tx ty
57 uB bnames _ _ = fail "Can't unify"
59 uApp bnames (xp@(P xnt x xty), xargs) (yp@(P ynt y yty), yargs)
60 | (x == y && all okToUnify [xnt, ynt]) ||
61 (holeIn env x && okToUnify ynt) ||
62 (okToUnify xnt && holeIn env y)
63 = do h <- un' bnames xp yp
64 uArgs bnames h xargs yargs
65 uApp bnames (xf, xargs) (yf, yargs)
66 = do un' bnames xf yf -- ignore result
67 uArgs bnames [] xargs yargs
69 okToUnify (DCon _ _) = True
70 okToUnify (TCon _) = True
71 okToUnify _ = False
73 uArgs bnames h [] [] = return h
74 uArgs bnames h (x:xs) (y:ys) =
75 case un' bnames x y of
76 OK h' -> do next <- combine bnames h h'
77 uArgs bnames next xs ys
78 _ -> do let x' = normalise ctxt env (substNames h x)
79 let y' = normalise ctxt env (substNames h y)
80 h' <- un' bnames x' y'
81 next <- combine bnames h h'
82 uArgs bnames next xs ys
84 combine bnames as [] = return as
85 combine bnames as ((n, t) : bs)
86 = case lookup n as of
87 Nothing -> combine bnames (as ++ [(n,t)]) bs
88 Just t' -> do un' bnames t t'
89 combine bnames as bs
91holeIn :: Env -> Name -> Bool
92holeIn env n = case lookup n env of
93 Just (Hole _) -> True
94 _ -> False