ed64e76 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Better type class resolutions

ed64e76Edwin Brady15 years ago

interp.idr+4−1

compare with master

unifiedsplit

@@ -17,14 +17,17 @@ using (G : Vect Ty n) {

18 data Expr : Vect Ty n -> Ty -> Set where

19 Var : (i : Fin n) -> Expr G (vlookup i G)

20− | Val : (x : interpTy a) -> Expr G a

20+ | Val : (x : Int) -> Expr G TyInt

21 | Lam : Expr (a :: G) t -> Expr G (TyFun a t)

22 | App : Expr G (TyFun a t) -> Expr G a -> Expr G t

23 | Op : (Int -> Int -> interpTy c) ->

24 Expr G TyInt -> Expr G TyInt -> Expr G c

25+ -- | Op' : (interpTy a -> interpTy b -> interpTy c) ->

26+ -- Expr G a -> Expr G b -> Expr G c

25 | If : Expr G TyBool -> Expr G a -> Expr G a -> Expr G a

27 | If : Expr G TyBool -> Expr G a -> Expr G a -> Expr G a

26 | Bind : Expr G a -> (interpTy a -> Expr G b) -> Expr G b;

28 | Bind : Expr G a -> (interpTy a -> Expr G b) -> Expr G b;

30+

28 interp : Env G -> [static] Expr G t -> interpTy t;

31 interp : Env G -> [static] Expr G t -> interpTy t;

29 interp env (Var i) = envLookup i env;

32 interp env (Var i) = envLookup i env;

30 interp env (Val x) = x;

33 interp env (Val x) = x;

lib/list.idr+5

@@ -23,9 +23,14 @@ drop 0 xs = xs;

23drop n Nil = Nil;

24drop n (Cons x xs) = drop (n-1) xs;

26+map : (a -> b) -> List a -> List b;

27+map f Nil = Nil;

28+map f (Cons x xs) = Cons (f x) (map f xs);

29+

26filter : (y -> Bool) -> List y -> List y;

30filter : (y -> Bool) -> List y -> List y;

27filter pred Nil = Nil;

31filter pred Nil = Nil;

28filter pred (Cons x xs) with (pred x, filter pred xs) {

32filter pred (Cons x xs) with (pred x, filter pred xs) {

29 filter pred (Cons x xs) | (True, fxs) = Cons x fxs;

33 filter pred (Cons x xs) | (True, fxs) = Cons x fxs;

30 filter pred (Cons x xs) | (False, fxs) = fxs;

34 filter pred (Cons x xs) | (False, fxs) = fxs;

31}

35}

36+

lib/prelude.idr+8

@@ -16,3 +16,11 @@ putStrLn x = putStr (x ++ "\n");

16readLine : IO String;

17readLine = mkForeign (FFun "readStr" Nil FString);

19+-- Show and instances

20+

21+data Show : Set -> Set where

22+ ShowInstance : (show : a -> String) -> Show a;

23+

24+show : Show a => a -> String;

25+show {{ShowInstance s}} v = s v;

26+

src/Core/Elaborate.hs+12−6

@@ -258,7 +258,7 @@ apply_elab n args =

258 env <- get_env

259 claims <- doClaims (normalise ctxt env ty) args []

260 prep_fill n (map fst claims)

261− elabClaims claims

261+ elabClaims [] True claims

262 complete_fill

263 end_unify

264 where

@@ -271,11 +271,17 @@ apply_elab n args =

271 doClaims t [] claims = return (reverse claims)

272 doClaims _ _ _ = fail $ "Wrong number of arguments for " ++ show n

273

274− elabClaims [] = return ()

274+ elabClaims failed r []

275+ | null failed = return ()

276+ | otherwise = if r then elabClaims [] False failed

277+ else return ()

275− elabClaims ((n, Nothing) : xs) = elabClaims xs

278+ elabClaims failed r ((n, Nothing) : xs) = elabClaims failed r xs

276− elabClaims ((n, Just elaboration) : xs) =

279+ elabClaims failed r (e@(n, Just elaboration) : xs)

280+ | r = try (do ES p _ _ <- get

281+ focus n; elaboration; elabClaims failed r xs)

282+ (elabClaims (e : failed) r xs)

277− do ES p _ _ <- get

283+ | otherwise = do ES p _ _ <- get

278− focus n; elaboration; elabClaims xs

284+ focus n; elaboration; elabClaims failed r xs

279

285

280 mkMN n@(MN _ _) = n

286 mkMN n@(MN _ _) = n

281 mkMN n@(UN [x]) = MN 0 x

287 mkMN n@(UN [x]) = MN 0 x

src/Core/ProofState.hs+1−1

@@ -260,7 +260,7 @@ solve ctxt env (Bind x (Guess ty val) sc)

260 | pureTerm val = do action (\ps -> ps { holes = holes ps \\ [x],

261 instances = instances ps \\ [x] })

262 return $ {- Bind x (Let ty val) sc -} instantiate val (pToV x sc)

263− | otherwise = fail "I see a hole in your solution."

263+ | otherwise = fail $ "I see a hole in your solution. " ++ showEnv env val

264solve _ _ h = fail $ "Not a guess " ++ show h

265

266intro :: Maybe Name -> RunTactic

src/Idris/Delaborate.hs+1−1

@@ -51,6 +51,6 @@ pshow :: IState -> Err -> String

51pshow i (Msg s) = s

52pshow i (CantUnify x y e) = "Can't unify " ++ show (delab i x)

53 ++ " with " ++ show (delab i y)

54− -- ++ "\n\t(" ++ pshow i e ++ ")"

54+-- ++ "\n\t(" ++ pshow i e ++ ")"

55pshow i (At f e) = show f ++ ":" ++ pshow i e

src/Idris/ElabDecls.hs+27−17

@@ -437,13 +437,13 @@ elab ist info pattern tm

437 ivs <- get_instances

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

439 solve

440− elabArgs ns (map (\x -> (lazyarg x, getTm x)) args))

440+ elabArgs [] True ns (map (\x -> (lazyarg x, getTm x)) args))

441 (do apply_elab f (map toElab args)

442 solve)

443 ivs' <- get_instances

444 when (not pattern) $

445 mapM_ (\n -> do focus n

446− resolveTC ist) (ivs' \\ ivs)

446+ resolveTC 10 ist) (ivs' \\ ivs)

447-- ivs <- get_instances

448-- when (not (null ivs)) $

449-- do t <- get_term

@@ -464,16 +464,22 @@ elab ist info pattern tm

464 elab' (PElabError e) = fail e

465 elab' x = fail $ "Not implemented " ++ show x

466

467− elabArgs [] _ = return ()

467+ elabArgs failed retry [] _

468+ | retry = let (ns, ts) = unzip (reverse failed) in

469+ elabArgs [] False ns ts

470+ | otherwise = return ()

468− elabArgs (n:ns) ((_, Placeholder) : args) = elabArgs ns args

471+ elabArgs failed r (n:ns) ((_, Placeholder) : args)

472+ = elabArgs failed r ns args

469− elabArgs (n:ns) ((lazy, t) : args)

473+ elabArgs failed r (n:ns) ((lazy, t) : args)

470− | lazy && not pattern

474+ | lazy && not pattern

471− = do focus n; elab' (PApp bi (PRef bi (UN ["lazy"]))

475+ = do elabArg n (PApp bi (PRef bi (UN ["lazy"]))

472− [pimp (UN ["a"]) Placeholder,

476+ [pimp (UN ["a"]) Placeholder,

473− pexp t]);

477+ pexp t]);

478+ | otherwise = elabArg n t

479+ where elabArg n t = if r

474− elabArgs ns args

480+ then try (do focus n; elabE t; elabArgs failed r ns args)

475− | otherwise

481+ (elabArgs ((n,(lazy, t)):failed) r ns args)

476− = do focus n; elabE t; elabArgs ns args

482+ else do focus n; elabE t; elabArgs failed r ns args

477

483

478trivial :: IState -> Elab ()

484trivial :: IState -> Elab ()

479trivial ist = try (elab ist toplevel False (PRefl (FC "prf" 0)))

485trivial ist = try (elab ist toplevel False (PRefl (FC "prf" 0)))

@@ -484,26 +490,30 @@ trivial ist = try (elab ist toplevel False (PRefl (FC "prf" 0)))

484 tryAll (x:xs) = try (elab ist toplevel False (PRef (FC "prf" 0) x))

490 tryAll (x:xs) = try (elab ist toplevel False (PRef (FC "prf" 0) x))

485 (tryAll xs)

491 (tryAll xs)

486

492

487−resolveTC :: IState -> Elab ()

493+resolveTC :: Int -> IState -> Elab ()

488−resolveTC ist = do t <- goal

494+resolveTC depth ist

495+ = do t <- goal

489 tm <- get_term

496 tm <- get_term

490 try (trivial ist)

497 try (trivial ist)

491 (blunderbuss t (map fst (toAlist (tt_ctxt ist))))

498 (blunderbuss t (map fst (toAlist (tt_ctxt ist))))

492 where

499 where

493 blunderbuss t [] = fail $ "Can't resolve type class " ++ show t

500 blunderbuss t [] = fail $ "Can't resolve type class " ++ show t

494− blunderbuss t (n:ns) | tcname n = try (resolve n)

501+ blunderbuss t (n:ns) | tcname n = try (resolve n depth)

495 (blunderbuss t ns)

502 (blunderbuss t ns)

496 | otherwise = blunderbuss t ns

503 | otherwise = blunderbuss t ns

497 tcname (UN (('@':_) : _)) = True

504 tcname (UN (('@':_) : _)) = True

498 tcname _ = False

505 tcname _ = False

499

506

507+ resolve n depth

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

509+ | otherwise

500− resolve n = do t <- goal

510+ = do t <- goal

501 let imps = case lookupCtxt n (idris_implicits ist) of

511 let imps = case lookupCtxt n (idris_implicits ist) of

502 Nothing -> []

512 Nothing -> []

503 Just args -> map isImp args

513 Just args -> map isImp args

504 args <- apply (Var n) imps

514 args <- apply (Var n) imps

505 mapM_ (\ (_,n) -> do focus n

515 mapM_ (\ (_,n) -> do focus n

506− resolveTC ist)

516+ resolveTC (depth - 1) ist)

507 (filter (\ (x, y) -> not x) (zip imps args))

517 (filter (\ (x, y) -> not x) (zip imps args))

508 solve

518 solve

509 where isImp (PImp _ _ _) = True

519 where isImp (PImp _ _ _) = True