bde101f · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Better inference for case blocks

Now look at the type of the patterns to infer what the argument type of the new function should be. This helps if, for example, the scrutinee function has some type which needs to be resolved to a specific type class instance, and we can't do this from the scrutinee alone.

commitbde101fbd0fac1a6f6e638edfe972a4737002b64 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSat 14 Nov 2015, 19:10 (11 years ago) parent1cc3acd

5 files changed+56−1

compare with master

unifiedsplit

docs/effects/simpleeff.rst+1−1 src/Idris/Elab/Term.hs+25 test/reg001/reg001.idr+9 test/tutorial006/run+1 test/tutorial006/tutorial006c.idr+20

docs/effects/simpleeff.rst+1−1

@@ -416,7 +416,7 @@ is going to input. We can use ``-1`` to indicate the end of input:

416416

417417 read_vec : Eff (p ** Vect p Int) [STDIO]

418418 read_vec = do putStr "Number (-1 when done): "

419− case the (Maybe Int) $ run (parseNumber (trim !getStr)) of

419+ case run (parseNumber (trim !getStr)) of

420420 Nothing => do putStrLn "Input error"

421421 read_vec

422422 Just v => if (v /= -1)

src/Idris/Elab/Term.hs+25

@@ -1028,12 +1028,22 @@ elab ist info emode opts fn tm

10281028 solve

10291029 elab' ina _ c@(PCase fc scr opts)

10301030 = do attack

1031+

10311032 tyn <- getNameFrom (sMN 0 "scty")

10321033 claim tyn RType

10331034 valn <- getNameFrom (sMN 0 "scval")

10341035 scvn <- getNameFrom (sMN 0 "scvar")

10351036 claim valn (Var tyn)

10361037 letbind scvn (Var tyn) (Var valn)

1038+

1039+ -- Start filling in the scrutinee type, if we can work one

1040+ -- out from the case options

1041+ let scrTy = getScrType (map fst opts)

1042+ case scrTy of

1043+ Nothing -> return ()

1044+ Just ty -> do focus tyn

1045+ elabE ina (Just fc) ty

1046+

10371047 focus valn

10381048 elabE (ina { e_inarg = True }) (Just fc) scr

10391049 -- Solve any remaining implicits - we need to solve as many

@@ -1084,6 +1094,21 @@ elab ist info emode opts fn tm

10841094 Just xs@(_:_) -> sNS n xs

10851095 _ -> n

10861096

1097+ getScrType [] = Nothing

1098+ getScrType (f : os) = maybe (getScrType os) Just (getAppType f)

1099+

1100+ getAppType (PRef _ _ n) =

1101+ case lookupTyName n (tt_ctxt ist) of

1102+ [(n', ty)] | isDConName n' (tt_ctxt ist) ->

1103+ case unApply (getRetTy ty) of

1104+ (P _ tyn _, args) ->

1105+ Just (PApp fc (PRef fc [] tyn)

1106+ (map pexp (map (const Placeholder) args)))

1107+ _ -> Nothing

1108+ _ -> Nothing -- ambiguity is no help to us!

1109+ getAppType (PApp _ t as) = getAppType t

1110+ getAppType _ = Nothing

1111+

10871112 inApp (P _ n _) = [n]

10881113 inApp (App _ f a) = inApp f ++ inApp a

10891114 inApp (Bind n (Let _ v) sc) = inApp v ++ inApp sc

test/reg001/reg001.idr+9

@@ -182,3 +182,12 @@ hVectEx1 = ["Hello",[1,2,3],42,(0,10)]

182182

183183vecfoo : HVect [String, List Nat, Nat, (Nat, Nat)]

184184vecfoo = put (S (S Z)) hVectEx1

185+

186+foom : Monad m => Int -> m Int

187+foom = pure

188+

189+bar : IO ()

190+bar = case foom 5 of

191+ Nothing => print 42

192+ Just n => print n

193+

test/tutorial006/run+1

@@ -1,4 +1,5 @@

11#!/usr/bin/env bash

22idris --nocolour --consolewidth 80 $@ tutorial006a.idr --check

33idris --nocolour --consolewidth 80 $@ tutorial006b.idr --check

4+idris --nocolour --consolewidth 80 $@ tutorial006c.idr -p effects --check

45rm -f *.ibc

test/tutorial006/tutorial006c.idrnew file+20

@@ -0,0 +1,20 @@

1+import Effects

2+import Effect.Exception

3+import Effect.StdIO

4+import Data.Vect

6+read_vec : Eff (p ** Vect p Int) [STDIO]

7+read_vec = do putStr "Number (-1 when done): "

8+ case run (parseNumber (trim !getStr)) of

9+ Nothing => do putStrLn "Input error"

10+ read_vec

11+ Just v => if (v /= -1)

12+ then do (_ ** xs) <- read_vec

13+ pure (_ ** v :: xs)

14+ else pure (_ ** [])

15+ where

16+ parseNumber : String -> Eff Int [EXCEPTION String]

17+ parseNumber str

18+ = if all (\x => isDigit x || x == '-') (unpack str)

19+ then pure (cast str)

20+ else raise "Not a number"