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

git.iko.soy/Idris-dev

Added case and pattern matching let bindings

Also pattern matching bind in do notation case notation currently has limitations: - only works on simple types (each pattern must have the same type, more specifically) - return type needs to be known at the point of elaboration

commit67c5734b8eb719c7a04a89fa7b6df898e0527bf0 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateFri 6 Jan 2012, 00:10 (15 years ago) parent4cfbff1

14 files changed+278−133

compare with master

unifiedsplit

src/Core/CoreParser.hs+1 src/Core/Elaborate.hs+93−84 src/Core/ProofShell.hs+2−2 src/Core/TT.hs+2 src/Idris/AbsSyntax.hs+15 src/Idris/ElabDecls.hs+32−24 src/Idris/ElabTerm.hs+50−10 src/Idris/Error.hs+1−1 src/Idris/Parser.hs+37−8 src/Idris/Prover.hs+4−4 test/README+1 test/test008/expected+3 test/test008/run+4 test/test008/test008.idr+33

src/Core/CoreParser.hs+1

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

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

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

2323 "do", "dsl", "import", "impossible",

24+ "case", "of",

2425 "infix", "infixl", "infixr", "prefix",

2526 "where", "with", "forall", "syntax", "proof",

2627 "using", "params", "namespace", "class", "instance",

src/Core/Elaborate.hs+93−84

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

2828 | Print Name

2929 | Tac (Elab ())

3030

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

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

3232 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

3435

35−proof :: ElabState -> ProofState

36−proof (ES p _ _) = p

36+proof :: ElabState aux -> ProofState

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

3738

38−saveState :: Elab ()

39+saveState :: Elab' aux ()

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

4041 put (ES p s (Just e))

4142

42−loadState :: Elab ()

43+loadState :: Elab' aux ()

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

4445 case e of

4546 Just st -> put st

4647 _ -> fail "Nothing to undo"

4748

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

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

4950erun f elab = do s <- get

5051 case runStateT elab s of

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

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

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

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

5556

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

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

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

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

5859

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

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

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

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

6162

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

6364initElaborator = newProof

6465

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

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

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

68− return (a, str)

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

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

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

69+ return (a, str)

6970

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

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+

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

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

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

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

7382 return ()

7483

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

7685

7786-- get the global context

78−get_context :: Elab Context

87+get_context :: Elab' aux Context

7988get_context = do ES p _ _ <- get

80− return (context p)

89+ return (context (fst p))

8190

8291-- get the proof term

83−get_term :: Elab Term

92+get_term :: Elab' aux Term

8493get_term = do ES p _ _ <- get

85− return (pterm p)

94+ return (pterm (fst p))

8695

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

88−get_env :: Elab Env

97+get_env :: Elab' aux Env

8998get_env = do ES p _ _ <- get

90− lift $ envAtFocus p

99+ lift $ envAtFocus (fst p)

91100

92−get_holes :: Elab [Name]

101+get_holes :: Elab' aux [Name]

93102get_holes = do ES p _ _ <- get

94− return (holes p)

103+ return (holes (fst p))

95104

96105-- get the current goal type

97−goal :: Elab Type

106+goal :: Elab' aux Type

98107goal = do ES p _ _ <- get

99− b <- lift $ goalAtFocus p

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

100109 return (binderTy b)

101110

102111-- typecheck locally

103−get_type :: Raw -> Elab Type

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

104113get_type tm = do ctxt <- get_context

105114 env <- get_env

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

107116 return (finalise ty)

108117

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

110−get_deferred :: Elab [Name]

119+get_deferred :: Elab' aux [Name]

111120get_deferred = do ES p _ _ <- get

112− return (deferred p)

121+ return (deferred (fst p))

113122

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

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

115124get_inj = do ES p _ _ <- get

116− return (injective p)

125+ return (injective (fst p))

117126

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

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

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

120129 else lift $ tfail (NotInjective tm l r)

121130

122131-- get instance argument names

123−get_instances :: Elab [Name]

132+get_instances :: Elab' aux [Name]

124133get_instances = do ES p _ _ <- get

125− return (instances p)

134+ return (instances (fst p))

126135

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

128−unique_hole :: Name -> Elab Name

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

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

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

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

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

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

132141 return n'

133142 where

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

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

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

140149 bound_in _ = []

141150

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

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

143152uniqueNameCtxt ctxt n hs

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

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

146155 | otherwise = return n

147156

148−elog :: String -> Elab ()

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

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

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

151160

152161-- The primitives, from ProofState

153162

154−attack :: Elab ()

163+attack :: Elab' aux ()

155164attack = processTactic' Attack

156165

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

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

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

159168

160−exact :: Raw -> Elab ()

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

161170exact t = processTactic' (Exact t)

162171

163−fill :: Raw -> Elab ()

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

164173fill t = processTactic' (Fill t)

165174

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

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

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

168177

169−complete_fill :: Elab ()

178+complete_fill :: Elab' aux ()

170179complete_fill = processTactic' CompleteFill

171180

172−solve :: Elab ()

181+solve :: Elab' aux ()

173182solve = processTactic' Solve

174183

175−start_unify :: Name -> Elab ()

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

176185start_unify n = processTactic' (StartUnify n)

177186

178−end_unify :: Elab ()

187+end_unify :: Elab' aux ()

179188end_unify = processTactic' EndUnify

180189

181−regret :: Elab ()

190+regret :: Elab' aux ()

182191regret = processTactic' Regret

183192

184−compute :: Elab ()

193+compute :: Elab' aux ()

185194compute = processTactic' Compute

186195

187−eval_in :: Raw -> Elab ()

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

188197eval_in t = processTactic' (EvalIn t)

189198

190−check_in :: Raw -> Elab ()

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

191200check_in t = processTactic' (CheckIn t)

192201

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

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

194203intro n = processTactic' (Intro n)

195204

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

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

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

198207

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

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

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

201210

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

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

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

204213

205−rewrite :: Raw -> Elab ()

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

206215rewrite tm = processTactic' (Rewrite tm)

207216

208−patvar :: Name -> Elab ()

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

209218patvar n = do env <- get_env

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

211220 else do n' <- case n of

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

214223 NS _ _ -> return n

215224 processTactic' (PatVar n')

216225

217−patbind :: Name -> Elab ()

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

218227patbind n = processTactic' (PatBind n)

219228

220−focus :: Name -> Elab ()

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

221230focus n = processTactic' (Focus n)

222231

223−movelast :: Name -> Elab ()

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

224233movelast n = processTactic' (MoveLast n)

225234

226−defer :: Name -> Elab ()

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

227236defer n = do n' <- unique_hole n

228237 processTactic' (Defer n')

229238

230−instanceArg :: Name -> Elab ()

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

231240instanceArg n = processTactic' (Instance n)

232241

233−proofstate :: Elab ()

242+proofstate :: Elab' aux ()

234243proofstate = processTactic' ProofState

235244

236−reorder_claims :: Name -> Elab ()

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

237246reorder_claims n = processTactic' (Reorder n)

238247

239−qed :: Elab Term

248+qed :: Elab' aux Term

240249qed = do processTactic' QED

241250 ES p _ _ <- get

242− return (pterm p)

251+ return (pterm (fst p))

243252

244−undo :: Elab ()

253+undo :: Elab' aux ()

245254undo = processTactic' Undo

246255

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

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

248257prepare_apply fn imps =

249258 do ty <- get_type fn

250259 ctxt <- get_context

251260 env <- get_env

252261 -- let claims = getArgs ty imps

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

254− ES p s prev <- get

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

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

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

257266 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)

259268-- case claims of

260269-- [] -> return ()

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

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

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

279288 mkMN (NS n xs) = NS (mkMN n) xs

280289

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

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

282291apply fn imps =

283292 do args <- prepare_apply fn imps

284293 fill (raw_apply fn (map Var args))

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

288297 -- so do nothing

289298 ptm <- get_term

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

291− ES p s prev <- get

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

292301 let (n, hs) = unified p

293302 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)

295304 end_unify

296305 return args

297306

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

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

299308apply_elab n args =

300309 do ty <- get_type (Var n)

301310 ctxt <- get_context

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

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

338347 mkMN (NS n ns) = NS (mkMN n) ns

339348

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

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

341350simple_app fun arg =

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

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

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

360369

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

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

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

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

364373arg n tyhole = do ty <- unique_hole tyhole

365374 claim ty RSet

366375 forall n (Var ty)

367376

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

370379try t1 t2 = do s <- get

371380 case runStateT t1 s of

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

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

374383 _ -> do put s; t2

375384

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

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

379388 where

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

381− Elab a -> -- last failure

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

383− Elab a

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

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

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

392+ Elab' aux a

384393 tryAll' [res] _ [] = res

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

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

src/Core/ProofShell.hs+2−2

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

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

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

4343processCommand (Tac e) state

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

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

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

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

4646 if (not (done ps'))

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

4848 else (state { prf = Nothing,

src/Core/TT.hs+2

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

8888showSep sep [x] = x

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

9090

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

92+

9193traceWhen True msg a = trace msg a

9294traceWhen False _ a = a

9395

src/Idris/AbsSyntax.hs+15

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

386386 | PPi Plicity Name PTerm PTerm

387387 | PLet Name PTerm PTerm PTerm

388388 | PApp FC PTerm [PArg]

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

389390 | PTrue FC

390391 | PFalse FC

391392 | PRefl FC

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

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

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

419420 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)

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

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

422424 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

446448

447449data PDo' t = DoExp FC t

448450 | DoBind FC Name t

451+ | DoBindP FC t t

449452 | DoLet FC Name t

453+ | DoLetP FC t t

450454 deriving (Eq, Functor)

451455{-!

452456deriving instance Binary PDo'

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

637641 = let args = getExps as in

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

639643 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

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

641647 se p (PRefl _) = "refl"

642648 se p (PResolveTC _) = "resolvetc"

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

675681 ni env (PRef _ n)

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

677683 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)

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

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

680687 ni env (PHidden tm) = ni env tm

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

694701 [] -> [n]

695702 _ -> []

696703 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)

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

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

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

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

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

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

827835 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)

828837 en t = t

829838

830839expandParamsD :: IState ->

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

881890 pri (PRefl _) = 1

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

883892 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)))

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

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

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

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

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

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

10061016 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'

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

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

10091022 PLam n ty' sc'

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

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

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

11661179 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)

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

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

11691183 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

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

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

11791193 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)

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

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

11821197 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

4141 ty' <- implicit syn n ty'

4242 let ty = addImpl i ty'

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

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

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

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

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

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

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

4848 let nty = normalise ctxt [] cty

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

5050 addIBC (IBCDef n)

5151 addDeferred ds

52+ mapM_ (elabDecl' info) is

5253

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

5455elabData info syn fc (PDatadecl n t_in dcons)

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

5859 i <- get

5960 t_in <- implicit syn n t_in

6061 let t = addImpl i t_in

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

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

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

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

6364 def' <- checkDef fc defer

6465 addDeferred def'

66+ mapM_ (elabDecl' info) is

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

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

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

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

7880 t_in <- implicit syn n t_in

7981 let t = addImpl i t_in

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

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

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

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

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

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

8486 def' <- checkDef fc defer

8587 addDeferred def'

88+ mapM_ (elabDecl' info) is

8689 ctxt <- getContext

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

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

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

128131 i <- get

129132 let tm = addImpl i tm_in

130133 logLvl 10 (showImp True tm)

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

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

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

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

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

134137 let vtm = getInferTerm tm'

135138 logLvl 2 (show vtm)

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

141144 i <- get

142145 let lhs = addImpl i lhs_in

143146 -- 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 []

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

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

147150 Error _ -> return ()

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

153156 i <- get

154157 let lhs = addImpl i lhs_in

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

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

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

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

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

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

158162 let lhs_tm = orderPats (getInferTerm lhs')

159163 let lhs_ty = getInferType lhs'

160164 logLvl 3 (show lhs_tm)

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

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

177181 logLvl 2 (showImp True rhs)

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

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

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

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

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

181185 (do pbinds lhs_tm

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

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

183187 psolve lhs_tm

184188 tt <- get_term

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

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

190+ return (tm, ds, is))

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

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

188193 def' <- checkDef fc defer

189194 addDeferred def'

195+ mapM_ (elabDecl' info) is

190196 ctxt <- getContext

191197 logLvl 5 $ "Rechecking"

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

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

213219 i <- get

214220 let lhs = addImpl i lhs_in

215221 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 []

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

218224 let lhs_tm = orderPats (getInferTerm lhs')

219225 let lhs_ty = getInferType lhs'

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

225231 let wval = addImpl i wval_in

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

227233 -- Elaborate wval in this context

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

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

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

230− (bindTyArgs PVTy bargs infP)

236+ (bindTyArgs PVTy bargs infP) []

231237 (do pbinds lhs_tm

232238 -- 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))

234240 psolve lhs_tm

235241 tt <- get_term

236− return (tt, d))

242+ return (tt, d, is))

237243 def' <- checkDef fc defer

238244 addDeferred def'

245+ mapM_ (elabDecl' info) is

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

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

241248 windex <- getName

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

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

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

264271 i <- get

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

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

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

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

267274 (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)

269276 psolve lhs_tm

270277 tt <- get_term

271− return (tt, d))

278+ return (tt, d, is))

272279 def' <- checkDef fc defer

273280 addDeferred def'

281+ mapM_ (elabDecl' info) is

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

275283 return $ Just (clhs, crhs)

276284 where

src/Idris/ElabTerm.hs+50−10

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

2121

2222toplevel = EInfo [] emptyContext id Nothing

2323

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

25+

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

2527-- elaborated, typechecked term.

2628--

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

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

3133

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

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

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

3436build ist info pattern fn tm

3537 = do elab ist info pattern False fn tm

38+ is <- getAux

3639 tt <- get_term

37− return $ runState (collectDeferred tt) []

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

41+ return (tm, ds, is)

3842

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

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

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

4246

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

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

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

4549buildTC ist info pattern tcgen fn tm

4650 = do elab ist info pattern tcgen fn tm

51+ is <- getAux

4752 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)

4958

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

51− Elab ()

60+ ElabD ()

5261elab ist info pattern tcgen fn tm

5362 = do elabE False tm

5463 when pattern -- convert remaining holes to pattern vars

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

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

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

217226 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")

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

219249

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+

220258 elabArgs ina failed retry [] _

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

222260 elabArgs ina [] False ns ts

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

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

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

249287

250−trivial :: IState -> Elab ()

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

288+trivial :: IState -> ElabD ()

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

290+ return ())

252291 (do env <- get_env

253− tryAll (map fst env))

292+ tryAll (map fst env)

293+ return ())

254294 where

255295 tryAll [] = fail "No trivial solution"

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

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

258298 (tryAll xs)

259299

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

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

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

262302resolveTC depth fn ist

263303 = try (trivial ist)

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

321361

322362-- Running tactics directly

323363

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

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

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

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

327367 attack; intro (bname g)

src/Idris/Error.hs+1−1

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

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

3535idrisCatch op handler = liftCatch catch op handler

3636

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

37+tclift :: TC a -> Idris a

3838tclift tc = case tc of

3939 OK v -> return v

4040 Error err -> do i <- get

src/Idris/Parser.hs+37−8

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

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

467467 (update (dropn n ns) sc)

468468 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)

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

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

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

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

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

517518 lchar '}'

518519 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)

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

520526 <|> try (pPair syn)

521527 <|> try (pList syn)

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

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

539545 <|> pSimpleExtExpr syn

540546

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

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

549+ rhs <- pExpr syn

550+ return (lhs, rhs)

551+

541552modifyConst :: SyntaxInfo -> FC -> PTerm -> PTerm

542553modifyConst syn fc (PConstant (I x))

543554 | not (inPattern syn)

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

616627 sc <- pExpr syn

617628 return (bindList PLam xt sc)

618629

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

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

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

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

623− return (PLet n ty v sc)

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

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

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

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

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)]))

624639

625640pPi syn =

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

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

675690 return (PDoBlock ds)

676691

677692pDo syn

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

679− e <- pExpr syn

680− return (DoLet fc i e)

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

694+ e <- pExpr syn

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

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

682700 e <- pExpr syn;

683701 return (DoBind fc i e))

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

703+ e <- pExpr syn;

704+ return (DoBindP fc i e))

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

685706 return (DoExp fc e))

686707

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

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

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

9991020 (map (fmap (expandDo dsl)) args)

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

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

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

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

10021025 (expandDo dsl r)

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

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

10101033 block b (DoBind fc n tm : rest)

10111034 = 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)]))]

10121039 block b (DoLet fc n tm : rest)

10131040 = PLet n Placeholder tm (block b rest)

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

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

10141043 block b (DoExp fc tm : rest)

10151044 = PApp fc b

10161045 [pexp tm,

src/Idris/Prover.hs+4−4

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

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

3434prove ctxt n ty

3535 = 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)

3737 iLOG $ "Adding " ++ show tm

3838 iputStrLn $ showProof n prf

3939 i <- get

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

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

4545 solveDeferred n

4646

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

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

4848elabStep st e = do case runStateT e st of

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

5050 Error a -> do i <- get

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

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

7676 showG b = tshow (binderTy b)

7777

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

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

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

8080 return v

8181

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

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

8383ploop d prompt prf e

8484 = do i <- get

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

test/README+1

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

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

88006: Provisional definitions; class resolution in patterns

99007: 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+