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

git.iko.soy/Idris-dev

on master help sign in

Change 'run' in neweffects to add defaults

889d848Edwin Brady13 years ago

libs/base/Language/Reflection.idr+2

compare with master

unifiedsplit

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

167 -- ^ apply both tactics in sequence

168 | Trivial

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

170+ | Instance

171+ -- ^ resolve a type class

170 | Solve

172 | Solve

171 -- ^ infer the proof target from the context

173 -- ^ infer the proof target from the context

172 | Intros

174 | Intros

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

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

6data StdIO : Effect where

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

8 GetStr : { () } StdIO String

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

10+ GetCh : { () } StdIO Char

10instance Handler StdIO IO where

12instance Handler StdIO IO where

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

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

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

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

13−

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

14−{-

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

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−-}

39--- The Effect and associated functions

18--- The Effect and associated functions

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

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

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

45putStr s = PutStr s

24putStr s = PutStr s

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

27+putChar c = PutCh c

28+

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

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

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

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

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

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

51getStr = GetStr

33getStr = GetStr

53−-- mkStrFn : Env IOStream xs ->

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

54−-- Eff IOStream xs a ->

36+getChar = GetCh

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

37+

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−--

libs/neweffects/Effects.idr+32−12

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

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

42 Nil : Env m Nil

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

44−

44+

45data EffElem : Effect -> Type ->

46 List EFFECT -> Type where

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

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

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

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

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+

99%reflection

113%reflection

100reflectEff : (P : Type) -> Tactic

114reflectEff : (P : Type) -> Tactic

101reflectEff (EffElem m a xs)

115reflectEff (EffElem m a xs)

102 = reflectListEffElem xs `Seq` Solve

116 = reflectListEffElem xs `Seq` Solve

103reflectEff (SubList xs ys)

117reflectEff (SubList xs ys)

104 = reflectSubList ys `Seq` Solve

118 = reflectSubList ys `Seq` Solve

119+reflectEff (Env m xs)

120+ = reflectDefaultList xs `Seq` Solve

105

121

106updateResTy : (val : t) ->

122updateResTy : (val : t) ->

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

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

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

232 = let env' = unlabel env in

248 = let env' = unlabel env in

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

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

234

250

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

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

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

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

237−

238−-- yuck :)

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

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

240 [default, default, default],

254 [default, default, default],

241 [default, default, default, default],

255 [default, default, default, default],

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

244 [default, default, default, default, default, default, default],

258 [default, default, default, default, default, default, default],

245 [default, default, default, default, default, default, default, default] |)

259 [default, default, default, default, default, default, default, default] |)

246

260

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

261+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)

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

249

263

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+

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

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

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

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

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

253

269

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

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

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

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

256

272

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

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

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

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

259

275

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+

260-- some higher order things

280-- some higher order things

261

281

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

282mapE : 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

673 | Equiv t

674 | MatchRefine Name

675 | LetTac Name t | LetTacTy Name t t

676− | Exact t | Compute | Trivial

676+ | Exact t | Compute | Trivial | TCInstance

677 | ProofSearch (Maybe Name) Name [Name]

678 | Solve

679 | Attack

src/Idris/ElabTerm.hs+2

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

969 when autoSolve solveAll

970 runT Compute = compute

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

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

972 runT (ProofSearch top n hints)

973 runT (ProofSearch top n hints)

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

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

974 runT (Focus n) = focus n

975 runT (Focus n) = focus n

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

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

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

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

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

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

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

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

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

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

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

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

1093reify ist t@(App _ _)

1095reify ist t@(App _ _)

src/Idris/ParseExpr.hs+1

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

1152 return $ TSeq t (mergeSeq ts)

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

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

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

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

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

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

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

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

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