@@ -1,13 +1,13 @@
1−module Idris.TypeSearch (
1+module Idris.TypeSearch {- (
22 searchByType, searchPred, defaultScoreFunction
3−) where
3+) -} where
44
55import Control.Applicative ((<$>), (<*>), (<|>))
66import Control.Arrow (first, second, (&&&))
77import Control.Monad (forM_, guard)
88
99import Data.Function (on)
10−import Data.List (find, minimumBy, partition, sortBy, (\\))
10+import Data.List (find, delete, deleteBy, minimumBy, partition, sortBy, (\\))
1111import Data.Map (Map)
1212import qualified Data.Map as M
1313import Data.Maybe (catMaybes, fromMaybe, isJust, maybeToList)
@@ -112,7 +112,7 @@ computeDagP :: Ord n
112112 -> TT n
113113 -> ([((n, TT n), Set n)], [(n, TT n)], TT n)
114114computeDagP removePred t = (reverse (map f args), reverse removedArgs , retTy) where
115− f (n, t) = ((n, t), M.keysSet (usedVars t))
115+ f (n, t) = ((n, t), M.keysSet (usedVars False t))
116116
117117 (numArgs, args, removedArgs, retTy) = go 0 [] [] t
118118
@@ -124,16 +124,19 @@ computeDagP removePred t = (reverse (map f args), reverse removedArgs , retTy) w
124124 go k args removedArgs retTy = (k, args, removedArgs, retTy)
125125
126126-- | Collect the names and types of all the free variables
127−usedVars :: Ord n => TT n -> Map n (TT n)
128−usedVars (V j) = error "unexpected! run vToP first"
129−usedVars (P Bound n t) = M.singleton n t `M.union` usedVars t
130−usedVars (Bind n binder t2) = (M.delete n (usedVars t2) `M.union`) $ case binder of
131− Let t v -> usedVars t `M.union` usedVars v
132− Guess t v -> usedVars t `M.union` usedVars v
133− b -> usedVars (binderTy b)
134−usedVars (App t1 t2) = usedVars t1 `M.union` usedVars t2
135−usedVars (Proj t _) = usedVars t
136−usedVars _ = M.empty
127+usedVars :: Ord n
128+ => Bool -- ^ only collect variables which must be determined due to injectivity
129+ -> TT n -> Map n (TT n)
130+usedVars inj = f where
131+ f (P Bound n t) = M.singleton n t `M.union` f t
132+ f (Bind n binder t2) = (M.delete n (f t2) `M.union`) $ case binder of
133+ Let t v -> f t `M.union` f v
134+ Guess t v -> f t `M.union` f v
135+ b -> f (binderTy b)
136+ f (App t1 t2) = f t1 `M.union` (if not inj || isInjective t1 then f t2 else M.empty)
137+ f (Proj t _) = f t
138+ f (V j) = error "unexpected! run vToP first"
139+ f _ = M.empty
137140
138141deleteFromDag :: Ord n => n -> [((n, TT n), (a, Set n))] -> [((n, TT n), (a, Set n))]
139142deleteFromDag name [] = []
@@ -179,7 +182,7 @@ type ArgsDAG = [((Name, Type), (Int, Set Name))]
179182
180183-- | The state corresponding to an attempted match of two types.
181184data State = State
182− { holes :: ![Name] -- ^ names which have yet to be resolved
185+ { holes :: ![(Name, Type)] -- ^ names which have yet to be resolved
183186 , args1 :: !ArgsDAG -- ^ arguments for the left type which have yet to be resolved
184187 , args2 :: !ArgsDAG -- ^ arguments for the right type which have yet to be resolved
185188 , classes1 :: ![(Name, Type)] -- ^ typeclass arguments for the left type which haven't been resolved
@@ -245,22 +248,23 @@ instance Ord Score where
245248-- types can be matched.
246249unifyWithHoles :: IState -> Int -> Type -> Type -> Maybe Score
247250unifyWithHoles istate maxScore type1 = \type2 -> let
248− (dag2, typeClassArgs2, retTy2) = makeDag (uniqueBinders argNames1 type2)
249− argNames2 = map (fst . fst) dag2
251+ (dag2, typeClassArgs2, retTy2) = makeDag (uniqueBinders (map fst argNames1) type2)
252+ argNames2 = map fst dag2
253+ usedNames = map fst (argNames1 ++ argNames2)
250254 startingHoles = argNames1 ++ argNames2
251255
252256 startingTypes = (retTy1, retTy2) : []
253257 in do
254258 state <- unifyQueue (State startingHoles dag1 dag2
255259 typeClassArgs1 typeClassArgs2
256− mempty startingHoles) startingTypes
260+ mempty usedNames) startingTypes
257261 getResults (Q.singleton (score state) state)
258262 where
259263 ctxt = tt_ctxt istate
260264 classInfo = idris_classes istate
261265
262266 (dag1, typeClassArgs1, retTy1) = makeDag type1
263− argNames1 = map (fst . fst) dag1
267+ argNames1 = map fst dag1
264268 makeDag :: Type -> (ArgsDAG, [(Name, Type)], Type)
265269 makeDag = first3 (zipWith (\i (ty, deps) -> (ty, (i, deps))) [0..] . reverseDag) .
266270 computeDagP (isTypeClassArg classInfo) . vToP
@@ -282,7 +286,7 @@ unifyWithHoles istate maxScore type1 = \type2 -> let
282286 findArgs = ((,) <$> findLeft name state <*> findRight name2 state) <|>
283287 ((,) <$> findLeft name2 state <*> findRight name state)
284288 matchnames = [name, name2]
285− holes' = holes \\ matchnames
289+ holes' = filter (not . (`elem` matchnames) . fst) holes
286290 deleteArgs = deleteLeft name . deleteLeft name2 . deleteRight name . deleteRight name2
287291 state' = modifyTypes (subst name term) $ deleteArgs
288292 (state { holes = holes'})
@@ -294,13 +298,15 @@ unifyWithHoles istate maxScore type1 = \type2 -> let
294298 (Nothing, Nothing) -> nextStep
295299 _ -> error ("Shouldn't happen. Watch the alpha conversion!\n" ++ show args1 ++ "\n\n" ++ show args2)
296300 where
297− varsInTy = map fst $ M.toList (usedVars term) --[]
301+ -- find variables which are determined uniquely by the type
302+ -- due to injectivity
303+ varsInTy = M.keys $ usedVars True term --[]
298304 toDelete = name : varsInTy
299305 deleteMany = foldr (.) id $ [ deleteLeft t . deleteRight t | t <- toDelete ]
300306
301307 inScore f state = state { score = f (score state) }
302308 state' = modifyTypes (subst name term) . deleteMany $
303− state { holes = holes \\ toDelete }
309+ state { holes = filter (not . (`elem` toDelete) . fst) holes }
304310 nextStep = resolveUnis xs state'
305311
306312
@@ -309,7 +315,7 @@ unifyWithHoles istate maxScore type1 = \type2 -> let
309315 unifyQueue state [] = return state
310316 unifyQueue state ((ty1, ty2) : queue) = do
311317 --trace ("go: \n" ++ show state) True `seq` return ()
312− res <- tcToMaybe $ match_unify ctxt [] ty1 ty2 [] (holes state) []
318+ res <- tcToMaybe $ match_unify ctxt [ (n, Pi ty) | (n, ty) <- holes state] ty1 ty2 [] (map fst $ holes state) []
313319 (state', queueAdditions) <- resolveUnis res state
314320 guard $ scoreCriterion (score state')
315321 unifyQueue state' (queue ++ queueAdditions)
@@ -386,6 +392,6 @@ unifyWithHoles istate maxScore type1 = \type2 -> let
386392 canBeFirst = map fst . filter (S.null . snd . snd)
387393
388394 -- try to match an argument from the left with an argument from the right
389− results1 = catMaybes [ unifyQueue (State (holes \\ [n1, n2]) (deleteFromDag n1 dag1)
395+ results1 = catMaybes [ unifyQueue (State (filter (not . (`elem` [n1,n2]) . fst) holes) (deleteFromDag n1 dag1)
390396 ((inArgTys subst2for1) $ deleteFromDag n2 dag2) c1 (map (second subst2for1) c2) scoreAcc usedNames) [(ty1, ty2)]
391397 | (n1, ty1) <- canBeFirst dag1, (n2, ty2) <- canBeFirst dag2, let subst2for1 = psubst n2 (P Bound n1 ty1)]