@@ -7,7 +7,7 @@ import Control.Arrow (first, second, (&&&))
77import Control.Monad (forM_, guard)
88
99import Data.Function (on)
10−import Data.List (find, minimumBy, sortBy, (\\))
10+import Data.List (find, minimumBy, partition, sortBy, (\\))
1111import Data.Map (Map)
1212import qualified Data.Map as M
1313import Data.Maybe (catMaybes, fromMaybe, isJust)
@@ -20,7 +20,7 @@ import Idris.AbsSyntaxTree (class_instances, defaultSyntax, Idris,
2020 IState (idris_classes, idris_docstrings, tt_ctxt),
2121 implicitAllowed, prettyDocumentedIst, prettyIst, PTerm, toplevel)
2222import Idris.Core.Evaluate (Context (definitions), Def (Function, TyDecl, CaseOp), normaliseC)
23−import Idris.Core.TT
23+import Idris.Core.TT hiding (score)
2424import Idris.Core.Unify (match_unify)
2525import Idris.Delaborate (delab, delabTy)
2626import Idris.Docstrings (noDocs, overview)
@@ -54,7 +54,7 @@ searchByType h pterm = do
5454 syn = defaultSyntax { implicitAllowed = True } -- syntax
5555 n = sMN 0 "searchType" -- name
5656
57−
57+-- | Conduct a type-directed search using a given match predicate
5858searchUsing :: (IState -> Type -> Type -> Maybe a) -> IState -> Type -> [(Name, (Type, a))]
5959searchUsing pred istate ty =
6060 concat . M.elems $ M.mapWithKey (\key -> M.toAscList . M.mapMaybe (f key)) (definitions ctxt)
@@ -64,7 +64,6 @@ searchUsing pred istate ty =
6464 guard $ not (special k)
6565 y <- get (fst4 x)
6666 let ny = normaliseC ctxt [] y
67− -- traceShow k False `seq` return ()
6867 val <- pred istate nty ny
6968 return (y, val)
7069 nty = normaliseC ctxt [] ty
@@ -80,42 +79,49 @@ searchUsing pred istate ty =
8079 special (SN _) = True
8180 special _ = False
8281
83−
84−tcToMaybe :: TC' e a -> Maybe a
85−tcToMaybe (OK x) = Just x
86−tcToMaybe (Error _) = Nothing
87−
88−
89−
82+-- Our default search predicate.
9083searchPred :: IState -> Type -> Type -> Maybe Score
9184searchPred istate ty1 = \ty2 -> case matcher ty2 of
92− Nothing -> Nothing
93− Just xs -> guard (not (null xs)) >> return (minimumBy (compare `on` defaultScoreFunction) xs)
85+ xs -> guard (not (null xs)) >> return (minimumBy (compare `on` defaultScoreFunction) xs)
9486 where
95− matcher = unifyWithHoles True istate ty1
96−
87+ matcher = unifyWithHoles istate ty1
9788
9889
90+typeFromDef :: (Def, b, c, d) -> Maybe Type
91+typeFromDef (def, _, _, _) = get def where
92+ get :: Def -> Maybe Type
93+ get (Function ty tm) = Just ty
94+ get (TyDecl _ ty) = Just ty
95+ -- get (Operator ty _ _) = Just ty
96+ get (CaseOp _ ty _ _ _ _) = Just ty
97+ get _ = Nothing
9998
10099reverseDag :: Ord k => [((k, a), Set k)] -> [((k, a), Set k)]
101100reverseDag xs = map f xs where
102101 f ((k, v), _) = ((k, v), S.fromList . map (fst . fst) $ filter (S.member k . snd) xs)
103102
104103-- run vToP first!
104+-- | Compute a directed acyclic graph corresponding to the
105+-- arguments of a function.
105106-- returns [(the name and type of the bound variable
106107-- the names in the type of the bound variable)]
107−computeDagP :: Ord n => TT n -> ([((n, TT n), Set n)], TT n)
108−computeDagP t = (reverse (map f args), retTy) where
109−
108+computeDagP :: Ord n
109+ => (TT n -> Bool) -- ^ filter to remove some arguments
110+ -> TT n
111+ -> ([((n, TT n), Set n)], [(n, TT n)], TT n)
112+computeDagP removePred t = (reverse (map f args), reverse removedArgs , retTy) where
110113 f (n, t) = ((n, t), M.keysSet (usedVars t))
111114
112− (numArgs, args, retTy) = go 0 [] t
115+ (numArgs, args, removedArgs, retTy) = go 0 [] [] t
113116
114117 -- NOTE : args are in reverse order
115− go k args (Bind n (Pi t) sc) = go (succ k) ( (n, t) : args ) sc
116− go k args retTy = (k, args, retTy)
117−
118+ go k args removedArgs (Bind n (Pi t) sc) = let arg = (n, t) in
119+ if removePred t
120+ then go k args (arg : removedArgs) sc
121+ else go (succ k) (arg : args) removedArgs sc
122+ go k args removedArgs retTy = (k, args, removedArgs, retTy)
118123
124+-- | Collect the names and types of all the free variables
119125usedVars :: Ord n => TT n -> Map n (TT n)
120126usedVars (V j) = error "unexpected! run vToP first"
121127usedVars (P Bound n t) = M.singleton n t `M.union` usedVars t
@@ -133,6 +139,8 @@ deleteFromDag name (((name2, ty), (ix, set)) : xs) = (if name == name2
133139 then id
134140 else (((name2, ty) , (ix, S.delete name set)) :) ) (deleteFromDag name xs)
135141
142+deleteFromArgList :: Ord n => n -> [(n, TT n)] -> [(n, TT n)]
143+deleteFromArgList n = filter ((/= n) . fst)
136144
137145data Score = Score
138146 { transposition :: Int
@@ -143,17 +151,17 @@ data Score = Score
143151
144152displayScore :: Score -> Doc a
145153displayScore (Score trans lapp rapp lclass rclass) = text $ case (lt, gt) of
146− (True , True ) -> "="
147− (True , False) -> "<"
148− (False, True ) -> ">"
154+ (True , True ) -> "=" -- types are isomorphic
155+ (True , False) -> "<" -- found type is more general than searched type
156+ (False, True ) -> ">" -- searched type is more general than found type
149157 (False, False) -> " "
150158 where lt = lapp + lclass == 0
151159 gt = rapp + rclass == 0
152160
153161
154162scoreCriterion :: Score -> Bool
155−scoreCriterion (Score a b c d e) = True {- not
156− ( (b > 0 && c > 0) || (b + c) > 2 ) -}
163+scoreCriterion (Score a b c d e) = not
164+ ( (b > 0 && c > 0) || (b + c) > 4 || d > 3 || e > 3 )
157165
158166defaultScoreFunction :: Score -> Int
159167defaultScoreFunction (Score a b c d e) = a + 9*b + 3*c + 12*d + 4*e + 100*(2*b + d)*(2*c + e)
@@ -163,141 +171,184 @@ instance Monoid Score where
163171 mempty = Score 0 0 0 0 0
164172 (Score a b c d e) `mappend` (Score a' b' c' d' e') = Score (a + a') (b + b') (c + c') (d + d') (e + e')
165173
166−
174+-- | A directed acyclic graph representing the arguments to a function
175+-- The 'Int' represents the position of the argument (1st argument, 2nd, etc.)
167176type ArgsDAG = [((Name, Type), (Int, Set Name))]
168−type ResType = ( [Name] , ArgsDAG , ArgsDAG )
169177
178+-- | The state corresponding to an attempted match of two types.
170179data State = State
171− { holes :: ![Name]
172− , args1 :: !ArgsDAG
173− , args2 :: !ArgsDAG
174− , score :: !Score
175− }
180+ { holes :: ![Name] -- ^ names which have yet to be resolved
181+ , args1 :: !ArgsDAG -- ^ arguments for the left type which have yet to be resolved
182+ , args2 :: !ArgsDAG -- ^ arguments for the right type which have yet to be resolved
183+ , classes1 :: ![(Name, Type)] -- ^ typeclass arguments for the left type which haven't been resolved
184+ , classes2 :: ![(Name, Type)] -- & typeclass arguments for the right type which haven't been resolved
185+ , score :: !Score -- ^ the score so far
186+ , usedNames :: ![Name] -- ^ all names that have been used
187+ } deriving Show
188+
189+modifyTypes :: (Type -> Type) -> State -> State
190+modifyTypes f (State h a1 a2 c1 c2 s un) =
191+ State h (modifyDag a1) (modifyDag a2)
192+ (modifyList c1) (modifyList c2)
193+ s un
194+ where
195+ modifyDag = map (first (second f))
196+ modifyList = map (second f)
197+
198+findNameInArgsDAG :: Name -> ArgsDAG -> Maybe (Type, Maybe Int)
199+findNameInArgsDAG name xs = fmap ((snd . fst) &&& (Just . fst . snd)) . find ((name ==) . fst . fst) $ xs
200+
201+findLeft, findRight :: Name -> State -> Maybe (Type, Maybe Int)
202+findLeft n (State _ a1 a2 c1 c2 _ _) = findNameInArgsDAG n a1 <|> ((,) <$> lookup n c1 <*> Nothing)
203+findRight n (State _ a1 a2 c1 c2 _ _) = findNameInArgsDAG n a2 <|> ((,) <$> lookup n c2 <*> Nothing)
204+
205+deleteLeft, deleteRight :: Name -> State -> State
206+deleteLeft n state = state { args1 = deleteFromDag n (args1 state) , classes1 = filter ((/= n) . fst) (classes1 state) }
207+deleteRight n state = state { args2 = deleteFromDag n (args2 state) , classes2 = filter ((/= n) . fst) (classes2 state) }
208+
209+
210+tcToMaybe :: TC' e a -> Maybe a
211+tcToMaybe (OK x) = Just x
212+tcToMaybe (Error _) = Nothing
213+
214+inArgTys :: (Type -> Type) -> ArgsDAG -> ArgsDAG
215+inArgTys = map . first . second
176216
177217
178218--DONT run vToP first!
179−unifyWithHoles :: Bool -> IState -> Type -> Type -> Maybe [Score]
180−unifyWithHoles debugParam istate type1 = \type2 -> let
181− (dag2, retTy2) = makeDag (uniqueBinders argNames1 type2)
219+-- | Try to match two types together in a unification-like procedure.
220+-- Returns a list of possible scores representing ways in which the two
221+-- types can be matched.
222+unifyWithHoles :: IState -> Type -> Type -> [Score]
223+unifyWithHoles istate type1 = \type2 -> let
224+ (dag2, typeClassArgs2, retTy2) = makeDag (uniqueBinders argNames1 type2)
182225 argNames2 = map (fst . fst) dag2
183226 startingHoles = argNames1 ++ argNames2
184227
185228 startingTypes = (retTy1, retTy2) : []
186− in do
187− state <- go (State startingHoles dag1 dag2 mempty) startingTypes
188− return $ processDags state
229+ in case unifyQueue (State startingHoles dag1 dag2
230+ typeClassArgs1 typeClassArgs2
231+ mempty startingHoles) startingTypes
232+ of Nothing -> []
233+ Just state -> possibleMatches state
189234 where
190235 ctxt = tt_ctxt istate
191236 classInfo = idris_classes istate
192− (dag1, retTy1) = makeDag type1
193− argNames1 = map (fst . fst) dag1
194− makeDag = first (zipWith (\i (ty, deps) -> (ty, (i, deps))) [0..] . reverseDag) . computeDagP . vToP
195237
196− matchf :: (Name, Term) -> Maybe (Name, Name)
197− matchf (name, P Bound name2 _) = Just (name, name2)
198− matchf _ = Nothing
238+ isTypeClassArg :: Type -> Bool
239+ isTypeClassArg ty = not (null (getClassName clss >>= flip lookupCtxt classInfo)) where
240+ (clss, args) = unApply ty
241+ getClassName (P (TCon _ _) className _) = [className]
242+ getClassName _ = []
243+
244+ (dag1, typeClassArgs1, retTy1) = makeDag type1
245+ argNames1 = map (fst . fst) dag1
246+ makeDag :: Type -> (ArgsDAG, [(Name, Type)], Type)
247+ makeDag = first3 (zipWith (\i (ty, deps) -> (ty, (i, deps))) [0..] . reverseDag) . computeDagP isTypeClassArg . vToP
248+ first3 f (a,b,c) = (f a, b, c)
199249
200250 -- update our state with the unification resolutions
201− updateDags :: [(Name, Type)] -> ResType -> Maybe (ResType, [(Type, Type)], Score)
202− updateDags [] res = Just (res, [], mempty)
203− updateDags ((name, term@(P Bound name2 _)) : xs) (holes, args1, args2) | isJust findArgs = do
251+ resolveUnis :: [(Name, Type)] -> State -> Maybe (State, [(Type, Type)])
252+ resolveUnis [] state = Just (state, [])
253+ resolveUnis ((name, term@(P Bound name2 _)) : xs)
254+ state@(State holes args1 args2 _ _ _ _) | isJust findArgs = do
204255 ((ty1, ix1), (ty2, ix2)) <- findArgs
205256
206− (res, queue, score) <- updateDags xs (holes', args1'', args2'')
207− --traceShow (ty1, ty2) False `seq` return ()
208− return $ (res, (ty1, ty2) : queue , score { transposition = transposition score + abs (ix2 - ix1) })
257+ (state'', queue) <- resolveUnis xs state'
258+ let transScore = fromMaybe 0 (abs <$> ((-) <$> ix1 <*> ix2))
259+ return $ (inScore (\s -> s { transposition = transposition s + transScore }) state'', (ty1, ty2) : queue)
209260 where
210− findArgs = ((,) <$> mgetType name args1 <*> mgetType name2 args2) <|>
211− ((,) <$> mgetType name2 args1 <*> mgetType name args2)
261+ mgetType name xs = fmap ((snd . fst) &&& (fst . snd)) . find ((name ==) . fst . fst) $ xs
262+ inScore f state = state { score = f (score state) }
263+ findArgs = ((,) <$> findLeft name state <*> findRight name2 state) <|>
264+ ((,) <$> findLeft name2 state <*> findRight name state)
212265 matchnames = [name, name2]
213266 holes' = holes \\ matchnames
214− substf = deleteFromDag name . deleteFromDag name2
215− args1' = substf args1
216− args2' = substf args2
217− args1'' = map (first . second $ subst name term) args1'
218− args2'' = map (first . second $ subst name term) args2'
219− mgetType name xs = fmap ((snd . fst) &&& (fst . snd)) . find ((name ==) . fst . fst) $ xs
220−
221− updateDags ((name, term) : xs) (holes, args1, args2) = case (mgetType name args1, mgetType name args2) of
222− (Just (_,ix), Nothing) -> thrd (\score -> score { leftApplied = succ (leftApplied score) }) <$> nextStep
223− (Nothing, Just (_, ix)) -> thrd (\score -> score { rightApplied = succ (rightApplied score) }) <$> nextStep
267+ deleteArgs = deleteLeft name . deleteLeft name2 . deleteRight name . deleteRight name2
268+ state' = modifyTypes (subst name term) $ deleteArgs
269+ (state { holes = holes'})
270+
271+ resolveUnis ((name, term) : xs)
272+ state@(State holes args1 args2 _ _ _ _) = case (findLeft name state, findRight name state) of
273+ (Just (_,ix), Nothing) -> first (inScore (\score -> score { leftApplied = succ (leftApplied score) })) <$> nextStep
274+ (Nothing, Just (_, ix)) -> first (inScore (\score -> score { rightApplied = succ (rightApplied score) })) <$> nextStep
224275 (Nothing, Nothing) -> nextStep
225276 _ -> error ("Shouldn't happen. Watch the alpha conversion!\n" ++ show args1 ++ "\n\n" ++ show args2)
226277 where
227− varsInTy = map fst $ M.toList (usedVars term)
228− deleteMany = foldr (.) id $ map deleteFromDag (name : varsInTy)
229− thrd f (a,b,c) = (a,b,f c)
230− nextStep = updateDags xs (holes \\ [name], updatef args1, updatef args2 )
231− updatef = map (first . second $ subst name term) . deleteMany
232− mgetType name xs = fmap ((snd . fst) &&& (fst . snd)) . find ((name ==) . fst . fst) $ xs
233−
234−
235− go :: State -> [(Type, Type)] -> Maybe State
236− --go (State holes args1 args2 score) queue | trace ("go\n\t" ++ show holes ++ "\n\t" ++ show args1 ++ "\n\t" ++ show args2 ++ "\n\t" ++ show queue) False = undefined
237− go state [] = return state
238− go (State holes args1 args2 score) ((ty1, ty2) : queue) = do
239− res <- tcToMaybe $ match_unify ctxt [] ty1 ty2 [] holes []
240− --trace ("UnifyResult: " ++ show (ty1, ty2, res, errors)) False `seq` return ()
241− --guard (null errors)
242− ((holes', args1', args2'), queueAdditions, scoreAdditions) <- updateDags res (holes, args1, args2)
243− let newScore = score `mappend` scoreAdditions
244− guard $ scoreCriterion newScore
245− go (State holes' args1' args2' newScore) (queue ++ queueAdditions)
246−
247−
248− processDags :: State -> [Score]
249− processDags (State [] [] [] scoreAcc) = [scoreAcc]
250− --processDags (State holes (_:_) [] scoreAcc) = []
251− --processDags (State holes [] (_:_) scoreAcc) = []
252− processDags (State holes dag1 dag2 scoreAcc) = concat [ processDags state | state <- allResults ] where
253−
254− results = catMaybes [ go (State (holes \\ (map nameOf [ty1, ty2])) (deleteFromDag (nameOf ty1) dag1)
255− (inArgTys (psubst (nameOf ty2) (P Bound (nameOf ty1) (typeOf ty1))) $ deleteFromDag (nameOf ty2) dag2) scoreAcc) [(typeOf ty1, typeOf ty2)]
256− | ty1 <- canBeFirst dag1, ty2 <- canBeFirst dag2 {-, exactTypeEquality ctxt (typeOf ty1) (typeOf ty2) -} ]
257−
258− results2 = [ State (holes \\ [nameOf ty])
259− (deleteFromDag (nameOf ty) dag1) dag2
260− (scoreAcc `mappend` (mempty { leftTypeClass = 1 }))
261− | ty <- typeClassArgs1 ]
262−
263− typeClassArgs1 = filter (isSaturatedClass . typeOf) dag1
264− typeClassArgs2 = filter (isSaturatedClass . typeOf) dag2
265−
266−
267− results3 = [ State (holes \\ [nameOf ty])
268− dag1 (deleteFromDag (nameOf ty) dag2)
269− (scoreAcc `mappend` (mempty { rightTypeClass = 1 }))
270− | ty <- typeClassArgs2 ]
271−
272− allResults :: [State]
273− allResults = {- (if not (null typeClasses) then (traceShow typeClasses False `seq` id) else id ) -}
274− (results ++ results2 ++ results3)
275− where
276− typeClasses = filter (isSaturatedClass . typeOf) (dag1 ++ dag2)
277−
278−
279− -- check if the canBeFirst thing is losing any possibilities
280−
281−
282− inArgTys = map . first . second
283− typeOf ((name, ty), set) = ty
284− nameOf ((name, ty), set) = name
285−
286− -- XXX : debug stuff
287− canBeFirst = if debugParam then filter (S.null . snd . snd) else id
288− holes = map (fst . fst) dag1 ++ map (fst . fst) dag2
289−
290− deleteIdx _ [] = []
291− deleteIdx idx l@(x@(i,_,_) : xs) = if i == idx then xs else x : deleteIdx idx xs
292−
293− isSaturatedClass :: Type -> Bool
294− isSaturatedClass ty = fromMaybe False $ do
278+ inScore f state = state { score = f (score state) }
279+ state' = modifyTypes (subst name term) . deleteLeft name . deleteRight name $
280+ state { holes = holes \\ [name]}
281+ nextStep = resolveUnis xs state'
282+
283+
284+ -- | resolve a queue of unification constraints
285+ unifyQueue :: State -> [(Type, Type)] -> Maybe State
286+ unifyQueue state [] = return state
287+ unifyQueue state ((ty1, ty2) : queue) = do
288+ res <- tcToMaybe $ match_unify ctxt [] ty1 ty2 [] (holes state) []
289+ (state', queueAdditions) <- resolveUnis res state
290+ guard $ scoreCriterion (score state')
291+ unifyQueue state' (queue ++ queueAdditions)
292+
293+ possClassInstances :: [Name] -> Type -> [([(Name, Type)], Type)]
294+ possClassInstances usedNames ty = do
295295 className <- getClassName clss
296− let possInstances = concatMap class_instances $ lookupCtxt className classInfo
297− return $ (SN (sInstanceN className (map argToName args))) `elem` possInstances
296+ classDef <- lookupCtxt className classInfo
297+ n <- class_instances classDef
298+ def <- lookupCtxt n (definitions ctxt)
299+ ty <- normaliseC ctxt [] <$> (case typeFromDef def of Just x -> [x]; Nothing -> [])
300+ let ty' = vToP (uniqueBinders usedNames ty)
301+ return (getArgTys ty', getRetTy ty')
298302 where
299303 (clss, args) = unApply ty
300− getClassName (P (TCon _ _) className _) = Just className
301− getClassName _ = Nothing
302− argToName arg = show (delab istate arg)
304+ getClassName (P (TCon _ _) className _) = [className]
305+ getClassName _ = []
306+
307+ -- | Find all possible matches starting from a given state.
308+ possibleMatches :: State -> [Score]
309+ possibleMatches (State [] [] [] [] [] scoreAcc _) = [scoreAcc]
310+ possibleMatches (State holes dag1 dag2 c1 c2 scoreAcc usedNames) =
311+ concat [ possibleMatches state | state <- results, scoreCriterion (score state) ] where
312+
313+ -- we only try to match arguments whose names don't appear in the types
314+ -- of any other arguments
315+ canBeFirst :: ArgsDAG -> [(Name, Type)]
316+ canBeFirst = map fst . filter (S.null . snd . snd)
317+
318+ -- this is done rather than concatenating all three results in hopes of narrowing
319+ -- the search tree
320+ results = fromMaybe [] $ find (not . null) [results1, results2, results3]
321+
322+ -- try to match an argument from the left with an argument from the right
323+ results1 = catMaybes [ unifyQueue (State (holes \\ [n1, n2]) (deleteFromDag n1 dag1)
324+ ((inArgTys subst2for1) $ deleteFromDag n2 dag2) c1 (map (second subst2for1) c2) scoreAcc usedNames) [(ty1, ty2)]
325+ | (n1, ty1) <- canBeFirst dag1, (n2, ty2) <- canBeFirst dag2, let subst2for1 = psubst n2 (P Bound n1 ty1)]
326+
327+ -- try to match a typeclass argument from the left with a typeclass argument from the right
328+ results2 = catMaybes [ unifyQueue (State (holes \\ [n1, n2]) dag1 (inArgTys subst2for1 dag2)
329+ (deleteFromArgList n1 c1) (map (second subst2for1) (deleteFromArgList n2 c2)) scoreAcc usedNames) [(ty1, ty2)]
330+ | (n1, ty1) <- c1, (n2, ty2) <- c2, let subst2for1 = psubst n2 (P Bound n1 ty1)]
331+
332+ -- try to hunt match a typeclass constraint by replacing it with an instance
333+ results3 = if null dag1 || null dag2 then catMaybes (results3A ++ results3B) else []
334+ typeClassArgs classes = [ ((n, ty), inst) | (n, ty) <- classes, inst <- possClassInstances usedNames ty ]
335+ noDeps (n, ty) = ((n, ty), (0, S.empty))
336+ results3A = [ unifyQueue
337+ (State ((holes \\ [n]) ++ newHoles) (dag1 ++ map noDeps newNonClassArgs) dag2
338+ (deleteFromArgList n c1 ++ newClassArgs) c2
339+ (scoreAcc `mappend` (mempty { leftTypeClass = 1 }))
340+ (usedNames ++ newHoles)
341+ )
342+ [(ty, inst)]
343+ | ((n, ty), (newArgs, inst)) <- typeClassArgs c1, let newHoles = map fst newArgs
344+ , let (newClassArgs, newNonClassArgs) = partition (isTypeClassArg . snd) newArgs ]
345+ results3B = [ unifyQueue
346+ (State ((holes \\ [n]) ++ newHoles) dag1 (dag2 ++ map noDeps newNonClassArgs)
347+ c1 (deleteFromArgList n c2 ++ newClassArgs)
348+ (scoreAcc `mappend` (mempty { rightTypeClass = 1 }))
349+ (usedNames ++ newHoles)
350+ )
351+ [(ty, inst)]
352+ | ((n, ty), (newArgs, inst)) <- typeClassArgs c2, let newHoles = map fst newArgs
353+ , let (newClassArgs, newNonClassArgs) = partition (isTypeClassArg . snd) newArgs ]
303354