889d848 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Change 'run' in neweffects to add defaults

In most cases, this is the easiest thing to do, creating a default resource value for the resource type using the 'Effect.Default' type class. Where it's not possible (or undesirable) there is a runInit (correspondingly runPureInit) function which allows explicit resource lists.

commit889d8487e196db2e1762c671c31746521331acaf authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSat 1 Feb 2014, 17:13 (13 years ago) parent9a926d5

6 files changed+48−49

compare with master

unifiedsplit

libs/base/Language/Reflection.idr+2 libs/neweffects/Effect/StdIO.idr+10−36 libs/neweffects/Effects.idr+32−12 src/Idris/AbsSyntaxTree.hs+1−1 src/Idris/ElabTerm.hs+2 src/Idris/ParseExpr.hs+1

libs/base/Language/Reflection.idr+2

@@ -167,6 +167,8 @@ data Tactic = Try Tactic Tactic

167167 -- ^ apply both tactics in sequence

168168 | Trivial

169169 -- ^ intelligently construct the proof target from the context

170+ | Instance

171+ -- ^ resolve a type class

170172 | Solve

171173 -- ^ infer the proof target from the context

172174 | Intros

libs/neweffects/Effect/StdIO.idr+10−36

@@ -6,35 +6,14 @@ import Control.IOExcept

66data StdIO : Effect where

77 PutStr : String -> { () } StdIO ()

88 GetStr : { () } StdIO String

9+ PutCh : Char -> { () } StdIO ()

10+ GetCh : { () } StdIO Char

911

1012instance Handler StdIO IO where

1113 handle () (PutStr s) k = do putStr s; k () ()

1214 handle () GetStr k = do x <- getLine; k x ()

13−

14−{-

15−instance Handler StdIO (IOExcept a) where

16− handle () (PutStr s) k = do ioe_lift (putStr s); k () ()

17− handle () GetStr k = do x <- ioe_lift getLine; k () x

18−

19−-- Handle effects in a pure way, for simulating IO for unit testing/proof

20−

21−data IOStream a = MkStream (List String -> (a, List String))

22−

23−instance Handler StdIO IOStream where

24− handle () (PutStr s) k

25− = MkStream (\x => case k () () of

26− MkStream f => let (res, str) = f x in

27− (res, s :: str))

28− handle {a} () GetStr k

29− = MkStream (\x => case x of

30− [] => cont "" []

31− (t :: ts) => cont t ts)

32− where

33− cont : String -> List String -> (a, List String)

34− cont t ts = case k () t of

35− MkStream f => f ts

36−

37−-}

15+ handle () (PutCh c) k = do putChar c; k () ()

16+ handle () GetCh k = do x <- getChar; k x ()

3817

3918--- The Effect and associated functions

4019

@@ -44,20 +23,15 @@ STDIO = MkEff () StdIO

4423putStr : Handler StdIO e => String -> { [STDIO] } Eff e ()

4524putStr s = PutStr s

4625

26+putChar : Handler StdIO e => Char -> { [STDIO] } Eff e ()

27+putChar c = PutCh c

28+

4729putStrLn : Handler StdIO e => String -> { [STDIO] } Eff e ()

4830putStrLn s = putStr (s ++ "\n")

4931

5032getStr : Handler StdIO e => { [STDIO] } Eff e String

5133getStr = GetStr

5234

53−-- mkStrFn : Env IOStream xs ->

54−-- Eff IOStream xs a ->

55−-- List String -> (a, List String)

56−-- mkStrFn {a} env p input = case mkStrFn' of

57−-- MkStream f => f input

58−-- where injStream : a -> IOStream a

59−-- injStream v = MkStream (\x => (v, []))

60−-- mkStrFn' : IOStream a

61−-- mkStrFn' = runWith injStream env p

62−--

63−--

35+getChar : Handler StdIO e => { [STDIO] } Eff e Char

36+getChar = GetCh

37+

libs/neweffects/Effects.idr+32−12

@@ -41,7 +41,7 @@ namespace Env

4141 data Env : (m : Type -> Type) -> List EFFECT -> Type where

4242 Nil : Env m Nil

4343 (::) : Handler eff m => a -> Env m xs -> Env m (MkEff a eff :: xs)

44−

44+

4545data EffElem : Effect -> Type ->

4646 List EFFECT -> Type where

4747 Here : EffElem x a (MkEff a x :: xs)

@@ -96,12 +96,28 @@ reflectSubList (x :: xs)

9696reflectSubList (x ++ y) = Refine "subListId" `Seq` Solve

9797reflectSubList _ = Refine "subListId" `Seq` Solve

9898

99+%reflection

100+reflectDefaultList : List a -> Tactic

101+reflectDefaultList [] = Refine "enil" `Seq` Solve

102+reflectDefaultList (x :: xs)

103+ = Refine "econs" `Seq`

104+ (Solve `Seq`

105+ (Instance `Seq`

106+ (Refine "default" `Seq`

107+ (Solve `Seq`

108+ (Instance `Seq`

109+ (reflectDefaultList xs))))))

110+reflectDefaultList (x ++ y) = Refine "Nil" `Seq` Solve

111+reflectDefaultList _ = Refine "Nil" `Seq` Solve

112+

99113%reflection

100114reflectEff : (P : Type) -> Tactic

101115reflectEff (EffElem m a xs)

102116 = reflectListEffElem xs `Seq` Solve

103117reflectEff (SubList xs ys)

104118 = reflectSubList ys `Seq` Solve

119+reflectEff (Env m xs)

120+ = reflectDefaultList xs `Seq` Solve

105121

106122updateResTy : (val : t) ->

107123 (xs : List EFFECT) -> EffElem e a xs -> e t a b ->

@@ -232,10 +248,8 @@ eff {xs = [l ::: x]} env (l :- prog) k

232248 = let env' = unlabel env in

233249 eff env' prog (\p', envk => k p' (relabel l envk))

234250

235−run : Applicative m => Env m xs -> Eff m a xs xs' -> m a

236−run env prog = eff env prog (\r, env => pure r)

237−

238−-- yuck :)

251+-- yuck :) Haven't got type class instances working nicely in tactic

252+-- proofs yet, so just brute force it.

239253syntax MkDefaultEnv = (| [], [default], [default, default],

240254 [default, default, default],

241255 [default, default, default, default],

@@ -244,19 +258,25 @@ syntax MkDefaultEnv = (| [], [default], [default, default],

244258 [default, default, default, default, default, default, default],

245259 [default, default, default, default, default, default, default, default] |)

246260

247−run' : Applicative m => {default MkDefaultEnv env : Env m xs} -> Eff m a xs xs' -> m a

248−run' {env} prog = eff env prog (\r, env => pure r)

261+run : Applicative m => {default MkDefaultEnv env : Env m xs} -> Eff m a xs xs' -> m a

262+run {env} prog = eff env prog (\r, env => pure r)

249263

250−runEnv : Applicative m => Env m xs -> Eff m a xs xs' ->

251− m (x : a ** Env m (xs' x))

252−runEnv env prog = eff env prog (\r, env => pure (r ** env))

264+runPure : {default MkDefaultEnv env : Env id xs} -> Eff id a xs xs' -> a

265+runPure {env} prog = eff env prog (\r, env => r)

266+

267+runInit : Applicative m => Env m xs -> Eff m a xs xs' -> m a

268+runInit env prog = eff env prog (\r, env => pure r)

253269

254−runPure : Env id xs -> Eff id a xs xs' -> a

255−runPure env prog = eff env prog (\r, env => r)

270+runPureInit : Env id xs -> Eff id a xs xs' -> a

271+runPureInit env prog = eff env prog (\r, env => r)

256272

257273runWith : (a -> m a) -> Env m xs -> Eff m a xs xs' -> m a

258274runWith inj env prog = eff env prog (\r, env => inj r)

259275

276+runEnv : Applicative m => Env m xs -> Eff m a xs xs' ->

277+ m (x : a ** Env m (xs' x))

278+runEnv env prog = eff env prog (\r, env => pure (r ** env))

279+

260280-- some higher order things

261281

262282mapE : Applicative m => (a -> {xs} Eff m b) -> List a -> {xs} Eff m (List b)

src/Idris/AbsSyntaxTree.hs+1−1

@@ -673,7 +673,7 @@ data PTactic' t = Intro [Name] | Intros | Focus Name

673673 | Equiv t

674674 | MatchRefine Name

675675 | LetTac Name t | LetTacTy Name t t

676− | Exact t | Compute | Trivial

676+ | Exact t | Compute | Trivial | TCInstance

677677 | ProofSearch (Maybe Name) Name [Name]

678678 | Solve

679679 | Attack

src/Idris/ElabTerm.hs+2

@@ -969,6 +969,7 @@ runTac autoSolve ist tac

969969 when autoSolve solveAll

970970 runT Compute = compute

971971 runT Trivial = do trivial' ist; when autoSolve solveAll

972+ runT TCInstance = runT (Exact (PResolveTC emptyFC))

972973 runT (ProofSearch top n hints)

973974 = do proofSearch' ist top n hints; when autoSolve solveAll

974975 runT (Focus n) = focus n

@@ -1088,6 +1089,7 @@ reflm n = sNS (sUN n) ["Reflection", "Language"]

10881089reify :: IState -> Term -> ElabD PTactic

10891090reify _ (P _ n _) | n == reflm "Intros" = return Intros

10901091reify _ (P _ n _) | n == reflm "Trivial" = return Trivial

1092+reify _ (P _ n _) | n == reflm "Instance" = return TCInstance

10911093reify _ (P _ n _) | n == reflm "Solve" = return Solve

10921094reify _ (P _ n _) | n == reflm "Compute" = return Compute

10931095reify ist t@(App _ _)

src/Idris/ParseExpr.hs+1

@@ -1152,6 +1152,7 @@ tactic syn = do reserved "intro"; ns <- sepBy (indentPropHolds gtProp *> name) (

11521152 return $ TSeq t (mergeSeq ts)

11531153 <|> do reserved "compute"; return Compute

11541154 <|> do reserved "trivial"; return Trivial

1155+ <|> do reserved "instance"; return TCInstance

11551156 <|> do reserved "solve"; return Solve

11561157 <|> do reserved "attack"; return Attack

11571158 <|> do reserved "state"; return ProofState