git.iko.soy/Idris-dev
on cbc60eb help sign in
Idris-dev/src/Unify.hs
80 lines 3.0 kB history raw
1{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, DeriveFunctor #-}
3module Unify(unify) where
5import Core
6import 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 (Bind x bx sx) (Bind y by sy)
32 = do h1 <- uB bnames bx by
33 h2 <- un' ((x,y):bnames) sx sy
34 combine bnames h1 h2
35 un' bnames x y | x == y = return []
36 | otherwise = fail "Can't unify"
38 uB bnames (Let tx vx) (Let ty vy)
39 = do h1 <- un' bnames tx ty
40 h2 <- un' bnames ty vy
41 combine bnames h1 h2
42 uB bnames (Guess tx vx) (Guess ty vy)
43 = do h1 <- un' bnames tx ty
44 h2 <- un' bnames ty vy
45 combine bnames h1 h2
46 uB bnames (Lam tx) (Lam ty) = un' bnames tx ty
47 uB bnames (Pi tx) (Pi ty) = un' bnames tx ty
48 uB bnames (Hole tx) (Hole ty) = un' bnames tx ty
49 uB bnames (PVar tx) (PVar ty) = un' bnames tx ty
50 uB bnames _ _ = fail "Can't unify"
52 uApp bnames (xp@(P xnt x xty), xargs) (yp@(P ynt y yty), yargs)
53 | (x == y && all okToUnify [xnt, ynt]) ||
54 (holeIn env x && okToUnify ynt) ||
55 (okToUnify xnt && holeIn env y)
56 = do h <- un' bnames xp yp
57 hargs <- zipWithM (un' bnames) xargs yargs
58 h' <- foldM (combine bnames) [] hargs
59 combine bnames h h'
60 uApp bnames (xf, xargs) (yf, yargs)
61 = do un' bnames xf yf -- ignore result
62 hargs <- zipWithM (un' bnames) xargs yargs
63 foldM (combine bnames) [] hargs
65 okToUnify (DCon _ _) = True
66 okToUnify (TCon _) = True
67 okToUnify _ = False
69 combine bnames as [] = return as
70 combine bnames as ((n, t) : bs)
71 = case lookup n as of
72 Nothing -> combine bnames (as ++ [(n,t)]) bs
73 Just t' -> do un' bnames t t'
74 combine bnames as bs
76holeIn :: Env -> Name -> Bool
77holeIn env n = case lookup n env of
78 Just (Hole _) -> True
79 _ -> False