21c3a30 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Give up type class resolution sooner

21c3a30Edwin Brady15 years ago

src/Core/Elaborate.hs+5−1

compare with master

unifiedsplit

@@ -427,7 +427,11 @@ tryAll xs = tryAll' [] (cantResolve, 0) (map fst xs)

427 OK (v, s') -> tryAll' ((do put s'

428 return v):cs) f xs

429 Error err -> do put s

430+ if (score err) < 100

431+ then

430− tryAll' cs (better err f) xs

432+ tryAll' cs (better err f) xs

433+ else

434+ tryAll' [] (better err f) xs -- give up

431

435

432 better err (f, i) = let s = score err in

436 better err (f, i) = let s = score err in

433 if (s >= i) then (lift (tfail err), s)

437 if (s >= i) then (lift (tfail err), s)

src/Core/TT.hs+2

@@ -39,6 +39,7 @@ instance Show FC where

40data Err = Msg String

41 | CantUnify Term Term Err Int -- Int is 'score' - how much we did unify

42+ | NoSuchVariable Name

42 | NotInjective Term Term Term

43 | NotInjective Term Term Term

43 | CantResolve Term

44 | CantResolve Term

44 | IncompleteTerm Term

45 | IncompleteTerm Term

@@ -50,6 +51,7 @@ data Err = Msg String

50score :: Err -> Int

51score :: Err -> Int

51score (CantUnify _ _ m s) = s + score m

52score (CantUnify _ _ m s) = s + score m

52score (CantResolve _) = 20

53score (CantResolve _) = 20

54+score (NoSuchVariable _) = 1000

53score _ = 0

55score _ = 0

55instance Show Err where

57instance Show Err where

src/Core/Typecheck.hs+1−1

@@ -53,7 +53,7 @@ check' holes ctxt env top = chk env top where

53 chk env (Var n)

54 | Just (i, ty) <- lookupTyEnv n env = return (P Bound n ty, ty)

55 | (P nt n' ty : _) <- lookupP Nothing n ctxt = return (P nt n' ty, ty)

56− | otherwise = do fail $ "No such variable " ++ show n ++ " in " ++ show (map fst env)

56+ | otherwise = do lift $ tfail $ NoSuchVariable n

57 chk env (RApp f a)

58 = do (fv, fty) <- chk env f

59 (av, aty) <- chk env a

src/Idris/AbsSyntax.hs+19−15

@@ -484,7 +484,7 @@ data PTerm = PQuote Raw

484 | PMetavar Name

485 | PProof [PTactic]

486 | PTactics [PTactic] -- as PProof, but no auto solving

487− | PElabError String -- error to report on elaboration

487+ | PElabError Err -- error to report on elaboration

488 | PImpossible -- special case for declaring when an LHS can't typecheck

489 deriving Eq

490{-!

@@ -777,7 +777,7 @@ showImp impl tm = se 10 tm where

777 se p PImpossible = "impossible"

778 se p Placeholder = "_"

779 se p (PDoBlock _) = "do block show not implemented"

780− se p (PElabError s) = s

780+ se p (PElabError s) = show s

781-- se p x = "Not implemented"

782

783 sArg (PImp _ _ n tm) = siArg (n, tm)

@@ -1141,9 +1141,9 @@ addImpl' :: Bool -> [Name] -> IState -> PTerm -> PTerm

1141addImpl' inpat env ist ptm = ai env ptm

1142 where

1143 ai env (PRef fc f)

1144− | not (f `elem` env) = aiFn inpat ist fc f []

1144+ | not (f `elem` env) = handleErr $ aiFn inpat ist fc f []

1145 ai env (PHidden (PRef fc f))

1146− | not (f `elem` env) = aiFn False ist fc f []

1146+ | not (f `elem` env) = handleErr $ aiFn False ist fc f []

1147 ai env (PEq fc l r) = let l' = ai env l

1148 r' = ai env r in

1149 PEq fc l' r'

@@ -1162,7 +1162,7 @@ addImpl' inpat env ist ptm = ai env ptm

1162 ai env (PApp fc (PRef _ f) as)

1163 | not (f `elem` env)

1164 = let as' = map (fmap (ai env)) as in

1165− aiFn False ist fc f as'

1165+ handleErr $ aiFn False ist fc f as'

1166 ai env (PApp fc f as) = let f' = ai env f

1167 as' = map (fmap (ai env)) as in

1168 mkPApp fc 1 f' as'

@@ -1185,30 +1185,34 @@ addImpl' inpat env ist ptm = ai env ptm

1185 ai env (PTactics ts) = PTactics (map (fmap (ai env)) ts)

1186 ai env tm = tm

1187

1188+ handleErr (Left err) = PElabError err

1189+ handleErr (Right x) = x

1190+

1188-- if in a pattern, and there are no arguments, and there's no possible

1191-- if in a pattern, and there are no arguments, and there's no possible

1189-- names with zero explicit arguments, don't add implicits.

1192-- names with zero explicit arguments, don't add implicits.

1190

1193

1191−aiFn :: Bool -> IState -> FC -> Name -> [PArg] -> PTerm

1194+aiFn :: Bool -> IState -> FC -> Name -> [PArg] -> Either Err PTerm

1192aiFn True ist fc f []

1195aiFn True ist fc f []

1193 = case lookupCtxt Nothing f (idris_implicits ist) of

1196 = case lookupCtxt Nothing f (idris_implicits ist) of

1194− [] -> PRef fc f

1197+ [] -> Right $ PRef fc f

1195 alts -> if (any (all imp) alts)

1198 alts -> if (any (all imp) alts)

1196 then aiFn False ist fc f [] -- use it as a constructor

1199 then aiFn False ist fc f [] -- use it as a constructor

1197− else PRef fc f

1200+ else Right $ PRef fc f

1198 where imp (PExp _ _ _) = False

1201 where imp (PExp _ _ _) = False

1199 imp _ = True

1202 imp _ = True

1200aiFn inpat ist fc f as

1203aiFn inpat ist fc f as

1201− | f `elem` primNames = PApp fc (PRef fc f) as

1204+ | f `elem` primNames = Right $ PApp fc (PRef fc f) as

1202aiFn inpat ist fc f as

1205aiFn inpat ist fc f as

1203 -- This is where namespaces get resolved by adding PAlternative

1206 -- This is where namespaces get resolved by adding PAlternative

1204 = case lookupCtxtName Nothing f (idris_implicits ist) of

1207 = case lookupCtxtName Nothing f (idris_implicits ist) of

1205− [(f',ns)] -> mkPApp fc (length ns) (PRef fc f') (insertImpl ns as)

1208+ [(f',ns)] -> Right $ mkPApp fc (length ns) (PRef fc f') (insertImpl ns as)

1206 [] -> if f `elem` idris_metavars ist

1209 [] -> if f `elem` idris_metavars ist

1207− then PApp fc (PRef fc f) as

1210+ then Right $ PApp fc (PRef fc f) as

1208− else mkPApp fc (length as) (PRef fc f) as

1211+ else Right $ mkPApp fc (length as) (PRef fc f) as

1212+ alts -> Right $

1209− alts -> PAlternative $

1213+ PAlternative $

1210− map (\(f', ns) -> mkPApp fc (length ns) (PRef fc f')

1214+ map (\(f', ns) -> mkPApp fc (length ns) (PRef fc f')

1211− (insertImpl ns as)) alts

1215+ (insertImpl ns as)) alts

1212 where

1216 where

1213 insertImpl :: [PArg] -> [PArg] -> [PArg]

1217 insertImpl :: [PArg] -> [PArg] -> [PArg]

1214 insertImpl (PExp p l ty : ps) (PExp _ _ tm : given) =

1218 insertImpl (PExp p l ty : ps) (PExp _ _ tm : given) =

src/Idris/DSL.hs+5−5

@@ -38,7 +38,7 @@ expandDo dsl (PReturn fc) = dsl_return dsl

38expandDo dsl (PDoBlock ds) = expandDo dsl $ block (dsl_bind dsl) ds

39 where

40 block b [DoExp fc tm] = tm

41− block b [a] = PElabError "Last statement in do block must be an expression"

41+ block b [a] = PElabError (Msg "Last statement in do block must be an expression")

42 block b (DoBind fc n tm : rest)

43 = PApp fc b [pexp tm, pexp (PLam n Placeholder (block b rest))]

44 block b (DoBindP fc p tm : rest)

@@ -53,7 +53,7 @@ expandDo dsl (PDoBlock ds) = expandDo dsl $ block (dsl_bind dsl) ds

53 = PApp fc b

54 [pexp tm,

55 pexp (PLam (MN 0 "bindx") Placeholder (block b rest))]

56− block b _ = PElabError "Invalid statement in do block"

56+ block b _ = PElabError (Msg "Invalid statement in do block")

58expandDo dsl (PIdiom fc e) = expandDo dsl $ unIdiom (dsl_apply dsl) (dsl_pure dsl) fc e

59expandDo dsl t = t

@@ -62,7 +62,7 @@ var :: DSL -> Name -> PTerm -> Int -> PTerm

62var dsl n t i = v' i t where

63 v' i (PRef fc x) | x == n =

64 case dsl_var dsl of

65− Nothing -> PElabError "No 'variable' defined in dsl"

65+ Nothing -> PElabError (Msg "No 'variable' defined in dsl")

66 Just v -> PApp fc v [pexp (mkVar fc i)]

67 v' i (PLam n ty sc)

68 | Nothing <- dsl_lambda dsl

@@ -85,10 +85,10 @@ var dsl n t i = v' i t where

85 v' i t = t

87 mkVar fc 0 = case index_first dsl of

88− Nothing -> PElabError "No index_first defined"

88+ Nothing -> PElabError (Msg "No index_first defined")

89 Just f -> f

90 mkVar fc n = case index_next dsl of

91− Nothing -> PElabError "No index_next defined"

91+ Nothing -> PElabError (Msg "No index_next defined")

92 Just f -> PApp fc f [pexp (mkVar fc (n-1))]

94unIdiom :: PTerm -> PTerm -> FC -> PTerm -> PTerm

src/Idris/Delaborate.hs+1

@@ -75,6 +75,7 @@ pshow i (NotInjective p x y) = "Can't verify injectivity of " ++ show (delab i p

75 " when unifying " ++ show (delab i x) ++ " and " ++

76 show (delab i y)

77pshow i (CantResolve c) = "Can't resolve type class " ++ show (delab i c)

78+pshow i (NoSuchVariable n) = "No such variable " ++ show n

78pshow i (IncompleteTerm t) = "Incomplete term " ++ show t

79pshow i (IncompleteTerm t) = "Incomplete term " ++ show t

79pshow i UniverseError = "Universe inconsistency"

80pshow i UniverseError = "Universe inconsistency"

80pshow i ProgramLineComment = "Program line next to comment"

81pshow i ProgramLineComment = "Program line next to comment"

src/Idris/ElabDecls.hs+1−1

@@ -391,7 +391,7 @@ elabClause info fc tcgen (PWith fname lhs_in withs wval_in withblock)

391 (clhs, clhsty) <- recheckC ctxt fc [] lhs_tm

392 logLvl 5 ("Checked " ++ show clhs)

393 let bargs = getPBtys lhs_tm

394− let wval = addImpl i wval_in

394+ let wval = addImplBound i (map fst bargs) wval_in

395 logLvl 5 ("Checking " ++ showImp True wval)

396 -- Elaborate wval in this context

397 ((wval', defer, is), _) <-

src/Idris/ElabTerm.hs+14−16

@@ -4,6 +4,7 @@ module Idris.ElabTerm where

5import Idris.AbsSyntax

6import Idris.DSL

7+import Idris.Delaborate

8import Core.Elaborate hiding (Tactic(..))

9import Core.Elaborate hiding (Tactic(..))

9import Core.TT

10import Core.TT

@@ -233,12 +234,6 @@ elab ist info pattern tcgen fn tm

233 when (not pattern || (ina && not tcgen)) $

234 when (not pattern || (ina && not tcgen)) $

234 mapM_ (\n -> do focus n

235 mapM_ (\n -> do focus n

235 resolveTC 7 fn ist) (ivs' \\ ivs)

236 resolveTC 7 fn ist) (ivs' \\ ivs)

236−-- ivs <- get_instances

237−-- when (not (null ivs)) $

238−-- do t <- get_term

239−-- trace (show ivs ++ "\n" ++ show t) $

240−-- mapM_ (\n -> do focus n

241−-- resolveTC ist) ivs

242 where tcArg (n, PConstraint _ _ Placeholder) = True

237 where tcArg (n, PConstraint _ _ Placeholder) = True

243 tcArg _ = False

238 tcArg _ = False

244

239

@@ -258,7 +253,7 @@ elab ist info pattern tcgen fn tm

258 elab' ina (PTactics ts)

253 elab' ina (PTactics ts)

259 | not pattern = do mapM_ (runTac False ist) ts

254 | not pattern = do mapM_ (runTac False ist) ts

260 | otherwise = elab' ina Placeholder

255 | otherwise = elab' ina Placeholder

261− elab' ina (PElabError e) = fail e

256+ elab' ina (PElabError e) = fail (pshow ist e)

262 elab' ina@(_, a) c@(PCase fc scr opts)

257 elab' ina@(_, a) c@(PCase fc scr opts)

263 = do attack

258 = do attack

264 tyn <- unique_hole (MN 0 "scty")

259 tyn <- unique_hole (MN 0 "scty")

@@ -344,15 +339,17 @@ trivial ist = try (do elab ist toplevel False False (MN 0 "tac") (PRefl (FC "prf

344

339

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

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

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

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

342+resolveTC 1 fn ist = try (trivial ist) (resolveTC 0 fn ist)

347resolveTC depth fn ist

343resolveTC depth fn ist

348 = try (trivial ist)

344 = try (trivial ist)

349 (do t <- goal

345 (do t <- goal

350 let (tc, ttypes) = unApply t

346 let (tc, ttypes) = unApply t

351− needsDefault t tc ttypes

347+ scopeOnly <- needsDefault t tc ttypes

352 tm <- get_term

348 tm <- get_term

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

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

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

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

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

355− blunderbuss t (map fst (ctxtAlist (tt_ctxt ist))))

352+ blunderbuss t depth' (map fst (ctxtAlist (tt_ctxt ist))))

356 where

353 where

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

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

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

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

@@ -361,17 +358,18 @@ resolveTC depth fn ist

361 = do focus a

358 = do focus a

362 fill (RConstant IType) -- default Int

359 fill (RConstant IType) -- default Int

363 solve

360 solve

361+ return False

364−-- needsDefault t f as

362+ needsDefault t f as

365−-- | all boundVar as = fail $ "Can't resolve " ++ show t

363+ | all boundVar as = return True -- fail $ "Can't resolve " ++ show t

366− needsDefault t f a = return ()

364+ needsDefault t f a = return False -- trace (show t) $ return ()

367

365

368 boundVar (P Bound _ _) = True

366 boundVar (P Bound _ _) = True

369 boundVar _ = False

367 boundVar _ = False

370

368

371− blunderbuss t [] = lift $ tfail $ CantResolve t

369+ blunderbuss t d [] = lift $ tfail $ CantResolve t

372− blunderbuss t (n:ns) | n /= fn && tcname n = try (resolve n depth)

370+ blunderbuss t d (n:ns) | n /= fn && tcname n = try (resolve n d)

373− (blunderbuss t ns)

371+ (blunderbuss t d ns)

374− | otherwise = blunderbuss t ns

372+ | otherwise = blunderbuss t d ns

375

373

376 resolve n depth

374 resolve n depth

377 | depth == 0 = fail $ "Can't resolve type class"

375 | depth == 0 = fail $ "Can't resolve type class"

src/Idris/IBC.hs+4−4

@@ -836,8 +836,8 @@ instance Binary PTerm where

836 put x1

837 PTactics x1 -> do putWord8 22

838 put x1

839− PElabError x1 -> do putWord8 23

839+-- PElabError x1 -> do putWord8 23

840− put x1

840+-- put x1

841 PImpossible -> putWord8 24

842 get

843 = do i <- getWord8

@@ -904,8 +904,8 @@ instance Binary PTerm where

904 return (PProof x1)

905 22 -> do x1 <- get

906 return (PTactics x1)

907− 23 -> do x1 <- get

907+-- 23 -> do x1 <- get

908− return (PElabError x1)

908+-- return (PElabError x1)

909 24 -> return PImpossible

910 _ -> error "Corrupted binary data for PTerm"

911