1bc3002 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Some Eff experimentation, adding a 'test' command

1bc3002Edwin Brady13 years ago

effects/Effects.idr+63−1

compare with master

unifiedsplit

@@ -79,7 +79,12 @@ findSubList (S n) ctxt goal

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

80 List EFFECT

81updateResTy {b} (MkEff a e :: xs) Here n = (MkEff b e) :: xs

82−updateResTy (x :: xs) (There p) n = x :: updateResTy xs p n

82+updateResTy (x :: xs) (There p) n = x :: updateResTy xs p n

83+

84+updateResTyImm : (xs : List EFFECT) -> EffElem e a xs -> Type ->

85+ List EFFECT

86+updateResTyImm (MkEff a e :: xs) Here b = (MkEff b e) :: xs

87+updateResTyImm (x :: xs) (There p) b = x :: updateResTyImm xs p b

84infix 5 :::, :-, :=

89infix 5 :::, :-, :=

@@ -111,6 +116,15 @@ data EffM : (m : Type -> Type) ->

111 new : Handler e m =>

116 new : Handler e m =>

112 res -> EffM m (MkEff res e :: xs) (MkEff res' e :: xs') a ->

117 res -> EffM m (MkEff res e :: xs) (MkEff res' e :: xs') a ->

113 EffM m xs xs' a

118 EffM m xs xs' a

119+ test : (prf : EffElem e (Either l r) xs) ->

120+ EffM m (updateResTyImm xs prf l) xs' t ->

121+ EffM m (updateResTyImm xs prf r) xs' t ->

122+ EffM m xs xs' t

123+ test_lbl : {x : lbl} ->

124+ (prf : EffElem e (LRes x (Either l r)) xs) ->

125+ EffM m (updateResTyImm xs prf (LRes x l)) xs' t ->

126+ EffM m (updateResTyImm xs prf (LRes x r)) xs' t ->

127+ EffM m xs xs' t

114 catch : Catchable m err =>

128 catch : Catchable m err =>

115 EffM m xs xs' a -> (err -> EffM m xs xs' a) ->

129 EffM m xs xs' a -> (err -> EffM m xs xs' a) ->

116 EffM m xs xs' a

130 EffM m xs xs' a

@@ -132,6 +146,27 @@ effect' : {a, b: _} -> {e : Effect} ->

132 EffM m xs (updateResTy xs prf eff) t

146 EffM m xs (updateResTy xs prf eff) t

133effect' {prf} e = effect prf e

147effect' {prf} e = effect prf e

134

148

149+data WrapEffM : (m : Type -> Type) ->

150+ List EFFECT -> List EFFECT -> Type -> Type where

151+ WEffM : EffM m xs xs' t -> WrapEffM m xs xs' t

152+

153+-- wrap subprograms to prevent lifting (need to guarantee same effects as

154+-- parent!)

155+

156+test_lbl' : {x : lbl} ->

157+ {default tactics { applyTactic findEffElem 20; solve; }

158+ prf : EffElem e (LRes x (Either l r)) xs} ->

159+ WrapEffM m (updateResTyImm xs prf (LRes x l)) xs' t ->

160+ WrapEffM m (updateResTyImm xs prf (LRes x r)) xs' t ->

161+ EffM m xs xs' t

162+test_lbl' {prf} (WEffM l) (WEffM r) = test_lbl prf l r

163+

164+test' : {default tactics { applyTactic findEffElem 20; solve; }

165+ prf : EffElem e (Either l r) xs} ->

166+ EffM m (updateResTyImm xs prf l) xs' t ->

167+ EffM m (updateResTyImm xs prf r) xs' t ->

168+ EffM m xs xs' t

169+test' {prf} l r = test prf l r

135

170

136-- for 'do' notation

171-- for 'do' notation

137

172

@@ -164,6 +199,29 @@ execEff (val :: env) Here eff' k

164execEff (val :: env) (There p) eff k

199execEff (val :: env) (There p) eff k

165 = execEff env p eff (\env', v => k (val :: env') v)

200 = execEff env p eff (\env', v => k (val :: env') v)

166

201

202+private

203+testEff : Env m xs -> (p : EffElem e (Either l r) xs) ->

204+ (Env m (updateResTyImm xs p l) -> m b) ->

205+ (Env m (updateResTyImm xs p r) -> m b) ->

206+ m b

207+testEff (Left err :: env) Here lk rk = lk (err :: env)

208+testEff (Right ok :: env) Here lk rk = rk (ok :: env)

209+testEff (val :: env) (There p) lk rk

210+ = testEff env p (\envk => lk (val :: envk))

211+ (\envk => rk (val :: envk))

212+

213+private

214+testEffLbl : {x : lbl} ->

215+ Env m xs -> (p : EffElem e (LRes x (Either l r)) xs) ->

216+ (Env m (updateResTyImm xs p (LRes x l)) -> m b) ->

217+ (Env m (updateResTyImm xs p (LRes x r)) -> m b) ->

218+ m b

219+testEffLbl ((lbl := Left err) :: env) Here lk rk = lk ((lbl := err) :: env)

220+testEffLbl ((lbl := Right ok) :: env) Here lk rk = rk ((lbl := ok) :: env)

221+testEffLbl (val :: env) (There p) lk rk

222+ = testEffLbl env p (\envk => lk (val :: envk))

223+ (\envk => rk (val :: envk))

224+

167-- Q: Instead of m b, implement as StateT (Env m xs') m b, so that state

225-- Q: Instead of m b, implement as StateT (Env m xs') m b, so that state

168-- updates can be propagated even through failing computations?

226-- updates can be propagated even through failing computations?

169

227

@@ -178,6 +236,10 @@ eff env (lift prf effP) k

178eff env (new r prog) k

236eff env (new r prog) k

179 = let env' = r :: env in

237 = let env' = r :: env in

180 eff env' prog (\(v :: envk), p' => k envk p')

238 eff env' prog (\(v :: envk), p' => k envk p')

239+eff env (test prf l r) k

240+ = testEff env prf (\envk => eff envk l k) (\envk => eff envk r k)

241+eff env (test_lbl prf l r) k

242+ = testEffLbl env prf (\envk => eff envk l k) (\envk => eff envk r k)

181eff env (catch prog handler) k

243eff env (catch prog handler) k

182 = catch (eff env prog k)

244 = catch (eff env prog k)

183 (\e => eff env (handler e) k)

245 (\e => eff env (handler e) k)

src/Idris/AbsSyntax.hs+7

@@ -684,6 +684,7 @@ expandParams dec ps ns infs tm = en tm

684 en (PAlternative a as) = PAlternative a (map en as)

685 en (PHidden t) = PHidden (en t)

686 en (PUnifyLog t) = PUnifyLog (en t)

687+ en (PNoImplicits t) = PNoImplicits (en t)

687 en (PDoBlock ds) = PDoBlock (map (fmap en) ds)

688 en (PDoBlock ds) = PDoBlock (map (fmap en) ds)

688 en (PProof ts) = PProof (map (fmap en) ts)

689 en (PProof ts) = PProof (map (fmap en) ts)

689 en (PTactics ts) = PTactics (map (fmap en) ts)

690 en (PTactics ts) = PTactics (map (fmap en) ts)

@@ -1011,6 +1012,7 @@ implicitise syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $

1011 imps False (n:env) sc

1012 imps False (n:env) sc

1012 imps top env (PHidden tm) = imps False env tm

1013 imps top env (PHidden tm) = imps False env tm

1013 imps top env (PUnifyLog tm) = imps False env tm

1014 imps top env (PUnifyLog tm) = imps False env tm

1015+ imps top env (PNoImplicits tm) = imps False env tm

1014 imps top env _ = return ()

1016 imps top env _ = return ()

1015

1017

1016 pibind using [] sc = sc

1018 pibind using [] sc = sc

@@ -1100,6 +1102,7 @@ addImpl' inpat env infns ist ptm = ai (zip env (repeat Nothing)) ptm

1100 ai env (PTactics ts) = PTactics (map (fmap (ai env)) ts)

1102 ai env (PTactics ts) = PTactics (map (fmap (ai env)) ts)

1101 ai env (PRefl fc tm) = PRefl fc (ai env tm)

1103 ai env (PRefl fc tm) = PRefl fc (ai env tm)

1102 ai env (PUnifyLog tm) = PUnifyLog (ai env tm)

1104 ai env (PUnifyLog tm) = PUnifyLog (ai env tm)

1105+ ai env (PNoImplicits tm) = PNoImplicits (ai env tm)

1103 ai env tm = tm

1106 ai env tm = tm

1104

1107

1105 handleErr (Left err) = PElabError err

1108 handleErr (Left err) = PElabError err

@@ -1364,6 +1367,8 @@ matchClause' names i x y = checkRpts $ match (fullApp x) (fullApp y) where

1364 match (PHidden x) (PHidden y) = match' x y

1367 match (PHidden x) (PHidden y) = match' x y

1365 match (PUnifyLog x) y = match' x y

1368 match (PUnifyLog x) y = match' x y

1366 match x (PUnifyLog y) = match' x y

1369 match x (PUnifyLog y) = match' x y

1370+ match (PNoImplicits x) y = match' x y

1371+ match x (PNoImplicits y) = match' x y

1367 match Placeholder _ = return []

1372 match Placeholder _ = return []

1368 match _ Placeholder = return []

1373 match _ Placeholder = return []

1369 match (PResolveTC _) _ = return []

1374 match (PResolveTC _) _ = return []

@@ -1411,6 +1416,7 @@ substMatchShadow n shs tm t = sm shs t where

1411 sm xs (PAlternative a as) = PAlternative a (map (sm xs) as)

1416 sm xs (PAlternative a as) = PAlternative a (map (sm xs) as)

1412 sm xs (PHidden x) = PHidden (sm xs x)

1417 sm xs (PHidden x) = PHidden (sm xs x)

1413 sm xs (PUnifyLog x) = PUnifyLog (sm xs x)

1418 sm xs (PUnifyLog x) = PUnifyLog (sm xs x)

1419+ sm xs (PNoImplicits x) = PNoImplicits (sm xs x)

1414 sm xs x = x

1420 sm xs x = x

1415

1421

1416 fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))

1422 fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))

@@ -1431,6 +1437,7 @@ shadow n n' t = sm t where

1431 sm (PAlternative a as) = PAlternative a (map sm as)

1437 sm (PAlternative a as) = PAlternative a (map sm as)

1432 sm (PHidden x) = PHidden (sm x)

1438 sm (PHidden x) = PHidden (sm x)

1433 sm (PUnifyLog x) = PUnifyLog (sm x)

1439 sm (PUnifyLog x) = PUnifyLog (sm x)

1440+ sm (PNoImplicits x) = PNoImplicits (sm x)

1434 sm x = x

1441 sm x = x

1435

1442

1436

1443

src/Idris/AbsSyntaxTree.hs+11−3

@@ -558,6 +558,7 @@ data PTerm = PQuote Raw

558 | PImpossible -- ^ Special case for declaring when an LHS can't typecheck

559 | PCoerced PTerm -- ^ To mark a coerced argument, so as not to coerce twice

560 | PUnifyLog PTerm -- ^ dump a trace of unifications when building term

561+ | PNoImplicits PTerm -- ^ never run implicit converions on the term

561 deriving Eq

562 deriving Eq

562{-!

563{-!

563deriving instance Binary PTerm

564deriving instance Binary PTerm

@@ -582,6 +583,7 @@ mapPT f t = f (mpt t) where

582 mpt (PProof ts) = PProof (map (fmap (mapPT f)) ts)

583 mpt (PProof ts) = PProof (map (fmap (mapPT f)) ts)

583 mpt (PTactics ts) = PTactics (map (fmap (mapPT f)) ts)

584 mpt (PTactics ts) = PTactics (map (fmap (mapPT f)) ts)

584 mpt (PUnifyLog tm) = PUnifyLog (mapPT f tm)

585 mpt (PUnifyLog tm) = PUnifyLog (mapPT f tm)

586+ mpt (PNoImplicits tm) = PNoImplicits (mapPT f tm)

585 mpt (PGoal fc r n sc) = PGoal fc (mapPT f r) n (mapPT f sc)

587 mpt (PGoal fc r n sc) = PGoal fc (mapPT f r) n (mapPT f sc)

586 mpt x = x

588 mpt x = x

587

589

@@ -682,9 +684,9 @@ instance Sized a => Sized (PArg' a) where

682deriving instance Binary PArg'

684deriving instance Binary PArg'

683!-}

685!-}

684

686

685−pimp n t = PImp 0 True n t ""

687+pimp n t = PImp 1 True n t ""

686−pexp t = PExp 0 False t ""

688+pexp t = PExp 1 False t ""

687−pconst t = PConstraint 0 False t ""

689+pconst t = PConstraint 1 False t ""

688ptacimp n s t = PTacImplicit 0 True n s t ""

690ptacimp n s t = PTacImplicit 0 True n s t ""

689

691

690type PArg = PArg' PTerm

692type PArg = PArg' PTerm

@@ -1178,6 +1180,7 @@ showImp ist impl colour tm = se 10 [] tm where

1178 se p bnd (PElabError s) = show s

1180 se p bnd (PElabError s) = show s

1179 se p bnd (PCoerced t) = se p bnd t

1181 se p bnd (PCoerced t) = se p bnd t

1180 se p bnd (PUnifyLog t) = "%unifyLog " ++ se p bnd t

1182 se p bnd (PUnifyLog t) = "%unifyLog " ++ se p bnd t

1183+ se p bnd (PNoImplicits t) = "%noimplicit " ++ se p bnd t

1181-- se p bnd x = "Not implemented"

1184-- se p bnd x = "Not implemented"

1182

1185

1183 slist' p bnd (PApp _ (PRef _ nil) _)

1186 slist' p bnd (PApp _ (PRef _ nil) _)

@@ -1245,6 +1248,7 @@ instance Sized PTerm where

1245 size (PAlternative a alts) = 1 + size alts

1248 size (PAlternative a alts) = 1 + size alts

1246 size (PHidden hidden) = size hidden

1249 size (PHidden hidden) = size hidden

1247 size (PUnifyLog tm) = size tm

1250 size (PUnifyLog tm) = size tm

1251+ size (PNoImplicits tm) = size tm

1248 size PType = 1

1252 size PType = 1

1249 size (PConstant const) = 1 + size const

1253 size (PConstant const) = 1 + size const

1250 size Placeholder = 1

1254 size Placeholder = 1

@@ -1280,6 +1284,7 @@ allNamesIn tm = nub $ ni [] tm

1280 ni env (PDPair _ l t r) = ni env l ++ ni env t ++ ni env r

1284 ni env (PDPair _ l t r) = ni env l ++ ni env t ++ ni env r

1281 ni env (PAlternative a ls) = concatMap (ni env) ls

1285 ni env (PAlternative a ls) = concatMap (ni env) ls

1282 ni env (PUnifyLog tm) = ni env tm

1286 ni env (PUnifyLog tm) = ni env tm

1287+ ni env (PNoImplicits tm) = ni env tm

1283 ni env _ = []

1288 ni env _ = []

1284

1289

1285-- Return names which are free in the given term.

1290-- Return names which are free in the given term.

@@ -1305,6 +1310,7 @@ namesIn uvars ist tm = nub $ ni [] tm

1305 ni env (PAlternative a as) = concatMap (ni env) as

1310 ni env (PAlternative a as) = concatMap (ni env) as

1306 ni env (PHidden tm) = ni env tm

1311 ni env (PHidden tm) = ni env tm

1307 ni env (PUnifyLog tm) = ni env tm

1312 ni env (PUnifyLog tm) = ni env tm

1313+ ni env (PNoImplicits tm) = ni env tm

1308 ni env _ = []

1314 ni env _ = []

1309

1315

1310-- Return which of the given names are used in the given term.

1316-- Return which of the given names are used in the given term.

@@ -1330,4 +1336,6 @@ usedNamesIn vars ist tm = nub $ ni [] tm

1330 ni env (PAlternative a as) = concatMap (ni env) as

1336 ni env (PAlternative a as) = concatMap (ni env) as

1331 ni env (PHidden tm) = ni env tm

1337 ni env (PHidden tm) = ni env tm

1332 ni env (PUnifyLog tm) = ni env tm

1338 ni env (PUnifyLog tm) = ni env tm

1339+ ni env (PNoImplicits tm) = ni env tm

1333 ni env _ = []

1340 ni env _ = []

1341+

src/Idris/DSL.hs+3

@@ -37,6 +37,8 @@ expandDo dsl (PDPair fc l t r) = PDPair fc (expandDo dsl l) (expandDo dsl t)

37 (expandDo dsl r)

38expandDo dsl (PAlternative a as) = PAlternative a (map (expandDo dsl) as)

39expandDo dsl (PHidden t) = PHidden (expandDo dsl t)

40+expandDo dsl (PNoImplicits t) = PNoImplicits (expandDo dsl t)

41+expandDo dsl (PUnifyLog t) = PUnifyLog (expandDo dsl t)

40expandDo dsl (PReturn fc) = dsl_return dsl

42expandDo dsl (PReturn fc) = dsl_return dsl

41expandDo dsl (PRewrite fc r t ty)

43expandDo dsl (PRewrite fc r t ty)

42 = PRewrite fc r (expandDo dsl t) ty

44 = PRewrite fc r (expandDo dsl t) ty

@@ -90,6 +92,7 @@ var dsl n t i = v' i t where

90 v' i (PHidden t) = PHidden (v' i t)

92 v' i (PHidden t) = PHidden (v' i t)

91 v' i (PIdiom f t) = PIdiom f (v' i t)

93 v' i (PIdiom f t) = PIdiom f (v' i t)

92 v' i (PDoBlock ds) = PDoBlock (map (fmap (v' i)) ds)

94 v' i (PDoBlock ds) = PDoBlock (map (fmap (v' i)) ds)

95+ v' i (PNoImplicits t) = PNoImplicits (v' i t)

93 v' i t = t

96 v' i t = t

95 mkVar fc 0 = case index_first dsl of

98 mkVar fc 0 = case index_first dsl of

src/Idris/ElabTerm.hs+1

@@ -142,6 +142,7 @@ elab ist info pattern tcgen fn tm

142 local f = do e <- get_env

143 return (f `elem` map fst e)

144

145+ elab' ina (PNoImplicits t) = elab' ina t -- skip elabE step

145 elab' ina PType = do apply RType []; solve

146 elab' ina PType = do apply RType []; solve

146 elab' ina (PConstant c) = do apply (RConstant c) []; solve

147 elab' ina (PConstant c) = do apply (RConstant c) []; solve

147 elab' ina (PQuote r) = do fill r; solve

148 elab' ina (PQuote r) = do fill r; solve

src/Idris/ParseExpr.hs+12

@@ -177,6 +177,7 @@ internalExpr syn =

177 try (app syn)

178 <|> try (matchApp syn)

179 <|> try (unifyLog syn)

180+ <|> try (noImplicits syn)

180 <|> recordType syn

181 <|> recordType syn

181 <|> try (simpleExpr syn)

182 <|> try (simpleExpr syn)

182 <|> lambda syn

183 <|> lambda syn

@@ -441,6 +442,17 @@ unifyLog syn = do lchar '%'; reserved "unifyLog";

441 return (PUnifyLog tm)

442 return (PUnifyLog tm)

442 <?> "unification log expression"

443 <?> "unification log expression"

443

444

445+{- | Parses a no implicits expression

446+NoImplicits ::=

447+ '%' 'noImplicits' SimpleExpr

448+ ;

449+-}

450+noImplicits :: SyntaxInfo -> IdrisParser PTerm

451+noImplicits syn = do lchar '%'; reserved "noImplicits";

452+ tm <- simpleExpr syn

453+ return (PNoImplicits tm)

454+ <?> "no implicits expression"

455+

444{- | Parses a function application expression

456{- | Parses a function application expression

445App ::=

457App ::=

446 'mkForeign' Arg Arg*

458 'mkForeign' Arg Arg*