ed64e76 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Better type class resolutions

commited64e76314f8eeebe8d52c70bd24197060805ca3 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateSat 5 Nov 2011, 10:23 (15 years ago) parent00052c8

7 files changed+58−26

compare with master

unifiedsplit

interp.idr+4−1 lib/list.idr+5 lib/prelude.idr+8 src/Core/Elaborate.hs+12−6 src/Core/ProofState.hs+1−1 src/Idris/Delaborate.hs+1−1 src/Idris/ElabDecls.hs+27−17

interp.idr+4−1

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

1717

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

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

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

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

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

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

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

2424 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

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

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

2729

30+

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

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

3033 interp env (Val x) = x;

lib/list.idr+5

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

2323drop n Nil = Nil;

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

2525

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+

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

2731filter pred Nil = Nil;

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

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

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

3135}

36+

lib/prelude.idr+8

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

1616readLine : IO String;

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

1818

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 =

258258 env <- get_env

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

260260 prep_fill n (map fst claims)

261− elabClaims claims

261+ elabClaims [] True claims

262262 complete_fill

263263 end_unify

264264 where

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

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

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

273273

274− elabClaims [] = return ()

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

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

277− do ES p _ _ <- get

278− focus n; elaboration; elabClaims xs

274+ elabClaims failed r []

275+ | null failed = return ()

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

277+ else return ()

278+ elabClaims failed r ((n, Nothing) : xs) = elabClaims failed r 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)

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

284+ focus n; elaboration; elabClaims failed r xs

279285

280286 mkMN n@(MN _ _) = n

281287 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)

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

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

262262 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

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

265265

266266intro :: Maybe Name -> RunTactic

src/Idris/Delaborate.hs+1−1

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

5151pshow i (Msg s) = s

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

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

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

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

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

5656

src/Idris/ElabDecls.hs+27−17

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

437437 ivs <- get_instances

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

439439 solve

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

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

441441 (do apply_elab f (map toElab args)

442442 solve)

443443 ivs' <- get_instances

444444 when (not pattern) $

445445 mapM_ (\n -> do focus n

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

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

447447-- ivs <- get_instances

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

449449-- do t <- get_term

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

464464 elab' (PElabError e) = fail e

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

466466

467− elabArgs [] _ = return ()

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

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

470− | lazy && not pattern

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

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

473− pexp t]);

474− elabArgs ns args

475− | otherwise

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

467+ elabArgs failed retry [] _

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

469+ elabArgs [] False ns ts

470+ | otherwise = return ()

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

472+ = elabArgs failed r ns args

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

474+ | lazy && not pattern

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

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

477+ pexp t]);

478+ | otherwise = elabArg n t

479+ where elabArg n t = if r

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

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

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

477483

478484trivial :: IState -> Elab ()

479485trivial 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)))

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

485491 (tryAll xs)

486492

487−resolveTC :: IState -> Elab ()

488−resolveTC ist = do t <- goal

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

494+resolveTC depth ist

495+ = do t <- goal

489496 tm <- get_term

490497 try (trivial ist)

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

492499 where

493500 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)

495502 (blunderbuss t ns)

496503 | otherwise = blunderbuss t ns

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

498505 tcname _ = False

499506

500− resolve n = do t <- goal

507+ resolve n depth

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

509+ | otherwise

510+ = do t <- goal

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

502512 Nothing -> []

503513 Just args -> map isImp args

504514 args <- apply (Var n) imps

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

506− resolveTC ist)

516+ resolveTC (depth - 1) ist)

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

508518 solve

509519 where isImp (PImp _ _ _) = True