git.iko.soy/Idris-dev
on master help sign in
In type-directed search, handle an additional possible case when processing unification results.
7395bdebmsherman
src/Idris/TypeSearch.hs+21−21
compare with master
unifiedsplit
@@ -8,6 +8,7 @@ import Control.Monad (forM_, guard)
8
8
9import Data.Function (on)
9import Data.Function (on)
10import Data.List (find, sortBy, (\\))
10import Data.List (find, sortBy, (\\))
11+import Data.Map (Map)
11import qualified Data.Map as M
12import qualified Data.Map as M
12import Data.Maybe (catMaybes, fromMaybe, isJust)
13import Data.Maybe (catMaybes, fromMaybe, isJust)
13import Data.Monoid (Monoid (mempty, mappend))
14import Data.Monoid (Monoid (mempty, mappend))
@@ -102,7 +103,7 @@ reverseDag xs = map f xs where
102computeDagP :: Ord n => TT n -> ([((n, TT n), Set n)], TT n)
103computeDagP :: Ord n => TT n -> ([((n, TT n), Set n)], TT n)
103computeDagP t = (reverse (map f args), retTy) where
104computeDagP t = (reverse (map f args), retTy) where
104
105
105− f (n, t) = ((n, t), usedVars t)
106+ f (n, t) = ((n, t), M.keysSet (usedVars t))
106
107
107 (numArgs, args, retTy) = go 0 [] t
108 (numArgs, args, retTy) = go 0 [] t
108
109
@@ -110,17 +111,17 @@ computeDagP t = (reverse (map f args), retTy) where
110 go k args (Bind n (Pi t) sc) = go (succ k) ( (n, t) : args ) sc
111 go k args (Bind n (Pi t) sc) = go (succ k) ( (n, t) : args ) sc
111 go k args retTy = (k, args, retTy)
112 go k args retTy = (k, args, retTy)
112
113
113− usedVars :: Ord n => TT n -> Set n
114− usedVars (V j) = error "unexpected! run vToP first"
115− usedVars (P Bound n t) = S.singleton n `S.union` usedVars t
116− usedVars (Bind n binder t2) = (S.delete n (usedVars t2) `S.union`) $ case binder of
117− Let t v -> usedVars t `S.union` usedVars v
118− Guess t v -> usedVars t `S.union` usedVars v
119− b -> usedVars (binderTy b)
120− usedVars (App t1 t2) = usedVars t1 `S.union` usedVars t2
121− usedVars (Proj t _) = usedVars t
122− usedVars _ = S.empty
123
114
115+usedVars :: Ord n => TT n -> Map n (TT n)
116+usedVars (V j) = error "unexpected! run vToP first"
117+usedVars (P Bound n t) = M.singleton n t `M.union` usedVars t
118+usedVars (Bind n binder t2) = (M.delete n (usedVars t2) `M.union`) $ case binder of
119+ Let t v -> usedVars t `M.union` usedVars v
120+ Guess t v -> usedVars t `M.union` usedVars v
121+ b -> usedVars (binderTy b)
122+usedVars (App t1 t2) = usedVars t1 `M.union` usedVars t2
123+usedVars (Proj t _) = usedVars t
124+usedVars _ = M.empty
124
125
125deleteFromDag :: Ord n => n -> [((n, TT n), (a, Set n))] -> [((n, TT n), (a, Set n))]
126deleteFromDag :: Ord n => n -> [((n, TT n), (a, Set n))] -> [((n, TT n), (a, Set n))]
126deleteFromDag name [] = []
127deleteFromDag name [] = []
@@ -205,18 +206,17 @@ unifyWithHoles debugParam istate type1 = \type2 -> let
205 mgetType name xs = fmap ((snd . fst) &&& (fst . snd)) . find ((name ==) . fst . fst) $ xs
206 mgetType name xs = fmap ((snd . fst) &&& (fst . snd)) . find ((name ==) . fst . fst) $ xs
206
207
207 updateDags ((name, term) : xs) (holes, args1, args2) = case (mgetType name args1, mgetType name args2) of
208 updateDags ((name, term) : xs) (holes, args1, args2) = case (mgetType name args1, mgetType name args2) of
208− (Just _, Nothing) -> thrd (\score -> score { leftApplied = succ (leftApplied score) }) <$>
209+ (Just (_,ix), Nothing) -> thrd (\score -> score { leftApplied = succ (leftApplied score) }) <$> nextStep
209− updateDags xs (holes', updatef args1, args2)
210− (Nothing, Just _) -> thrd (\score -> score { rightApplied = succ (rightApplied score) }) <$>
210+ (Nothing, Just (_, ix)) -> thrd (\score -> score { rightApplied = succ (rightApplied score) }) <$> nextStep
211− updateDags xs (holes', args1, updatef args2)
211+ (Nothing, Nothing) -> nextStep
212− _ -> error "Shouldn't happen. Watch the alpha conversion!"
212+ _ -> error ("Shouldn't happen. Watch the alpha conversion!\n" ++ show args1 ++ "\n\n" ++ show args2)
213 where
213 where
214+ varsInTy = map fst $ M.toList (usedVars term)
215+ deleteMany = foldr (.) id $ map deleteFromDag (name : varsInTy)
214 thrd f (a,b,c) = (a,b,f c)
216 thrd f (a,b,c) = (a,b,f c)
215− holes' = holes \\ [name]
217+ nextStep = updateDags xs (holes \\ [name], updatef args1, updatef args2 )
216− updatef = map (first . second $ subst name term) . deleteFromDag name
217− args1' = deleteFromDag name args1
218− args1'' = map (first . second $ subst name term) args1'
218+ updatef = map (first . second $ subst name term) . deleteMany
219− mgetType name xs = fmap (snd . fst) . find ((name ==) . fst . fst) $ xs
219+ mgetType name xs = fmap ((snd . fst) &&& (fst . snd)) . find ((name ==) . fst . fst) $ xs
220
220
221
221
222 go :: State -> [(Type, Type)] -> Maybe State
222 go :: State -> [(Type, Type)] -> Maybe State