bde101f · Idris-dev · git.iko.soy

docs/effects/simpleeff.rst+1−1

compare with master

unifiedsplit

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

416

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

418 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

420 Nothing => do putStrLn "Input error"

421 read_vec

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

src/Idris/Elab/Term.hs+25

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

1028 solve

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

1030 = do attack

1031+

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

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

1032 claim tyn RType

1033 claim tyn RType

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

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

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

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

1035 claim valn (Var tyn)

1036 claim valn (Var tyn)

1036 letbind scvn (Var tyn) (Var valn)

1037 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+

1037 focus valn

1047 focus valn

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

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

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

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

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

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

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

1085 _ -> n

1095 _ -> n

1086

1096

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+

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

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

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

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

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

1114 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)]

182

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

184vecfoo = 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 @@

1#!/usr/bin/env bash

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

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

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

4rm -f *.ibc

5rm -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

5+

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"