265d9a4 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Improve elaboration efficiency by cutting down on excessive backtracking

265d9a4Edwin Brady14 years ago

lib/Language/Reflection.idr+1

compare with master

unifiedsplit

@@ -10,6 +10,7 @@ data TT = Var TTName

10 | App TTName TT TT

12data Tactic = Try Tactic Tactic

13+ | GoalType TTName Tactic -- only run if the goal has the right type

13 | Refine TTName

14 | Refine TTName

14 | Seq Tactic Tactic

15 | Seq Tactic Tactic

15 | Trivial

16 | Trivial

src/Core/Unify.hs+34−13

@@ -21,18 +21,21 @@ type Injs = [(TT Name, TT Name, TT Name)]

21type Fails = [(TT Name, TT Name, Env, Err)]

23data UInfo = UI Int Injs Fails

24+ deriving Show

25unify :: Context -> Env -> TT Name -> TT Name -> TC ([(Name, TT Name)],

26unify :: Context -> Env -> TT Name -> TT Name -> TC ([(Name, TT Name)],

26 Injs, Fails)

27 Injs, Fails)

27unify ctxt env topx topy =

28unify ctxt env topx topy =

28-- trace ("Unifying " ++ show (topx, topy)) $

29-- trace ("Unifying " ++ show (topx, topy)) $

30+ -- don't bother if topx and topy are different at the head

29− case runStateT (un' False [] topx topy) (UI 0 [] []) of

31+ case runStateT (un False [] topx topy) (UI 0 [] []) of

30− OK (v, UI _ inj []) -> return (filter notTrivial v, inj, [])

32+ OK (v, UI _ inj []) -> return (filter notTrivial v, inj, [])

31− _ ->

33+-- Error e@(CantUnify False _ _ _ _ _) -> tfail e

34+ res ->

32 let topxn = normalise ctxt env topx

35 let topxn = normalise ctxt env topx

33 topyn = normalise ctxt env topy in

36 topyn = normalise ctxt env topy in

34−-- trace ("Unifying " ++ show (topx, topy) ++ "\n\n==>\n" ++ show (topxn, topyn) ++ "\n\n") $

37+-- trace ("Unifying " ++ show (topx, topy) ++ "\n\n==>\n" ++ show (topxn, topyn) ++ "\n\n" ++ show res ++ "\n\n") $

35− case runStateT (un' False [] topxn topyn)

38+ case runStateT (un False [] topxn topyn)

36 (UI 0 [] []) of

39 (UI 0 [] []) of

37 OK (v, UI _ inj fails) ->

40 OK (v, UI _ inj fails) ->

38 return (filter notTrivial v, inj, reverse fails)

41 return (filter notTrivial v, inj, reverse fails)

@@ -41,6 +44,10 @@ unify ctxt env topx topy =

41 notTrivial (x, P _ x' _) = x /= x'

44 notTrivial (x, P _ x' _) = x /= x'

42 notTrivial _ = True

45 notTrivial _ = True

47+ headDiff (P (DCon _ _) x _) (P (DCon _ _) y _) = x /= y

48+ headDiff (P (TCon _ _) x _) (P (TCon _ _) y _) = x /= y

49+ headDiff _ _ = False

50+

44 injective (P (DCon _ _) _ _) = True

51 injective (P (DCon _ _) _ _) = True

45 injective (P (TCon _ _) _ _) = True

52 injective (P (TCon _ _) _ _) = True

46 injective (App f a) = injective f

53 injective (App f a) = injective f

@@ -59,6 +66,16 @@ unify ctxt env topx topy =

59 then return r

66 then return r

60 else do put (UI s i f); u2

67 else do put (UI s i f); u2

69+ un :: Bool -> [(Name, Name)] -> TT Name -> TT Name ->

70+ StateT UInfo

71+ TC [(Name, TT Name)]

72+ un fn names x y

73+ = let (xf, _) = unApply x

74+ (yf, _) = unApply y in

75+ if headDiff xf yf then unifyFail x y else

76+ uplus (un' fn names x y)

77+ (un' fn names (hnf ctxt env x) (hnf ctxt env y))

78+

62 un' :: Bool -> [(Name, Name)] -> TT Name -> TT Name ->

79 un' :: Bool -> [(Name, Name)] -> TT Name -> TT Name ->

63 StateT UInfo

80 StateT UInfo

64 TC [(Name, TT Name)]

81 TC [(Name, TT Name)]

@@ -102,10 +119,10 @@ unify ctxt env topx topy =

102 (do hf <- un' True bnames fx fy

119 (do hf <- un' True bnames fx fy

103 let ax' = hnormalise hf ctxt env (substNames hf ax)

120 let ax' = hnormalise hf ctxt env (substNames hf ax)

104 let ay' = hnormalise hf ctxt env (substNames hf ay)

121 let ay' = hnormalise hf ctxt env (substNames hf ay)

105− ha <- un' False bnames ax' ay'

122+ ha <- un False bnames ax' ay'

106 sc 1

123 sc 1

107 combine bnames hf ha)

124 combine bnames hf ha)

108− (do ha <- un' False bnames ax ay

125+ (do ha <- un False bnames ax ay

109 let fx' = hnormalise ha ctxt env (substNames ha fx)

126 let fx' = hnormalise ha ctxt env (substNames ha fx)

110 let fy' = hnormalise ha ctxt env (substNames ha fy)

127 let fy' = hnormalise ha ctxt env (substNames ha fy)

111 hf <- un' False bnames fx' fy'

128 hf <- un' False bnames fx' fy'

@@ -141,8 +158,9 @@ unify ctxt env topx topy =

141 let r = recoverable x y

158 let r = recoverable x y

142 let err = CantUnify r

159 let err = CantUnify r

143 topx topy (CantUnify r x y (Msg "") [] s) (errEnv env) s

160 topx topy (CantUnify r x y (Msg "") [] s) (errEnv env) s

161+ if (not r) then lift $ tfail err

144− put (UI s i ((x, y, env, err) : f))

162+ else do put (UI s i ((x, y, env, err) : f))

145− return [] -- lift $ tfail err

163+ return [] -- lift $ tfail err

146

164

147 -- shortcut failure, if we *know* nothing can fix it

165 -- shortcut failure, if we *know* nothing can fix it

148 unifyFail x y = do UI s i f <- get

166 unifyFail x y = do UI s i f <- get

@@ -198,12 +216,15 @@ unify ctxt env topx topy =

198 recoverable (P (DCon _ _) x _) (P (DCon _ _) y _)

216 recoverable (P (DCon _ _) x _) (P (DCon _ _) y _)

199 | x == y = True

217 | x == y = True

200 | otherwise = False

218 | otherwise = False

219+ recoverable (P (TCon _ _) x _) (P (TCon _ _) y _)

220+ | x == y = True

221+ | otherwise = False

201−-- recoverable (P (DCon _ _) x _) (P (TCon _ _) y _) = False

222+ recoverable (P (DCon _ _) x _) (P (TCon _ _) y _) = False

202−-- recoverable (P (TCon _ _) x _) (P (DCon _ _) y _) = False

223+ recoverable (P (TCon _ _) x _) (P (DCon _ _) y _) = False

203 recoverable p@(P _ n _) (App f a) = recoverable p f

224 recoverable p@(P _ n _) (App f a) = recoverable p f

204− recoverable (App f a) p@(P _ _ _) = recoverable f p

225+-- recoverable (App f a) p@(P _ _ _) = recoverable f p

205 recoverable (App f a) (App f' a')

226 recoverable (App f a) (App f' a')

206− = recoverable f f' && recoverable a a'

227+ = recoverable f f' -- && recoverable a a'

207 recoverable _ _ = True

228 recoverable _ _ = True

208

229

209errEnv = map (\(x, b) -> (x, binderTy b))

230errEnv = map (\(x, b) -> (x, binderTy b))

src/Idris/AbsSyntaxTree.hs+1

@@ -473,6 +473,7 @@ data PTactic' t = Intro [Name] | Intros | Focus Name

473 | Try (PTactic' t) (PTactic' t)

474 | TSeq (PTactic' t) (PTactic' t)

475 | ReflectTac t -- see Language.Reflection module

476+ | GoalType String (PTactic' t)

476 | Qed | Abandon

477 | Qed | Abandon

477 deriving (Show, Eq, Functor)

478 deriving (Show, Eq, Functor)

478{-!

479{-!

src/Idris/ElabTerm.hs+52−42

@@ -112,7 +112,8 @@ elab ist info pattern tcgen fn tm

112 elab' ina (PResolveTC fc)

113 | pattern = do c <- unique_hole (MN 0 "c")

114 instanceArg c

115+ | otherwise = do g <- goal

115− | otherwise = try (resolveTC 2 fn ist)

116+ try (resolveTC 2 fn ist)

116 (do c <- unique_hole (MN 0 "c")

117 (do c <- unique_hole (MN 0 "c")

117 instanceArg c)

118 instanceArg c)

118 elab' ina (PRefl fc t) = elab' ina (PApp fc (PRef fc eqCon) [pimp (MN 0 "a") Placeholder,

119 elab' ina (PRefl fc t) = elab' ina (PApp fc (PRef fc eqCon) [pimp (MN 0 "a") Placeholder,

@@ -147,9 +148,7 @@ elab ist info pattern tcgen fn tm

147 ctxt <- get_context

148 ctxt <- get_context

148 let (tc, _) = unApply ty

149 let (tc, _) = unApply ty

149 let as' = pruneByType tc ctxt as

150 let as' = pruneByType tc ctxt as

150− let as'' = as' -- pruneAlt as'

151− try (tryAll (zip (map (elab' ina) as'') (map showHd as'')))

151+ tryAll (zip (map (elab' ina) as') (map showHd as'))

152− (tryAll (zip (map (elab' ina) as') (map showHd as')))

153 where showHd (PApp _ h _) = show h

152 where showHd (PApp _ h _) = show h

154 showHd x = show x

153 showHd x = show x

155 elab' ina (PAlternative False as)

154 elab' ina (PAlternative False as)

@@ -290,24 +289,26 @@ elab ist info pattern tcgen fn tm

290 ctxt <- get_context

289 ctxt <- get_context

291 let guarded = isConName Nothing f ctxt

290 let guarded = isConName Nothing f ctxt

292-- when True

291-- when True

293− tryWhen True

292+ (ns, committed) <- tryWhen True

294 (do ns <- apply (Var f) (map isph args)

293 (do ns <- apply (Var f) (map isph args)

294+ return (ns, True)) -- commit to this branch here

295+ (do apply_elab f (map (toElab (ina || not isinf, guarded)) args)

296+ mkSpecialised ist fc f (map getTm args') tm

297+ solve

298+ return ([], False))

299+ when committed $

295− let (ns', eargs)

300+ do let (ns', eargs) = unzip $

296− = unzip $

297 sortBy (\(_,x) (_,y) ->

301 sortBy (\(_,x) (_,y) ->

298 compare (priority x) (priority y))

302 compare (priority x) (priority y))

299 (zip ns args)

303 (zip ns args)

300− try

304+ tryWhen True

301− (elabArgs (ina || not isinf, guarded)

305+ (elabArgs (ina || not isinf, guarded)

302− [] False ns' (map (\x -> (lazyarg x, getTm x)) eargs))

306+ [] False ns' (map (\x -> (lazyarg x, getTm x)) eargs))

303− (elabArgs (ina || not isinf, guarded)

307+ (elabArgs (ina || not isinf, guarded)

304− [] False (reverse ns')

308+ [] False (reverse ns')

305− (map (\x -> (lazyarg x, getTm x)) (reverse eargs)))

309+ (map (\x -> (lazyarg x, getTm x)) (reverse eargs)))

306− mkSpecialised ist fc f (map getTm args') tm

310+ mkSpecialised ist fc f (map getTm args') tm

307− solve)

308− (do apply_elab f (map (toElab (ina || not isinf, guarded)) args)

309− mkSpecialised ist fc f (map getTm args') tm

310− solve)

311+ solve

311-- ptm <- get_term

312-- ptm <- get_term

312-- elog (show ptm)

313-- elog (show ptm)

313 ivs' <- get_instances

314 ivs' <- get_instances

@@ -405,10 +406,10 @@ elab ist info pattern tcgen fn tm

405 failed' <- -- trace (show (n, t, hs, tm)) $

406 failed' <- -- trace (show (n, t, hs, tm)) $

406 case n `elem` hs of

407 case n `elem` hs of

407 True ->

408 True ->

408− if r

409+-- if r

409− then try (do focus n; elabE ina t; return failed)

410+-- then try (do focus n; elabE ina t; return failed)

410− (return ((n,(lazy, t)):failed))

411+-- (return ((n,(lazy, t)):failed))

411− else do focus n; elabE ina t; return failed

412+ do focus n; elabE ina t; return failed

412 False -> return failed

413 False -> return failed

413 elabArgs ina failed r ns args

414 elabArgs ina failed r ns args

414

415

@@ -459,17 +460,17 @@ pruneByType (P _ n _) c as

459pruneByType t _ as = as

460pruneByType t _ as = as

460

461

461trivial :: IState -> ElabD ()

462trivial :: IState -> ElabD ()

462−trivial ist = try (do elab ist toplevel False False (MN 0 "tac")

463+trivial ist = try' (do elab ist toplevel False False (MN 0 "tac")

463 (PRefl (FC "prf" 0) Placeholder)

464 (PRefl (FC "prf" 0) Placeholder)

464− return ())

465+ return ())

465− (do env <- get_env

466+ (do env <- get_env

466− tryAll (map fst env)

467+ tryAll (map fst env)

467− return ())

468+ return ()) True

468 where

469 where

469 tryAll [] = fail "No trivial solution"

470 tryAll [] = fail "No trivial solution"

470− tryAll (x:xs) = try (elab ist toplevel False False

471+ tryAll (x:xs) = try' (elab ist toplevel False False

471 (MN 0 "tac") (PRef (FC "prf" 0) x))

472 (MN 0 "tac") (PRef (FC "prf" 0) x))

472− (tryAll xs)

473+ (tryAll xs) True

473

474

474findInstances :: IState -> Term -> [Name]

475findInstances :: IState -> Term -> [Name]

475findInstances ist t

476findInstances ist t

@@ -481,19 +482,19 @@ findInstances ist t

481

482

482resolveTC :: Int -> Name -> IState -> ElabD ()

483resolveTC :: Int -> Name -> IState -> ElabD ()

483resolveTC 0 fn ist = fail $ "Can't resolve type class"

484resolveTC 0 fn ist = fail $ "Can't resolve type class"

484−resolveTC 1 fn ist = try (trivial ist) (resolveTC 0 fn ist)

485+resolveTC 1 fn ist = try' (trivial ist) (resolveTC 0 fn ist) True

485resolveTC depth fn ist

486resolveTC depth fn ist

486 = do hnf_compute

487 = do hnf_compute

487− try (trivial ist)

488+ try' (trivial ist)

488− (do t <- goal

489+ (do t <- goal

489− let insts = findInstances ist t

490+ let insts = findInstances ist t

490− let (tc, ttypes) = unApply t

491+ let (tc, ttypes) = unApply t

491− scopeOnly <- needsDefault t tc ttypes

492+ scopeOnly <- needsDefault t tc ttypes

492− tm <- get_term

493+ tm <- get_term

493-- traceWhen (depth > 6) ("GOAL: " ++ show t ++ "\nTERM: " ++ show tm) $

494-- traceWhen (depth > 6) ("GOAL: " ++ show t ++ "\nTERM: " ++ show tm) $

494-- (tryAll (map elabTC (map fst (ctxtAlist (tt_ctxt ist)))))

495-- (tryAll (map elabTC (map fst (ctxtAlist (tt_ctxt ist)))))

495− let depth' = if scopeOnly then 2 else depth

496+ let depth' = if scopeOnly then 2 else depth

496− blunderbuss t depth' insts)

497+ blunderbuss t depth' insts) True

497 where

498 where

498 elabTC n | n /= fn && tcname n = (resolve n depth, show n)

499 elabTC n | n /= fn && tcname n = (resolve n depth, show n)

499 | otherwise = (fail "Can't resolve", show n)

500 | otherwise = (fail "Can't resolve", show n)

@@ -512,8 +513,8 @@ resolveTC depth fn ist

512

513

513 blunderbuss t d [] = lift $ tfail $ CantResolve t

514 blunderbuss t d [] = lift $ tfail $ CantResolve t

514 blunderbuss t d (n:ns)

515 blunderbuss t d (n:ns)

515− | n /= fn && tcname n = try (resolve n d)

516+ | n /= fn && tcname n = try' (resolve n d)

516− (blunderbuss t d ns)

517+ (blunderbuss t d ns) True

517 | otherwise = blunderbuss t d ns

518 | otherwise = blunderbuss t d ns

518

519

519 resolve n depth

520 resolve n depth

@@ -570,8 +571,8 @@ runTac autoSolve ist tac = do env <- get_env

570 runT (Intro xs) = mapM_ (\x -> do attack; intro (Just x)) xs

571 runT (Intro xs) = mapM_ (\x -> do attack; intro (Just x)) xs

571 runT Intros = do g <- goal

572 runT Intros = do g <- goal

572 attack; intro (bname g)

573 attack; intro (bname g)

573− try (runT Intros)

574+ try' (runT Intros)

574− (return ())

575+ (return ()) True

575 where

576 where

576 bname (Bind n _ _) = Just n

577 bname (Bind n _ _) = Just n

577 bname _ = Nothing

578 bname _ = Nothing

@@ -653,6 +654,13 @@ runTac autoSolve ist tac = do env <- get_env

653-- trace (show p ++ "\n\n") $

654-- trace (show p ++ "\n\n") $

654 return ()

655 return ()

655 where tacticTy = tacm "Tactic"

656 where tacticTy = tacm "Tactic"

657+ runT (GoalType n tac) = do g <- goal

658+ case unApply g of

659+ (P _ n' _, _) ->

660+ if nsroot n' == UN n

661+ then runT tac

662+ else fail "Wrong goal type"

663+ _ -> fail "Wrong goal type"

656 runT x = fail $ "Not implemented " ++ show x

664 runT x = fail $ "Not implemented " ++ show x

657

665

658 runReflected t = do t' <- reify t

666 runReflected t = do t' <- reify t

@@ -670,6 +678,8 @@ runTac autoSolve ist tac = do env <- get_env

670 reifyAp t [Constant (Str x)]

678 reifyAp t [Constant (Str x)]

671 | t == tacm "Refine" = return $ Refine (UN x) []

679 | t == tacm "Refine" = return $ Refine (UN x) []

672 reifyAp t [l, r] | t == tacm "Seq" = liftM2 TSeq (reify l) (reify r)

680 reifyAp t [l, r] | t == tacm "Seq" = liftM2 TSeq (reify l) (reify r)

681+ reifyAp t [Constant (Str n), x]

682+ | t == tacm "GoalType" = liftM (GoalType n) (reify x)

673 reifyAp f args = fail ("Unknown tactic " ++ show (f, args)) -- shouldn't happen

683 reifyAp f args = fail ("Unknown tactic " ++ show (f, args)) -- shouldn't happen

674

684

675solveAll = try (do solve; solveAll) (return ())

685solveAll = try (do solve; solveAll) (return ())

test/reg008/expectednew file

No changes to the content.

test/reg008/reg008.idrnew file+15

@@ -0,0 +1,15 @@

1+module NatCmp

3+data Cmp : Nat -> Nat -> Type where

4+ cmpLT : (y : _) -> Cmp x (x + S y)

5+ cmpEQ : Cmp x x

6+ cmpGT : (x : _) -> Cmp (y + S x) y

8+total cmp : (x, y : Nat) -> Cmp x y

9+cmp O O = cmpEQ

10+cmp O (S k) = cmpLT _

11+cmp (S k) O = cmpGT _

12+cmp (S x) (S y) with (cmp x y)

13+ cmp (S x) (S (x + (S k))) | cmpLT k = cmpLT k

14+ cmp (S x) (S x) | cmpEQ = cmpEQ

15+ cmp (S (y + (S k))) (S y) | cmpGT k = cmpGT k

test/reg008/runnew file+3

@@ -0,0 +1,3 @@

1+#!/bin/bash

2+idris $@ reg008.idr --check

3+rm -f *.ibc