67c5734 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Added case and pattern matching let bindings

67c5734Edwin Brady15 years ago

src/Core/CoreParser.hs+1

compare with master

unifiedsplit

@@ -21,6 +21,7 @@ idrisDef = haskellDef {

21 reservedOpNames = [":", "..", "=", "\\", "|", "<-", "->", "=>", "**"],

22 reservedNames = ["let", "in", "data", "Set",

23 "do", "dsl", "import", "impossible",

24+ "case", "of",

24 "infix", "infixl", "infixr", "prefix",

25 "infix", "infixl", "infixr", "prefix",

25 "where", "with", "forall", "syntax", "proof",

26 "where", "with", "forall", "syntax", "proof",

26 "using", "params", "namespace", "class", "instance",

27 "using", "params", "namespace", "class", "instance",

src/Core/Elaborate.hs+93−84

@@ -28,24 +28,25 @@ data Command = Theorem Name Raw

28 | Print Name

29 | Tac (Elab ())

31−data ElabState = ES ProofState String (Maybe ElabState)

31+data ElabState aux = ES (ProofState, aux) String (Maybe (ElabState aux))

32 deriving Show

33−type Elab a = StateT ElabState TC a

33+type Elab' aux a = StateT (ElabState aux) TC a

34+type Elab a = Elab' () a

35−proof :: ElabState -> ProofState

36+proof :: ElabState aux -> ProofState

36−proof (ES p _ _) = p

37+proof (ES (p, _) _ _) = p

38−saveState :: Elab ()

39+saveState :: Elab' aux ()

39saveState = do e@(ES p s _) <- get

40saveState = do e@(ES p s _) <- get

40 put (ES p s (Just e))

41 put (ES p s (Just e))

42−loadState :: Elab ()

43+loadState :: Elab' aux ()

43loadState = do (ES p s e) <- get

44loadState = do (ES p s e) <- get

44 case e of

45 case e of

45 Just st -> put st

46 Just st -> put st

46 _ -> fail "Nothing to undo"

47 _ -> fail "Nothing to undo"

48−erun :: FC -> Elab a -> Elab a

49+erun :: FC -> Elab' aux a -> Elab' aux a

49erun f elab = do s <- get

50erun f elab = do s <- get

50 case runStateT elab s of

51 case runStateT elab s of

51 OK (a, s') -> do put s'

52 OK (a, s') -> do put s'

@@ -53,82 +54,90 @@ erun f elab = do s <- get

53 Error (At f e) -> lift $ Error (At f e)

54 Error (At f e) -> lift $ Error (At f e)

54 Error e -> lift $ Error (At f e)

55 Error e -> lift $ Error (At f e)

56−runElab :: Elab a -> ProofState -> TC (a, ElabState)

57+runElab :: aux -> Elab' aux a -> ProofState -> TC (a, ElabState aux)

57−runElab e ps = runStateT e (ES ps "" Nothing)

58+runElab a e ps = runStateT e (ES (ps, a) "" Nothing)

59−execElab :: Elab a -> ProofState -> TC ElabState

60+execElab :: aux -> Elab' aux a -> ProofState -> TC (ElabState aux)

60−execElab e ps = execStateT e (ES ps "" Nothing)

61+execElab a e ps = execStateT e (ES (ps, a) "" Nothing)

62initElaborator :: Name -> Context -> Type -> ProofState

63initElaborator :: Name -> Context -> Type -> ProofState

63initElaborator = newProof

64initElaborator = newProof

65−elaborate :: Context -> Name -> Type -> Elab a -> TC (a, String)

66+elaborate :: Context -> Name -> Type -> aux -> Elab' aux a -> TC (a, String)

66−elaborate ctxt n ty elab = do let ps = initElaborator n ctxt ty

67+elaborate ctxt n ty d elab = do let ps = initElaborator n ctxt ty

67− (a, ES ps' str _) <- runElab elab ps

68+ (a, ES ps' str _) <- runElab d elab ps

68− return (a, str)

69+ return (a, str)

71+updateAux :: (aux -> aux) -> Elab' aux ()

72+updateAux f = do ES (ps, a) l p <- get

73+ put (ES (ps, f a) l p)

74+

75+getAux :: Elab' aux aux

76+getAux = do ES (ps, a) _ _ <- get

77+ return a

78+

70−processTactic' t = do ES p logs prev <- get

79+processTactic' t = do ES (p, a) logs prev <- get

71 (p', log) <- lift $ processTactic t p

80 (p', log) <- lift $ processTactic t p

72− put (ES p' (logs ++ log) prev)

81+ put (ES (p', a) (logs ++ log) prev)

73 return ()

82 return ()

75-- Some handy gadgets for pulling out bits of state

84-- Some handy gadgets for pulling out bits of state

77-- get the global context

86-- get the global context

78−get_context :: Elab Context

87+get_context :: Elab' aux Context

79get_context = do ES p _ _ <- get

88get_context = do ES p _ _ <- get

80− return (context p)

89+ return (context (fst p))

82-- get the proof term

91-- get the proof term

83−get_term :: Elab Term

92+get_term :: Elab' aux Term

84get_term = do ES p _ _ <- get

93get_term = do ES p _ _ <- get

85− return (pterm p)

94+ return (pterm (fst p))

87-- get the local context at the currently in focus hole

96-- get the local context at the currently in focus hole

88−get_env :: Elab Env

97+get_env :: Elab' aux Env

89get_env = do ES p _ _ <- get

98get_env = do ES p _ _ <- get

90− lift $ envAtFocus p

99+ lift $ envAtFocus (fst p)

100

92−get_holes :: Elab [Name]

101+get_holes :: Elab' aux [Name]

93get_holes = do ES p _ _ <- get

102get_holes = do ES p _ _ <- get

94− return (holes p)

103+ return (holes (fst p))

104

96-- get the current goal type

105-- get the current goal type

97−goal :: Elab Type

106+goal :: Elab' aux Type

98goal = do ES p _ _ <- get

107goal = do ES p _ _ <- get

99− b <- lift $ goalAtFocus p

108+ b <- lift $ goalAtFocus (fst p)

100 return (binderTy b)

109 return (binderTy b)

101

110

102-- typecheck locally

111-- typecheck locally

103−get_type :: Raw -> Elab Type

112+get_type :: Raw -> Elab' aux Type

104get_type tm = do ctxt <- get_context

113get_type tm = do ctxt <- get_context

105 env <- get_env

114 env <- get_env

106 (val, ty) <- lift $ check ctxt env tm

115 (val, ty) <- lift $ check ctxt env tm

107 return (finalise ty)

116 return (finalise ty)

108

117

109-- get holes we've deferred for later definition

118-- get holes we've deferred for later definition

110−get_deferred :: Elab [Name]

119+get_deferred :: Elab' aux [Name]

111get_deferred = do ES p _ _ <- get

120get_deferred = do ES p _ _ <- get

112− return (deferred p)

121+ return (deferred (fst p))

113

122

114−get_inj :: Elab [(Term, Term, Term)]

123+get_inj :: Elab' aux [(Term, Term, Term)]

115get_inj = do ES p _ _ <- get

124get_inj = do ES p _ _ <- get

116− return (injective p)

125+ return (injective (fst p))

117

126

118−checkInjective :: (Term, Term, Term) -> Elab ()

127+checkInjective :: (Term, Term, Term) -> Elab' aux ()

119checkInjective (tm, l, r) = if isInjective tm then return ()

128checkInjective (tm, l, r) = if isInjective tm then return ()

120 else lift $ tfail (NotInjective tm l r)

129 else lift $ tfail (NotInjective tm l r)

121

130

122-- get instance argument names

131-- get instance argument names

123−get_instances :: Elab [Name]

132+get_instances :: Elab' aux [Name]

124get_instances = do ES p _ _ <- get

133get_instances = do ES p _ _ <- get

125− return (instances p)

134+ return (instances (fst p))

126

135

127-- given a desired hole name, return a unique hole name

136-- given a desired hole name, return a unique hole name

128−unique_hole :: Name -> Elab Name

137+unique_hole :: Name -> Elab' aux Name

129unique_hole n = do ES p _ _ <- get

138unique_hole n = do ES p _ _ <- get

130− let bs = bound_in (pterm p) ++ bound_in (ptype p)

139+ let bs = bound_in (pterm (fst p)) ++ bound_in (ptype (fst p))

131− n' <- uniqueNameCtxt (context p) n (holes p ++ bs)

140+ n' <- uniqueNameCtxt (context (fst p)) n (holes (fst p) ++ bs)

132 return n'

141 return n'

133 where

142 where

134 bound_in (Bind n b sc) = n : bi b ++ bound_in sc

143 bound_in (Bind n b sc) = n : bi b ++ bound_in sc

@@ -139,73 +148,73 @@ unique_hole n = do ES p _ _ <- get

139 bound_in (App f a) = bound_in f ++ bound_in a

148 bound_in (App f a) = bound_in f ++ bound_in a

140 bound_in _ = []

149 bound_in _ = []

141

150

142−uniqueNameCtxt :: Context -> Name -> [Name] -> Elab Name

151+uniqueNameCtxt :: Context -> Name -> [Name] -> Elab' aux Name

143uniqueNameCtxt ctxt n hs

152uniqueNameCtxt ctxt n hs

144 | n `elem` hs = uniqueNameCtxt ctxt (nextName n) hs

153 | n `elem` hs = uniqueNameCtxt ctxt (nextName n) hs

145 | [_] <- lookupTy Nothing n ctxt = uniqueNameCtxt ctxt (nextName n) hs

154 | [_] <- lookupTy Nothing n ctxt = uniqueNameCtxt ctxt (nextName n) hs

146 | otherwise = return n

155 | otherwise = return n

147

156

148−elog :: String -> Elab ()

157+elog :: String -> Elab' aux ()

149elog str = do ES p logs prev <- get

158elog str = do ES p logs prev <- get

150 put (ES p (logs ++ str ++ "\n") prev)

159 put (ES p (logs ++ str ++ "\n") prev)

151

160

152-- The primitives, from ProofState

161-- The primitives, from ProofState

153

162

154−attack :: Elab ()

163+attack :: Elab' aux ()

155attack = processTactic' Attack

164attack = processTactic' Attack

156

165

157−claim :: Name -> Raw -> Elab ()

166+claim :: Name -> Raw -> Elab' aux ()

158claim n t = processTactic' (Claim n t)

167claim n t = processTactic' (Claim n t)

159

168

160−exact :: Raw -> Elab ()

169+exact :: Raw -> Elab' aux ()

161exact t = processTactic' (Exact t)

170exact t = processTactic' (Exact t)

162

171

163−fill :: Raw -> Elab ()

172+fill :: Raw -> Elab' aux ()

164fill t = processTactic' (Fill t)

173fill t = processTactic' (Fill t)

165

174

166−prep_fill :: Name -> [Name] -> Elab ()

175+prep_fill :: Name -> [Name] -> Elab' aux ()

167prep_fill n ns = processTactic' (PrepFill n ns)

176prep_fill n ns = processTactic' (PrepFill n ns)

168

177

169−complete_fill :: Elab ()

178+complete_fill :: Elab' aux ()

170complete_fill = processTactic' CompleteFill

179complete_fill = processTactic' CompleteFill

171

180

172−solve :: Elab ()

181+solve :: Elab' aux ()

173solve = processTactic' Solve

182solve = processTactic' Solve

174

183

175−start_unify :: Name -> Elab ()

184+start_unify :: Name -> Elab' aux ()

176start_unify n = processTactic' (StartUnify n)

185start_unify n = processTactic' (StartUnify n)

177

186

178−end_unify :: Elab ()

187+end_unify :: Elab' aux ()

179end_unify = processTactic' EndUnify

188end_unify = processTactic' EndUnify

180

189

181−regret :: Elab ()

190+regret :: Elab' aux ()

182regret = processTactic' Regret

191regret = processTactic' Regret

183

192

184−compute :: Elab ()

193+compute :: Elab' aux ()

185compute = processTactic' Compute

194compute = processTactic' Compute

186

195

187−eval_in :: Raw -> Elab ()

196+eval_in :: Raw -> Elab' aux ()

188eval_in t = processTactic' (EvalIn t)

197eval_in t = processTactic' (EvalIn t)

189

198

190−check_in :: Raw -> Elab ()

199+check_in :: Raw -> Elab' aux ()

191check_in t = processTactic' (CheckIn t)

200check_in t = processTactic' (CheckIn t)

192

201

193−intro :: Maybe Name -> Elab ()

202+intro :: Maybe Name -> Elab' aux ()

194intro n = processTactic' (Intro n)

203intro n = processTactic' (Intro n)

195

204

196−introTy :: Raw -> Maybe Name -> Elab ()

205+introTy :: Raw -> Maybe Name -> Elab' aux ()

197introTy ty n = processTactic' (IntroTy ty n)

206introTy ty n = processTactic' (IntroTy ty n)

198

207

199−forall :: Name -> Raw -> Elab ()

208+forall :: Name -> Raw -> Elab' aux ()

200forall n t = processTactic' (Forall n t)

209forall n t = processTactic' (Forall n t)

201

210

202−letbind :: Name -> Raw -> Raw -> Elab ()

211+letbind :: Name -> Raw -> Raw -> Elab' aux ()

203letbind n t v = processTactic' (LetBind n t v)

212letbind n t v = processTactic' (LetBind n t v)

204

213

205−rewrite :: Raw -> Elab ()

214+rewrite :: Raw -> Elab' aux ()

206rewrite tm = processTactic' (Rewrite tm)

215rewrite tm = processTactic' (Rewrite tm)

207

216

208−patvar :: Name -> Elab ()

217+patvar :: Name -> Elab' aux ()

209patvar n = do env <- get_env

218patvar n = do env <- get_env

210 if (n `elem` map fst env) then do apply (Var n) []; solve

219 if (n `elem` map fst env) then do apply (Var n) []; solve

211 else do n' <- case n of

220 else do n' <- case n of

@@ -214,48 +223,48 @@ patvar n = do env <- get_env

214 NS _ _ -> return n

223 NS _ _ -> return n

215 processTactic' (PatVar n')

224 processTactic' (PatVar n')

216

225

217−patbind :: Name -> Elab ()

226+patbind :: Name -> Elab' aux ()

218patbind n = processTactic' (PatBind n)

227patbind n = processTactic' (PatBind n)

219

228

220−focus :: Name -> Elab ()

229+focus :: Name -> Elab' aux ()

221focus n = processTactic' (Focus n)

230focus n = processTactic' (Focus n)

222

231

223−movelast :: Name -> Elab ()

232+movelast :: Name -> Elab' aux ()

224movelast n = processTactic' (MoveLast n)

233movelast n = processTactic' (MoveLast n)

225

234

226−defer :: Name -> Elab ()

235+defer :: Name -> Elab' aux ()

227defer n = do n' <- unique_hole n

236defer n = do n' <- unique_hole n

228 processTactic' (Defer n')

237 processTactic' (Defer n')

229

238

230−instanceArg :: Name -> Elab ()

239+instanceArg :: Name -> Elab' aux ()

231instanceArg n = processTactic' (Instance n)

240instanceArg n = processTactic' (Instance n)

232

241

233−proofstate :: Elab ()

242+proofstate :: Elab' aux ()

234proofstate = processTactic' ProofState

243proofstate = processTactic' ProofState

235

244

236−reorder_claims :: Name -> Elab ()

245+reorder_claims :: Name -> Elab' aux ()

237reorder_claims n = processTactic' (Reorder n)

246reorder_claims n = processTactic' (Reorder n)

238

247

239−qed :: Elab Term

248+qed :: Elab' aux Term

240qed = do processTactic' QED

249qed = do processTactic' QED

241 ES p _ _ <- get

250 ES p _ _ <- get

242− return (pterm p)

251+ return (pterm (fst p))

243

252

244−undo :: Elab ()

253+undo :: Elab' aux ()

245undo = processTactic' Undo

254undo = processTactic' Undo

246

255

247−prepare_apply :: Raw -> [(Bool, Int)] -> Elab [Name]

256+prepare_apply :: Raw -> [(Bool, Int)] -> Elab' aux [Name]

248prepare_apply fn imps =

257prepare_apply fn imps =

249 do ty <- get_type fn

258 do ty <- get_type fn

250 ctxt <- get_context

259 ctxt <- get_context

251 env <- get_env

260 env <- get_env

252 -- let claims = getArgs ty imps

261 -- let claims = getArgs ty imps

253 claims <- mkClaims (normalise ctxt env ty) imps []

262 claims <- mkClaims (normalise ctxt env ty) imps []

254− ES p s prev <- get

263+ ES (p, a) s prev <- get

255 -- reverse the claims we made so that args go left to right

264 -- reverse the claims we made so that args go left to right

256 let n = length (filter not (map fst imps))

265 let n = length (filter not (map fst imps))

257 let (h : hs) = holes p

266 let (h : hs) = holes p

258− put (ES (p { holes = h : (reverse (take n hs) ++ drop n hs) }) s prev)

267+ put (ES (p { holes = h : (reverse (take n hs) ++ drop n hs) }, a) s prev)

259-- case claims of

268-- case claims of

260-- [] -> return ()

269-- [] -> return ()

261-- (h : _) -> reorder_claims h

270-- (h : _) -> reorder_claims h

@@ -278,7 +287,7 @@ prepare_apply fn imps =

278 mkMN n@(UN x) = MN 0 x

287 mkMN n@(UN x) = MN 0 x

279 mkMN (NS n xs) = NS (mkMN n) xs

288 mkMN (NS n xs) = NS (mkMN n) xs

280

289

281−apply :: Raw -> [(Bool, Int)] -> Elab [Name]

290+apply :: Raw -> [(Bool, Int)] -> Elab' aux [Name]

282apply fn imps =

291apply fn imps =

283 do args <- prepare_apply fn imps

292 do args <- prepare_apply fn imps

284 fill (raw_apply fn (map Var args))

293 fill (raw_apply fn (map Var args))

@@ -288,14 +297,14 @@ apply fn imps =

288 -- so do nothing

297 -- so do nothing

289 ptm <- get_term

298 ptm <- get_term

290 let dontunify = [] -- map fst (filter (not.snd) (zip args imps))

299 let dontunify = [] -- map fst (filter (not.snd) (zip args imps))

291− ES p s prev <- get

300+ ES (p, a) s prev <- get

292 let (n, hs) = unified p

301 let (n, hs) = unified p

293 let unify = (n, filter (\ (n, t) -> not (n `elem` dontunify)) hs)

302 let unify = (n, filter (\ (n, t) -> not (n `elem` dontunify)) hs)

294− put (ES (p { unified = unify }) s prev)

303+ put (ES (p { unified = unify }, a) s prev)

295 end_unify

304 end_unify

296 return args

305 return args

297

306

298−apply_elab :: Name -> [Maybe (Int, Elab ())] -> Elab ()

307+apply_elab :: Name -> [Maybe (Int, Elab' aux ())] -> Elab' aux ()

299apply_elab n args =

308apply_elab n args =

300 do ty <- get_type (Var n)

309 do ty <- get_type (Var n)

301 ctxt <- get_context

310 ctxt <- get_context

@@ -337,7 +346,7 @@ apply_elab n args =

337 mkMN n@(UN x) = MN 0 x

346 mkMN n@(UN x) = MN 0 x

338 mkMN (NS n ns) = NS (mkMN n) ns

347 mkMN (NS n ns) = NS (mkMN n) ns

339

348

340−simple_app :: Elab () -> Elab () -> Elab ()

349+simple_app :: Elab' aux () -> Elab' aux () -> Elab' aux ()

341simple_app fun arg =

350simple_app fun arg =

342 do a <- unique_hole (MN 0 "a")

351 do a <- unique_hole (MN 0 "a")

343 b <- unique_hole (MN 0 "b")

352 b <- unique_hole (MN 0 "b")

@@ -360,13 +369,13 @@ simple_app fun arg =

360

369

361-- Abstract over an argument of unknown type, giving a name for the hole

370-- Abstract over an argument of unknown type, giving a name for the hole

362-- which we'll fill with the argument type too.

371-- which we'll fill with the argument type too.

363−arg :: Name -> Name -> Elab ()

372+arg :: Name -> Name -> Elab' aux ()

364arg n tyhole = do ty <- unique_hole tyhole

373arg n tyhole = do ty <- unique_hole tyhole

365 claim ty RSet

374 claim ty RSet

366 forall n (Var ty)

375 forall n (Var ty)

367

376

368-- Try a tactic, if it fails, try another

377-- Try a tactic, if it fails, try another

369−try :: Elab a -> Elab a -> Elab a

378+try :: Elab' aux a -> Elab' aux a -> Elab' aux a

370try t1 t2 = do s <- get

379try t1 t2 = do s <- get

371 case runStateT t1 s of

380 case runStateT t1 s of

372 OK (v, s') -> do put s'

381 OK (v, s') -> do put s'

@@ -374,13 +383,13 @@ try t1 t2 = do s <- get

374 _ -> do put s; t2

383 _ -> do put s; t2

375

384

376-- Try a selection of tactics. Exactly one must work, all others must fail

385-- Try a selection of tactics. Exactly one must work, all others must fail

377−tryAll :: [(Elab a, String)] -> Elab a

386+tryAll :: [(Elab' aux a, String)] -> Elab' aux a

378tryAll xs = tryAll' [] (fail "Nothing to try") (map fst xs)

387tryAll xs = tryAll' [] (fail "Nothing to try") (map fst xs)

379 where

388 where

380− tryAll' :: [Elab a] -> -- successes

389+ tryAll' :: [Elab' aux a] -> -- successes

381− Elab a -> -- last failure

390+ Elab' aux a -> -- last failure

382− [Elab a] -> -- still to try

391+ [Elab' aux a] -> -- still to try

383− Elab a

392+ Elab' aux a

384 tryAll' [res] _ [] = res

393 tryAll' [res] _ [] = res

385 tryAll' (_:_) _ [] = fail $ "Couldn't resolve alternative: "

394 tryAll' (_:_) _ [] = fail $ "Couldn't resolve alternative: "

386 ++ showSep ", " (map snd xs)

395 ++ showSep ", " (map snd xs)

src/Core/ProofShell.hs+2−2

@@ -41,8 +41,8 @@ processCommand (Print n) state =

41 [tm] -> (state, show tm)

42 _ -> (state, "No such name")

43processCommand (Tac e) state

44− | Just ps <- prf state = case execElab e ps of

44+ | Just ps <- prf state = case execElab () e ps of

45− OK (ES ps' resp _) ->

45+ OK (ES (ps', _) resp _) ->

46 if (not (done ps'))

47 then (state { prf = Just ps' }, resp)

48 else (state { prf = Nothing,

src/Core/TT.hs+2

@@ -88,6 +88,8 @@ showSep sep [] = ""

88showSep sep [x] = x

89showSep sep (x:xs) = x ++ sep ++ showSep sep xs

91+pmap f (x, y) = (f x, f y)

92+

91traceWhen True msg a = trace msg a

93traceWhen True msg a = trace msg a

92traceWhen False _ a = a

94traceWhen False _ a = a

src/Idris/AbsSyntax.hs+15

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

386 | PPi Plicity Name PTerm PTerm

387 | PLet Name PTerm PTerm PTerm

388 | PApp FC PTerm [PArg]

389+ | PCase FC PTerm [(PTerm, PTerm)]

389 | PTrue FC

390 | PTrue FC

390 | PFalse FC

391 | PFalse FC

391 | PRefl FC

392 | PRefl FC

@@ -417,6 +418,7 @@ mapPT f t = f (mpt t) where

417 mpt (PPi p n t s) = PPi p n (mapPT f t) (mapPT f s)

418 mpt (PPi p n t s) = PPi p n (mapPT f t) (mapPT f s)

418 mpt (PLet n ty v s) = PLet n (mapPT f ty) (mapPT f v) (mapPT f s)

419 mpt (PLet n ty v s) = PLet n (mapPT f ty) (mapPT f v) (mapPT f s)

419 mpt (PApp fc t as) = PApp fc (mapPT f t) (map (fmap (mapPT f)) as)

420 mpt (PApp fc t as) = PApp fc (mapPT f t) (map (fmap (mapPT f)) as)

421+ mpt (PCase fc c os) = PCase fc (mapPT f c) (map (pmap (mapPT f)) os)

420 mpt (PEq fc l r) = PEq fc (mapPT f l) (mapPT f r)

422 mpt (PEq fc l r) = PEq fc (mapPT f l) (mapPT f r)

421 mpt (PPair fc l r) = PPair fc (mapPT f l) (mapPT f r)

423 mpt (PPair fc l r) = PPair fc (mapPT f l) (mapPT f r)

422 mpt (PDPair fc l t r) = PDPair fc (mapPT f l) (mapPT f t) (mapPT f r)

424 mpt (PDPair fc l t r) = PDPair fc (mapPT f l) (mapPT f t) (mapPT f r)

@@ -446,7 +448,9 @@ type PTactic = PTactic' PTerm

446

448

447data PDo' t = DoExp FC t

449data PDo' t = DoExp FC t

448 | DoBind FC Name t

450 | DoBind FC Name t

451+ | DoBindP FC t t

449 | DoLet FC Name t

452 | DoLet FC Name t

453+ | DoLetP FC t t

450 deriving (Eq, Functor)

454 deriving (Eq, Functor)

451{-!

455{-!

452deriving instance Binary PDo'

456deriving instance Binary PDo'

@@ -637,6 +641,8 @@ showImp impl tm = se 10 tm where

637 = let args = getExps as in

641 = let args = getExps as in

638 bracket p 1 $ se 1 f ++ if impl then concatMap sArg as

642 bracket p 1 $ se 1 f ++ if impl then concatMap sArg as

639 else concatMap seArg args

643 else concatMap seArg args

644+ se p (PCase _ scr opts) = "case " ++ se 10 scr ++ " of " ++ showSep " | " (map sc opts)

645+ where sc (l, r) = se 10 l ++ " => " ++ se 10 r

640 se p (PHidden tm) = "." ++ se 0 tm

646 se p (PHidden tm) = "." ++ se 0 tm

641 se p (PRefl _) = "refl"

647 se p (PRefl _) = "refl"

642 se p (PResolveTC _) = "resolvetc"

648 se p (PResolveTC _) = "resolvetc"

@@ -675,6 +681,7 @@ allNamesIn tm = nub $ ni [] tm

675 ni env (PRef _ n)

681 ni env (PRef _ n)

676 | not (n `elem` env) = [n]

682 | not (n `elem` env) = [n]

677 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)

683 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)

684+ ni env (PCase _ c os) = ni env c ++ concatMap (ni env) (map snd os)

678 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc

685 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc

679 ni env (PPi _ n ty sc) = ni env ty ++ ni (n:env) sc

686 ni env (PPi _ n ty sc) = ni env ty ++ ni (n:env) sc

680 ni env (PHidden tm) = ni env tm

687 ni env (PHidden tm) = ni env tm

@@ -694,6 +701,7 @@ namesIn ist tm = nub $ ni [] tm

694 [] -> [n]

701 [] -> [n]

695 _ -> []

702 _ -> []

696 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)

703 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)

704+ ni env (PCase _ c os) = ni env c ++ concatMap (ni env) (map snd os)

697 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc

705 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc

698 ni env (PPi _ n ty sc) = ni env ty ++ ni (n:env) sc

706 ni env (PPi _ n ty sc) = ni env ty ++ ni (n:env) sc

699 ni env (PEq _ l r) = ni env l ++ ni env r

707 ni env (PEq _ l r) = ni env l ++ ni env r

@@ -825,6 +833,7 @@ expandParams dec ps ns tm = en tm

825 | n `elem` ns = PApp fc (PRef fc (dec n))

833 | n `elem` ns = PApp fc (PRef fc (dec n))

826 (map (pexp . (PRef fc)) (map fst ps))

834 (map (pexp . (PRef fc)) (map fst ps))

827 en (PApp fc f as) = PApp fc (en f) (map (fmap en) as)

835 en (PApp fc f as) = PApp fc (en f) (map (fmap en) as)

836+ en (PCase fc c os) = PCase fc (en c) (map (pmap en) os)

828 en t = t

837 en t = t

829

838

830expandParamsD :: IState ->

839expandParamsD :: IState ->

@@ -881,6 +890,7 @@ getPriority i tm = pri tm

881 pri (PRefl _) = 1

890 pri (PRefl _) = 1

882 pri (PEq _ l r) = max 1 (max (pri l) (pri r))

891 pri (PEq _ l r) = max 1 (max (pri l) (pri r))

883 pri (PApp _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.getTm) as)))

892 pri (PApp _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.getTm) as)))

893+ pri (PCase _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.snd) as)))

884 pri (PPair _ l r) = max 1 (max (pri l) (pri r))

894 pri (PPair _ l r) = max 1 (max (pri l) (pri r))

885 pri (PDPair _ l t r) = max 1 (max (pri l) (max (pri t) (pri r)))

895 pri (PDPair _ l t r) = max 1 (max (pri l) (max (pri t) (pri r)))

886 pri (PAlternative as) = maximum (map pri as)

896 pri (PAlternative as) = maximum (map pri as)

@@ -1004,6 +1014,9 @@ addImpl ist ptm = ai [] ptm

1004 ai env (PApp fc f as) = let f' = ai env f

1014 ai env (PApp fc f as) = let f' = ai env f

1005 as' = map (fmap (ai env)) as in

1015 as' = map (fmap (ai env)) as in

1006 mkPApp fc 1 f' as'

1016 mkPApp fc 1 f' as'

1017+ ai env (PCase fc c os) = let c' = ai env c

1018+ os' = map (pmap (ai env)) os in

1019+ PCase fc c' os'

1007 ai env (PLam n ty sc) = let ty' = ai env ty

1020 ai env (PLam n ty sc) = let ty' = ai env ty

1008 sc' = ai (n:env) sc in

1021 sc' = ai (n:env) sc in

1009 PLam n ty' sc'

1022 PLam n ty' sc'

@@ -1164,6 +1177,7 @@ substMatch n tm t = sm t where

1164 sm (PLam x t sc) = PLam x (sm t) (sm sc)

1177 sm (PLam x t sc) = PLam x (sm t) (sm sc)

1165 sm (PPi p x t sc) = PPi p x (sm t) (sm sc)

1178 sm (PPi p x t sc) = PPi p x (sm t) (sm sc)

1166 sm (PApp f x as) = PApp f (sm x) (map (fmap sm) as)

1179 sm (PApp f x as) = PApp f (sm x) (map (fmap sm) as)

1180+ sm (PCase f x as) = PCase f (sm x) (map (pmap sm) as)

1167 sm (PEq f x y) = PEq f (sm x) (sm y)

1181 sm (PEq f x y) = PEq f (sm x) (sm y)

1168 sm (PPair f x y) = PPair f (sm x) (sm y)

1182 sm (PPair f x y) = PPair f (sm x) (sm y)

1169 sm (PDPair f x t y) = PDPair f (sm x) (sm t) (sm y)

1183 sm (PDPair f x t y) = PDPair f (sm x) (sm t) (sm y)

@@ -1177,6 +1191,7 @@ shadow n n' t = sm t where

1177 sm (PLam x t sc) = PLam x (sm t) (sm sc)

1191 sm (PLam x t sc) = PLam x (sm t) (sm sc)

1178 sm (PPi p x t sc) = PPi p x (sm t) (sm sc)

1192 sm (PPi p x t sc) = PPi p x (sm t) (sm sc)

1179 sm (PApp f x as) = PApp f (sm x) (map (fmap sm) as)

1193 sm (PApp f x as) = PApp f (sm x) (map (fmap sm) as)

1194+ sm (PCase f x as) = PCase f (sm x) (map (pmap sm) as)

1180 sm (PEq f x y) = PEq f (sm x) (sm y)

1195 sm (PEq f x y) = PEq f (sm x) (sm y)

1181 sm (PPair f x y) = PPair f (sm x) (sm y)

1196 sm (PPair f x y) = PPair f (sm x) (sm y)

1182 sm (PDPair f x t y) = PDPair f (sm x) (sm t) (sm y)

1197 sm (PDPair f x t y) = PDPair f (sm x) (sm t) (sm y)

src/Idris/ElabDecls.hs+32−24

@@ -41,14 +41,15 @@ elabType info syn fc n ty' = {- let ty' = piBind (params info) ty_in

41 ty' <- implicit syn n ty'

42 let ty = addImpl i ty'

43 logLvl 2 $ show n ++ " type " ++ showImp True ty

44− ((ty', defer), log) <- tclift $ elaborate ctxt n (Set (UVal 0))

44+ ((ty', defer, is), log) <- tclift $ elaborate ctxt n (Set (UVal 0)) []

45− (erun fc (build i info False n ty))

45+ (erun fc (build i info False n ty))

46 (cty, _) <- recheckC ctxt fc [] ty'

47 logLvl 2 $ "---> " ++ show cty

48 let nty = normalise ctxt [] cty

49 ds <- checkDef fc ((n, nty):defer)

50 addIBC (IBCDef n)

51 addDeferred ds

52+ mapM_ (elabDecl' info) is

53elabData :: ElabInfo -> SyntaxInfo -> FC -> PData -> Idris ()

54elabData :: ElabInfo -> SyntaxInfo -> FC -> PData -> Idris ()

54elabData info syn fc (PDatadecl n t_in dcons)

55elabData info syn fc (PDatadecl n t_in dcons)

@@ -58,10 +59,11 @@ elabData info syn fc (PDatadecl n t_in dcons)

58 i <- get

59 i <- get

59 t_in <- implicit syn n t_in

60 t_in <- implicit syn n t_in

60 let t = addImpl i t_in

61 let t = addImpl i t_in

61− ((t', defer), log) <- tclift $ elaborate ctxt n (Set (UVal 0))

62+ ((t', defer, is), log) <- tclift $ elaborate ctxt n (Set (UVal 0)) []

62− (erun fc (build i info False n t))

63+ (erun fc (build i info False n t))

63 def' <- checkDef fc defer

64 def' <- checkDef fc defer

64 addDeferred def'

65 addDeferred def'

66+ mapM_ (elabDecl' info) is

65 (cty, _) <- recheckC ctxt fc [] t'

67 (cty, _) <- recheckC ctxt fc [] t'

66 logLvl 2 $ "---> " ++ show cty

68 logLvl 2 $ "---> " ++ show cty

67 updateContext (addTyDecl n cty) -- temporary, to check cons

69 updateContext (addTyDecl n cty) -- temporary, to check cons

@@ -78,11 +80,12 @@ elabCon info syn (n, t_in, fc)

78 t_in <- implicit syn n t_in

80 t_in <- implicit syn n t_in

79 let t = addImpl i t_in

81 let t = addImpl i t_in

80 logLvl 2 $ show fc ++ ":Constructor " ++ show n ++ " : " ++ showImp True t

82 logLvl 2 $ show fc ++ ":Constructor " ++ show n ++ " : " ++ showImp True t

81− ((t', defer), log) <- tclift $ elaborate ctxt n (Set (UVal 0))

83+ ((t', defer, is), log) <- tclift $ elaborate ctxt n (Set (UVal 0)) []

82− (erun fc (build i info False n t))

84+ (erun fc (build i info False n t))

83 logLvl 2 $ "Rechecking " ++ show t'

85 logLvl 2 $ "Rechecking " ++ show t'

84 def' <- checkDef fc defer

86 def' <- checkDef fc defer

85 addDeferred def'

87 addDeferred def'

88+ mapM_ (elabDecl' info) is

86 ctxt <- getContext

89 ctxt <- getContext

87 (cty, _) <- recheckC ctxt fc [] t'

90 (cty, _) <- recheckC ctxt fc [] t'

88 logLvl 2 $ "---> " ++ show n ++ " : " ++ show cty

91 logLvl 2 $ "---> " ++ show n ++ " : " ++ show cty

@@ -128,8 +131,8 @@ elabVal info aspat tm_in

128 i <- get

131 i <- get

129 let tm = addImpl i tm_in

132 let tm = addImpl i tm_in

130 logLvl 10 (showImp True tm)

133 logLvl 10 (showImp True tm)

131− ((tm', defer), _) <- tclift $ elaborate ctxt (MN 0 "val") infP

134+ ((tm', defer, is), _) <- tclift $ elaborate ctxt (MN 0 "val") infP []

132− (build i info aspat (MN 0 "val") (infTerm tm))

135+ (build i info aspat (MN 0 "val") (infTerm tm))

133 logLvl 3 ("Value: " ++ show tm')

136 logLvl 3 ("Value: " ++ show tm')

134 let vtm = getInferTerm tm'

137 let vtm = getInferTerm tm'

135 logLvl 2 (show vtm)

138 logLvl 2 (show vtm)

@@ -141,7 +144,7 @@ elabClause info fc tcgen (PClause fname lhs_in [] PImpossible [])

141 i <- get

144 i <- get

142 let lhs = addImpl i lhs_in

145 let lhs = addImpl i lhs_in

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

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

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

147+ case elaborate ctxt (MN 0 "patLHS") infP []

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

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

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

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

147 Error _ -> return ()

150 Error _ -> return ()

@@ -153,8 +156,9 @@ elabClause info fc tcgen (PClause fname lhs_in withs rhs_in whereblock)

153 i <- get

156 i <- get

154 let lhs = addImpl i lhs_in

157 let lhs = addImpl i lhs_in

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

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

159+ ((lhs', dlhs, []), _) <-

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

160+ tclift $ elaborate ctxt (MN 0 "patLHS") infP []

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

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

158 let lhs_tm = orderPats (getInferTerm lhs')

162 let lhs_tm = orderPats (getInferTerm lhs')

159 let lhs_ty = getInferType lhs'

163 let lhs_ty = getInferType lhs'

160 logLvl 3 (show lhs_tm)

164 logLvl 3 (show lhs_tm)

@@ -176,17 +180,19 @@ elabClause info fc tcgen (PClause fname lhs_in withs rhs_in whereblock)

176 -- TODO: but don't do names in scope

180 -- TODO: but don't do names in scope

177 logLvl 2 (showImp True rhs)

181 logLvl 2 (showImp True rhs)

178 ctxt <- getContext -- new context with where block added

182 ctxt <- getContext -- new context with where block added

179− ((rhs', defer), _) <-

183+ ((rhs', defer, is), _) <-

180− tclift $ elaborate ctxt (MN 0 "patRHS") clhsty

184+ tclift $ elaborate ctxt (MN 0 "patRHS") clhsty []

181 (do pbinds lhs_tm

185 (do pbinds lhs_tm

182− (_, _) <- erun fc (build i info False fname rhs)

186+ (_, _, is) <- erun fc (build i info False fname rhs)

183 psolve lhs_tm

187 psolve lhs_tm

184 tt <- get_term

188 tt <- get_term

185− return $ runState (collectDeferred tt) [])

189+ let (tm, ds) = runState (collectDeferred tt) []

190+ return (tm, ds, is))

186 logLvl 2 $ "---> " ++ show rhs'

191 logLvl 2 $ "---> " ++ show rhs'

187 when (not (null defer)) $ iLOG $ "DEFERRED " ++ show defer

192 when (not (null defer)) $ iLOG $ "DEFERRED " ++ show defer

188 def' <- checkDef fc defer

193 def' <- checkDef fc defer

189 addDeferred def'

194 addDeferred def'

195+ mapM_ (elabDecl' info) is

190 ctxt <- getContext

196 ctxt <- getContext

191 logLvl 5 $ "Rechecking"

197 logLvl 5 $ "Rechecking"

192 (crhs, crhsty) <- recheckC ctxt fc [] rhs'

198 (crhs, crhsty) <- recheckC ctxt fc [] rhs'

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

213 i <- get

219 i <- get

214 let lhs = addImpl i lhs_in

220 let lhs = addImpl i lhs_in

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

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

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

222+ ((lhs', dlhs, []), _) <- tclift $ elaborate ctxt (MN 0 "patLHS") infP []

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

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

218 let lhs_tm = orderPats (getInferTerm lhs')

224 let lhs_tm = orderPats (getInferTerm lhs')

219 let lhs_ty = getInferType lhs'

225 let lhs_ty = getInferType lhs'

@@ -225,17 +231,18 @@ elabClause info fc tcgen (PWith fname lhs_in withs wval_in withblock)

225 let wval = addImpl i wval_in

231 let wval = addImpl i wval_in

226 logLvl 5 ("Checking " ++ showImp True wval)

232 logLvl 5 ("Checking " ++ showImp True wval)

227 -- Elaborate wval in this context

233 -- Elaborate wval in this context

228− ((wval', defer), _) <-

234+ ((wval', defer, is), _) <-

229 tclift $ elaborate ctxt (MN 0 "withRHS")

235 tclift $ elaborate ctxt (MN 0 "withRHS")

230− (bindTyArgs PVTy bargs infP)

236+ (bindTyArgs PVTy bargs infP) []

231 (do pbinds lhs_tm

237 (do pbinds lhs_tm

232 -- TODO: may want where here - see winfo abpve

238 -- TODO: may want where here - see winfo abpve

233− (_', d) <- erun fc (build i info False fname (infTerm wval))

239+ (_', d, is) <- erun fc (build i info False fname (infTerm wval))

234 psolve lhs_tm

240 psolve lhs_tm

235 tt <- get_term

241 tt <- get_term

236− return (tt, d))

242+ return (tt, d, is))

237 def' <- checkDef fc defer

243 def' <- checkDef fc defer

238 addDeferred def'

244 addDeferred def'

245+ mapM_ (elabDecl' info) is

239 (cwval, cwvalty) <- recheckC ctxt fc [] (getInferTerm wval')

246 (cwval, cwvalty) <- recheckC ctxt fc [] (getInferTerm wval')

240 logLvl 3 ("With type " ++ show cwvalty ++ "\nRet type " ++ show ret_ty)

247 logLvl 3 ("With type " ++ show cwvalty ++ "\nRet type " ++ show ret_ty)

241 windex <- getName

248 windex <- getName

@@ -262,15 +269,16 @@ elabClause info fc tcgen (PWith fname lhs_in withs wval_in withblock)

262 logLvl 3 ("New RHS " ++ show rhs)

269 logLvl 3 ("New RHS " ++ show rhs)

263 ctxt <- getContext -- New context with block added

270 ctxt <- getContext -- New context with block added

264 i <- get

271 i <- get

265− ((rhs', defer), _) <-

272+ ((rhs', defer, is), _) <-

266− tclift $ elaborate ctxt (MN 0 "wpatRHS") clhsty

273+ tclift $ elaborate ctxt (MN 0 "wpatRHS") clhsty []

267 (do pbinds lhs_tm

274 (do pbinds lhs_tm

268− (_, d) <- erun fc (build i info False fname rhs)

275+ (_, d, is) <- erun fc (build i info False fname rhs)

269 psolve lhs_tm

276 psolve lhs_tm

270 tt <- get_term

277 tt <- get_term

271− return (tt, d))

278+ return (tt, d, is))

272 def' <- checkDef fc defer

279 def' <- checkDef fc defer

273 addDeferred def'

280 addDeferred def'

281+ mapM_ (elabDecl' info) is

274 (crhs, crhsty) <- recheckC ctxt fc [] rhs'

282 (crhs, crhsty) <- recheckC ctxt fc [] rhs'

275 return $ Just (clhs, crhs)

283 return $ Just (clhs, crhs)

276 where

284 where

src/Idris/ElabTerm.hs+50−10

@@ -21,6 +21,8 @@ data ElabInfo = EInfo { params :: [(Name, PTerm)],

22toplevel = EInfo [] emptyContext id Nothing

24+type ElabD a = Elab' [PDecl] a

25+

24-- Using the elaborator, convert a term in raw syntax to a fully

26-- Using the elaborator, convert a term in raw syntax to a fully

25-- elaborated, typechecked term.

27-- elaborated, typechecked term.

26--

28--

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

30-- Also find deferred names in the term and their types

32-- Also find deferred names in the term and their types

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

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

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

35+ ElabD (Term, [(Name, Type)], [PDecl])

34build ist info pattern fn tm

36build ist info pattern fn tm

35 = do elab ist info pattern False fn tm

37 = do elab ist info pattern False fn tm

38+ is <- getAux

36 tt <- get_term

39 tt <- get_term

37− return $ runState (collectDeferred tt) []

40+ let (tm, ds) = runState (collectDeferred tt) []

41+ return (tm, ds, is)

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

43-- Build a term autogenerated as a typeclass method definition

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

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

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

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

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

47buildTC :: IState -> ElabInfo -> Bool -> Bool -> Name -> PTerm ->

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

48+ ElabD (Term, [(Name, Type)], [PDecl])

45buildTC ist info pattern tcgen fn tm

49buildTC ist info pattern tcgen fn tm

46 = do elab ist info pattern tcgen fn tm

50 = do elab ist info pattern tcgen fn tm

51+ is <- getAux

47 tt <- get_term

52 tt <- get_term

48− return $ runState (collectDeferred tt) []

53+ let (tm, ds) = runState (collectDeferred tt) []

54+ return (tm, ds, is)

55+

56+-- Returns the set of declarations we need to add to complete the definition

57+-- (most likely case blocks to elaborate)

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

59elab :: IState -> ElabInfo -> Bool -> Bool -> Name -> PTerm ->

51− Elab ()

60+ ElabD ()

52elab ist info pattern tcgen fn tm

61elab ist info pattern tcgen fn tm

53 = do elabE False tm

62 = do elabE False tm

54 when pattern -- convert remaining holes to pattern vars

63 when pattern -- convert remaining holes to pattern vars

@@ -215,8 +224,37 @@ elab ist info pattern tcgen fn tm

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

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

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

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

217 elab' ina (PElabError e) = fail e

226 elab' ina (PElabError e) = fail e

227+ elab' ina c@(PCase fc scr opts)

228+ = do attack

229+ tyn <- unique_hole (MN 0 "scty")

230+ claim tyn RSet

231+ valn <- unique_hole (MN 0 "scval")

232+ scvn <- unique_hole (MN 0 "scvar")

233+ claim valn (Var tyn)

234+ letbind scvn (Var tyn) (Var valn)

235+ focus valn

236+ elabE True scr

237+ args <- get_env

238+ cname <- unique_hole (mkCaseName fn)

239+ elab' ina (PMetavar cname)

240+ let newdef = PClauses fc [] cname (caseBlock fc cname (reverse args) opts)

241+ -- fail $ "Not implemented " ++ show c ++ "\n" ++ show args

242+ -- elaborate case

243+ updateAux (newdef : )

244+ solve -- trace (show newdef) solve

245+ where mkCaseName (NS n ns) = NS (mkCaseName n) ns

246+ mkCaseName (UN x) = UN (x ++ "_case")

247+ mkCaseName (MN i x) = MN i (x ++ "_case")

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

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

219

249

250+ caseBlock :: FC -> Name -> [(Name, Binder Term)] -> [(PTerm, PTerm)] -> [PClause]

251+ caseBlock fc n env opts

252+ = let args = map (PRef fc) (map fst (init env)) in

253+ map (mkClause args) opts

254+ where mkClause args (l, r)

255+ = PClause n (PApp fc (PRef fc n)

256+ (map pexp args ++ [pexp l])) [] r []

257+

220 elabArgs ina failed retry [] _

258 elabArgs ina failed retry [] _

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

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

222 elabArgs ina [] False ns ts

260 elabArgs ina [] False ns ts

@@ -247,17 +285,19 @@ pruneAlt xs = map prune xs

247 headIs f (PApp _ (PRef _ f') _) = f == f'

285 headIs f (PApp _ (PRef _ f') _) = f == f'

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

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

249

287

250−trivial :: IState -> Elab ()

288+trivial :: IState -> ElabD ()

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

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

290+ return ())

252 (do env <- get_env

291 (do env <- get_env

253− tryAll (map fst env))

292+ tryAll (map fst env)

293+ return ())

254 where

294 where

255 tryAll [] = fail "No trivial solution"

295 tryAll [] = fail "No trivial solution"

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

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

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

297 (MN 0 "tac") (PRef (FC "prf" 0) x))

258 (tryAll xs)

298 (tryAll xs)

259

299

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

300+resolveTC :: Int -> Name -> IState -> ElabD ()

261resolveTC 0 fn ist = fail $ "Can't resolve type class"

301resolveTC 0 fn ist = fail $ "Can't resolve type class"

262resolveTC depth fn ist

302resolveTC depth fn ist

263 = try (trivial ist)

303 = try (trivial ist)

@@ -321,7 +361,7 @@ collectDeferred t = return t

321

361

322-- Running tactics directly

362-- Running tactics directly

323

363

324−runTac :: Bool -> IState -> PTactic -> Elab ()

364+runTac :: Bool -> IState -> PTactic -> ElabD ()

325runTac autoSolve ist tac = runT (fmap (addImpl ist) tac) where

365runTac autoSolve ist tac = runT (fmap (addImpl ist) tac) where

326 runT (Intro []) = do g <- goal

366 runT (Intro []) = do g <- goal

327 attack; intro (bname g)

367 attack; intro (bname g)

src/Idris/Error.hs+1−1

@@ -34,7 +34,7 @@ liftCatch catchError m h =

34idrisCatch :: Idris a -> (IOError -> Idris a) -> Idris a

35idrisCatch op handler = liftCatch catch op handler

37−tclift :: Show a => TC a -> Idris a

37+tclift :: TC a -> Idris a

38tclift tc = case tc of

39 OK v -> return v

40 Error err -> do i <- get

src/Idris/Parser.hs+37−8

@@ -466,6 +466,7 @@ pExt syn (Rule (s:ssym) ptm _)

466 update ns (PLet n ty val sc) = PLet n (update ns ty) (update ns val)

467 (update (dropn n ns) sc)

468 update ns (PApp fc t args) = PApp fc (update ns t) (map (fmap (update ns)) args)

469+ update ns (PCase fc c opts) = PCase fc (update ns c) (map (pmap (update ns)) opts)

469 update ns (PPair fc l r) = PPair fc (update ns l) (update ns r)

470 update ns (PPair fc l r) = PPair fc (update ns l) (update ns r)

470 update ns (PDPair fc l t r) = PDPair fc (update ns l) (update ns t) (update ns r)

471 update ns (PDPair fc l t r) = PDPair fc (update ns l) (update ns t) (update ns r)

471 update ns (PAlternative as) = PAlternative (map (update ns) as)

472 update ns (PAlternative as) = PAlternative (map (update ns) as)

@@ -516,6 +517,11 @@ pSimpleExpr syn =

516 ts <- endBy (pTactic syn) (lchar ';')

517 ts <- endBy (pTactic syn) (lchar ';')

517 lchar '}'

518 lchar '}'

518 return (PTactics ts)

519 return (PTactics ts)

520+ <|> do reserved "case"; fc <- pfc; scr <- pExpr syn; reserved "of";

521+ lchar '{'

522+ opts <- sepBy1 (pCaseOpt syn) (lchar '|')

523+ lchar '}'

524+ return (PCase fc scr opts)

519 <|> try (do x <- pfName; fc <- pfc; return (PRef fc x))

525 <|> try (do x <- pfName; fc <- pfc; return (PRef fc x))

520 <|> try (pPair syn)

526 <|> try (pPair syn)

521 <|> try (pList syn)

527 <|> try (pList syn)

@@ -538,6 +544,11 @@ pSimpleExpr syn =

538 <|> do lchar '_'; return Placeholder

544 <|> do lchar '_'; return Placeholder

539 <|> pSimpleExtExpr syn

545 <|> pSimpleExtExpr syn

540

546

547+pCaseOpt :: SyntaxInfo -> IParser (PTerm, PTerm)

548+pCaseOpt syn = do lhs <- pExpr syn; symbol "=>";

549+ rhs <- pExpr syn

550+ return (lhs, rhs)

551+

541modifyConst :: SyntaxInfo -> FC -> PTerm -> PTerm

552modifyConst :: SyntaxInfo -> FC -> PTerm -> PTerm

542modifyConst syn fc (PConstant (I x))

553modifyConst syn fc (PConstant (I x))

543 | not (inPattern syn)

554 | not (inPattern syn)

@@ -616,11 +627,15 @@ pLambda syn = do lchar '\\';

616 sc <- pExpr syn

627 sc <- pExpr syn

617 return (bindList PLam xt sc)

628 return (bindList PLam xt sc)

618

629

619−pLet syn = do reserved "let"; n <- pName;

630+pLet syn = try (do reserved "let"; n <- pName;

620− ty <- option Placeholder (do lchar ':'; pExpr' syn)

631+ ty <- option Placeholder (do lchar ':'; pExpr' syn)

621− lchar '='; v <- pExpr syn

632+ lchar '='; v <- pExpr syn

622− reserved "in"; sc <- pExpr syn

633+ reserved "in"; sc <- pExpr syn

623− return (PLet n ty v sc)

634+ return (PLet n ty v sc))

635+ <|> (do reserved "let"; fc <- pfc; pat <- pExpr' syn

636+ symbol "="; v <- pExpr syn

637+ reserved "in"; sc <- pExpr syn

638+ return (PCase fc v [(pat, sc)]))

624

639

625pPi syn =

640pPi syn =

626 try (do lazy <- option False (do lchar '|'; return True)

641 try (do lazy <- option False (do lchar '|'; return True)

@@ -675,12 +690,18 @@ pDoBlock syn

675 return (PDoBlock ds)

690 return (PDoBlock ds)

676

691

677pDo syn

692pDo syn

678− = do reserved "let"; i <- pName; reservedOp "="; fc <- pfc

693+ = try (do reserved "let"; i <- pName; reservedOp "="; fc <- pfc

679− e <- pExpr syn

694+ e <- pExpr syn

680− return (DoLet fc i e)

695+ return (DoLet fc i e))

696+ <|> try (do reserved "let"; i <- pExpr' syn; reservedOp "="; fc <- pfc

697+ sc <- pExpr syn

698+ return (DoLetP fc i sc))

681 <|> try (do i <- pName; symbol "<-"; fc <- pfc

699 <|> try (do i <- pName; symbol "<-"; fc <- pfc

682 e <- pExpr syn;

700 e <- pExpr syn;

683 return (DoBind fc i e))

701 return (DoBind fc i e))

702+ <|> try (do i <- pExpr' syn; symbol "<-"; fc <- pfc

703+ e <- pExpr syn;

704+ return (DoBindP fc i e))

684 <|> try (do e <- pExpr syn; fc <- pfc

705 <|> try (do e <- pExpr syn; fc <- pfc

685 return (DoExp fc e))

706 return (DoExp fc e))

686

707

@@ -997,6 +1018,8 @@ expandDo dsl (PLet n ty v tm) = PLet n (expandDo dsl ty) (expandDo dsl v) (expan

997expandDo dsl (PPi p n ty tm) = PPi p n (expandDo dsl ty) (expandDo dsl tm)

1018expandDo dsl (PPi p n ty tm) = PPi p n (expandDo dsl ty) (expandDo dsl tm)

998expandDo dsl (PApp fc t args) = PApp fc (expandDo dsl t)

1019expandDo dsl (PApp fc t args) = PApp fc (expandDo dsl t)

999 (map (fmap (expandDo dsl)) args)

1020 (map (fmap (expandDo dsl)) args)

1021+expandDo dsl (PCase fc s opts) = PCase fc (expandDo dsl s)

1022+ (map (pmap (expandDo dsl)) opts)

1000expandDo dsl (PPair fc l r) = PPair fc (expandDo dsl l) (expandDo dsl r)

1023expandDo dsl (PPair fc l r) = PPair fc (expandDo dsl l) (expandDo dsl r)

1001expandDo dsl (PDPair fc l t r) = PDPair fc (expandDo dsl l) (expandDo dsl t)

1024expandDo dsl (PDPair fc l t r) = PDPair fc (expandDo dsl l) (expandDo dsl t)

1002 (expandDo dsl r)

1025 (expandDo dsl r)

@@ -1009,8 +1032,14 @@ expandDo dsl (PDoBlock ds) = expandDo dsl $ block (dsl_bind dsl) ds

1009 block b [a] = PElabError "Last statement in do block must be an expression"

1032 block b [a] = PElabError "Last statement in do block must be an expression"

1010 block b (DoBind fc n tm : rest)

1033 block b (DoBind fc n tm : rest)

1011 = PApp fc b [pexp tm, pexp (PLam n Placeholder (block b rest))]

1034 = PApp fc b [pexp tm, pexp (PLam n Placeholder (block b rest))]

1035+ block b (DoBindP fc p tm : rest)

1036+ = PApp fc b [pexp tm, pexp (PLam (MN 0 "bpat") Placeholder

1037+ (PCase fc (PRef fc (MN 0 "bpat"))

1038+ [(p, block b rest)]))]

1012 block b (DoLet fc n tm : rest)

1039 block b (DoLet fc n tm : rest)

1013 = PLet n Placeholder tm (block b rest)

1040 = PLet n Placeholder tm (block b rest)

1041+ block b (DoLetP fc p tm : rest)

1042+ = PCase fc tm [(p, block b rest)]

1014 block b (DoExp fc tm : rest)

1043 block b (DoExp fc tm : rest)

1015 = PApp fc b

1044 = PApp fc b

1016 [pexp tm,

1045 [pexp tm,

src/Idris/Prover.hs+4−4

@@ -33,7 +33,7 @@ showProof n ps = show n ++ " = proof {" ++ "\n" ++

33prove :: Context -> Name -> Type -> Idris ()

34prove ctxt n ty

35 = do let ps = initElaborator n ctxt ty

36− (tm, prf) <- ploop True ("-" ++ show n) [] (ES ps "" Nothing)

36+ (tm, prf) <- ploop True ("-" ++ show n) [] (ES (ps, []) "" Nothing)

37 iLOG $ "Adding " ++ show tm

38 iputStrLn $ showProof n prf

39 i <- get

@@ -44,7 +44,7 @@ prove ctxt n ty

44 updateContext (addCasedef n True False [(P Ref n ty, ptm)] ty)

45 solveDeferred n

47−elabStep :: ElabState -> Elab a -> Idris (a, ElabState)

47+elabStep :: ElabState [PDecl] -> ElabD a -> Idris (a, ElabState [PDecl])

48elabStep st e = do case runStateT e st of

49 OK (a, st') -> return (a, st')

50 Error a -> do i <- get

@@ -75,11 +75,11 @@ dumpState ist ps@(PS nm (h:hs) _ tm _ _ _ i _ _ ctxy _ _)

75 showG (Guess t v) = tshow t ++ " =?= " ++ tshow v

76 showG b = tshow (binderTy b)

78−lifte :: ElabState -> Elab a -> Idris a

78+lifte :: ElabState [PDecl] -> ElabD a -> Idris a

79lifte st e = do (v, _) <- elabStep st e

80 return v

82−ploop :: Bool -> String -> [String] -> ElabState -> Idris (Term, [String])

82+ploop :: Bool -> String -> [String] -> ElabState [PDecl] -> Idris (Term, [String])

83ploop d prompt prf e

84 = do i <- get

85 when d $ lift $ dumpState i (proof e)

test/README+1

@@ -7,3 +7,4 @@ Tests:

7005: Num class resolution [regression]; span & break; ad-hoc overloading

8006: Provisional definitions; class resolution in patterns

9007: Applicative and idiom brackets

10+008: case and pattern matching let

test/test008/expectednew file+3

@@ -0,0 +1,3 @@

1+First and second? 2

2+1

3+2

test/test008/runnew file+4

@@ -0,0 +1,4 @@

1+#!/bin/bash

2+idris test008.idr -o test008

3+./test008

4+rm -f test008 test008.ibc

test/test008/test008.idrnew file+33

@@ -0,0 +1,33 @@

1+module main;

3+testlist : List (String, Int);

4+testlist = [("foo", 1), ("bar", 2)];

6+getVal : String -> a -> List (String, a) -> a;

7+getVal x b xs = case lookup x xs of {

8+ Just v => case lookup x xs of {

9+ Just v' => v

10+ }

11+ | Nothing => b

12+ };

13+

14+foo : (Int, String);

15+foo = (4, "foo");

16+

17+

18+ioVals : IO (String, String);

19+ioVals = do { return ("First", "second"); };

20+

21+main : IO ();

22+main = do { (a, b) <- ioVals;

23+ putStr (show a ++ " and " ++ show b ++ "? ");

24+ let x = "bar";

25+ putStrLn (show (getVal x 7 testlist));

26+ let ((y, z) :: _) = testlist;

27+ print z;

28+ case lookup x testlist of {

29+ Just v => putStrLn (show v)

30+ | Nothing => putStrLn "Not there!"

31+ };

32+ };

33+