git.iko.soy/Idris-dev
on d9516ef help sign in
Idris-dev/src/Core/Unify.hs
139 lines 5.5 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
29 (un' False [] (normalise ctxt env topx) (normalise ctxt env topy))
30 (UI 0 [] []) of
31 OK (v, UI _ inj fails) -> return (filter notTrivial v, inj, reverse fails)
32-- OK (_, UI s _ ((_,_,f):fs)) -> tfail $ CantUnify topx topy f s
33 Error e -> tfail e
34 where
35 notTrivial (x, P _ x' _) = x /= x'
36 notTrivial _ = True
38 injective (P (DCon _ _) _ _) = True
39 injective (P (TCon _ _) _ _) = True
40 injective (App f a) = injective f
41 injective _ = False
43 notP (P _ _ _) = False
44 notP _ = True
46 sc i = do UI s x f <- get
47 put (UI (s+i) x f)
49 uplus u1 u2 = do UI s i f <- get
50 r <- u1
51 UI s _ f' <- get
52 if (length f == length f')
53 then return r
54 else do put (UI s i f); u2
56 un' :: Bool -> [(Name, Name)] -> TT Name -> TT Name ->
57 StateT UInfo
58 TC [(Name, TT Name)]
59 un' fn bnames (P Bound x _) (P Bound y _)
60 | (x,y) `elem` bnames = do sc 1; return []
61 un' fn bnames (P Bound x _) tm
62 | holeIn env x = do UI s i f <- get
63 when (notP tm && fn) $ put (UI s ((tm, topx, topy) : i) f)
64 sc 1
65 return [(x, tm)]
66 un' fn bnames tm (P Bound y _)
67 | holeIn env y = do UI s i f <- get
68 when (notP tm && fn) $ put (UI s ((tm, topx, topy) : i) f)
69 sc 1
70 return [(y, tm)]
71 un' fn bnames (V i) (P Bound x _)
72 | fst (bnames!!i) == x || snd (bnames!!i) == x = do sc 1; return []
73 un' fn bnames (P Bound x _) (V i)
74 | fst (bnames!!i) == x || snd (bnames!!i) == x = do sc 1; return []
76 un' fn bnames (App fx ax) (App fy ay)
77 = do uplus -- do the second one if the first adds any errors
78 (do hf <- un' True bnames fx fy
79 let ax' = normalise ctxt env (substNames hf ax)
80 let ay' = normalise ctxt env (substNames hf ay)
81 ha <- un' False bnames ax' ay'
82 sc 1
83 combine bnames hf ha)
84 (do ha <- un' False bnames ax ay
85 let fx' = normalise ctxt env (substNames ha fx)
86 let fy' = normalise ctxt env (substNames ha fy)
87 hf <- un' False bnames fx' fy'
88 sc 1
89 combine bnames hf ha)
91 un' fn bnames x (Bind n (Lam t) (App y (P Bound n' _)))
92 | n == n' = un' False bnames x y
93 un' fn bnames (Bind n (Lam t) (App x (P Bound n' _))) y
94 | n == n' = un' False bnames x y
95 un' fn bnames (Bind x bx sx) (Bind y by sy)
96 = do h1 <- uB bnames bx by
97 h2 <- un' False ((x,y):bnames) sx sy
98 combine bnames h1 h2
99 un' fn bnames x y
100 | OK True <- convEq' ctxt x y = do sc 1; return []
101 | otherwise = do UI s i f <- get
102 let err = CantUnify topx topy (CantUnify x y (Msg "") s) s
103 put (UI s i ((x, y, env, err) : f))
104 return [] -- lift $ tfail err
106 uB bnames (Let tx vx) (Let ty vy)
107 = do h1 <- un' False bnames tx ty
108 h2 <- un' False bnames ty vy
109 sc 1
110 combine bnames h1 h2
111 uB bnames (Guess tx vx) (Guess ty vy)
112 = do h1 <- un' False bnames tx ty
113 h2 <- un' False bnames ty vy
114 sc 1
115 combine bnames h1 h2
116 uB bnames (Lam tx) (Lam ty) = do sc 1; un' False bnames tx ty
117 uB bnames (Pi tx) (Pi ty) = do sc 1; un' False bnames tx ty
118 uB bnames (Hole tx) (Hole ty) = un' False bnames tx ty
119 uB bnames (PVar tx) (PVar ty) = un' False bnames tx ty
120 uB bnames x y = do UI s i f <- get
121 let err = CantUnify topx topy
122 (CantUnify (binderTy x) (binderTy y) (Msg "") s)
123 s
124 put (UI s i ((binderTy x, binderTy y, env, err) : f))
125 return [] -- lift $ tfail err
127 combine bnames as [] = return as
128 combine bnames as ((n, t) : bs)
129 = case lookup n as of
130 Nothing -> combine bnames (as ++ [(n,t)]) bs
131 Just t' -> do un' False bnames t t'
132 sc 1
133 combine bnames as bs
135holeIn :: Env -> Name -> Bool
136holeIn env n = case lookup n env of
137 Just (Hole _) -> True
138 _ -> False