114a307 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Prevent possibility of unbounded computation in :search

114a307bmsherman12 years ago

src/Idris/TypeSearch.hs+72−49

compare with master

unifiedsplit

@@ -10,14 +10,14 @@ import Data.Function (on)

10import Data.List (find, minimumBy, partition, sortBy, (\\))

11import Data.Map (Map)

12import qualified Data.Map as M

13−import Data.Maybe (catMaybes, fromMaybe, isJust)

13+import Data.Maybe (catMaybes, fromMaybe, isJust, maybeToList)

14import Data.Monoid (Monoid (mempty, mappend))

15import Data.Set (Set)

16import qualified Data.Set as S

17import qualified Data.Text as T (pack, isPrefixOf)

19import Idris.AbsSyntax (addUsingConstraints, addImpl, getContext, getIState, putIState, implicit)

20−import Idris.AbsSyntaxTree (class_instances, defaultSyntax, Idris,

20+import Idris.AbsSyntaxTree (class_instances, ClassInfo, defaultSyntax, Idris,

21 IState (idris_classes, idris_docstrings, tt_ctxt),

22 implicitAllowed, prettyDocumentedIst, prettyIst, PTerm, toplevel)

23import Idris.Core.Evaluate (Context (definitions), Def (Function, TyDecl, CaseOp), normaliseC)

@@ -218,6 +218,25 @@ inArgTys :: (Type -> Type) -> ArgsDAG -> ArgsDAG

218inArgTys = map . first . second

219

220

221+typeclassUnify :: Ctxt ClassInfo -> Context -> Type -> Type -> Maybe [(Name, Type)]

222+typeclassUnify classInfo ctxt ty tyTry = do

223+ res <- tcToMaybe $ match_unify ctxt [] ty retTy [] holes []

224+ guard $ null (holes \\ map fst res)

225+ let argTys' = map (second $ foldr (.) id [ subst n t | (n, t) <- res ]) tcArgs

226+ return argTys'

227+ where

228+ tyTry' = vToP tyTry

229+ holes = map fst nonTcArgs

230+ retTy = getRetTy tyTry'

231+ (tcArgs, nonTcArgs) = partition (isTypeClassArg classInfo . snd) $ getArgTys tyTry'

232+

233+isTypeClassArg :: Ctxt ClassInfo -> Type -> Bool

234+isTypeClassArg classInfo ty = not (null (getClassName clss >>= flip lookupCtxt classInfo)) where

235+ (clss, args) = unApply ty

236+ getClassName (P (TCon _ _) className _) = [className]

237+ getClassName _ = []

238+

239+

221--DONT run vToP first!

240--DONT run vToP first!

222-- | Try to match two types together in a unification-like procedure.

241-- | Try to match two types together in a unification-like procedure.

223-- Returns a list of possible scores representing ways in which the two

242-- Returns a list of possible scores representing ways in which the two

@@ -238,16 +257,11 @@ unifyWithHoles istate type1 = \type2 -> let

238 ctxt = tt_ctxt istate

257 ctxt = tt_ctxt istate

239 classInfo = idris_classes istate

258 classInfo = idris_classes istate

240

259

241− isTypeClassArg :: Type -> Bool

242− isTypeClassArg ty = not (null (getClassName clss >>= flip lookupCtxt classInfo)) where

243− (clss, args) = unApply ty

244− getClassName (P (TCon _ _) className _) = [className]

245− getClassName _ = []

246−

247 (dag1, typeClassArgs1, retTy1) = makeDag type1

260 (dag1, typeClassArgs1, retTy1) = makeDag type1

248 argNames1 = map (fst . fst) dag1

261 argNames1 = map (fst . fst) dag1

249 makeDag :: Type -> (ArgsDAG, [(Name, Type)], Type)

262 makeDag :: Type -> (ArgsDAG, [(Name, Type)], Type)

250− makeDag = first3 (zipWith (\i (ty, deps) -> (ty, (i, deps))) [0..] . reverseDag) . computeDagP isTypeClassArg . vToP

263+ makeDag = first3 (zipWith (\i (ty, deps) -> (ty, (i, deps))) [0..] . reverseDag) .

264+ computeDagP (isTypeClassArg classInfo) . vToP

251 first3 f (a,b,c) = (f a, b, c)

265 first3 f (a,b,c) = (f a, b, c)

252

266

253 -- update our state with the unification resolutions

267 -- update our state with the unification resolutions

@@ -278,9 +292,13 @@ unifyWithHoles istate type1 = \type2 -> let

278 (Nothing, Nothing) -> nextStep

292 (Nothing, Nothing) -> nextStep

279 _ -> error ("Shouldn't happen. Watch the alpha conversion!\n" ++ show args1 ++ "\n\n" ++ show args2)

293 _ -> error ("Shouldn't happen. Watch the alpha conversion!\n" ++ show args1 ++ "\n\n" ++ show args2)

280 where

294 where

295+ varsInTy = map fst $ M.toList (usedVars term) --[]

296+ toDelete = name : varsInTy

297+ deleteMany = foldr (.) id $ [ deleteLeft t . deleteRight t | t <- toDelete ]

298+

281 inScore f state = state { score = f (score state) }

299 inScore f state = state { score = f (score state) }

282− state' = modifyTypes (subst name term) . deleteLeft name . deleteRight name $

300+ state' = modifyTypes (subst name term) . deleteMany $

283− state { holes = holes \\ [name]}

301+ state { holes = holes \\ toDelete }

284 nextStep = resolveUnis xs state'

302 nextStep = resolveUnis xs state'

285

303

286

304

@@ -288,12 +306,13 @@ unifyWithHoles istate type1 = \type2 -> let

288 unifyQueue :: State -> [(Type, Type)] -> Maybe State

306 unifyQueue :: State -> [(Type, Type)] -> Maybe State

289 unifyQueue state [] = return state

307 unifyQueue state [] = return state

290 unifyQueue state ((ty1, ty2) : queue) = do

308 unifyQueue state ((ty1, ty2) : queue) = do

309+ --trace ("go: \n" ++ show state) True `seq` return ()

291 res <- tcToMaybe $ match_unify ctxt [] ty1 ty2 [] (holes state) []

310 res <- tcToMaybe $ match_unify ctxt [] ty1 ty2 [] (holes state) []

292 (state', queueAdditions) <- resolveUnis res state

311 (state', queueAdditions) <- resolveUnis res state

293 guard $ scoreCriterion (score state')

312 guard $ scoreCriterion (score state')

294 unifyQueue state' (queue ++ queueAdditions)

313 unifyQueue state' (queue ++ queueAdditions)

295

314

296− possClassInstances :: [Name] -> Type -> [([(Name, Type)], Type)]

315+ possClassInstances :: [Name] -> Type -> [Type]

297 possClassInstances usedNames ty = do

316 possClassInstances usedNames ty = do

298 className <- getClassName clss

317 className <- getClassName clss

299 classDef <- lookupCtxt className classInfo

318 classDef <- lookupCtxt className classInfo

@@ -301,57 +320,61 @@ unifyWithHoles istate type1 = \type2 -> let

301 def <- lookupCtxt n (definitions ctxt)

320 def <- lookupCtxt n (definitions ctxt)

302 ty <- normaliseC ctxt [] <$> (case typeFromDef def of Just x -> [x]; Nothing -> [])

321 ty <- normaliseC ctxt [] <$> (case typeFromDef def of Just x -> [x]; Nothing -> [])

303 let ty' = vToP (uniqueBinders usedNames ty)

322 let ty' = vToP (uniqueBinders usedNames ty)

304− return (getArgTys ty', getRetTy ty')

323+ return ty'

305 where

324 where

306− (clss, args) = unApply ty

325+ (clss, _) = unApply ty

307 getClassName (P (TCon _ _) className _) = [className]

326 getClassName (P (TCon _ _) className _) = [className]

308 getClassName _ = []

327 getClassName _ = []

309

328

329+

330+ collect :: [State] -> [Score]

331+ collect states = concat [ possibleMatches state | state <- states, scoreCriterion (score state) ]

332+

310 -- | Find all possible matches starting from a given state.

333 -- | Find all possible matches starting from a given state.

334+ -- We go in stages rather than concatenating all three results in hopes of narrowing

335+ -- the search tree. Once we advance in a phase, there should be no going back.

311 possibleMatches :: State -> [Score]

336 possibleMatches :: State -> [Score]

337+

338+ -- Stage 3 - we're done!

312 possibleMatches (State [] [] [] [] [] scoreAcc _) = [scoreAcc]

339 possibleMatches (State [] [] [] [] [] scoreAcc _) = [scoreAcc]

340+

341+ -- Stage 2 - match typeclasses

342+ possibleMatches (State [] [] [] c1 c2 scoreAcc usedNames) =

343+ collect (if null results2 then results3 else results2)

344+ where

345+ -- try to match a typeclass argument from the left with a typeclass argument from the right

346+ results2 =

347+ catMaybes [ unifyQueue (State [] [] []

348+ (deleteFromArgList n1 c1) (map (second subst2for1) (deleteFromArgList n2 c2)) scoreAcc usedNames) [(ty1, ty2)]

349+ | (n1, ty1) <- c1, (n2, ty2) <- c2, let subst2for1 = psubst n2 (P Bound n1 ty1)]

350+

351+ -- try to hunt match a typeclass constraint by replacing it with an instance

352+ results3 = results3A ++ results3B

353+ typeClassArgs classes = [ ((n, ty), inst) | (n, ty) <- classes, inst <- possClassInstances usedNames ty ]

354+ results3A = [ State [] [] []

355+ (deleteFromArgList n c1 ++ newClassArgs) c2

356+ (scoreAcc `mappend` (mempty { leftTypeClass = 1 }))

357+ (usedNames ++ newHoles)

358+ | ((n, ty), inst) <- typeClassArgs c1

359+ , newClassArgs <- maybeToList $ typeclassUnify classInfo ctxt ty inst

360+ , let newHoles = map fst newClassArgs ]

361+ results3B = [ State [] [] []

362+ c1 (deleteFromArgList n c2 ++ newClassArgs)

363+ (scoreAcc `mappend` (mempty { rightTypeClass = 1 }))

364+ (usedNames ++ newHoles)

365+ | ((n, ty), inst) <- typeClassArgs c2

366+ , newClassArgs <- maybeToList $ typeclassUnify classInfo ctxt ty inst

367+ , let newHoles = map fst newClassArgs ]

368+

369+ -- Stage 1 - match arguments

313− possibleMatches (State holes dag1 dag2 c1 c2 scoreAcc usedNames) =

370+ possibleMatches (State holes dag1 dag2 c1 c2 scoreAcc usedNames) = collect results1 where

314− concat [ possibleMatches state | state <- results, scoreCriterion (score state) ] where

315

371

316 -- we only try to match arguments whose names don't appear in the types

372 -- we only try to match arguments whose names don't appear in the types

317 -- of any other arguments

373 -- of any other arguments

318 canBeFirst :: ArgsDAG -> [(Name, Type)]

374 canBeFirst :: ArgsDAG -> [(Name, Type)]

319 canBeFirst = map fst . filter (S.null . snd . snd)

375 canBeFirst = map fst . filter (S.null . snd . snd)

320

376

321− -- this is done rather than concatenating all three results in hopes of narrowing

322− -- the search tree

323− results = fromMaybe [] $ find (not . null) [results1, results2, results3]

324−

325 -- try to match an argument from the left with an argument from the right

377 -- try to match an argument from the left with an argument from the right

326 results1 = catMaybes [ unifyQueue (State (holes \\ [n1, n2]) (deleteFromDag n1 dag1)

378 results1 = catMaybes [ unifyQueue (State (holes \\ [n1, n2]) (deleteFromDag n1 dag1)

327 ((inArgTys subst2for1) $ deleteFromDag n2 dag2) c1 (map (second subst2for1) c2) scoreAcc usedNames) [(ty1, ty2)]

379 ((inArgTys subst2for1) $ deleteFromDag n2 dag2) c1 (map (second subst2for1) c2) scoreAcc usedNames) [(ty1, ty2)]

328 | (n1, ty1) <- canBeFirst dag1, (n2, ty2) <- canBeFirst dag2, let subst2for1 = psubst n2 (P Bound n1 ty1)]

380 | (n1, ty1) <- canBeFirst dag1, (n2, ty2) <- canBeFirst dag2, let subst2for1 = psubst n2 (P Bound n1 ty1)]

329−

330− -- try to match a typeclass argument from the left with a typeclass argument from the right

331− results2 = catMaybes [ unifyQueue (State (holes \\ [n1, n2]) dag1 (inArgTys subst2for1 dag2)

332− (deleteFromArgList n1 c1) (map (second subst2for1) (deleteFromArgList n2 c2)) scoreAcc usedNames) [(ty1, ty2)]

333− | (n1, ty1) <- c1, (n2, ty2) <- c2, let subst2for1 = psubst n2 (P Bound n1 ty1)]

334−

335− -- try to hunt match a typeclass constraint by replacing it with an instance

336− results3 = if null dag1 || null dag2 then catMaybes (results3A ++ results3B) else []

337− typeClassArgs classes = [ ((n, ty), inst) | (n, ty) <- classes, inst <- possClassInstances usedNames ty ]

338− noDeps (n, ty) = ((n, ty), (0, S.empty))

339− results3A = [ unifyQueue

340− (State ((holes \\ [n]) ++ newHoles) (dag1 ++ map noDeps newNonClassArgs) dag2

341− (deleteFromArgList n c1 ++ newClassArgs) c2

342− (scoreAcc `mappend` (mempty { leftTypeClass = 1 }))

343− (usedNames ++ newHoles)

344− )

345− [(ty, inst)]

346− | ((n, ty), (newArgs, inst)) <- typeClassArgs c1, let newHoles = map fst newArgs

347− , let (newClassArgs, newNonClassArgs) = partition (isTypeClassArg . snd) newArgs ]

348− results3B = [ unifyQueue

349− (State ((holes \\ [n]) ++ newHoles) dag1 (dag2 ++ map noDeps newNonClassArgs)

350− c1 (deleteFromArgList n c2 ++ newClassArgs)

351− (scoreAcc `mappend` (mempty { rightTypeClass = 1 }))

352− (usedNames ++ newHoles)

353− )

354− [(ty, inst)]

355− | ((n, ty), (newArgs, inst)) <- typeClassArgs c2, let newHoles = map fst newArgs

356− , let (newClassArgs, newNonClassArgs) = partition (isTypeClassArg . snd) newArgs ]

357−