12bd089 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Added lifting of unsolved metavariables to global functions

12bd089Edwin Brady15 years ago

lib/Makefile+6−1

compare with master

unifiedsplit

@@ -1,4 +1,9 @@

1+SRCS = prelude.idr list.idr nat.idr prelude.idr vect.idr

1check: .PHONY

3check: .PHONY

2− miniidris --noprelude --check *.idr

4+ for x in *.idr ; do \

5+ echo "Checking $$x"; \

6+ miniidris --noprelude --check $$x; \

7+ done

4.PHONY:

9.PHONY:

src/Core/Elaborate.hs+8

@@ -81,6 +81,11 @@ get_type tm = do ctxt <- get_context

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

82 return (finalise ty)

84+-- get holes we've deferred for later definition

85+get_deferred :: Elab [Name]

86+get_deferred = do (p, _) <- get

87+ return (deferred p)

88+

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

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

85unique_hole :: Name -> Elab Name

90unique_hole :: Name -> Elab Name

86unique_hole n = do (p, _) <- get

91unique_hole n = do (p, _) <- get

@@ -162,6 +167,9 @@ focus n = processTactic' (Focus n)

162movelast :: Name -> Elab ()

167movelast :: Name -> Elab ()

163movelast n = processTactic' (MoveLast n)

168movelast n = processTactic' (MoveLast n)

164

169

170+defer :: Name -> Elab ()

171+defer n = processTactic' (Defer n)

172+

165proofstate :: Elab ()

173proofstate :: Elab ()

166proofstate = processTactic' ProofState

174proofstate = processTactic' ProofState

167

175

src/Core/ProofState.hs+15−2

@@ -23,7 +23,7 @@ data ProofState = PS { thname :: Name,

23 pterm :: Term, -- current proof term

24 ptype :: Type, -- original goal

25 unified :: (Name, [(Name, Term)]),

26− defer :: [(Name, Type)], -- names we'll need to define

26+ deferred :: [Name], -- names we'll need to define

27 previous :: Maybe ProofState, -- for undo

28 context :: Context,

29 plog :: String,

@@ -52,6 +52,7 @@ data Tactic = Attack

52 | PatVar Name

53 | PatBind Name

54 | Focus Name

55+ | Defer Name

55 | MoveLast Name

56 | MoveLast Name

56 | ProofState

57 | ProofState

57 | Undo

58 | Undo

@@ -138,7 +139,6 @@ goal h tm = g [] tm where

138 gb env (Let t v) = g env t `mplus` g env v

139 gb env (Let t v) = g env t `mplus` g env v

139 gb env (Guess t v) = g env t `mplus` g env v

140 gb env (Guess t v) = g env t `mplus` g env v

140 gb env t = g env (binderTy t)

141 gb env t = g env (binderTy t)

141−

142tactic :: Hole -> RunTactic -> StateT TState TC ()

143tactic h f = do ps <- get

144 tm' <- atH (context ps) [] (pterm ps)

@@ -188,6 +188,18 @@ movelast n ctxt env t = do action (\ps -> let hs = holes ps in

188 else ps)

189 return t

190

191+defer :: Name -> RunTactic

192+defer n ctxt env (Bind x (Hole t) (P nt x' ty)) | x == x' =

193+ do action (\ps -> let hs = holes ps in

194+ ps { holes = hs \\ [x] })

195+ return (Bind n (GHole (mkTy (reverse env) t))

196+ (mkApp (P nt n ty) (map getP (reverse env))))

197+ where

198+ mkTy [] t = t

199+ mkTy ((n,b) : bs) t = Bind n (Pi (binderTy b)) (mkTy bs t)

200+

201+ getP (n, b) = P Bound n (binderTy b)

202+

191-- Hmmm. YAGNI?

203-- Hmmm. YAGNI?

192regret :: RunTactic

204regret :: RunTactic

193regret = undefined

205regret = undefined

@@ -373,3 +385,4 @@ process t h = tactic (Just h) (mktac t)

373 mktac (EvalIn r) = eval_in r

385 mktac (EvalIn r) = eval_in r

374 mktac (Focus n) = focus n

386 mktac (Focus n) = focus n

375 mktac (MoveLast n) = movelast n

387 mktac (MoveLast n) = movelast n

388+ mktac (Defer n) = defer n

src/Core/TT.hs+2

@@ -118,6 +118,7 @@ data Binder b = Lam { binderTy :: b }

118 | NLet { binderTy :: b,

119 binderVal :: b }

120 | Hole { binderTy :: b}

121+ | GHole { binderTy :: b}

121 | Guess { binderTy :: b,

122 | Guess { binderTy :: b,

122 binderVal :: b }

123 binderVal :: b }

123 | PVar { binderTy :: b }

124 | PVar { binderTy :: b }

@@ -303,6 +304,7 @@ showEnv' env t dbg = se 10 env t where

303

304

304 sb env n (Lam t) = showb env "\\ " " => " n t

305 sb env n (Lam t) = showb env "\\ " " => " n t

305 sb env n (Hole t) = showb env "? " ". " n t

306 sb env n (Hole t) = showb env "? " ". " n t

307+ sb env n (GHole t) = showb env "?defer " ". " n t

306 sb env n (Pi t) = showb env "(" ") -> " n t

308 sb env n (Pi t) = showb env "(" ") -> " n t

307 sb env n (PVar t) = showb env "pat " ". " n t

309 sb env n (PVar t) = showb env "pat " ". " n t

308 sb env n (PVTy t) = showb env "pty " ". " n t

310 sb env n (PVTy t) = showb env "pty " ". " n t

src/Core/Typecheck.hs+19

@@ -92,6 +92,12 @@ check ctxt env (RBind n b sc)

92 let tt' = normalise ctxt env tt

93 isSet ctxt env tt'

94 return (Hole tv')

95+ checkBinder (GHole t)

96+ = do (tv, tt) <- check ctxt env t

97+ let tv' = normalise ctxt env tv

98+ let tt' = normalise ctxt env tt

99+ isSet ctxt env tt'

100+ return (GHole tv')

95 checkBinder (Guess t v)

101 checkBinder (Guess t v)

96 = do (tv, tt) <- check ctxt env t

102 = do (tv, tt) <- check ctxt env t

97 (vv, vt) <- check ctxt env v

103 (vv, vt) <- check ctxt env v

@@ -106,6 +112,13 @@ check ctxt env (RBind n b sc)

106 let tt' = normalise ctxt env tt

112 let tt' = normalise ctxt env tt

107 isSet ctxt env tt'

113 isSet ctxt env tt'

108 return (PVar tv')

114 return (PVar tv')

115+ checkBinder (PVTy t)

116+ = do (tv, tt) <- check ctxt env t

117+ let tv' = normalise ctxt env tv

118+ let tt' = normalise ctxt env tt

119+ isSet ctxt env tt'

120+ return (PVTy tv')

121+ checkBinder x = fail (show x)

109

122

110 discharge n (Lam t) scv sct

123 discharge n (Lam t) scv sct

111 = return (Bind n (Lam t) scv, Bind n (Pi t) sct)

124 = return (Bind n (Lam t) scv, Bind n (Pi t) sct)

@@ -119,12 +132,18 @@ check ctxt env (RBind n b sc)

119 = do -- A hole can't appear in the type of its scope

132 = do -- A hole can't appear in the type of its scope

120 checkNotHoley 0 sct

133 checkNotHoley 0 sct

121 return (Bind n (Hole t) scv, sct)

134 return (Bind n (Hole t) scv, sct)

135+ discharge n (GHole t) scv sct

136+ = do -- A hole can't appear in the type of its scope

137+ checkNotHoley 0 sct

138+ return (Bind n (GHole t) scv, sct)

122 discharge n (Guess t v) scv sct

139 discharge n (Guess t v) scv sct

123 = do -- A hole can't appear in the type of its scope

140 = do -- A hole can't appear in the type of its scope

124 checkNotHoley 0 sct

141 checkNotHoley 0 sct

125 return (Bind n (Guess t v) scv, sct)

142 return (Bind n (Guess t v) scv, sct)

126 discharge n (PVar t) scv sct

143 discharge n (PVar t) scv sct

127 = return (Bind n (PVar t) scv, Bind n (PVTy t) sct)

144 = return (Bind n (PVar t) scv, Bind n (PVTy t) sct)

145+ discharge n (PVTy t) scv sct

146+ = return (Bind n (PVTy t) scv, sct)

128

147

129 checkNotHoley i (V v)

148 checkNotHoley i (V v)

130 | v == i = fail "You can't put a hole where a hole don't belong"

149 | v == i = fail "You can't put a hole where a hole don't belong"

src/Idris/AbsSyntax.hs+21−2

@@ -29,11 +29,12 @@ data IState = IState { tt_ctxt :: Context,

29 idris_log :: String,

30 idris_options :: IOption,

31 idris_name :: Int,

32+ idris_metavars :: [Name],

32 imported :: [FilePath],

33 imported :: [FilePath],

33 idris_prims :: [(Name, ([E.Name], E.Term))]

34 idris_prims :: [(Name, ([E.Name], E.Term))]

34 }

35 }

36−idrisInit = IState emptyContext [] emptyContext "" defaultOpts 0 [] []

37+idrisInit = IState emptyContext [] emptyContext "" defaultOpts 0 [] [] []

38-- The monad for the main REPL - reading and processing files and updating

39-- The monad for the main REPL - reading and processing files and updating

39-- global state (hence the IO inner monad).

40-- global state (hence the IO inner monad).

@@ -54,12 +55,27 @@ getName = do i <- get;

54 put (i { idris_name = idx + 1 })

55 put (i { idris_name = idx + 1 })

55 return idx

56 return idx

58+checkUndefined :: Name -> Idris ()

59+checkUndefined n = do i <- getContext

60+ case lookupCtxt n i of

61+ Just _ -> fail $ show n ++ " already defined"

62+ _ -> return ()

63+

57setContext :: Context -> Idris ()

64setContext :: Context -> Idris ()

58setContext ctxt = do i <- get; put (i { tt_ctxt = ctxt } )

65setContext ctxt = do i <- get; put (i { tt_ctxt = ctxt } )

60updateContext :: (Context -> Context) -> Idris ()

67updateContext :: (Context -> Context) -> Idris ()

61updateContext f = do i <- get; put (i { tt_ctxt = f (tt_ctxt i) } )

68updateContext f = do i <- get; put (i { tt_ctxt = f (tt_ctxt i) } )

70+addDeferred :: [(Name, Type)] -> Idris ()

71+addDeferred ns = do mapM_ (\(n, t) -> updateContext (addTyDecl n t)) ns

72+ i <- get

73+ put (i { idris_metavars = map fst ns ++ idris_metavars i })

74+

75+solveDeferred :: Name -> Idris ()

76+solveDeferred n = do i <- get

77+ put (i { idris_metavars = idris_metavars i \\ [n] })

78+

63iputStrLn :: String -> Idris ()

79iputStrLn :: String -> Idris ()

64iputStrLn = lift.putStrLn

80iputStrLn = lift.putStrLn

@@ -87,6 +103,7 @@ iLOG = logLvl 1

103

88data Command = Quit | Help | Eval PTerm

104data Command = Quit | Help | Eval PTerm

89 | Compile String

105 | Compile String

106+ | Metavars

90 | TTShell

107 | TTShell

91 | NOP

108 | NOP

109

@@ -162,6 +179,7 @@ data PTerm = PQuote Raw

162 | Placeholder

179 | Placeholder

163 | PDoBlock [PDo]

180 | PDoBlock [PDo]

164 | PReturn

181 | PReturn

182+ | PMetavar Name

165 | PElabError String -- error to report on elaboration

183 | PElabError String -- error to report on elaboration

166

184

167data PDo = DoExp PTerm

185data PDo = DoExp PTerm

@@ -258,6 +276,7 @@ showImp impl tm = se 10 tm where

258 se p (PPair l r) = "(" ++ se 10 l ++ ", " ++ se 10 r ++ ")"

276 se p (PPair l r) = "(" ++ se 10 l ++ ", " ++ se 10 r ++ ")"

259 se p PSet = "Set"

277 se p PSet = "Set"

260 se p (PConstant c) = show c

278 se p (PConstant c) = show c

279+ se p (PMetavar n) = "?" ++ show n

261 se p Placeholder = "_"

280 se p Placeholder = "_"

262

281

263 seArg arg = " " ++ se 0 arg

282 seArg arg = " " ++ se 0 arg

@@ -312,7 +331,7 @@ getInferTerm tm = error ("getInferTerm " ++ show tm)

312getInferType (Bind n b sc) = Bind n b $ getInferType sc

331getInferType (Bind n b sc) = Bind n b $ getInferType sc

313getInferType (App (App _ ty) _) = ty

332getInferType (App (App _ ty) _) = ty

314

333

315−-- Handy primitives: Unit, False, Pair, MkPair

334+-- Handy primitives: Unit, False, Pair, MkPair, mkForeign

316

335

317unitTy = MN 0 "__Unit"

336unitTy = MN 0 "__Unit"

318unitCon = MN 0 "__II"

337unitCon = MN 0 "__II"

src/Idris/Compiler.hs+2

@@ -13,6 +13,8 @@ import Control.Monad.State

13import Epic.Epic hiding (Term, Type, Name, fn, compile)

14import qualified Epic.Epic as E

16+primDefs = [UN ["mkForeign"]]

17+

16compile :: FilePath -> Idris ()

18compile :: FilePath -> Idris ()

17compile f = do ds <- mkDecls

19compile f = do ds <- mkDecls

18 lift $ compileWith [Debug] (mkProgram ds) f

20 lift $ compileWith [Debug] (mkProgram ds) f

src/Idris/ElabDecls.hs+49−20

@@ -30,17 +30,21 @@ toplevel = EInfo [] emptyContext id

30elabType :: ElabInfo -> Name -> PTerm -> Idris ()

31elabType info n_in ty_in = let ty = piBind (params info) ty_in

32 n = liftname info n_in in

33+ do checkUndefined n

33− do ctxt <- getContext

34+ ctxt <- getContext

34 logLvl 2 $ "Type " ++ showImp True ty

35 logLvl 2 $ "Type " ++ showImp True ty

35− (ty', log) <- tclift $ elaborate ctxt n (Set 0) (build info False ty)

36+ ((ty', defer), log) <- tclift $ elaborate ctxt n (Set 0) (build info False ty)

36 (cty, _) <- tclift $ recheck ctxt [] ty'

37 (cty, _) <- tclift $ recheck ctxt [] ty'

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

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

38− updateContext (addTyDecl n (normalise ctxt [] cty))

39+ let nty = normalise ctxt [] cty

40+ addDeferred ((n, nty):defer)

40elabData :: ElabInfo -> PData -> Idris ()

42elabData :: ElabInfo -> PData -> Idris ()

41elabData info (PDatadecl n t dcons)

43elabData info (PDatadecl n t dcons)

44+ = do checkUndefined n

42− = do ctxt <- getContext

45+ ctxt <- getContext

43− (t', log) <- tclift $ elaborate ctxt n (Set 0) (build info False t)

46+ ((t', defer), log) <- tclift $ elaborate ctxt n (Set 0) (build info False t)

47+ addDeferred defer

44 (cty, _) <- tclift $ recheck ctxt [] t'

48 (cty, _) <- tclift $ recheck ctxt [] t'

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

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

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

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

@@ -49,17 +53,20 @@ elabData info (PDatadecl n t dcons)

50elabCon :: ElabInfo -> (Name, PTerm) -> Idris (Name, Type)

54elabCon :: ElabInfo -> (Name, PTerm) -> Idris (Name, Type)

51elabCon info (n, t)

55elabCon info (n, t)

56+ = do checkUndefined n

52− = do ctxt <- getContext

57+ ctxt <- getContext

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

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

54− (t', log) <- tclift $ elaborate ctxt n (Set 0) (build info False t)

59+ ((t', defer), log) <- tclift $ elaborate ctxt n (Set 0) (build info False t)

55-- logLvl 2 $ "Rechecking " ++ show t'

60-- logLvl 2 $ "Rechecking " ++ show t'

61+ addDeferred defer

56 (cty, _) <- tclift $ recheck ctxt [] t'

62 (cty, _) <- tclift $ recheck ctxt [] t'

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

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

58 return (n, cty)

64 return (n, cty)

60elabClauses :: ElabInfo -> Name -> [PClause] -> Idris ()

66elabClauses :: ElabInfo -> Name -> [PClause] -> Idris ()

61elabClauses info n_in cs = let n = liftname info n_in in

67elabClauses info n_in cs = let n = liftname info n_in in

68+ do solveDeferred n

62− do pats <- mapM (elabClause info) cs

69+ pats <- mapM (elabClause info) cs

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

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

64 show l ++ " = " ++

71 show l ++ " = " ++

65 show r) pats))

72 show r) pats))

@@ -78,8 +85,8 @@ elabVal :: ElabInfo -> PTerm -> Idris (Term, Type)

78elabVal info tm

85elabVal info tm

79 = do ctxt <- getContext

86 = do ctxt <- getContext

80 logLvl 10 (show tm)

87 logLvl 10 (show tm)

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

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

82− (build info False (infTerm tm))

89+ (build info False (infTerm tm))

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

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

84 let vtm = getInferTerm tm'

91 let vtm = getInferTerm tm'

85 logLvl 2 (show vtm)

92 logLvl 2 (show vtm)

@@ -90,8 +97,8 @@ elabClause info (PClause fname lhs rhs whereblock)

90 = do ctxt <- getContext

97 = do ctxt <- getContext

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

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

92 -- pattern bindings

99 -- pattern bindings

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

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

94− (build info True (infTerm lhs))

101+ (build info True (infTerm lhs))

95 let lhs_tm = getInferTerm lhs'

102 let lhs_tm = getInferTerm lhs'

96 let lhs_ty = getInferType lhs'

103 let lhs_ty = getInferType lhs'

97 logLvl 3 (show lhs_tm)

104 logLvl 3 (show lhs_tm)

@@ -104,12 +111,15 @@ elabClause info (PClause fname lhs rhs whereblock)

104 -- Now build the RHS, using the type of the LHS as the goal.

111 -- Now build the RHS, using the type of the LHS as the goal.

105 logLvl 2 (showImp True rhs)

112 logLvl 2 (showImp True rhs)

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

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

107− (rhs', _) <- tclift $ elaborate ctxt (MN 0 "patRHS") clhsty

114+ ((rhs', defer), _) <- tclift $ elaborate ctxt (MN 0 "patRHS") clhsty

108− (do pbinds lhs_tm

115+ (do pbinds lhs_tm

109− build winfo False rhs

116+ (_, d) <- build winfo False rhs

110− psolve lhs_tm

117+ psolve lhs_tm

111− get_term)

118+ tt <- get_term

119+ return (tt, d))

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

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

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

122+ addDeferred defer

113 (crhs, crhsty) <- tclift $ recheck ctxt [] rhs'

123 (crhs, crhsty) <- tclift $ recheck ctxt [] rhs'

114 return (clhs, crhs)

124 return (clhs, crhs)

115 where

125 where

@@ -165,9 +175,12 @@ elabDecl' info (PParams ns ps) = mapM_ (elabDecl' pinfo) ps

165-- If building a pattern match, we convert undeclared variables from

175-- If building a pattern match, we convert undeclared variables from

166-- holes to pattern bindings.

176-- holes to pattern bindings.

167

177

178+-- Also find deferred names in the term and their types

179+

168−build :: ElabInfo -> Bool -> PTerm -> Elab Term

180+build :: ElabInfo -> Bool -> PTerm -> Elab (Term, [(Name, Type)])

169build info pattern tm = do elab info pattern tm

181build info pattern tm = do elab info pattern tm

170− get_term

182+ tt <- get_term

183+ return $ runState (collectDeferred tt) []

171

184

172elab :: ElabInfo -> Bool -> PTerm -> Elab ()

185elab :: ElabInfo -> Bool -> PTerm -> Elab ()

173elab info pattern tm = do elab' tm

186elab info pattern tm = do elab' tm

@@ -235,12 +248,28 @@ elab info pattern tm = do elab' tm

235 = do simple_app (elab' f) (elab' (getTm arg))

248 = do simple_app (elab' f) (elab' (getTm arg))

236 solve

249 solve

237 elab' Placeholder = fail $ "Can't deal with a placeholder here"

250 elab' Placeholder = fail $ "Can't deal with a placeholder here"

251+ elab' (PMetavar n) = do attack; defer n; solve

238 elab' (PElabError e) = fail e

252 elab' (PElabError e) = fail e

239 elab' x = fail $ "Not implemented " ++ show x

253 elab' x = fail $ "Not implemented " ++ show x

240

254

241 elabArgs [] _ = return ()

255 elabArgs [] _ = return ()

242 elabArgs (n:ns) (Placeholder : args) = elabArgs ns args

256 elabArgs (n:ns) (Placeholder : args) = elabArgs ns args

243 elabArgs (n:ns) (t : args) = do focus n; elab' t; elabArgs ns args

257 elabArgs (n:ns) (t : args) = do focus n; elab' t; elabArgs ns args

244−

258+

259+collectDeferred :: Term -> State [(Name, Type)] Term

260+collectDeferred (Bind n (GHole t) app) =

261+ do ds <- get

262+ put ((n, t) : ds)

263+ return app

264+collectDeferred (Bind n b t) = do b' <- cdb b

265+ t' <- collectDeferred t

266+ return (Bind n b' t')

267+ where

268+ cdb (Let t v) = liftM2 Let (collectDeferred t) (collectDeferred v)

269+ cdb (Guess t v) = liftM2 Guess (collectDeferred t) (collectDeferred v)

270+ cdb b = do ty' <- collectDeferred (binderTy b)

271+ return (b { binderTy = ty' })

272+collectDeferred (App f a) = liftM2 App (collectDeferred f) (collectDeferred a)

273+collectDeferred t = return t

245

274

246

275

src/Idris/Parser.hs+1

@@ -212,6 +212,7 @@ pfName = try iName

212pSimpleExpr syn =

213 try (do symbol "!["; t <- pTerm; lchar ']'

214 return $ PQuote t)

215+ <|> try (do lchar '?'; x <- iName; return (PMetavar x))

215 <|> try (do reserved "return"; return PReturn)

216 <|> try (do reserved "return"; return PReturn)

216 <|> try (do x <- pfName; return (PRef x))

217 <|> try (do x <- pfName; return (PRef x))

217 <|> try (do lchar '('; l <- pExpr syn; lchar ','; r <- pExpr syn; lchar ')';

218 <|> try (do lchar '('; l <- pExpr syn; lchar ','; r <- pExpr syn; lchar ')';

src/Idris/REPL.hs+6−1

@@ -16,7 +16,7 @@ import Core.TT

16import System.Console.Readline

17import Control.Monad

18import Control.Monad.State

19−

19+import Data.List

21repl :: Idris ()

22repl = do x <- lift $ readline "Idris> "

@@ -54,5 +54,10 @@ process TTShell = do ist <- get

54 shst' <- lift $ runShell shst

55 return ()

56process (Compile f) = do compile f

57+process Metavars = do ist <- get

58+ let mvs = idris_metavars ist \\ primDefs

59+ case mvs of

60+ [] -> iputStrLn "No global metavariables to solve"

61+ _ -> iputStrLn $ "Global metavariables:\n\t" ++ show mvs

57process NOP = return ()

62process NOP = return ()

src/Idris/REPLParser.hs+1

@@ -23,5 +23,6 @@ pCmd = try (do cmd ["q", "quit"]; return Quit)

23 <|> try (do cmd ["h", "?", "help"]; return Help)

24 <|> try (do cmd ["ttshell"]; return TTShell)

25 <|> try (do cmd ["c", "compile"]; f <- identifier; return (Compile f))

26+ <|> try (do cmd ["m", "metavars"]; return Metavars)

26 <|> do t <- pFullExpr defaultSyntax; return (Eval t)

27 <|> do t <- pFullExpr defaultSyntax; return (Eval t)

27 <|> do eof; return NOP

28 <|> do eof; return NOP