16708a9 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

More flexibility using overloading functions in patterns

16708a9Edwin Brady15 years ago

src/Idris/AbsSyntax.hs+5−1

compare with master

unifiedsplit

@@ -299,7 +299,7 @@ impl = Imp False Dynamic

299expl = Exp False Dynamic

300constraint = Constraint False Static

301

302−data FnOpt = Inlinable | Partial | Abstract | Private

302+data FnOpt = Inlinable | Partial | Abstract | Private | TCGen

303 deriving (Show, Eq)

304

305type FnOpts = [FnOpt]

@@ -771,6 +771,10 @@ existsCon = UN "Ex_intro"

771piBind :: [(Name, PTerm)] -> PTerm -> PTerm

772piBind [] t = t

773piBind ((n, ty):ns) t = PPi expl n ty (piBind ns t)

774+

775+tcname (UN ('@':_)) = True

776+tcname (NS n _) = tcname n

777+tcname _ = False

774

778

775-- Dealing with parameters

779-- Dealing with parameters

776

780

src/Idris/Delaborate.hs+1−1

@@ -56,7 +56,7 @@ pshow :: IState -> Err -> String

56pshow i (Msg s) = s

57pshow i (CantUnify x y e) = "Can't unify " ++ show (delab i x)

58 ++ " with " ++ show (delab i y)

59−-- ++ "\n\t(" ++ pshow i e ++ ")"

59+ ++ "\n\t(" ++ pshow i e ++ ")"

60pshow i (IncompleteTerm t) = "Incomplete term " ++ show t

61pshow i UniverseError = "Universe inconsistency"

62pshow i ProgramLineComment = "Program line next to comment"

src/Idris/ElabDecls.hs+15−13

@@ -93,7 +93,7 @@ elabClauses :: ElabInfo -> FC -> FnOpts -> Name -> [PClause] -> Idris ()

93elabClauses info fc opts n_in cs_in = let n = liftname info n_in in

94 do let cs = genClauses cs_in

95 solveDeferred n

96− pats_in <- mapM (elabClause info fc) cs

96+ pats_in <- mapM (elabClause info fc (TCGen `elem` opts)) cs

97 let pats = mapMaybe id pats_in

98 logLvl 3 (showSep "\n" (map (\ (l,r) ->

99 show l ++ " = " ++

@@ -135,18 +135,18 @@ elabVal info aspat tm_in

135 logLvl 2 (show vtm)

136 recheckC ctxt (FC "prompt" 0) [] vtm

137

138−elabClause :: ElabInfo -> FC -> PClause -> Idris (Maybe (Term, Term))

138+elabClause :: ElabInfo -> FC -> Bool -> PClause -> Idris (Maybe (Term, Term))

139−elabClause info fc (PClause fname lhs_in [] PImpossible [])

139+elabClause info fc tcgen (PClause fname lhs_in [] PImpossible [])

140 = do ctxt <- getContext

141 i <- get

142 let lhs = addImpl i lhs_in

143 -- if the LHS type checks, it is possible, so report an error

144 case elaborate ctxt (MN 0 "patLHS") infP

145− (erun fc (build i info True fname (infTerm lhs))) of

145+ (erun fc (buildTC i info True tcgen fname (infTerm lhs))) of

146 OK _ -> fail $ show fc ++ ":" ++ show lhs ++ " is a possible case"

147 Error _ -> return ()

148 return Nothing

149−elabClause info fc (PClause fname lhs_in withs rhs_in whereblock)

149+elabClause info fc tcgen (PClause fname lhs_in withs rhs_in whereblock)

150 = do ctxt <- getContext

151 -- Build the LHS as an "Infer", and pull out its type and

152 -- pattern bindings

@@ -154,7 +154,7 @@ elabClause info fc (PClause fname lhs_in withs rhs_in whereblock)

154 let lhs = addImpl i lhs_in

155 logLvl 5 ("LHS: " ++ showImp True lhs)

156 ((lhs', dlhs), _) <- tclift $ elaborate ctxt (MN 0 "patLHS") infP

157− (erun fc (build i info True fname (infTerm lhs)))

157+ (erun fc (buildTC i info True tcgen fname (infTerm lhs)))

158 let lhs_tm = orderPats (getInferTerm lhs')

159 let lhs_ty = getInferType lhs'

160 logLvl 3 (show lhs_tm)

@@ -205,7 +205,7 @@ elabClause info fc (PClause fname lhs_in withs rhs_in whereblock)

205 -- _ -> MN i (show n)) . l

206 }

207

208−elabClause info fc (PWith fname lhs_in withs wval_in withblock)

208+elabClause info fc tcgen (PWith fname lhs_in withs wval_in withblock)

209 = do ctxt <- getContext

210 -- Build the LHS as an "Infer", and pull out its type and

211 -- pattern bindings

@@ -213,7 +213,7 @@ elabClause info fc (PWith fname lhs_in withs wval_in withblock)

213 let lhs = addImpl i lhs_in

214 logLvl 5 ("LHS: " ++ showImp True lhs)

215 ((lhs', dlhs), _) <- tclift $ elaborate ctxt (MN 0 "patLHS") infP

216− (erun fc (build i info True fname (infTerm lhs)))

216+ (erun fc (buildTC i info True tcgen fname (infTerm lhs)))

217 let lhs_tm = orderPats (getInferTerm lhs')

218 let lhs_ty = getInferType lhs'

219 let ret_ty = getRetTy lhs_ty

@@ -363,7 +363,8 @@ elabClass info syn fc constraints tn ps ds

363 case lookup n mtys of

364 Just (syn, ty) -> do let ty' = insertConstraint c ty

365 let ds = map (decorateid defaultdec)

366− [PTy syn fc n ty', d]

366+ [PTy syn fc n ty',

367+ PClauses fc (TCGen:opts) n cs]

367 iLOG (show ds)

368 iLOG (show ds)

368 return (n, (defaultdec n, ds))

369 return (n, (defaultdec n, ds))

369 _ -> fail $ show n ++ " is not a method"

370 _ -> fail $ show n ++ " is not a method"

@@ -387,7 +388,7 @@ elabClass info syn fc constraints tn ps ds

387 iLOG (showImp True ty)

388 iLOG (showImp True ty)

388 iLOG (showImp True lhs ++ " = " ++ showImp True rhs)

389 iLOG (showImp True lhs ++ " = " ++ showImp True rhs)

389 return [PTy syn fc cfn ty,

390 return [PTy syn fc cfn ty,

390− PClauses fc [Inlinable] cfn [PClause cfn lhs [] rhs []]]

391+ PClauses fc [Inlinable,TCGen] cfn [PClause cfn lhs [] rhs []]]

391

392

392 tfun cn c syn all (m, ty)

393 tfun cn c syn all (m, ty)

393 = do let ty' = insertConstraint c ty

394 = do let ty' = insertConstraint c ty

@@ -401,7 +402,7 @@ elabClass info syn fc constraints tn ps ds

401 iLOG (show (m, ty', capp, margs))

402 iLOG (show (m, ty', capp, margs))

402 iLOG (showImp True lhs ++ " = " ++ showImp True rhs)

403 iLOG (showImp True lhs ++ " = " ++ showImp True rhs)

403 return [PTy syn fc m ty',

404 return [PTy syn fc m ty',

404− PClauses fc [Inlinable] m [PClause m lhs [] rhs []]]

405+ PClauses fc [Inlinable,TCGen] m [PClause m lhs [] rhs []]]

405

406

406 getMArgs (PPi (Imp _ _) n ty sc) = IA : getMArgs sc

407 getMArgs (PPi (Imp _ _) n ty sc) = IA : getMArgs sc

407 getMArgs (PPi (Exp _ _) n ty sc) = EA : getMArgs sc

408 getMArgs (PPi (Exp _ _) n ty sc) = EA : getMArgs sc

@@ -457,7 +458,8 @@ elabInstance info syn fc cs n ps t ds

457 let lhs = PRef fc iname

458 let lhs = PRef fc iname

458 let rhs = PApp fc (PRef fc (instanceName ci))

459 let rhs = PApp fc (PRef fc (instanceName ci))

459 (map (pexp . mkMethApp) mtys)

460 (map (pexp . mkMethApp) mtys)

460− let idecl = PClauses fc [Inlinable] iname [PClause iname lhs [] rhs wb]

461+ let idecl = PClauses fc [Inlinable, TCGen] iname

462+ [PClause iname lhs [] rhs wb]

461 iLOG (show idecl)

463 iLOG (show idecl)

462 elabDecl info idecl

464 elabDecl info idecl

463 where

465 where

@@ -495,7 +497,7 @@ elabInstance info syn fc cs n ps t ds

495

497

496 insertDef meth def ns decls

498 insertDef meth def ns decls

497 | null $ filter (clauseFor meth ns) decls

499 | null $ filter (clauseFor meth ns) decls

498− = decls ++ [PClauses fc [Inlinable] meth

500+ = decls ++ [PClauses fc [Inlinable,TCGen] meth

499 [PClause meth (PApp fc (PRef fc meth) []) []

501 [PClause meth (PApp fc (PRef fc meth) []) []

500 (PApp fc (PRef fc def) []) []]]

502 (PApp fc (PRef fc def) []) []]]

501 | otherwise = decls

503 | otherwise = decls

src/Idris/ElabTerm.hs+87−74

@@ -32,14 +32,25 @@ toplevel = EInfo [] emptyContext id Nothing

32build :: IState -> ElabInfo -> Bool -> Name -> PTerm ->

33 Elab (Term, [(Name, Type)])

34build ist info pattern fn tm

35− = do elab ist info pattern fn tm

35+ = do elab ist info pattern False fn tm

36 tt <- get_term

37 return $ runState (collectDeferred tt) []

39+-- Build a term autogenerated as a typeclass method definition

40+-- (Separate, so we don't go overboard resolving things that we don't

41+-- know about yet on the LHS of a pattern def)

42+

43+buildTC :: IState -> ElabInfo -> Bool -> Bool -> Name -> PTerm ->

44+ Elab (Term, [(Name, Type)])

45+buildTC ist info pattern tcgen fn tm

46+ = do elab ist info pattern tcgen fn tm

47+ tt <- get_term

48+ return $ runState (collectDeferred tt) []

49+

39−elab :: IState -> ElabInfo -> Bool -> Name -> PTerm ->

50+elab :: IState -> ElabInfo -> Bool -> Bool -> Name -> PTerm ->

40 Elab ()

51 Elab ()

41−elab ist info pattern fn tm

52+elab ist info pattern tcgen fn tm

42− = do elabE tm

53+ = do elabE False tm

43 when pattern -- convert remaining holes to pattern vars

54 when pattern -- convert remaining holes to pattern vars

44 mkPat

55 mkPat

45 where

56 where

@@ -47,66 +58,66 @@ elab ist info pattern fn tm

47 Placeholder -> (True, priority arg)

58 Placeholder -> (True, priority arg)

48 _ -> (False, priority arg)

59 _ -> (False, priority arg)

50− toElab arg = case getTm arg of

61+ toElab ina arg = case getTm arg of

51 Placeholder -> Nothing

62 Placeholder -> Nothing

52− v -> Just (priority arg, elabE v)

63+ v -> Just (priority arg, elabE ina v)

54 mkPat = do hs <- get_holes

65 mkPat = do hs <- get_holes

55 case hs of

66 case hs of

56 (h: hs) -> do patvar h; mkPat

67 (h: hs) -> do patvar h; mkPat

57 [] -> return ()

68 [] -> return ()

59− elabE t = {- do g <- goal

70+ elabE ina t = {- do g <- goal

60 tm <- get_term

71 tm <- get_term

61 trace ("Elaborating " ++ show t ++ " : " ++ show g ++ "\n\tin " ++ show tm)

72 trace ("Elaborating " ++ show t ++ " : " ++ show g ++ "\n\tin " ++ show tm)

62− $ -} elab' t

73+ $ -} elab' ina t

64 local f = do e <- get_env

75 local f = do e <- get_env

65 return (f `elem` map fst e)

76 return (f `elem` map fst e)

67− elab' PSet = do fill RSet; solve

78+ elab' ina PSet = do fill RSet; solve

68− elab' (PConstant c) = do apply (RConstant c) []; solve

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

69− elab' (PQuote r) = do fill r; solve

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

70− elab' (PTrue fc) = try (elab' (PRef fc unitCon))

81+ elab' ina (PTrue fc) = try (elab' ina (PRef fc unitCon))

71− (elab' (PRef fc unitTy))

82+ (elab' ina (PRef fc unitTy))

72− elab' (PFalse fc) = elab' (PRef fc falseTy)

83+ elab' ina (PFalse fc) = elab' ina (PRef fc falseTy)

73− elab' (PResolveTC (FC "HACK" _)) -- for chasing parent classes

84+ elab' ina (PResolveTC (FC "HACK" _)) -- for chasing parent classes

74 = resolveTC 2 fn ist

85 = resolveTC 2 fn ist

75− elab' (PResolveTC fc) = do c <- unique_hole (MN 0 "c")

86+ elab' ina (PResolveTC fc) = do c <- unique_hole (MN 0 "c")

76− instanceArg c

87+ instanceArg c

77− elab' (PRefl fc) = elab' (PApp fc (PRef fc eqCon) [pimp (MN 0 "a") Placeholder,

88+ elab' ina (PRefl fc) = elab' ina (PApp fc (PRef fc eqCon) [pimp (MN 0 "a") Placeholder,

78 pimp (MN 0 "x") Placeholder])

89 pimp (MN 0 "x") Placeholder])

79− elab' (PEq fc l r) = elab' (PApp fc (PRef fc eqTy) [pimp (MN 0 "a") Placeholder,

90+ elab' ina (PEq fc l r) = elab' ina (PApp fc (PRef fc eqTy) [pimp (MN 0 "a") Placeholder,

80 pimp (MN 0 "b") Placeholder,

91 pimp (MN 0 "b") Placeholder,

81 pexp l, pexp r])

92 pexp l, pexp r])

82− elab' (PPair fc l r) = try (elabE (PApp fc (PRef fc pairTy)

93+ elab' ina (PPair fc l r) = try (elabE True (PApp fc (PRef fc pairTy)

83 [pexp l,pexp r]))

94 [pexp l,pexp r]))

84− (elabE (PApp fc (PRef fc pairCon)

95+ (elabE True (PApp fc (PRef fc pairCon)

85 [pimp (MN 0 "A") Placeholder,

96 [pimp (MN 0 "A") Placeholder,

86 pimp (MN 0 "B") Placeholder,

97 pimp (MN 0 "B") Placeholder,

87 pexp l, pexp r]))

98 pexp l, pexp r]))

88− elab' (PDPair fc l@(PRef _ n) t r)

99+ elab' ina (PDPair fc l@(PRef _ n) t r)

89 = case t of

100 = case t of

90 Placeholder -> try asType asValue

101 Placeholder -> try asType asValue

91 _ -> asType

102 _ -> asType

92− where asType = elab' (PApp fc (PRef fc sigmaTy)

103+ where asType = elab' ina (PApp fc (PRef fc sigmaTy)

93 [pexp t,

104 [pexp t,

94 pexp (PLam n Placeholder r)])

105 pexp (PLam n Placeholder r)])

95− asValue = elab' (PApp fc (PRef fc existsCon)

106+ asValue = elab' ina (PApp fc (PRef fc existsCon)

96 [pimp (MN 0 "a") t,

107 [pimp (MN 0 "a") t,

97 pimp (MN 0 "P") Placeholder,

108 pimp (MN 0 "P") Placeholder,

98 pexp l, pexp r])

109 pexp l, pexp r])

99− elab' (PDPair fc l t r) = elab' (PApp fc (PRef fc existsCon)

110+ elab' ina (PDPair fc l t r) = elab' ina (PApp fc (PRef fc existsCon)

100 [pimp (MN 0 "a") t,

111 [pimp (MN 0 "a") t,

101 pimp (MN 0 "P") Placeholder,

112 pimp (MN 0 "P") Placeholder,

102 pexp l, pexp r])

113 pexp l, pexp r])

103− elab' (PAlternative as)

114+ elab' ina (PAlternative as)

104 = let as' = pruneAlt as in

115 = let as' = pruneAlt as in

105− try (tryAll (zip (map elab' as') (map showHd as')))

116+ try (tryAll (zip (map (elab' ina) as') (map showHd as')))

106− (tryAll (zip (map elab' as) (map showHd as)))

117+ (tryAll (zip (map (elab' ina) as) (map showHd as)))

107 where showHd (PApp _ h _) = show h

118 where showHd (PApp _ h _) = show h

108 showHd x = show x

119 showHd x = show x

109− elab' (PRef fc n) | pattern && not (inparamBlock n)

120+ elab' ina (PRef fc n) | pattern && not (inparamBlock n)

110 = do ctxt <- get_context

121 = do ctxt <- get_context

111 let sc = case lookupTy Nothing n ctxt of

122 let sc = case lookupTy Nothing n ctxt of

112 [] -> True

123 [] -> True

@@ -119,22 +130,22 @@ elab ist info pattern fn tm

119 where inparamBlock n = case lookupCtxtName Nothing n (inblock info) of

130 where inparamBlock n = case lookupCtxtName Nothing n (inblock info) of

120 [] -> False

131 [] -> False

121 _ -> True

132 _ -> True

122− elab' (PRef fc n) = erun fc $ do apply (Var n) []; solve

133+ elab' ina (PRef fc n) = erun fc $ do apply (Var n) []; solve

123− elab' (PLam n Placeholder sc)

134+ elab' ina (PLam n Placeholder sc)

124− = do attack; intro (Just n); elabE sc; solve

135+ = do attack; intro (Just n); elabE True sc; solve

125− elab' (PLam n ty sc)

136+ elab' ina (PLam n ty sc)

126 = do tyn <- unique_hole (MN 0 "lamty")

137 = do tyn <- unique_hole (MN 0 "lamty")

127 claim tyn RSet

138 claim tyn RSet

128 attack

139 attack

129 introTy (Var tyn) (Just n)

140 introTy (Var tyn) (Just n)

130 -- end_unify

141 -- end_unify

131 focus tyn

142 focus tyn

132− elabE ty

143+ elabE True ty

133− elabE sc

144+ elabE True sc

134 solve

145 solve

135− elab' (PPi _ n Placeholder sc)

146+ elab' ina (PPi _ n Placeholder sc)

136− = do attack; arg n (MN 0 "ty"); elabE sc; solve

147+ = do attack; arg n (MN 0 "ty"); elabE True sc; solve

137− elab' (PPi _ n ty sc)

148+ elab' ina (PPi _ n ty sc)

138 = do attack; tyn <- unique_hole (MN 0 "ty")

149 = do attack; tyn <- unique_hole (MN 0 "ty")

139 claim tyn RSet

150 claim tyn RSet

140 n' <- case n of

151 n' <- case n of

@@ -142,10 +153,10 @@ elab ist info pattern fn tm

142 _ -> return n

153 _ -> return n

143 forall n' (Var tyn)

154 forall n' (Var tyn)

144 focus tyn

155 focus tyn

145− elabE ty

156+ elabE True ty

146− elabE sc

157+ elabE True sc

147 solve

158 solve

148− elab' (PLet n ty val sc)

159+ elab' ina (PLet n ty val sc)

149 = do attack;

160 = do attack;

150 tyn <- unique_hole (MN 0 "letty")

161 tyn <- unique_hole (MN 0 "letty")

151 claim tyn RSet

162 claim tyn RSet

@@ -155,27 +166,31 @@ elab ist info pattern fn tm

155 case ty of

166 case ty of

156 Placeholder -> return ()

167 Placeholder -> return ()

157 _ -> do focus tyn

168 _ -> do focus tyn

158− elabE ty

169+ elabE True ty

159 focus valn

170 focus valn

160− elabE val

171+ elabE True val

161− elabE sc

172+ elabE True sc

162 solve

173 solve

163− elab' (PApp fc (PRef _ f) args')

174+ elab' ina (PApp fc (PRef _ f) args')

164 = do let args = {- case lookupCtxt f (inblock info) of

175 = do let args = {- case lookupCtxt f (inblock info) of

165 Just ps -> (map (pexp . (PRef fc)) ps ++ args')

176 Just ps -> (map (pexp . (PRef fc)) ps ++ args')

166 _ ->-} args'

177 _ ->-} args'

167 ivs <- get_instances

178 ivs <- get_instances

179+ -- HACK: we shouldn't resolve type classes if we're defining an instance

180+ -- function or default defition.

181+ let isinf = f == inferCon || tcname f

168 try (do ns <- apply (Var f) (map isph args)

182 try (do ns <- apply (Var f) (map isph args)

169 solve

183 solve

170 let (ns', eargs)

184 let (ns', eargs)

171 = unzip $

185 = unzip $

172 sortBy (\(_,x) (_,y) -> compare (priority x) (priority y))

186 sortBy (\(_,x) (_,y) -> compare (priority x) (priority y))

173 (zip ns args)

187 (zip ns args)

188+ elabArgs (ina || not isinf)

174− elabArgs [] False ns' (map (\x -> (lazyarg x, getTm x)) eargs))

189+ [] False ns' (map (\x -> (lazyarg x, getTm x)) eargs))

175− (do apply_elab f (map toElab args)

190+ (do apply_elab f (map (toElab (ina || not isinf)) args)

176 solve)

191 solve)

177 ivs' <- get_instances

192 ivs' <- get_instances

178− when (not pattern) $

193+ when (not pattern || (ina && not tcgen)) $

179 mapM_ (\n -> do focus n

194 mapM_ (\n -> do focus n

180 resolveTC 7 fn ist) (ivs' \\ ivs)

195 resolveTC 7 fn ist) (ivs' \\ ivs)

181-- ivs <- get_instances

196-- ivs <- get_instances

@@ -187,37 +202,37 @@ elab ist info pattern fn tm

187 where tcArg (n, PConstraint _ _ Placeholder) = True

202 where tcArg (n, PConstraint _ _ Placeholder) = True

188 tcArg _ = False

203 tcArg _ = False

189

204

190− elab' (PApp fc f [arg])

205+ elab' a (PApp fc f [arg])

191 = erun fc $

206 = erun fc $

192− do simple_app (elabE f) (elabE (getTm arg))

207+ do simple_app (elabE a f) (elabE True (getTm arg))

193 solve

208 solve

194− elab' Placeholder = do (h : hs) <- get_holes

209+ elab' ina Placeholder = do (h : hs) <- get_holes

195− movelast h

210+ movelast h

196− elab' (PMetavar n) = let n' = case namespace info of

211+ elab' ina (PMetavar n) = let n' = case namespace info of

197 Just xs@(_:_) -> NS n xs

212 Just xs@(_:_) -> NS n xs

198 _ -> n in

213 _ -> n in

199− do attack; defer n'; solve

214+ do attack; defer n'; solve

200− elab' (PProof ts) = do mapM_ (runTac True ist) ts

215+ elab' ina (PProof ts) = do mapM_ (runTac True ist) ts

201− elab' (PTactics ts) = do mapM_ (runTac False ist) ts

216+ elab' ina (PTactics ts) = do mapM_ (runTac False ist) ts

202− elab' (PElabError e) = fail e

217+ elab' ina (PElabError e) = fail e

203− elab' x = fail $ "Something's gone wrong. Did you miss a semi-colon somewhere?"

218+ elab' ina x = fail $ "Something's gone wrong. Did you miss a semi-colon somewhere?"

204

219

205− elabArgs failed retry [] _

220+ elabArgs ina failed retry [] _

206 | retry = let (ns, ts) = unzip (reverse failed) in

221 | retry = let (ns, ts) = unzip (reverse failed) in

207− elabArgs [] False ns ts

222+ elabArgs ina [] False ns ts

208 | otherwise = return ()

223 | otherwise = return ()

209− elabArgs failed r (n:ns) ((_, Placeholder) : args)

224+ elabArgs ina failed r (n:ns) ((_, Placeholder) : args)

210− = elabArgs failed r ns args

225+ = elabArgs ina failed r ns args

211− elabArgs failed r (n:ns) ((lazy, t) : args)

226+ elabArgs ina failed r (n:ns) ((lazy, t) : args)

212 | lazy && not pattern

227 | lazy && not pattern

213 = do elabArg n (PApp bi (PRef bi (UN "lazy"))

228 = do elabArg n (PApp bi (PRef bi (UN "lazy"))

214 [pimp (UN "a") Placeholder,

229 [pimp (UN "a") Placeholder,

215 pexp t]);

230 pexp t]);

216 | otherwise = elabArg n t

231 | otherwise = elabArg n t

217 where elabArg n t = if r

232 where elabArg n t = if r

218− then try (do focus n; elabE t; elabArgs failed r ns args)

233+ then try (do focus n; elabE ina t; elabArgs ina failed r ns args)

219− (elabArgs ((n,(lazy, t)):failed) r ns args)

234+ (elabArgs ina ((n,(lazy, t)):failed) r ns args)

220− else do focus n; elabE t; elabArgs failed r ns args

235+ else do focus n; elabE ina t; elabArgs ina failed r ns args

221

236

222pruneAlt :: [PTerm] -> [PTerm]

237pruneAlt :: [PTerm] -> [PTerm]

223pruneAlt xs = map prune xs

238pruneAlt xs = map prune xs

@@ -233,12 +248,13 @@ pruneAlt xs = map prune xs

233 headIs f _ = True -- keep if it's not an application

248 headIs f _ = True -- keep if it's not an application

234

249

235trivial :: IState -> Elab ()

250trivial :: IState -> Elab ()

236−trivial ist = try (elab ist toplevel False (MN 0 "tac") (PRefl (FC "prf" 0)))

251+trivial ist = try (elab ist toplevel False False (MN 0 "tac") (PRefl (FC "prf" 0)))

237 (do env <- get_env

252 (do env <- get_env

238 tryAll (map fst env))

253 tryAll (map fst env))

239 where

254 where

240 tryAll [] = fail "No trivial solution"

255 tryAll [] = fail "No trivial solution"

241− tryAll (x:xs) = try (elab ist toplevel False (MN 0 "tac") (PRef (FC "prf" 0) x))

256+ tryAll (x:xs) = try (elab ist toplevel False False

257+ (MN 0 "tac") (PRef (FC "prf" 0) x))

242 (tryAll xs)

258 (tryAll xs)

243

259

244resolveTC :: Int -> Name -> IState -> Elab ()

260resolveTC :: Int -> Name -> IState -> Elab ()

@@ -271,9 +287,6 @@ resolveTC depth fn ist

271 blunderbuss t (n:ns) | n /= fn && tcname n = try (resolve n depth)

287 blunderbuss t (n:ns) | n /= fn && tcname n = try (resolve n depth)

272 (blunderbuss t ns)

288 (blunderbuss t ns)

273 | otherwise = blunderbuss t ns

289 | otherwise = blunderbuss t ns

274− tcname (UN ('@':_)) = True

275− tcname (NS n _) = tcname n

276− tcname _ = False

277

290

278 resolve n depth

291 resolve n depth

279 | depth == 0 = fail $ "Can't resolve type class"

292 | depth == 0 = fail $ "Can't resolve type class"

@@ -316,7 +329,7 @@ runTac autoSolve ist tac = runT (fmap (addImpl ist) tac) where

316 bname (Bind n _ _) = Just n

329 bname (Bind n _ _) = Just n

317 bname _ = Nothing

330 bname _ = Nothing

318 runT (Intro xs) = mapM_ (\x -> do attack; intro (Just x)) xs

331 runT (Intro xs) = mapM_ (\x -> do attack; intro (Just x)) xs

319− runT (Exact tm) = do elab ist toplevel False (MN 0 "tac") tm

332+ runT (Exact tm) = do elab ist toplevel False False (MN 0 "tac") tm

320 when autoSolve solveAll

333 when autoSolve solveAll

321 runT (Refine fn [])

334 runT (Refine fn [])

322 = do (fn', imps) <- case lookupCtxtName Nothing fn (idris_implicits ist) of

335 = do (fn', imps) <- case lookupCtxtName Nothing fn (idris_implicits ist) of

@@ -345,7 +358,7 @@ runTac autoSolve ist tac = runT (fmap (addImpl ist) tac) where

345 letn <- unique_hole (MN 0 "rewrite_rule")

358 letn <- unique_hole (MN 0 "rewrite_rule")

346 letbind letn (Var tyn) (Var valn)

359 letbind letn (Var tyn) (Var valn)

347 focus valn

360 focus valn

348− elab ist toplevel False (MN 0 "tac") tm

361+ elab ist toplevel False False (MN 0 "tac") tm

349 rewrite (Var letn)

362 rewrite (Var letn)

350 when autoSolve solveAll

363 when autoSolve solveAll

351 runT (LetTac n tm)

364 runT (LetTac n tm)

@@ -357,7 +370,7 @@ runTac autoSolve ist tac = runT (fmap (addImpl ist) tac) where

357 letn <- unique_hole n

370 letn <- unique_hole n

358 letbind letn (Var tyn) (Var valn)

371 letbind letn (Var tyn) (Var valn)

359 focus valn

372 focus valn

360− elab ist toplevel False (MN 0 "tac") tm

373+ elab ist toplevel False False (MN 0 "tac") tm

361 when autoSolve solveAll

374 when autoSolve solveAll

362 runT Compute = compute

375 runT Compute = compute

363 runT Trivial = do trivial ist; when autoSolve solveAll

376 runT Trivial = do trivial ist; when autoSolve solveAll

tutorial/Makefile+1−1

@@ -3,7 +3,7 @@ PAPER = idris-tutorial

3all: ${PAPER}.pdf

5TEXFILES = ${PAPER}.tex intro.tex starting.tex miscellany.tex typesfuns.tex \

6− classes.tex modules.tex interp.tex

6+ classes.tex modules.tex interp.tex views.tex

8DIAGS =

tutorial/idris-tutorial.tex+1−1

@@ -25,10 +25,10 @@

25\input{classes}

26\input{modules}

27\input{interp}

28+\input{views}

29%Planned sections

30%Planned sections

31−\section{Views}

32\section{Theorem Proving}

33\section{Provisional Definitions}

34\section{Syntax Extensions}

tutorial/views.texnew file+69

@@ -0,0 +1,69 @@

1+\section{Views and the ``\texttt{with}'' rule}

3+\subsection{Dependent pattern matching}

5+Since types can depend on values, the form of some arguments can be determined

6+by the value of others. For example, if we were to write down the implicit

7+length arguments to \texttt{app}, we'd see that the form of the length argument was

8+determined by whether the vector was empty or not:

10+\begin{SaveVerbatim}{appdep}

11+

12+app : Vect a n -> Vect a m -> Vect a (n + m);

13+app {n=O} [] [] = [];

14+app {n=S k} (x :: xs) ys = x :: app xs ys;

15+

16+\end{SaveVerbatim}

17+\useverb{appdep}

18+

19+\noindent

20+If \texttt{n} was a successor in the \texttt{[]} case, or zero in the

21+\texttt{::} case, the definition

22+would not be well typed.

23+

24+\subsection{The \texttt{with} rule --- matching intermediate values}

25+

26+Very often, we need to match on the result of an intermediate computation.

27+\Idris{} provides a construct for this, the \texttt{with} rule,

28+inspired by views in \Epigram~\cite{view-left},

29+which takes account of the

30+fact that matching on a value in a dependently typed language can affect what

31+we know about the forms of other values. In its simplest form, the \texttt{with} rule

32+adds another argument to the function being defined, e.g. we have already seen

33+a vector filter function, defined as follows:

34+

35+\begin{SaveVerbatim}{vfilterdef}

36+

37+filter : (a -> Bool) -> Vect a n -> (p ** Vect a p);

38+filter p [] = ( _ ** [] );

39+filter p (x :: xs) with filter p xs {

40+ | ( _ ** xs' )

41+ = if (p x) then ( _ ** x :: xs' ) else ( _ ** xs' );

42+}

43+

44+\end{SaveVerbatim}

45+\useverb{vfilterdef}

46+

47+\noindent

48+Here, the \texttt{with} clause allows us to deconstruct the result of

49+\texttt{filter p xs}.

50+Effectively, it adds this value as an extra argument, which we place after the

51+vertical bar.

52+

53+If the intermediate computation itself has a dependent type, then the result

54+can affect the forms of other arguments --- we can learn the form of one value by

55+testing another. For example, a \texttt{Nat} is either even or odd. If it's even it will

56+be the sum of two equal \texttt{Nat}s. Otherwise, it is the sum of two equal \texttt{Nat}s

57+plus one:

58+

59+\begin{SaveVerbatim}{parity}

60+

61+data Parity : Nat -> Set where

62+ even : Parity (n + n)

63+ | odd : Parity (S (n + n));

64+

65+\end{SaveVerbatim}

66+\useverb{parity}

67+

68+

69+