git.iko.soy/Idris-dev
on 35ec145 help sign in
Idris-dev/src/Core/Unify.hs
145 lines 5.8 kB history raw
1{-# LANGUAGE PatternGuards #-}
3module Core.Unify(unify, Fails) where
5import Core.TT
6import Core.Evaluate
8import Control.Monad
9import Control.Monad.State
10import Debug.Trace
12-- Unification is applied inside the theorem prover. We're looking for holes
13-- which can be filled in, by matching one term's normal form against another.
14-- Returns a list of hole names paired with the term which solves them, and
15-- a list of things which need to be injective.
17-- terms which need to be injective, with the things we're trying to unify
18-- at the time
20type Injs = [(TT Name, TT Name, TT Name)]
21type Fails = [(TT Name, TT Name, Env, Err)]
23data UInfo = UI Int Injs Fails
25unify :: Context -> Env -> TT Name -> TT Name -> TC ([(Name, TT Name)],
26 Injs, Fails)
27unify ctxt env topx topy
28 = -- case runStateT (un' False [] topx topy) (UI 0 [] []) of
29 -- OK (v, UI _ inj []) -> return (filter notTrivial v, inj, [])
30 let topxn = normalise ctxt env topx
31 topyn = normalise ctxt env topy in
32 case runStateT (un' False [] topxn topyn)
33 (UI 0 [] []) of
34 OK (v, UI _ inj fails) -> return (filter notTrivial v, inj, reverse fails)
35-- OK (_, UI s _ ((_,_,f):fs)) -> tfail $ CantUnify topx topy f s
36 Error e -> tfail e
37 where
38 notTrivial (x, P _ x' _) = x /= x'
39 notTrivial _ = True
41 injective (P (DCon _ _) _ _) = True
42 injective (P (TCon _ _) _ _) = True
43 injective (App f a) = injective f
44 injective _ = False
46 notP (P _ _ _) = False
47 notP _ = True
49 sc i = do UI s x f <- get
50 put (UI (s+i) x f)
52 uplus u1 u2 = do UI s i f <- get
53 r <- u1
54 UI s _ f' <- get
55 if (length f == length f')
56 then return r
57 else do put (UI s i f); u2
59 un' :: Bool -> [(Name, Name)] -> TT Name -> TT Name ->
60 StateT UInfo
61 TC [(Name, TT Name)]
62 un' fn bnames (P Bound x _) (P Bound y _)
63 | (x,y) `elem` bnames = do sc 1; return []
64 un' fn bnames (P Bound x _) tm
65 | holeIn env x = do UI s i f <- get
66 when (notP tm && fn) $ put (UI s ((tm, topx, topy) : i) f)
67 sc 1
68 return [(x, tm)]
69 un' fn bnames tm (P Bound y _)
70 | holeIn env y = do UI s i f <- get
71 when (notP tm && fn) $ put (UI s ((tm, topx, topy) : i) f)
72 sc 1
73 return [(y, tm)]
74 un' fn bnames (V i) (P Bound x _)
75 | fst (bnames!!i) == x || snd (bnames!!i) == x = do sc 1; return []
76 un' fn bnames (P Bound x _) (V i)
77 | fst (bnames!!i) == x || snd (bnames!!i) == x = do sc 1; return []
79 un' fn bnames (App fx ax) (App fy ay)
80 = do uplus -- do the second one if the first adds any errors
81 (do hf <- un' True bnames fx fy
82 let ax' = hnormalise hf ctxt env (substNames hf ax)
83 let ay' = hnormalise hf ctxt env (substNames hf ay)
84 ha <- un' False bnames ax' ay'
85 sc 1
86 combine bnames hf ha)
87 (do ha <- un' False bnames ax ay
88 let fx' = hnormalise ha ctxt env (substNames ha fx)
89 let fy' = hnormalise ha ctxt env (substNames ha fy)
90 hf <- un' False bnames fx' fy'
91 sc 1
92 combine bnames hf ha)
93 where hnormalise [] _ _ t = t
94 hnormalise ns ctxt env t = normalise ctxt env t
95 un' fn bnames x (Bind n (Lam t) (App y (P Bound n' _)))
96 | n == n' = un' False bnames x y
97 un' fn bnames (Bind n (Lam t) (App x (P Bound n' _))) y
98 | n == n' = un' False bnames x y
99 un' fn bnames (Bind x bx sx) (Bind y by sy)
100 = do h1 <- uB bnames bx by
101 h2 <- un' False ((x,y):bnames) sx sy
102 combine bnames h1 h2
103 un' fn bnames x y
104 | OK True <- convEq' ctxt x y = do sc 1; return []
105 | otherwise = do UI s i f <- get
106 let err = CantUnify topx topy (CantUnify x y (Msg "") [] s) (errEnv env) s
107 put (UI s i ((x, y, env, err) : f))
108 return [] -- lift $ tfail err
110 uB bnames (Let tx vx) (Let ty vy)
111 = do h1 <- un' False bnames tx ty
112 h2 <- un' False bnames ty vy
113 sc 1
114 combine bnames h1 h2
115 uB bnames (Guess tx vx) (Guess ty vy)
116 = do h1 <- un' False bnames tx ty
117 h2 <- un' False bnames ty vy
118 sc 1
119 combine bnames h1 h2
120 uB bnames (Lam tx) (Lam ty) = do sc 1; un' False bnames tx ty
121 uB bnames (Pi tx) (Pi ty) = do sc 1; un' False bnames tx ty
122 uB bnames (Hole tx) (Hole ty) = un' False bnames tx ty
123 uB bnames (PVar tx) (PVar ty) = un' False bnames tx ty
124 uB bnames x y = do UI s i f <- get
125 let err = CantUnify topx topy
126 (CantUnify (binderTy x) (binderTy y) (Msg "") [] s)
127 (errEnv env) s
128 put (UI s i ((binderTy x, binderTy y, env, err) : f))
129 return [] -- lift $ tfail err
131 combine bnames as [] = return as
132 combine bnames as ((n, t) : bs)
133 = case lookup n as of
134 Nothing -> combine bnames (as ++ [(n,t)]) bs
135 Just t' -> do un' False bnames t t'
136 sc 1
137 combine bnames as bs
139errEnv = map (\(x, b) -> (x, binderTy b))
141holeIn :: Env -> Name -> Bool
142holeIn env n = case lookup n env of
143 Just (Hole _) -> True
144 _ -> False