0e3d87e · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

More flexible type class instances (on functions)

Supports this sort of thing: instance Functor (\x => Int -> x) where map f intf = \x => f (intf x) instance Applicative (\x => Int -> x) where pure v = \x => v (<$>) f a = \x => f x (a x) instance Monad (\x => Int -> x) where f >>= k = \x => k (f x) x

commit0e3d87e84836172a3664614873233d36901073eb authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSun 24 Nov 2013, 00:59 (13 years ago) parentdbbdbb2

8 files changed+63−8

compare with master

unifiedsplit

src/Core/ProofState.hs+1 src/Core/Unify.hs+9 src/Idris/AbsSyntax.hs+4−2 src/Idris/ElabDecls.hs+7−4 src/Idris/ElabTerm.hs+4−2 test/reg027/expected+2 test/reg027/reg027.idr+32 test/reg027/run+4

src/Core/ProofState.hs+1

@@ -530,6 +530,7 @@ forall :: Name -> Raw -> RunTactic

530530forall n ty ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =

531531 do (tyv, tyt) <- lift $ check ctxt env ty

532532 unify' ctxt env tyt (TType (UVar 0))

533+ unify' ctxt env t (TType (UVar 0))

533534 return $ Bind n (Pi tyv) (Bind x (Hole t) (P Bound x t))

534535forall n ty ctxt env _ = fail "Can't pi bind here"

535536

src/Core/Unify.hs+9

@@ -263,6 +263,15 @@ unify ctxt env topx topy dont holes =

263263-- = un' False ((x,y):bnames) sx sy

264264-- un' fn bnames (Bind x (PVTy _) sx) (Bind y (PVTy _) sy)

265265-- = un' False ((x,y):bnames) sx sy

266+

267+ -- f D unifies with t -> D. This is dubious, but it helps with type

268+ -- class resolution for type classes over functions.

269+

270+ un' fn bnames (App f x) (Bind n (Pi t) y)

271+ | noOccurrence n y && x == y

272+ = un' False bnames f (Bind (MN 0 "uv") (Lam (TType (UVar 0)))

273+ (Bind n (Pi t) (V 1)))

274+

266275 un' fn bnames (Bind x bx sx) (Bind y by sy)

267276 = do h1 <- uB bnames bx by

268277 h2 <- un' False ((x,y):bnames) sx sy

src/Idris/AbsSyntax.hs+4−2

@@ -1396,11 +1396,13 @@ matchClause' names i x y = checkRpts $ match (fullApp x) (fullApp y) where

13961396 match (PApp _ x []) (PRef f n) = match x (PRef f n)

13971397 match (PRef _ n) tm@(PRef _ n')

13981398 | n == n' && not names &&

1399− (not (isConName n (tt_ctxt i)) || tm == Placeholder)

1399+ (not (isConName n (tt_ctxt i) || isFnName n (tt_ctxt i))

1400+ || tm == Placeholder)

14001401 = return [(n, tm)]

14011402 | n == n' = return []

14021403 match (PRef _ n) tm

1403− | not names && (not (isConName n (tt_ctxt i)) || tm == Placeholder)

1404+ | not names && (not (isConName n (tt_ctxt i) ||

1405+ isFnName n (tt_ctxt i)) || tm == Placeholder)

14041406 = return [(n, tm)]

14051407 match (PEq _ l r) (PEq _ l' r') = do ml <- match' l l'

14061408 mr <- match' r r'

src/Idris/ElabDecls.hs+7−4

@@ -48,7 +48,7 @@ checkDef fc ns = do ctxt <- getContext

4848

4949-- | Elaborate a top-level type declaration - for example, "foo : Int -> Int".

5050elabType :: ElabInfo -> SyntaxInfo -> String ->

51− FC -> FnOpts -> Name -> PTerm -> Idris ()

51+ FC -> FnOpts -> Name -> PTerm -> Idris Type

5252elabType info syn doc fc opts n ty' = {- let ty' = piBind (params info) ty_in

5353 n = liftname info n_in in -}

5454 do checkUndefined fc n

@@ -102,6 +102,7 @@ elabType info syn doc fc opts n ty' = {- let ty' = piBind (params info) ty_in

102102 addIBC (IBCCoercion n)

103103 when corec $ do setAccessibility n Frozen

104104 addIBC (IBCAccess n Frozen)

105+ return nty

105106 where

106107 -- for making an internalapp, we only want the explicit ones, and don't

107108 -- want the parameters, so just take the arguments which correspond to the

@@ -1416,7 +1417,8 @@ elabInstance info syn fc cs n ps t expn ds

14161417 Nothing -> do mapM_ (checkNotOverlapping i t) (class_instances ci)

14171418 addInstance intInst n iname

14181419 Just _ -> addInstance intInst n iname

1419− elabType info syn "" fc [] iname t

1420+ tt_ty <- elabType info syn "" fc [] iname t

1421+ let nty = normalise (tt_ctxt i) [] tt_ty

14201422 let ips = zip (class_params ci) ps

14211423 let ns = case n of

14221424 NS n ns' -> ns'

@@ -1471,9 +1473,9 @@ elabInstance info syn fc cs n ps t expn ds

14711473 [t'] -> let tret = getRetType t

14721474 tret' = getRetType (delab i t') in

14731475 case matchClause i tret' tret of

1474− Right _ -> overlapping tret tret'

1476+ Right ms -> overlapping tret tret'

14751477 Left _ -> case matchClause i tret tret' of

1476− Right _ -> overlapping tret tret'

1478+ Right ms -> overlapping tret tret'

14771479 Left _ -> return ()

14781480 _ -> return ()

14791481 overlapping t t' = tclift $ tfail (At fc (Msg $

@@ -1622,6 +1624,7 @@ elabDecl' what info (PTy doc s f o n ty)

16221624 | what /= EDefns

16231625 = do iLOG $ "Elaborating type decl " ++ show n ++ show o

16241626 elabType info s doc f o n ty

1627+ return ()

16251628elabDecl' what info (PPostulate doc s f o n ty)

16261629 | what /= EDefns

16271630 = do iLOG $ "Elaborating postulate " ++ show n ++ show o

src/Idris/ElabTerm.hs+4−2

@@ -653,7 +653,7 @@ resolveTC :: Int -> Name -> IState -> ElabD ()

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

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

655655resolveTC depth fn ist

656− = do hnf_compute

656+ = do compute

657657 g <- goal

658658 ptm <- get_term

659659 hs <- get_holes

@@ -719,7 +719,9 @@ resolveTC depth fn ist

719719 [] -> []

720720 [args] -> map isImp (snd args) -- won't be overloaded!

721721 ps <- get_probs

722− args <- match_apply (Var n) imps

722+ tm <- get_term

723+ args <- try' (match_apply (Var n) imps)

724+ (apply (Var n) imps) True

723725 ps' <- get_probs

724726 when (length ps < length ps') $ fail "Can't apply type class"

725727-- traceWhen (all boundVar ttypes) ("Progress: " ++ show t ++ " with " ++ show n) $

test/reg027/expectednew file+2

@@ -0,0 +1,2 @@

1+<<int fn>>

2+6

test/reg027/reg027.idrnew file+32

@@ -0,0 +1,32 @@

1+module Main

3+instance Show (Int -> b) where

4+ show x = "<<int fn>>"

6+instance Show (Char -> b) where

7+ show x = "<<char fn>>"

9+IntFn : Type -> Type

10+IntFn = \x => Int -> x

11+

12+instance Functor IntFn where -- (\x => Int -> x) where

13+ map f intf = \x => f (intf x)

14+

15+instance Applicative (\x => Int -> x) where

16+ pure v = \x => v

17+ (<$>) f a = \x => f x (a x)

18+

19+instance Monad (\x => Int -> x) where

20+ f >>= k = \x => k (f x) x

21+

22+dbl : IntFn Int

23+dbl x = x * 2

24+

25+foo : Int -> String

26+foo = do val <- dbl

27+ \x => show val

28+

29+main : IO ()

30+main = do print dbl

31+ putStrLn (foo 3)

32+

test/reg027/runnew file+4

@@ -0,0 +1,4 @@

1+#!/usr/bin/env bash

2+idris $@ reg027.idr -o reg027

3+./reg027

4+rm -f reg027 *.ibc